Tactics: ctx-solver-simplify not Simplifying

[sameer]

Hello,

I'm a maintainer for the Rust bindings for z3 and we have a failing unit test for the ctx-solver-simplify tactic. Trying to understand whether this is the new expected behavior. It worked on z3 v4.8.10, but not on v4.8.12

In v4.8.10:

(declare-const x Bool)
(declare-const y Int)
(assert x)
(assert (>= y 1))
(assert (>= y 2))
(apply ctx-solver-simplify)
; Removes (>= y 1) in the output goal
(goals
(goal
  x
  (>= y 2)
  :precision precise :depth 1)
)

In v4.8.12:

(declare-const x Bool)
(declare-const y Int)
(assert x)
(assert (>= y 1))
(assert (>= y 2))
(apply ctx-solver-simplify)
; Leaves (>= y 1) in the output goal
(goals
(goal
  x
  (>= y 1)
  (>= y 2)
  :precision precise :depth 1)
)

Is this behavior expected?

[NikolajBjorner]

The behavior of ctx-solver-simplify is going to be fragile between versions. It would be nice that it removed y >= 2, but there are no guarantees and I prefer not to associate an SLA for this feature.

[sameer]

That's fair, do you know if there's a specific tactic that would be more stable here?

[NikolajBjorner]

There is currently unit-subsume-simplify. It accomplishes the simplification you want for this particular example. Stronger subsumption simplification is possible, though, so maybe good to revisit if you have a use case.

[sameer]

Thanks Nikolaj! :slightly_smiling_face:

[NikolajBjorner]

There is a new tactic as well. It seeks to generalize unit-subsume-simplify. The commit message has more information.

[vielfarbig]

Thank you very much Nikolaj! The solver-subsumption tactic is working for my Use-Case instead of the ctx-solver-simplify or unit-subsume-simplify.

I have the following in v4.11.2 with z3py (z3-solver package):

(declare-const x Int)
(declare-const y Int)
(assert (or (= x 1) (= x 0)))
(assert (or (= y 1) (= y 0)))
(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))
(assert (<= (+ (* -1.0 x) (* 1.0 y) ) 0))
(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))
(assert (<= (+ (* 0.0 x) (* 0.0 y) ) 0))
(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))
(assert (<= (+ (* 0.0 x) (* 0.0 y) ) 0))
(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))

The following always together with propagate-ineqs

With the solver-subsumption I get the desired

[[x == 1, y == 0]]

otherwise I the get the following for ctx-solver-simplify

[[Or(x == 1, x == 0),
  Or(y == 1, y == 0),
  1*ToReal(x) + -1*ToReal(y) > ToReal(0),
  -1*ToReal(x) + 1*ToReal(y) <= ToReal(0),
  0*ToReal(x) + 0*ToReal(y) <= ToReal(0)]]

and for unit-subsume-simplify

[[Or(x == 1, x == 0),
  Or(y == 1, y == 0),
  1*ToReal(x) + -1*ToReal(y) > ToReal(0)]]

For reference I used the following code:

from z3 import *

t = Then('solver-subsumption',
         'propagate-ineqs')

g = Goal()

assertion_terms = ['(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))', '(assert (<= (+ (* -1.0 x) (* 1.0 y) ) 0))',
                   '(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))', '(assert (<= (+ (* 0.0 x) (* 0.0 y) ) 0))',
                   '(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))', '(assert (<= (+ (* 0.0 x) (* 0.0 y) ) 0))',
                   '(assert (> (+ (* 1.0 x) (* -1.0 y) ) 0))']
smt2_string = '(declare-const x Int) (declare-const y Int) (assert (or (= x 1) (= x 0))) (assert (or (= y 1) (= y 0))) '
for assertion_term in assertion_terms:
    smt2_string += assertion_term + " "

print(smt2_string)
g.add(parse_smt2_string(smt2_string))

r = t(g)

print(r)