I am confused by the use of soft constraints in z3. When running this program, I obtain the following output.
from z3 import *
o = Solver()
expr = f"""
(declare-const v Real)
(declare-const v1 Bool)
(assert-soft v1)
(assert (= v1 (<= 0 v)))
(assert (> 10 v))
"""
p = parse_smt2_string(expr)
o.add(p)
print(o.check())
print(o.model())
output: [v1 = False, v = -1]
Would someone please know why is the soft constraint not satisfied while there exist values for v which allow it?
Similarly, this program does not return the expected output:
from z3 import *
o = Optimize()
expr = f"""
(declare-const v1 Real)
(declare-const e Bool)
(assert (= e (<= 6 v1)))
(assert-soft e)
"""
p = parse_smt2_string(expr)
o.add(p)
print(o.check())
print(o.model())
It returns [v1 = 0, e = False]. Why can't the soft constraints be fulfilled?
It appears parse_smt2_string does not preserve soft assertions.
If you add print(o.sexpr()) right before you call check, it prints:
(declare-fun v () Real)
(declare-fun v1 () Bool)
(assert (= v1 (<= (to_real 0) v)))
(assert (> (to_real 10) v))
As you see, the soft-constraint has disappeared. So, what z3 sees is not what you thought it did. This explains the unexpected output.
I know that parse_smt2_string isn't exactly faithful, in the sense that it doesn't handle arbitrary SMTLib inputs. Whether this particular case is supported, I'm not sure. File it as an issue at https://github.com/Z3Prover/z3/issues and the developers might take a look.