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)