Different ways of axiomatising a contains-function

问题:

Axiomatising the contains-operation on lists (on Rise4Fun) as

(declare-fun Seq.in ((List Int) Int) Bool)

(assert (forall ((e Int))
  (not (Seq.in nil e))))

(assert (forall ((xs (List Int)) (e Int))
  (iff
    (not (= xs nil))
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

enables Z3 4.0 to refute the assertion

(declare-const x Int)
(assert (Seq.in nil x))
(check-sat) ; UNSAT, as expected

The in my eyes equivalent axiomatisation

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

results in unknown.

Could this be a problem with triggers or is there something specific to the List domain that could explain the difference in behaviour?

回答1:

Your script at rise4fun disables the :mbqi engine. Thus, Z3 will try to solve the problems using only E-matching. When patterns (aka triggers) are not provided, Z3 will infer the triggers for us. Z3 uses many heuristics for inferring patterns/triggers. One of them is relevant for your script, and explains what is going on. Z3 will never select a pattern/trigger that produces a "matching loop". We say a pattern/trigger P produces a matching loop for quantifier Q when an instance of Q will produce a new matching for P. Let us consider the quantifier

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

Z3 will not select (Seq.in xs e) as a pattern/trigger for this quantifier because it will produce a matching loop. Suppose we have a ground term (Seq.in a b). This term matches the pattern (Seq.in xs e). Instantiating the quantifier with a will b will produce the term (Seq.in (tail a) b) that also matches the pattern (Seq.in xs e). Instantiating the quantifier with (tail a) and b will produce the term (Seq.in (tail (tail a)) b) which also matches the pattern (Seq.in xs e), and so on.

During the search, Z3 will block matching loops using several thresholds. However, the performance is usually affected. Thus, by default, Z3 will not select (Seq.in xs e) as pattern. Instead, it will select (Seq.in (tail xs) e). This pattern does not produce a matching loop, but it also prevents Z3 from proving the second and third queries to be unsatisfiable. Any limitation of the E-matching engine is usually handled by the :mbqi engine. However, :mbqi is disabled in your script.

If you provide the patterns for the second and third queries in your script. Z3 will prove all examples to be unsat. Here is your example with explicit patterns/triggers:

http://rise4fun.com/Z3/DkZd

The first example goes through even without using patterns because only the first quantifier is needed to prove the example to be unsat.

(assert (forall ((e Int))
  (not (Seq.in nil e))))

Note that (Seq.in nil e) is a perfect pattern for this quantifier, and it is the one selected by Z3.