how to suppress simplification of formulas to True or False?

2
votes

is it possible to disable automatic simplifications of boolean expressions in Z3?

For example, the expression 2 > 1 becomes True automatically while I would like it to stay 2 > 1:

>>> t = 2 > 1
>>> t
True

I found several options by calling help_simplify() in Z3Py. However, none of them seems to relate to my problem.

In another tutorial (http://citeseerx.ist.psu.edu/viewdoc/download?rep=rep1&type=pdf&doi=10.1.1.225.8231) an option "CONTEXT SIMPLIFIER" was mentioned: "This setting can be used to simplify sub-formulas to true or false." However, I could not find this option in Z3Py.

Background: I would like to be able to use expressions like And(2>1, 1!=2) where 2>1 and 1!=2 are automatically generated earlier and sometimes contain no variables (constants). Z3Py simplifies this to And(True, False) which is not accepted, because "At least one of the arguments must be a Z3 expression or probe". Therefore, I would like to suppress the simplification. Or is there a way to make And(True, False) an accepted expression?

Thanks in advance!

1
z3z3py
well, I just noticed that this simplification is already done by the python interactive shell: it evaluates the simple comparison 2 > 1 before Z3Py actually could even do it. However, my question remains: how to suppress this and hand Z3Py the term "2 > 1" and/or how to allow And(True,False) expressions? - Carsten Rütz

1 Answers

1
votes

Indeed, this is because simple expressions like 2>1 are simplified to True/False by Python. Most operators (like Implies, Xor, ...) were fine with this, but the And and Or operators were not. They had a different implementation because they can be used for probes as well as expressions. I have now added a little bit more code to make them behave like the other Boolean operators (for fix see here). I hope this fixes this problem while not introducing any new problems with probes. I'd be grateful if other could test this some more.