Optimising z3 input

Question

I am trying to optimize z3 python input that is generated from my models. I am able to run it on models up 15k constraints (200 states) and then z3 stops finishing in reasonable time (<10 minutes). Is there a way to optimize the constraints that are generated from my models ?

Model for 3 states:

http://pastebin.com/EHZ1P20C

Answer 1

The performance of the script http://pastebin.com/F5iuhN42 can be improved by using a custom strategy. Z3 allows users to define custom strategies/solvers. This tutorial shows how to define strategies/tactics using the Z3 Python API. In the script http://pastebin.com/F5iuhN42, if we replace the line

s = Solver()

with

s = Then('simplify', 'elim-term-ite', 'solve-eqs', 'smt').solver()

the runtime will decrease from 30 secs to 1 sec (on my machine).

The procedure Then is creating a strategy/tactic composed of 4 steps:

• Simplifier (i.e., a rewriter that applies rules such as x + 1 - x + y ==> 1 + y

• Elimination of expressions of the form If(a, b, c) where b and c are not Boolean. The script makes extensive use this kind of expression. The tactic elim-term-ite will apply transformations that eliminate this kind of expression.

• Equational solver. It applies transformations such as x = a And F[x] ==> F[a]. In the script above, this tactic can eliminate more than 1000 variables.

• The tactic smt invokes a general purpose SMT solver in Z3.

The method .solver() converts a Z3 tactic/strategy into a solver object that provides the add and check methods. The tutorial that I included in the beginning of the message has more details.