Question of quantifier instantiation strategies

[dyd1024]

I am interested in if there are some strategies for quantifier instantiation? For example: f(n1, x0) != f(n1, y0), ForAll([i] , Implies( (i < n1), f(i, x0) == f(i, y0) ) ) How can I know which strategies are chosen when solving the above formula, such as MBQI, E-matching, etc. Thanks.

[Joshua27]

You can have a look at Z3's parameters for SMT solving: https://microsoft.github.io/z3guide/programming/Parameters/#smt E-Matching and MBQI are used by default.

[NikolajBjorner]

The method of instantiation isn't directly exposed. It can be mined for by using debug tracing, which is a low level activity. I have added a tag to proof objects created from the newer core.

Example:

C:\z3\build>type 7094.smt2 (declare-fun v () Int) (assert (forall ((V Int)) (= 0 (ite (= 1 (mod 7 V)) 1 0)))) (assert (= 0 (ite (= 1 (+ v v (mod 0 0))) 1 0))) (assert (= 0 (ite (= 0 (mod 1 v)) 1 0))) (check-sat) C:\z3\build>z3 7094.smt2 /v:2 sat.smt=true solver.proof.log=log.smt2 (sat.copy :learned 0) (sat.solver) (sat.stats :conflicts :restarts :learned/bin :gc :time) (sat.stats :decisions :clauses/bin :units :memory ) (sat.stats 0 0 0 6/6 0/0 6 0 23.48 0.00) (mbqi.check) (sat.solver) (sat.stats :conflicts :restarts :learned/bin :gc :time) (sat.stats :decisions :clauses/bin :units :memory ) (sat.stats 0 0 0 11/5 0/0 0 0 24.00 0.00) (sat.stats 4 15 0 15/5 8/1 0 0 24.00 0.01) (mbqi.check l_true) (sat.stats 1 6 0 6/6 1/0 6 0 24.00 0.03) unsat

C:\z3\build>type 7094.smt2

C:\z3\build>z3 log.smt2 (proofs -arith 1) (verified-smt (arith (not (= (mod 0 0) (mod0 0 0)))) (= (mod 0 0) (mod0 0 0))) (proofs -arith 2) (verified-smt (arith (not (= (mod 1 0) (mod0 1 0)))) (= (mod 1 0) (mod0 1 0))) (proofs -arith 3) (verified-smt (arith (not (= (div 1 v) (div0 1 v)))) (= (div 1 v) (div0 1 v))) (proofs +tseitin 1 -arith 3) (proofs +tseitin 2 -arith 3) (proofs +tseitin 2 -arith 4) (verified-smt (arith (not (= v 0)) (not (= (+ #82 #77) 1))) (= (+ ( v #67) (mod 1 v)) 1) (= v 0)) (proofs +tseitin 2 -arith 5) (verified-smt (arith (not (= v 0)) (not (>= (mod 1 v) 0))) (>= (mod 1 v) 0) (= v 0)) (proofs +tseitin 2 -arith 6) (verified-smt (arith (not (= v 0)) (not (<= (- #77 #69) (- 1)))) (= v 0) (<= (- (mod 1 v) (if #71 v #72)) (- 1))) (proofs +tseitin 2 -arith 7) (verified-smt (arith (not (= v 0)) (not (<= ( v #67) 1))) (= v 0) (<= ( v (div 1 v)) 1)) (proofs +tseitin 2 -arith 7 -nla 1) (verified-smt (nla 1 (= 0 (- v)) 1 (= 0 (- v)) 1 (= 1 (+ ( v #67) (mod 1 v))) 1 (= 1 (+ ( v #67) (mod 1 v))) 1 (= (div 1 v) (div0 1 v)) 1 (= (div 1 v) (div0 1 v)) 1 (= 0 (if (>= v 0) v (- v))) 1 (= 0 (if (>= v 0) v (- v))) ...) (= (+ (mod 1 v) ( #93 #69)) 1) (not (= 0 (- v))) (not (= 1 (+ #82 #77))) (not (= (div0 1 v) (div 1 v))) (not (= 0 (if #71 v #72)))) (proofs +tseitin 2 -arith 7 -nla 2) (verified-smt (nla 1 (= 0 (- v)) 1 (= 0 (- v)) 1 (= 1 (+ ( v #67) (mod 1 v))) 1 (= 1 (+ ( v #67) (mod 1 v))) 1 (= (div 1 v) (div0 1 v)) 1 (= (div 1 v) (div0 1 v)) 1 (= 0 (if (>= v 0) v (- v))) 1 (= 0 (if (>= v 0) v (- v))) ...) (not (= 0 (if #71 v #72))) (= (+ (mod 1 v) (* #93 #69)) 1) (not (= 1 (+ #82 #77))) (not (= (div0 1 v) (div 1 v))) (not (= 0 (- v)))) (proofs +tseitin 2 -arith 7 -nla 2 -inst 1) (verified-smt (inst (forall (vars (V Int)) (not (= 1 #26))) true (bind (- 6)) (gen 0) mbqi)) (proofs +tseitin 2 +rup 1 -arith 7 -nla 2 -inst 1)