Puzzling (and fragile) result from e-matching-related SMT query

user_1551481 0
Viewed 90

For the following smt file (which has been minimised a lot from a Viper/Boogie-generated example) , Z3 returns unknown (very fast).

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
(set-option :pp.bv_literals 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 3)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)
; (options as set by Boogie)

(declare-sort T@Seq 0)
(declare-fun Append (T@Seq T@Seq) T@Seq)
(declare-fun Empty () T@Seq)
(declare-fun Singleton (Int) T@Seq)
(declare-fun dummy () Bool)
(declare-fun Contains (T@Seq Int) Bool)
; Empty ++ s == s
(assert (forall ((s T@Seq) ) (! (= (Append Empty s) s)
 :qid |_0314cbp.11:15|
 :skolemid |0|
 :pattern ( (Append Empty s))
)))
; (strange axiom)
; forall s0,s1 :: {s0++s1} s0 != Empty ==> dummy
(assert (forall ((s0 T@Seq) (s1 T@Seq) ) (!  (=> (not (= s0 Empty)) dummy)
 :qid |_0314cbp.17:15|
 :skolemid |3|
 :pattern ( (Append s0 s1))
)))
; forall s0,s1,x :: {(Contains s0++s1 x)} Contains s0++s1 x <==> (Contains s0 x || Contains s1 x)
(assert (forall ((s0@@0 T@Seq) (s1@@0 T@Seq) (x Int) ) (!  (and (=>     (Contains (Append s0@@0 s1@@0) x) (or (Contains s0@@0 x) (Contains s1@@0 x))) (=> (or (Contains s0@@0 x) (Contains s1@@0 x)) (Contains (Append s0@@0 s1@@0) x)))
 :qid |_0314cbp.22:15|
 :skolemid |4|
 :pattern ( (Contains (Append s0@@0 s1@@0) x))
)))
(declare-fun s () T@Seq)
(declare-fun s1 () T@Seq) ; spurious term, used for assumption
(declare-fun i () Int)
(declare-fun f (Int) Bool)
(push 1)
(assert (not
; forall x_1 :: {(Contains s x_1)} f x_1
(=> (and (forall ((x_1 Int) ) (! (f x_1)
 :qid |_0314cbp.34:20|
 :skolemid |5|
 :pattern ( (Contains s x_1))
)) (= s1 (Append s (Singleton 1)))) (=> (Contains (Append s (Singleton 1)) i ) ( f i ))))
)
(check-sat)
(pop 1)
; Invalid

My understanding is that this result is expected; the only way to obtain unsat that I'm aware of, is to instantiate the last quantifier (inside the last asserted formula), whose pattern is (Contains s x_1). This term is not known in the context; what is possible is for the known (Contains (Append s (Singleton 1)) i ) to cause the quantifier with :qid |_0314cbp.22:15| to be instantiated, which yields the disjunction (or (Contains s i ) (Contains (Singleton 1) i)). If/when Z3 branches on this disjunction, the former case will have the term to get unsat from the last axiom with, but the latter will not. As is explained elsewhere, Z3 will backtrack the instantiations made between such case-splits.

What's surprising to me about the example is that many modifications can be made to it to obtain an unsat result, and these either weaken the logical assumptions made, or leave them unchanged; in each case I don't understand why the same reasoning as above would not apply to explain that unknown should be expected. For example:

  1. The assumption (= s1 (Append s (Singleton 1))) is spurious; the term s1 is not used anywhere else in the problem, and (Append s (Singleton 1)) is a known term in the following implication (so its presence should not affect potential e-matching). However, removing it, or replacing it with true (i.e. weakening the assumptions made) will result in unsat.

  2. Removing either of the first two quantifiers (the second of which has no logical meaning) will result in unsat.

  3. Rewriting the third axiom to express an implication (Contains s0++s1 x ==> (Contains s0 x || Contains s1 x)) rather than an if-and-only-if will result in unsat.

  4. Removing the (push 1) and (pop 1) will result in unsat.

My main question is, are these (changes of) behaviours expected, and how can I explain them? In addition, if there is a good way to see what Z3 does with the problem, and try to uncover more information for myself, I'd be happy to do so.

I have tried the example (and its variants) using the Axiom Profiler tool; there I was able to see that the same number of quantifier instantiations are made (3), but in the case of the axiom about distributing Contains over Append, sometimes a simplified term seems to be learned by Z3, rather than the full quantifier body. I can provide more details of this if they would be useful.

z3
0 Answers
Related