How to serialize and deserialize a z3::model (c++)?

[ngsrinivas]

Hello,

I'm attempting to find the easiest method to serialize and deserialize a z3 model using the C++ api. We have a multi-process setup where queries are discharged from one process to another via RPC, and the second process runs the z3 solver (check() and get_model() functions). The second process must return the model to the first process so that it can construct a z3::model C++ object out of it.

What's the easiest/right way to do this? I've looked at the Z3 model (c++) api. I found that Z3_model_to_string() can be used to construct a serialized smt2lib string from a model. However, I couldn't find a corresponding deserializing function. Please help?

Srinivas

[NikolajBjorner]

The Z3_model_to_string creates an SMT2 compliant set of definitions.
You should be able to do the following:

• std::ostringstream strm;
• strm << model;
• auto model_string = model.str();

Then in separate process:

• auto s = solver()
• s.from_string(model_string)
• auto is_sat = s.check()
• assert (is_sat == l_true)
• auto serialized_model = s.model();

I can see that the C++ API doesn't have a model.to_string() method. I will add this next so future generations don't need stringstream.

[ngsrinivas]

Nikolaj, thanks for your prompt reply! I followed your overall scheme by doing:

      ostringstream strm;
      z3::model mdl = s.get_model();
      strm << mdl;
      string serialized_model = strm.str();

in one process, and

    s.from_string(serialized_model);
    auto is_sat = s.check();
    assert (is_sat == z3::sat);
    z3::model mdl = s.get_model();
    z3::expr input = c.bv_const("input", 64);
    cout << mdl.eval(input) << endl;

in another. (Note: If I use s.model(), I get the following error, so I substituted s.model() with with s.get_model()).

error: no member named 'model' in 'z3::solver'
    z3::model mdl = s.model();
                    ~ ^

Unfortunately, the model object mdl doesn't really evaluate anything. I have a variable called input in my formula, which evaluates to #x0000000000000001 when I print the entire serialized_model in both the processes. However, the output of the last line is

input

My Z3 version is 4.8.9.

What am I missing? Thank you for your kind help!

Srinivas

[NikolajBjorner]

You want to
Z3_set_ast_print_mode(s.ctx(), Z3_PRINT_SMTLIB2_COMPLIANT)

[NikolajBjorner]

I need to check this on my end: the declarations are parsed, but I don't see them in the model as advertised.

[ngsrinivas]

Nikolaj,

You want to
Z3_set_ast_print_mode(s.ctx(), Z3_PRINT_SMTLIB2_COMPLIANT)

I added this statement to the location where the model is printed in the first process. Unfortunately, that didn't help. :(

I noted that the value is visible in the serialized model that I receive in the second process, e.g., if I print the serialized_model string, I see

(define-fun input () (_ BitVec 64)
  #xfffffffffffffc01)

but the constructed model seems not to evaluate anything to its value in the model (e.g., the input example above).

Please let me know if I can clarify or provide more info to get help on this. Thanks!

[NikolajBjorner]

This is what I meant by:

I need to check this on my end: the declarations are parsed, but I don't see them in the model as advertised.

[NikolajBjorner]

Here is a test for the fix that was checked in (Python sets the Z3_PRINT_SMTLIB2_COMPLIANT by default, C++ does not):

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))

[NikolajBjorner]

I have fixed the issue identified. You should be able to reparse models using the latest version in the repository.

[ngsrinivas]

That worked fantastic! Thank you so much for your kind and prompt help with this!

[Kingloko]

Does the example code above still work?
I tried it on a fresh vm that only pip installed z3-solver and I'm seeing unexpected results.

[NikolajBjorner]

this is not a supported scenario, sorry.
When z3 parses definitions they get added to the model returned by the command-line front-end. The definitions don't make it into the state of the solver created over the programmatic API.

[Kingloko]

Is there any other method to serialize/deserialize models in python? I find myself in a similar situation as OP but I'm using python instead of c++.

[ngsrinivas]

@Kingloko, FWIW we refactored the z3 C++ client-server implementation from our system into a standalone tool. Here it is.

https://github.com/smartnic/z3validation

Sharing in case it's useful to you.