When choosing instantiations for quantified assumptions (without mbqi), Z3 searches its e-graph of ground terms (modulo equalities) for possible matches. I understood that this e-graph consists of the ground terms present in the original problem, plus those which are formed during the proof search. However, it seems that a ground term mentioned under a quantifier is not used as a candidate for matching, until the surrounding quantifier itself is instantiated.
For example, if I write:
(assert
(forall ((n Int) ) (!
(and (f 0) (g n))
:pattern ((g n))
)))
(assert (forall ((n Int) ) (!
(not (= (h n) n))
:pattern ((f n))
)))
(assert (= (h 0) 0))
(check-sat)
Then Z3 reports unknown. Whereas if I pull the conjunction of (f 0) out of the forall (as in the full example below) then Z3 reports unsat (and if I track statistics, I can see that the second quantifier is instantiated.
I find this behaviour a bit confusing, and I wondered whether or not it is intended? If so, what is the rationale behind this choice? I think it could be affecting some of our axiomatisations (but need to debug the details further).
By the way, we tried using a let expression to pull the ground term out of the quantifier, but (probably because let expressions are just substituted back in again?) we didn't see a difference.
The full version of the example is here:
(set-option :print-success true) ; Boogie: false
(set-option :global-decls true) ; Boogie: default
(set-option :auto_config false) ; Usually a good idea
(set-option :smt.mbqi false)
(set-option :model.v2 true)
(set-option :smt.phase_selection 0)
(set-option :smt.restart_strategy 0)
(set-option :smt.restart_factor |1.5|)
(set-option :smt.arith.random_initial_value true)
(set-option :smt.case_split 5)
(set-option :smt.delay_units true)
(set-option :smt.delay_units_threshold 16)
(set-option :nnf.sk_hack true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.qi.cost "(+ weight generation)")
(set-option :type_check true)
(set-option :smt.bv.reflect true)
(set-option :smt.qi.profile true)
(declare-fun f (Int) Bool)
(declare-fun g (Int) Bool)
(declare-fun h (Int) Int)
(assert
(forall ((n Int) ) (!
(and (f 0) (g n))
:pattern ((g n))
)))
; this version of the above axiom lets us get "unsat"
;(assert
; (and (f 0) (forall ((n Int) ) (!
; (g n)
; :pattern ((g n)))
; )))
(assert (forall ((n Int) ) (!
(not (= (h n) n))
:pattern ((f n))
)))
(assert (= (h 0) 0))
(check-sat)
(get-info :all-statistics)
FWIW, given what I know about Z3's quantifier instantiation mechanisms these days, it's pretty clear that this behaviour is expected; ground terms that happen to be under a quantifier won't make it into the E-graph until the quantifier is instantiated.