Datatypes and quantifier patterns/triggers

Question

I observed a difference in Z3's quantifier triggering behaviour (I tried 4.4.0 and 4.4.2.3f02beb8203b) that I cannot explain. Consider the following program:

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-datatypes () ((Snap
  (Snap.unit)
  (Snap.combine (Snap.first Snap) (Snap.second Snap))
)))

(declare-fun fun (Snap Int) Bool)
(declare-fun bar (Int) Int)
(declare-const s1 Snap)
(declare-const s2 Snap)

(assert (forall ((i Int)) (!
  (> (bar i) 0)
  :pattern ((fun s1 i))
)))

(assert (fun s2 5))

(assert (not (> (bar 5) 0)))
(check-sat) ; unsat

As far as my understanding goes, the unsat is unexpected: Z3 should not be able to trigger the forall since it is guarded by the pattern (fun s1 i), and Z3 should not be able (and actually isn't) to prove that s1 = s2.

In contrast, if I declare Snap to be an uninterpreted sort, then the final check-sat yields unknown - which is what I would expect:

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-sort Snap 0)

...

(check-sat) ; unknown

If I assume s1 and s2 to be different, i.e.

(assert (not (= s1 s2)))

then the final check-sat yields unknown in both cases.

For convenience, here is the example on rise4fun.

Q: Is the difference in behaviour a bug, or is it intended?

Answer 1

The assertion (not (= s1 s2)) is essential. With pattern based quantifier instantiation, the pattern matches if the current state of the search satisfies s1 = s2. In the case of algebraic data-types, Z3 tries to satisfy formulas with algebraic data-types by building a least model in terms of constructor applications. In the case of Snap as an algebraic data-type the least model for s1, s2 have them both as Snap.unit. At that point, the trigger is enabled because the terms E-match. In other words, modulo the congruences, the variable I can be instantiated such that (fun s1 I) matches (fun s2 5), but setting I <- 5. After the trigger is enabled, the quantifier is instantiated and the axiom

(=> (forall I F(I))  (F(5))) 

is added (where F is the formula under the quantifier).

This then enables to infer the contradiction and infer unsat.

When Snap is uninterpreted, Z3 attempts to construct a model where terms s1 and s2 are different. Since there is nothing to force these terms to be equal they remain distinct

Answer 2

It's not a bug since z3 doesn't say unsat for a sat formula (or sat for an unsat one). In presence of quantified formulas, SMT solvers are (in general) not complete. So they sometimes answer unknown when they are not sure that the input formula in sat.

For your example:

a - It's normal that, with matching techniques, z3 does not prove the formula when you assume that s1 and s2 are different. In fact, there is no ground term of the form (fun s1 5) that matches the pattern (fun s1 i), and that would allow the generation of the useful instance (> (bar 5) 0) from your quantified formula;

b - When you don't assume that s1 and s2 are different, you would not be able to get the proof too. Except that z3 probably assumes internally that s1 = s2 when Snap is a datatype. This is correct as long as there is nothing that contradicts s1 = s2. Thanks to this and to matching modulo equality, the ground term (fun s2 5) matches the pattern (fun s1 i), and the needed instance to prove unsatisfiability is generated.