Does ctx-solver-simplify (and similar tactics) produce equivalent formulas, or just SAT-equivalent, or am I doing things completely wrong?

3
votes

I'm trying to make z3 (I'm using z3py) to simplify some formulas for me (so that I can have more or less human-readable output). Using ctx-solver-simplify tactic seemed a good choice for me since in a couple of passes it would produce nice compact formulas. But soon I've run into a situation when the output of ctx-solver-simplify does not seem to be equivalent to the original formula (it looks more like being satisfiability-equivalent or so). Also, it might be the case that I'm not dealing with tactics correctly.

Here's what I was trying to do: http://rise4fun.com/Z3Py/g5sX. So, I construct a formula Set2 (everything before the definition of Set2 is just a setup needed to define it) which has a particular satisfying assignment. After applying ctx-solver-simplify, I get a single formula (as a goal) for which this assignment is not satisfying. So what am I dong wrong?

  • Am I wrong assuming that ctx-solver-simplify would produce an equivalent formula?
  • Am I handling the tactics and their output in the wrong way?
  • Anything else?

Thanks.

1
z3

1 Answers

1
votes

I have been looking into this, but have so far been unable to reproduce the bug directly with our current branch. A bug in the context simplifier was fixed a little while ago, and it could be manifesting itself with the online version of Z3. There are still a few things I can do to double check if we can reproduce the bug and I will update this post with what I find.