Strange unsat core with sequences

[GerhardSchellhorn]

Unsat result seems to be wrong (detailed analysis in email from 23.1.19).

(set-option :smt.auto-config false) ; disable automatic self configuration (set-option :smt.mbqi false) ; disable model-based quantifier instantiation (set-option :smt.ematching true) ; enable ematching (set-option :smt.macro-finder true) (set-option :smt.pull_nested_quantifiers false) (set-option :unsat_core true) (set-option :timeout 50)

;;;sorts (declare-sort elem)

;;;lists (define-sort list () (Seq elem))

;;(declare-fun prepend (elem list) list) ;; prepend an element to a list (axiom commented out)

;;;operations

;; replaces the nth-element (zero-based) with a new one. Unspecified for n >= length (and n < 0) ;; axioms commented out (declare-fun put (list Int elem) list)

(declare-fun __nat-valid (Int) Bool) ;; same as n >= 0 (axiom commented out) (declare-fun get (list Int) elem) ;; get the nth-element (zero-based). Unspecified for n >= length (and n < 0)

;;;axioms

;;; adding the commented axioms below (to give meaningful interpretations to nat-valid and put) does not change the result ;;; (assert ;;; (forall ((n Int)) ;;; (! ;;; (= ; <-> ;;; (nat-valid n) ;;; (>= n 0) ;;; ) ;;; :pattern (__nat-valid n) ;;; )))

;;; prepend(a,x) = seq.unit(a) seq.++ x ;;; (assert ;;; (forall ((a elem) (x list)) ;;; (! ;;; (= (preprend a x) (seq.++ (seq.unit a) x)) ;;; :pattern (prepend a x) ;;; )))

;; get(x,n) = a <-> seq.extract(x,n) = seq.unit(a)

(assert

(forall ((n Int) (x list) (a elem)) (! (=> (__nat-valid n) (= ; <-> (= (get x n) a) (= (seq.at x n) (seq.unit a)) )) :pattern (= (get x n) a) ) ))

;; if the above axiom is replaced with the same axiom, but named (as commented out below), the result becomes "unknown" ;;; (assert ;;; (! ;;; (forall ((n Int) (x list) (a elem)) ;;; (! ;;; (=> (__nat-valid n) (= ; <-> ;;; (= (get x n) a) ;;; (= (seq.at x n) (seq.unit a)) ;;; )) ;;; :pattern (= (get x n) a) ;;; )) ;;; :named get-vs-extract ;;; ))

;; put(seq.unit(b) + x,0,a) = prepend(a,x) ;;(assert (! ;; (forall ((b elem) (x list) (a elem)) ;; (! ;; (= (put (seq.++ (seq.unit b) x) 0 a) (prepend a x)) ;; :pattern (put (seq.++ (seq.unit b) x) 0 a) ;; )) ;; :named list-del--put-zero))

;;; n >= 0 => put(seq.unit(b) ++ x, n + 1, a) = prepend(b,put(x,n,a)) ;;; (assert (! (forall ((n Int) (b elem) (x list) (a elem)) ;;; (=> (_nat-valid n) ;;; (= (put (seq.++ (seq.unit b) x) (+ n 1) a) ;;; (+ b (put x n a))))) ;;; :named list-del--put-succ))

;; n >= 0 -> get(seq.unit(a) ++ x, n + 1) = get(x,n)

(assert (! (forall ((n Int) (a elem) (x list)) (=> (nat-valid n) (= (get (seq.++ (seq.unit a) x) (+ n 1)) (get x n)) )) :named list-del--get-succ)) ;; adding precondition n < x.length (as commented out below) changes the result to "unknown"
;(assert (! (forall ((n Int) (a elem) (x list)) ; (=> (and (nat-valid n) (< n (seq.len x))) ; (= (get (seq.++ (seq.unit a) x) (+ n 1)) (get x n)))) ; :named list-del--get-succ))

;; get(seq.unit(a) ++ x,0) = a (redundant, provable from the unnamed definition of get) ;;(assert (! ;; (forall ((a elem) (x list)) ;; (! ;; (= (get (seq.++ (seq.unit a) x) 0) a) ;; :pattern (get (seq.++ (seq.unit a) x) 0) ;; )) ;; :named list-del--get-zero))

;;;goal ;; it is not possible (for any x,m,a,n) that all of the following hold ;; 1. m, n are different natural numbers (integers >=0) ;; 2. m < x.length ;; 3. get(put(x,m,a),n) is different from get(x,n)

;; the goal should be provable with the full axioms, when the recursive definition of get is included. ;; the rec.def. enforces that for lists put(x,m,a) and x, which have the same length, ;; getting element n with n > x.length is for both lists equal to get(seq.empty, n - x.length) ;; (I assume however, that induction is required) ;; Without the axioms for put, a proof should not be possible.

