Upgrade OptiMathSAT to 1.7.5 #815
Conversation
|
@masinag Wow! Fantastic! Thanks a lot! Please, add yourself to the CONTRIBUTORS file as detailed here: https://pysmt.readthedocs.io/en/latest/development.html#licensing |
|
I see that two tests are failing but if I run the single file they pass: I am trying to figure out what is happening, do you have any ideas? |
|
Hey @mikand, after some digging, I found out the following issue. Sometimes, the outputs of self._msat_lib.msat_get_model_value(self.msat_env(), msat_obj_term)and self._msat_lib.msat_objective_value_term(self.msat_env(), msat_obj, self._msat_lib.MSAT_OPTIMUM, None, None)don't match. That is, the value of the objective in the optimum model and the optimum objective value are different (the latter seems to contain the correct value). Reproducibility from pysmt.optimization.goal import MaximizationGoal
from pysmt.shortcuts import Implies, Optimizer, Symbol, Iff
from pysmt.typing import INT, BOOL
import optimathsat
x = Symbol("x", INT)
y = Symbol("y", INT)
a = Symbol("a", BOOL)
b = Symbol("b", BOOL)
c = Symbol("c", BOOL)
d = Symbol("d", BOOL)
e = Symbol("e", BOOL)
assertions = [
Iff((0 < (x + y)), a),
Iff((((2 * x) + (3 * y)) < -10), c),
((a | b) & (c | d)),
Implies(e, (10 < x)),
Implies((10 < x), e),
(x <= 100),
(y <= 100),
a,
b,
e,
]
goals = [MaximizationGoal(x), MaximizationGoal(y)]
goals = [MaximizationGoal(x), MaximizationGoal(y)]
with Optimizer("optimsat") as s:
env = s.msat_env()
s.add_assertions(assertions)
for _, obj_values in s.pareto_optimize(goals):
print("Value:", end=" ")
obj_iter = optimathsat.msat_create_objective_iterator(env)
while optimathsat.msat_objective_iterator_has_next(obj_iter):
_, obj = optimathsat.msat_objective_iterator_next(obj_iter)
msat_obj_term = optimathsat.msat_objective_get_term(env, obj)
cost_fn = s.converter.back(msat_obj_term)
msat_model_value = s.converter.back(optimathsat.msat_get_model_value(env, msat_obj_term))
print("(model-val {}: {})".format(cost_fn, msat_model_value), end=" ")
msat_value = optimathsat.msat_objective_value_term(env, obj, optimathsat.MSAT_OPTIMUM, None, None)
value = s.converter.back(msat_value)
print("(obj-val {}: {})".format(cost_fn, value), end=" ")
optimathsat.msat_destroy_objective_iterator(obj_iter)
print()with output Value: (model-val x: 11) (obj-val x: 100) (model-val y: 100) (obj-val y: 100) I think this might be a bug in OptiMathSAT, but I need to investigate further, since it's very hard to reproduce. I'll let you know if I make any progress 😄 |
|
Also, with the above example, if I dump the smt-lib file with "debug.api_call_trace=3" and feed it to the command-line executable*, it gives the correct answer 😅 *I also have to manually modify "opt.priority=par" as it is set after initialization. Maybe PySMT sets some other options? |
|
Thanks for the investigation, @masinag !! I am not aware of special options passed by PySMT, but you can have a look at the |
Fix #810.
Hi, we released a new version of OptiMathSAT. The broken tests are now fixed.
I tested it on Linux and MacOS (I compiled it for arm64 only, I hope this is not a problem).
Bindings generation on Windows is still broken, but it was also broken with the previous version: