CODEWITHSUNDEEP
z3
user1861926
user1861926

Reputation: 67

Asymmetric behavior in ctx-solver-simplify

I'm seeing rather surprising behavior from ctx-solver-simplify, where the order of parameters to z3.And() seems to matter, using the latest version of Z3 from the master branch of https://git01.codeplex.com/z3 (89c1785b):

#!/usr/bin/python
import z3

a, b = z3.Bools('a b')
p = z3.Not(a)
q = z3.Or(a, b)
for e in z3.And(p, q), z3.And(q, p):
  print e, '->', z3.Tactic('ctx-solver-simplify')(e)

produces:

And(Not(a), Or(a, b)) -> [[Not(a), Or(a, b)]]
And(Or(a, b), Not(a)) -> [[b, Not(a)]]

Is this a bug in Z3?

Upvotes: 2

Views: 821

Answers (2)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

No, this is not a bug. The tactic ctx-solver-simplify is very expensive and inherently asymmetric. That is, the order the sub-formulas are visited affect the final result. This tactic is implemented in the file src/smt/tactic/ctx_solver_simplify_tactic.cpp. The code is quite readable. Note that, it uses a "SMT" solver (m_solver), and makes several calls to m_solver.check() while traversing the input formula. Each one of these calls can be quite expensive. For particular problem domains, we can implement a version of this tactic that is even more expensive, and avoids the asymmetry described in your question.

EDIT:

You may also consider the tactic ctx-simplify, it is cheaper than ctx-solver-simplify, but it is symmetric. The tactic ctx-simplify will essentially applies rules such as:

A \/ F[A] ==> A \/ F[false]
x != c \/ F[x] ==> F[c]

Where F[A] is a formula that may contain A. It is cheaper than ctx-solver-simplify because it does not invoke a SMT solver when it is traversing the formula. Here is an example using this tactic (also available online):

a, b = Bools('a b')
p = Not(a)
q = Or(a, b)
c = Bool('c')
t = Then('simplify', 'propagate-values', 'ctx-simplify')
for e in Or(c, And(p, q)), Or(c, And(q, p)):
  print e, '->', t(e)

Regarding humand-readability, this was never a goal when implementing any tactic. Please, tell us if the tactic above is not good enough for your purposes.

Upvotes: 2

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

I think it will be better to write a custom tactic because there are other tradeoffs when you essentially ask for canonicity. Z3 does not have any tactics that convert formulas into a canonical form. So if you want something that always produces the same answer for formulas that are ground equivalent you will have to write a new normalizer that ensures this.

The ctx_solver_simplify_tactic furthermore makes some tradeoffs when simplifying formulas: it avoids simplifying the same sub-formula multiple times. If it did, it could increase the size of the resulting formula significantly (exponentially).

Upvotes: 2

Related Questions