Checking syntactic equivalence of two constraints efficiently in Z3

Question

Supposed I have two constraints(c1,c2) and I want to check whether they are syntactic identical:

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

Option 1: We could turn this into a satisfiability problem like this post: Whether two boolexpr are equal

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

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

But both of those two options have a big overhead as the size of constraints increase. e.g. invoking the toString() method in Expr is very expensive for large constraints.

Two questions:

1. How to check whether two constraints are syntactically identical efficiently in Z3(Java version)?

2. If we don't have a good solution for 1, I am considering writing a wrapper for the Expr object and using a factory method to avoid generating duplicated(syntactically) objects from Z3. Then I have to design my own equal() and hashCode() functions. But I still can't figure out an efficient way so far.

Answer 1

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

Answer 2

Not really an answer, but way too long for a comment.

invoking the toString() method in Expr is very expensive for large constraints.

I'd suggest to look at the toString implementation. There's one possible reason for it being slow: dumb String concatenation instead of using StringBuilder. If so, then you might want to provide a faster implementation. However, solving a CSP whose printing takes too long is pretty futile, anyway.

How to check whether two constraints are syntactically identical efficiently in Z3

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

You'd probably need to normalize the expressions using commutativity, associativity, and maybe also other rules. For this you need some arbitrary but equals-consistent ordering on the terms.

You surely don't want to check all pairs of constraints for equality. Here, putting the constrains into buckets according to their hash code helps. No idea, if the provided hashCode is usable for this purpose.

Then I have to design my own equal() and hashCode() functions. But I still can't figure out an efficient way so far.

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