How to check whether two z3 boolean expressions are equivalent?

[jumormt]

Thanks for the great work!

Suppose we have two boolean expressions as following:

1. expr1: C1 || (C1 && C2)
2. expr2: C2

Note that C1 and C2 are both bool_const.

Is it a way to check whether these two expressions (expr1, expr2) are equivalent?

z3::eq(expr1, expr2) returns false here. I have also tried the tactic "simplify" which cannot transform expr1 to C2.

The tactic "ctx-solver-simplify" seems to work but could bring trade-offs especially when the boolean expression becomes large. Also, it can introduce some auxiliary variables like let a!1, which is not readable for me. It would be nice if you can explain why that happens. :-)

[NikolajBjorner]

1. z3::eq checks that expr1, expr2 are the same identical abstract syntax trees.
2. simplify is a heuristic rewriting feature that performs best effort rewriting. It does not convert equivalent expressions into the same expression.
3. you check such properties by making a satisfiability query. You create a formula (expr1 != expr2). Check if that formula is satisfiable. If it is unsat, then expr1 and expr2 are equivalent.

[jumormt]

Thanks for your quick reply. I'll try the formula expr1 != expr2.