Z3 Solver outputting the satisfying model?

Question

In Z3, if the input script is written in SMTLib format, is it possible to output the model (value assignments satisfying the model)? The get-model returns an interpretation satisfying the constraints. Is there any way to extract the concrete values from these interpretations. I am aware that we can use the python/C++ API to get model values.

Taylor T. Johnson Taylor T. Johnson · Accepted Answer · 2014-07-09T21:55:06

You probably want to use get-value, here's a minimal example (rise4fun link: http://rise4fun.com/Z3/wR81 ):

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (>= (* 2 x) (+ y z)))
(declare-fun f (Int) Int)
(declare-fun g (Int Int) Int)
(assert (< (f x) (g x x)))
(assert (> (f y) (g x x)))
(check-sat) ; sat
(get-model) ; returns:
; (model 
;  (define-fun z () Int
;    0)
;  (define-fun y () Int
;    (- 38))
;  (define-fun x () Int
;    0)
;  (define-fun g ((x!1 Int) (x!2 Int)) Int
;    (ite (and (= x!1 0) (= x!2 0)) 0
;      0))
;  (define-fun f ((x!1 Int)) Int
;    (ite (= x!1 0) (- 1)
;    (ite (= x!1 (- 38)) 1
;      (- 1))))
;)
(get-value (x)) ; returns ((x 0))
(get-value ((f x))) ; returns (((f x) (- 1)))

You'd potentially then have to parse this depending on what you're trying to do, etc.

For more details, check out the SMT-LIB standard:

http://smtlib.cs.uiowa.edu/language.shtml

The latest version is: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf

You can see some examples of get-value on page 39 / figure 3.5.

Z3 Solver outputting the satisfying model?

1 Answers