Simplifying Equations with Python z3 API

I'm trying to learn how to accomplish a few things when working with expressions in the Python z3 API.

I would like to be able to simplify/reduce sets of equations that contain intermediate variables. Say I have the Equations (A = B && C) and (C = D || E). In z3 these would be represented as (Bool('A') == And(Bool('B'), Bool('C')) and (Bool('C') == Or(Bool('D'), Bool('E')). Is there some function or series of functions that can be used to produce the simplified and reduced equation (A = B && (D || E))?
I would like to be able to convert a z3 expression into sum of products form (i.e Or(minterm1, minterm2,...).
An efficient way of determining the logical equivalence of two boolean equations.
A way of returning a boolean equations as formatted strings (i.e NOT in the nested function form used to declare the function.)

If anyone has any insight on any of these items, your input would be very much appreciated. Also, if any further clarification as to what is desired is needed, please let me know.

Thanks,

Solution

Great questions.

No, not in general. You can get z3 to simplify equations, but your notion of "simple" is unlikely to match what it will consider simple for its internal purposes. People often ask for this feature, but it is in general a very hard problem, and not at all clear what's meant by simple. Having said that, z3 does have a notion of Goal and Tactic, and there is even a simplify tactic that you can use. It will simplify the formulas, but having it behave precisely the way you want it to behave is a fool's errand.

See this great resource on tactics and perhaps you can play around to see to get something that works for you: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm
The simplify tactic does have a som option, I believe. That might do the trick. Again, see the above link, where they have the example:
```
s = Then(With('simplify', arith_lhs=True, som=True),
     'normalize-bounds', 'lia2pb', 'pb2bv', 
     'bit-blast', 'sat').solver()
```
The nugget som=True tells the solver to use sum-of-minterms. Again, your mileage might vary depending on the exact structure of your formulas, and z3 might introduce new names that might defeat the purpose.
Absolutely! This is what z3 excels at. Simply assert f != g where f and g are your equations. If z3 says unsat, then you know they are equivalent for all assignments to variables. If it gives you a model, that forms a counter-example to their equaivalence. (The negated-equality trick is very common in SMT solving: A formula is a tautology precisely when its negation is unsatisfiable. So, you can assert the negation of what you want and see if it comes back with unsat.)

Note that this is what SMT (and SAT) solvers excel at.
For any formula f you build, you can issue print f and it'll print it. But as you probably already observed, it will not look like your textbook logical formulas. The pretty-printer has some options to control its behaviour, but it's probably not quite what you want.

However, the API provides functions to walk down the AST and extract nodes as you wish. So, you can write your own pretty printer if you so desire. Doing so isn't terribly difficult, but that doesn't mean it's simple: There are many cases to consider and in my experience, such printers are usually not that hard to fool; i.e., produce something vastly worse for small changes to the input.

From a practical perspective, while z3 and its high-level APIs in Python, C, Java, etc., is capable of doing everything you want, it's not going to be out-of-the-box except for #3. My recommendation would be to code everything else yourself, and rely on z3 for checking equality where it excels at. Of course, this all depends on precisely what you're trying to do. Best of luck!