how to use declare-fun with values in Z3 SMTLIB

Question

while prowling stackoverflow and the internet for bits of info about Z3 i came across an example which looks like a planning problem. They (declare-fun myFunc (Int Int) Int) and later use expression of the form (assert (= (myFunc 3 3) 9) ) (assert (= (myFunc 4 4) 16 )

to fill it with values. I havent seen this kind of expression in other examples, i read it like "it is true that the function myFunc with parameters 3 3 evalutaes to 9". I converted one of my functions which does a simple calculation to this form of 'lookup-function'. Great performance boost !! Applying this to another function which should return a Bool turned out to be not so easy. The model shows me that it has this internal form:

; define neighbor-property by position distance, instead of row/col-distance
(declare-fun isPosNeighbor ( Int Int Int ) Bool )    ; this is later filled with values

(assert (= (isPosNeighbor 0 0 0 ) false  ) ) ; provide the default value
(assert (= (isPosNeighbor   1   0  1 ) true ) ) 
(assert (= (isPosNeighbor   1   1  2 ) true ) ) 
(assert (= (isPosNeighbor   1   3  4 ) true ) ) 
(assert (= (isPosNeighbor   1   5  6 ) true ) ) 

(assert (= (isPosNeighbor  10   0 10 ) true ) ) 
(assert (= (isPosNeighbor  10   1 11 ) true ) ) 
(assert (= (isPosNeighbor  10   2 12 ) true ) ) 
(assert (= (isPosNeighbor  10   3 13 ) true ) ) 
(assert (= (isPosNeighbor  10  12 22 ) true ) ) 

(check-sat)
(get-model)
(eval  (isPosNeighbor 33 4 1))   ; should return false

How can i force isPosNeighbor to return false for values not given? How can i influence the final true in the ite-sequence ?

sat 
(model (define-fun isPosNeighbor ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
  (ite (and (= x!0 0) (= x!1 0) (= x!2 0)) false 
  (ite (and (= x!0 1) (= x!1 0) (= x!2 1)) true
  (ite (and (= x!0 1) (= x!1 1) (= x!2 2)) true 
  (ite (and (= x!0 1) (= x!1 7) (= x!2 8)) true 
  (ite (and (= x!0 1) (= x!1 8) (= x!2 9)) true 
  (ite (and (= x!0 10) (= x!1 0) (= x!2 10)) true 
  (ite (and (= x!0 10) (= x!1 1) (= x!2 11)) true 
  (ite (and (= x!0 10) (= x!1 2) (= x!2 12)) true 
  (ite (and (= x!0 10) (= x!1 3) (= x!2 13)) true
  (ite (and (= x!0 10) (= x!1 12) (= x!2 22)) true 
    true                ;; <<<< how to set this default-value ??
   ))))))))))) ) 

   true

the planning problem is in this post on stackoverflow: Does Z3 take a longer time to give an unsat result compared to a sat result? — DvH

Patrick Trentin Patrick Trentin · Accepted Answer · 2018-08-20T11:31:48

One can adjust the default value by rewriting the input formula as follows:

(set-option :produce-models true)

(define-fun isPosNeighbor ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    (ite (or
            (and (= x!0  1) (= x!1  0) (= x!2  1))
            (and (= x!0  1) (= x!1  1) (= x!2  2))
            (and (= x!0  1) (= x!1  7) (= x!2  8))
            (and (= x!0  1) (= x!1  8) (= x!2  9))
            (and (= x!0 10) (= x!1  0) (= x!2 10))
            (and (= x!0 10) (= x!1  1) (= x!2 11)) 
            (and (= x!0 10) (= x!1  2) (= x!2 12)) 
            (and (= x!0 10) (= x!1  3) (= x!2 13))
            (and (= x!0 10) (= x!1 12) (= x!2 22)) 
        ) true false
))

(check-sat)
(get-model)

(eval  (isPosNeighbor 33 4 1))
(eval  (isPosNeighbor 0 0 0)) 
(eval  (isPosNeighbor 1 0 1))

Note that there is no need to provide a special case for 0 0 0.

Moreover, if the value of the function is not know a priori, true and false can be replaced with arbitrary Boolean expressions.

The output matches the desired behaviour:

~$ z3 t.smt2 
sat
(model 
)
false
false
true

how to use declare-fun with values in Z3 SMTLIB

1 Answers