(assert (! (not (forall ((x list) (m Int) (a elem) (n Int)) (not (and (not (= (get (put x m a) n) (get x n))) (and (not (= m n)) (and (< m (seq.len x)) (and (nat-valid m) (nat-valid n))) ))))) :named goal))

(check-sat) ;; returns (goal) (get-unsat-core)

[NikolajBjorner]

It is very possibly a good case for having more transparent proof tracing. In a nutshell here is what goes on. You have an axiom:

    (forall ((n Int) (x list) (a elem))          
           (= (get x n) a) (= (seq.at x n) (seq.unit a)))

Instantiate it with:

     n = n, x = empty, a = (get empty n)

The result is

           (= (get empty n) (get empty n))  (= (seq.at empty n) (seq.unit a)))

This simplifies to

           (= (seq.at empty n) (seq.unit a)))

The theory of sequences implies that

          (= (seq.at empty n) empty)

On the other hand,

          (not (= (seq.unit a) empty))

This is a contradiction.

If you add the (__nat-valid n) dependency, then this requires the "goal" assumption. This is why the core is (goal). However, the real issue is that the quantified axiom is inconsistent.

Z3 requires some opportune terms to be present for instantation to catch this. This is where the other terms are useful. It ends up using the disequality

      (not (= (get x n) (get y n))

from goal (I use y as short for (put x m a)) to produce something with "empty" that then can be used to instantiate the unsound axiom.

[GerhardSchellhorn]

Dear Nikolaj,

thanks for the feedback.

(= (seq.at empty n) empty)

I see that this axiom is of course contradictory to my axiom for get. I assumed that (seq.at empty n) would be unspecified (like my get). So I will simply change the axiom.

I relied on what's on rise4fun, Is there some documentation I missed where I can find the exact axioms (might be relevant for other functions, where I assume the result is unspecified, when outside the intended range)?

As a minor thing, I still don't understand is why naming the axiom changes the result from "unsat" to "unknown".

But ok, from the tests I did together with your info, it now seems that (= (seq.at x n) empty) is equivalent to n >= x.length in general. Right?

More importantly, coming back to my question from the last mail, I I would really like to understand why Z3 cannot prove the other trivial example I sent (which is one of many), and whether there is something systematic I can do about it. I attach the example here again, now with the get-axiom constrained by n <= x.length (which I had already checked not to be provable in the original mail).

Thanks for your patience, best regards

Gerhard

;; commenting out the first five lines (i.e. using default settings) does not help (set-option :smt.auto-config false) ; disable automatic self configuration (set-option :smt.mbqi false) ; disable model-based quantifier instantiation (set-option :smt.ematching true) ; enable ematching (set-option :smt.macro-finder true) (set-option :smt.pull_nested_quantifiers false)

(set-option :unsat_core true) (set-option :timeout 50)

;;;sorts (declare-sort elem)

;;;lists (define-sort list () (Seq elem))

;;;operations (declare-fun get (list Int) elem) ;; get the nth-element (zero-based). Unspecified for n >= length (and n < 0)

;; n >= 0 and n < x.length => (get(x,n) = a <-> seq.extract(x,n) = seq.unit(a)) (assert (! (forall ((n Int) (x list) (a elem)) (! (=> (and (>= n 0) (< n (seq.len x))) (= ; <-> (= (get x n) a) (= (seq.at x n) (seq.unit a)) )) :pattern (= (get x n) a) )) :named getdef ))

;; get (append(seq.unit(a),y),0) = seq.unit(a) ;; not proved (assert (! (not (forall ((a elem) (y list)) (= (get (seq.++ (seq.unit a) y) 0) a)
)) :named getgoalbase))

;; the goal that results from rewriting with the axiom above is proved
;;(assert (! (not ;; (forall ((a elem) (y list)) ;; (= (seq.at (seq.++ (seq.unit a) y) 0) (seq.unit a)) ;; )) ;; :named atgoalbase))

(check-sat) ;(get-unsat-core)

[NikolajBjorner]

not sure what is actionable: The last example produced "unknown". (get-info :reason-unknown) says it is due to incomplete quantifier instantiation. MBQI is disabled, by re-enabling MBQI the example diverges (also disable the 50ms timeout). So pattern-based quantifier instantiation just gives up very quickly. There aren't any triggers that it can use. MBQI on the other hand fails to find a finite model (for "get").

There is a little "dirty" Z3 secret too. You get use "seq.nth" for the nth element of a sequence.

 (define-fun get ((x list) (n Int)) elem (seq.nth x n))