Checking the syntactic equivalence of two constraints is effective in Z3

Question

Suppose I have two constraints (c1, c2), and I want to check if they are syntactically identical:

c1: f(x)>1 && g(y)=2 c2: f(x)>1 && g(y)=2 

Option 1: We could turn this into a feasibility problem, such as a message: Will the two boolexpr be equal

Option 2: We could also turn them into strings and compare equality:

 if(c1.toString().equals(c2.toString())) ///do somthing 

But both of these parameters have a large overhead, as the size of the restrictions increases. for example, calling the toString () method in Expr is very expensive for large restrictions.

Two questions:

• How to check if two restrictions are strongly syntactically identical in Z3 (Java version)?

• If we do not have a good solution for 1, I consider creating a wrapper for the Expr object and using the factory method to avoid creating duplicate (syntactically) objects from Z3. Then I have to create my own equal () and hashCode () functions. But so far I still can’t find an effective way.

Answer 1

The Expr class derives from AST, which has the functions equals , compareTo and hashCode for this purpose. Since Z3 uses hash consing, this is very efficient, essentially just comparing pointers (and, in Java, casting).

Answer 2

Not quite an answer, but too long for comment.

calling the toString () method in Expr is very expensive for big restrictions.

I would suggest looking at the implementation of toString . There's one possible reason for this slow: dumb string concatenation instead of using StringBuilder . If so, then you might want to provide a faster implementation. However, a CSP solution whose printing takes too much time is useless anyway.

How to check if two restrictions in Z3 are very syntactically identical

I bet that using toString is not the way to go, since a && b and b && a equivalent, but their string representations are not.

You will probably need to normalize expressions using commutativity, associativity, and possibly other rules. To do this, you need some kind of arbitrary but equals consistent ordering in terms.

Of course, you do not want to check all pairs of equality constraints. Here, putting restrictions in buckets according to their hash code helps. I do not know if the provided hashCode applicable for this purpose.

Then I have to create my own equal () and hashCode () functions. But so far I still can’t find an effective way.

After normalization, this should be pretty simple. If you perform normalization and map each expression to a canonical representation (as String#intern does), you can use reference equality for equals . For hashCode you need a combining formula for each node tree, for example, you can calculate the hash code a && b as f(111 * ha + hb) , where ha and hb are hash codes a and b , respectively, and f(x) = x ^ (x>>15) or something like that.