CODEWITHSUNDEEP
z3
MockedMan.Object
MockedMan.Object

Reputation: 275

Z3 Solver outputting the satisfying model?

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.

Upvotes: 1

Views: 477

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

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.

Upvotes: 2

Related Questions