[YICES-HELP] Using Yices for MaxSMT w/ difference-logic

[Michael D. Moffitt]

 (Resending... apologies if this is received twice)

Hello,

I'm using Yices to do MaxSMT on a difference-logic instance:

   yices -v 2 < moffittOpt.yices

with this input file:

   http://jeeves.eecs.umich.edu/moffittOpt.yices

After a few seconds, the verbosity trace hits an "r" and reports "unknown".
It gives me a solution with a cost of 7... I don't think that's the optimal
solution (e.g., if you duplicate all the constraints, it will find a
solution of cost 12, not 14).  I get the feeling that it's hitting a time
out, but I'm not sure.  The exact output is below.  Is there something else
I need to do for it to give me an optimal solution?

 - Mike



.cost(9)..cost(7)...........c..........c.r
unknown
(= x13 101) (= x1 -90) (= x11 259) (= x12 -78) (= x5 -120) (= x16 -129) (=
x7 -188) (= x2 -31) (= x14 -48) (= x19 33) (= x8 -121) (= x3 -142) (= x15
159) (= x6 -16) (= x18 -51) (= x4 -131) (= x9 -46) (= x10 0) (= x17 49) (=
x0 -148)
cost: 7


-- 
Michael D. Moffitt
mmoffitt at umich.edu
http://www.eecs.umich.edu/~mmoffitt/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/yices-help/attachments/20070228/18d5779d/attachment.html