How to speed up / optimize queries involving lots of quantifiers

[logicReasoner]

I use Z3 from inside a C++ program. Currently it takes more than 5 seconds on a rather powerful machine to check the satisfiability of some auto-generated constraints. Can you please give me any tips on how to optimize Z3 (its code or switching to another tactic) or to rewrite my SMT lib code in order to make it much faster?

I create the solver using:

auto solver = (z3::tactic(context, "qe") & z3::tactic(context, "smt")).mk_solver();

As evident below, there are lots of forall and a few exists quantifiers. Here is a sample snippet (a part of a larger program):

(set-info :status unknown)
(declare-sort SomeType 0)
 (declare-sort EType 0)
 (declare-fun f1 (SomeType SomeType) Bool)
(declare-fun p1 (EType SomeType) Bool)
(declare-fun f2 (EType) Bool)
(declare-fun p2 (EType SomeType) Bool)
(declare-fun p3 (EType SomeType) Bool)
(declare-fun p4 (EType SomeType) Bool)
(declare-fun |53464| () SomeType)
(declare-fun |9127| () SomeType)

....

(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x51 (p3 constVarX0 y)))
 (let (($x23 (f1 x y)))
 (let (($x54 (and (and (f2 constVarX0) (p3 constVarX0 x)) $x23)))
 (=> $x54 $x51)))))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x57 (p4 constVarX0 y)))
 (let (($x23 (f1 x y)))
 (let (($x60 (and (and (f2 constVarX0) (p4 constVarX0 x)) $x23)))
 (=> $x60 $x57)))))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) )(let (($x64 (not (p2 constVarX0 x))))
 (=> (and (f2 constVarX0) (p1 constVarX0 x)) $x64)))
 )
(assert
 (forall ((constVarX0 EType) (constVarX1 EType) (x SomeType) (y SomeType) )(let (($x46 (p2 constVarX1 x)))
 (let (($x77 (not $x46)))
 (let (($x38 (p1 constVarX1 y)))
 (let (($x40 (f2 constVarX1)))
 (let (($x78 (p2 constVarX0 y)))
 (let (($x82 (and (and (f2 constVarX0) (p1 constVarX0 x)) $x78)))
 (=> (and (and $x82 $x40) $x38) $x77))))))))
 )
(assert
 (forall ((x SomeType) (y SomeType) (z SomeType) )(=> (and (f1 x y) (f1 y z)) (f1 x z)))
 )
(assert
 (forall ((x SomeType) )(f1 x x))
 )
(assert
 (forall ((x SomeType) (y SomeType) )(=> (and (f1 x y) (f1 y x)) (= x y)))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x38 (p1 constVarX0 y)))
 (let (($x31 (f1 y x)))
 (let (($x42 (and (and (f2 constVarX0) (p1 constVarX0 x)) $x31)))
 (=> $x42 $x38)))))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x45 (p2 constVarX0 y)))
 (let (($x23 (f1 x y)))
 (let (($x48 (and (and (f2 constVarX0) (p2 constVarX0 x)) $x23)))
 (=> $x48 $x45)))))
 )
(assert
 (forall ((constVarX0 EType) (constVarX1 EType) (x SomeType) )(let (($x92 (p5 constVarX0 "in")))
 (let (($x38 (p1 constVarX0 x)))
 (let (($x40 (f2 constVarX0)))
 (let (($x94 (and $x40 $x38)))
 (let (($x96 (and (and $x94 (p4 constVarX0 |24149|)) $x92)))
 (=> (and $x96 (f1 x |9127|)) (f1 x |53464|))))))))
 )
(assert
 (forall ((constVarX0 EType) (constVarX1 EType) (x SomeType) )(let (($x104 (f1 x |2217|)))
 (let (($x92 (p5 constVarX0 "in")))
 (let (($x38 (p1 constVarX0 x)))
 (let (($x40 (f2 constVarX0)))
 (let (($x94 (and $x40 $x38)))
 (let (($x107 (and (and $x94 (p4 constVarX0 |43869|)) $x92)))
 (=> (and $x107 $x104) (f1 x |53444|)))))))))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x38 (p1 constVarX0 y)))
 (let (($x31 (f1 y x)))
 (let (($x101 (and (and (f3 constVarX0) (p1 constVarX0 x)) $x31)))
 (=> $x101 $x38)))))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x45 (p2 constVarX0 y)))
 (let (($x23 (f1 x y)))
 (let (($x113 (and (and (f3 constVarX0) (p2 constVarX0 x)) $x23)))
 (=> $x113 $x45)))))
 )
(assert
 (forall ((constVarX0 EType) (x SomeType) (y SomeType) )(let (($x51 (p3 constVarX0 y)))
 (let (($x23 (f1 x y)))
 (let (($x117 (and (and (f3 constVarX0) (p3 constVarX0 x)) $x23)))
 (=> $x117 $x51)))))
 )

...
(assert
 (f1 |51093| |5249|))
(assert
 (f1 |32261| |5249|))
(assert
 (not (f1 |53469| |713|)))
(check-sat)

[nunoplopes]

If you want it fast: 1) don't use user-defined sorts. Use a small bit-vector instead if possible 2) Combine all assert into one, with a single forall quantifier 3) maybe negate the formula to swap the exists/forall quantifiers if appropriate 4) Play with tactics. qe may or may not be good for you. There's also qe-light. Or ufbv if using bit-vectors 5) Consider doing some pre-processing on your side to remove some of the quantifiers. Some seem like trivial axioms that you can inline. 6) etc.

I'm not aware of any tutorial on how to make SMT solvers run fast. It's all in people's brains. It comes with experience.

[logicReasoner]

@nunoplopes thanks for the tips! Can you give some examples on how to rewrite my code above regarding your points 1, 2, 5 (using bit-vectors; combining asserts; and inlining axioms)? The code is auto-generated but I could tweak the generator where suitable.

Thanks in advance!