Bounded model checking with Z3 - Building the Expressions

2
votes

we are using Z3 for bounded model checking. To this end, we supply a whole bunch of expressions of the following form:

state_A_1 && !state_B_1 && sometrigger => !state_A_2 & state_B_2

In other words, we encode the passage of time (steps) by supplying a separate expression for each time step. Obviously, this results in several thousands of expressions.

While the time it takes for Z3 to solve those is acceptable (for the complexity of state machines we have), it takes quite a long time (several seconds) to build all of these expressions through the Z3 JNI Java API.

So here is my question: is there an easier way to tell Z3 to create all these time-unrolled expressions through some specialized API?

2
z3model-checking
Would you mind to quantify a bit "long time" and many many expressions ? Also how do you build these expressions (read from text file, or computed on the fly ? – Heyji
The expressions were built on the fly from another data structure by calling the Java/JNI API. It can be several thousands of expressions, building them takes several seconds. – Markus Völter

2 Answers

1
votes

Maybe you can make a function that encodes the timestep (e.g. TimeStep new = Next(old)).

Z3 has a "macro finder" that can transform an uninterpreted function plus a quantifier to expanded expressions. Maybe it's faster to create the expansion this way because it's all Z3 internal.

Otherwise, I have found expression creation performance to be good. I wonder if your code might just be very inefficient? Profile it. How did you conclude that Z3 is slow?

0
votes

I am not aware of any fast API in Z3 that would improve your situation. Several thousands of expressions in several seconds is not that bad a priori. You still have the traditionnal apporaches like profiling and parallel processing.

Also if your problem allows is, rather than working with boolean variable, you could think of factorizing them into bitvectors and working at vector level (i.e. deal with group of variables at once rather than dealing with all variable one by one) which could (if your problem allows it) save some time.