Custom theory solver for order theory?

Question

My program, bounded synthesizer of reactive finite state systems, produces SMT queries to annotate a product automaton of the (uninterpreted) system and a specification. Essentially it is a model checking with uninterpreted functions. If the annotation exists => the model found by Z3 satisfies the spec. The queries contain:

• datatype (to encode states of a system and of a specification automaton)
• >= (greater), > (strictly) (to specify ranking function of states of automaton system*spec, which is used to search lassos with bad states)or in other words, ordering of states of that automaton, which
• uninterpreted functions with boolean domain and range
• all clauses are horn clauses

An example is https://dl.dropboxusercontent.com/u/444947/posts/full_arbiter2.smt2 ('forall' are used to encode "don't care" inputs to functions)

Currently queries take strictly greater > operator from integers arithmetic (that is a ranking function has Int range).

Question: is it worth developing a custom theory solver in Z3 for such queries? It could exploit DFS based search of lassos which might be faster than integers theory solver (or diff-neg tactic).

Or Z3 already efficiently handles this? (efficiently means "comparable to graph-based search of lassos").

Answer 1

Arithmetic is not the bottleneck of your benchmark. We can check that by using

valgrind --tool=callgrind z3 full_arbiter2.smt2 
kcachegrind

Valgrind and kcachegrind are available in most Linux distros. So, I don't think you will get a significant performance improvement if you implement a solver for order theory. One bottleneck is the datatype theory. You may get a performance boost if you encode the types Q and T using Bit-vectors. Another bottleneck is quantifier reasoning. Have you tried to expand them before invoking Z3? In Z3, the qe (quantifier elimination) tactic will essentially expand Boolean quantifiers. I got a small speedup by replacing

(check-sat)

with

(check-sat-using (then qe smt))