asking queries in smtlib2 format and parsing resultant models

[sunbeomso]

In OCaml, it is possible to export Z3 expressions into files in smtlib2 format (using api in https://z3prover.github.io/api/html/ml/Z3.SMT.html).

I wonder, whether Z3 provides OCaml apis for parsing resulting models (i.e., getting values for some variables or expressions) when queries in smtlib2 format are asked to Z3 (and the satisfying models are found by Z3).

[NikolajBjorner]

Models are printed as SMTLIB2 declarations. The provides a way to round-trip models.
Python example

from z3 import *

s1 = Solver()
x, y = Ints('x y')
s1.add(x > y)
s1.check()
m1 = s1.model()
print(m1.sexpr())
ms = m1.sexpr()

s2 = Solver()
s2.from_string(ms)
s2.check()
print(s2.model())
print(s2.model().eval(x))

[sunbeomso]

@NikolajBjorner

Thanks for your help. However, the provided code does not seem to work. Could you check that please?

print(ms) outputs:

(define-fun y () Int
  0)
(define-fun x () Int
  1)

However, print(s2.from_string(ms)) outputsNone, and print(s2.model()) and print(s2.model().eval(x)) output [] and x, respectively.

[NikolajBjorner]

s2.check()
is important.
The parsed declarations are used to convert a model of "nothing" into a model of included declarations

[sunbeomso]

@NikolajBjorner

Sorry for my previous description which was not detailed enough.
My results in the previous description are the ones that were obtained after invoking s2.check(), as described below.

Am I missing something?

from z3 import *

s1 = Solver()
x, y = Ints('x y')
s1.add(x > y)
s1.check()
m1 = s1.model()
print(m1.sexpr())
ms = m1.sexpr()

s2 = Solver()
s2.from_string(ms)
s2.check()
print(s2.from_string(ms)) # outputs "None"
print(s2.model()) # outputs "[]"
print(s2.model().eval(x)) # outputs "x"

[NikolajBjorner]

maybe you are using an old version of Z3 that didn't properly populate the model with the input declarations?

C:\z3\build\python>python 5160.py
(define-fun x () Int
  1)
(define-fun y () Int
  0)
None
[y = 0, x = 1]
1

[sunbeomso]

@NikolajBjorner

Thanks for the hint!

I was able to obtain the desired result with Z3 4.8.10 (I was using Z3 4.8.8).