Keep getting "unknown" result with :pattern usage in SMTLIB v2 input

Question

I'm encountering a problem when using the SMTLIBv2 input format and patterns with Z3: I keep getting the result "unknown" with the following input:

(declare-datatypes () ((L L0 L1)))
(declare-fun path () (List L))
(declare-fun checkTransition ((List L)) Bool)

(define-fun isCons ((p (List L))) Bool
    (not (= p nil))
)

; configuration options for :pattern, taken from the Z3 tutorial
(set-option :auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false)    ; disable model-based quantifier instantiation

(assert (isCons path))
(assert (isCons (tail path)))
(assert (= nil (tail (tail path))))
(assert (= L0 (head path)))             ; initial state constraint

(assert
    (forall ((p (List L)))
    (!
        (implies
            (and    (isCons p)
                    (isCons (tail p)))
            (and    (=  L0  (head p))           ; transition from L0
                    (=  L1  (head (tail p)))))  ; to L1
    :pattern ((checkTransition p))
    )
    )
)
(assert (checkTransition path))

(check-sat)
(get-model)

I use a list to represent the possible paths through a transition system. The transition system in this case consists only of states L0 and L1 which are linked by a transition from L0 to L1. By assert statements I limit the paths to such that start with L0 and are of length 2. I expect to get as a model the path (L0 (cons (L1 (cons nil)))).

I already tried to boil it down to a minimal example that still shows the problem, resulting in the code above. I want to use the pattern to implement a recursive check on 'path', to ensure that each two consecutive nodes in the list comply with some (transition) constraint. The check for consecutive cons is used as a stopping condition for this recursive check. Although in the example above I removed the recursive check via checkTransition, it still does not work. The whole idea goes back to an article by Milicevic and Kugler in which they use Z3 2.0 and the .net API to represent a Model Checking problem in such a way.

I'm aware that pattern instantiation can lead to the result "unknown", but I was wondering why it already happens with such a simple (?) example. Am I using the pattern in a wrong way to achieve quantifier support?

Any ideas on this problem are more than welcome!

Regards Carsten

P.S.: I use Z3 version 4.3.2 on MacOS X (10.8.3) The mentioned article: Milicevic, A. & Kugler, H., 2011. Model checking using SMT and theory of lists. NASA Formal Methods, pp.282–297.

EDIT based on comments of mhs:

The problem of not getting a model seems to occur from version 4.3.2 (unstable). I did some troubleshooting with different versions:

Z3 4.3.0 32bit, WinXP 32bit, from installer
- result: unknown, but gives a model
Z3 version 4.3.1, git checkout 89c1785b73225a1b363c0e485f854613121b70a7, MacOS X, self compiled, this is the newest version in the master branch....
- result: unknown, but gives a model
various other checkouts of the master branch, all <= 4.3.1 yield the same result.
Z3 version 4.3.2, nightly built z3-4.3.2.197b2e8ddb91-x64-osx-10.8.2, MacOS X...
- result: unknown, gives NO model
Z3 version 4.3.2, nightly built z3-4.3.2.96f4606a7f2d-x64-osx-10.8.2, MacOS X...
- result: unknown, gives NO model

interesting?

Malte Schwerhoff Malte Schwerhoff · Accepted Answer · 2013-04-04T08:43:31

I just tried your example on Z3 4.3.0 on Win 7 x64 and I get the result

unknown

(model 
  (define-fun path () (List L)
    (insert L0 (insert L1 nil)))

  (define-fun checkTransition ((x!1 (List L))) Bool
    (ite (= x!1 (insert L0 (insert L1 nil))) true
      true))
)

Isn't that the model for path you expected?

I assume that you get unknown because your problem is under-specified, though I cannot put my finger on a concrete problem. If you give Z3 something to refute, for example by appending

(assert (not (= L1 (head (tail path)))))
(check-sat)

to your code, then you'll get unsat as expected.

Keep getting "unknown" result with :pattern usage in SMTLIB v2 input

2 Answers