Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

Models

Z3 has the ability to produce models as part of the output. Models assign values to the constants in the input and generate partial function graphs for predicates and function symbols. You can enable model generation by using the switch /m.

For instance, if you use z3 /m example1.smt, where example1.smt is the following benchmark:

(benchmark example1
:status sat
:logic QF_LIA
:extrafuns ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int))
:formula (and (>= (- x1 x2) 1)
              (<= (- x1 x2) 3)
              (= x1 (+ (* 2 x3) x5))
              (= x3 x5)
              (= x2 (* 6 x4)))
)
   

Z3 produces a model where x1 = -3, x2 = -6, and the other variables are set to -1.

The model comprises of a set of partitions, each partition is printed as: *k, where k is a non-negative number. Each partition is associated with a set of constants from the input, enclosed in {}, and is associated with a concrete value. Concrete values may be one of the following kinds:

• boolean, which is either true or false.

• numeral: an integer, bit-vector constant or rational number.

• array: represented as a finite map and an 'else' value.

• tuple: represented as a constructor and a sequence of values.

• uninterpreted: represented as typename!k where k is a non-negative integer.

Z3 also produces interpretations for free functions. Consider the following example:

(benchmark example2
:logic QF_UF
:extrasorts (A B C D)
:extrafuns  ((x A) (y B) (w A) (z C) (u D))
:extrafuns  ((f A A B) (g A B B) (h1 B A B) (h2 B B B))
:formula (and (= (g x y) (h1 y x)) 
              (= (f x x) (h2 y y)) 
              (not (= (f x x) (f x w))))
)
   

Z3 produces the following model:

partitions:
*2 {x} -> A!0
*3 {y} -> B!0
*4 -> B!1
*5 -> B!2
*6 {w} -> A!1
*7 -> B!3
function interpretations:
g -> {
  else -> *4
}
h1 -> {
  else -> *4
}
f -> {
  *2 *6 -> *7
  else -> *5
}
h2 -> {
  else -> *5
}
sat
   

For example, in the model above, we can find the value of f(x, w) in the following way:

• The constants x and w are in the partitions *2 and *6 respectively

• The interpretation of f contains and entry *2 *6 -> *7.

• B!3 is associated with partition *7.

Thus, the value of f(x, w) is B!3.

Similarly, the value of f(x, x) is B!2 because there is no entry *2 *2 in the interpretation of f, thus the else entry is used: else -> *5.

By default Z3, produces a full (and compact) interpretation for free functions. The option PARTIAL_MODELS=true can be used to force Z3 to produce partial interpretations. When this option is used, Z3 will produce the following model for the previous example:

partitions:
*2 {x} -> A!0
*3 {y} -> B!0
*4 -> B!1
*5 -> B!2
*6 {w} -> A!1
*7 -> B!3
function interpretations:
g -> {
  *2 *3 -> *4
  else -> #unspecified
}
h1 -> {
  *3 *2 -> *4
  else -> #unspecified
}
f -> {
  *2 *2 -> *5
  *2 *6 -> *7
  else -> #unspecified
}
h2 -> {
  *3 *3 -> *5
  else -> #unspecified
}

The option PARTIAL_MODELS=true is also useful for benchmarks that contain quantifiers. Z3 is not complete, and the produced model should be viewed as a potential model. Consider the following benchmark:

(benchmark example3
:logic AUFLIA
:extrafuns  ((a Int))
:extrafuns  ((f Int Int))
:formula (and (forall (x Int) (>= (f x) (+ x 1)))
              (= (f 10) 20)
              (= (f a) (+ a 4)))
)

The command z3 /m PARTIAL_MODELS=true example3.smt will produce the following potential model:

partitions:
*2 -> 10:int
*3 -> 20:int
*4 {a} -> -4:int
*5 -> 0:int
function interpretations:
f -> {
  *2 -> *3
  *4 -> *5
  else -> #unspecified
}

Note that, the model specifies the value of f at 10 and a. This is a side effect of the heuristics used by Z3 to deal with quantifiers. If the command z3 /m example3.smt, then Z3 will produce the following potential (and wrong) model:

partitions:
*3 -> 20:int
*4 {a} -> -4:int
*5 -> 0:int
function interpretations:
f -> {
  *4 -> *5
  else -> *3
}