3

Is it possible to serialize/deserialize a Z3 context (from C#)? If not, is this feature planned ?

I think this feature is important for real world applications.

SBertoli
  • 43
  • 5
  • This may be relevant: http://stackoverflow.com/questions/7726607/is-it-possible-to-clone-z3-context – AKX Mar 07 '12 at 06:46

1 Answers1

1

This is not directly supported in the current API. The next release will support multiple solvers, and we will provide commands for copying the assertions from one solver to another, and retrieving the assertions. With these commands, one can implement serialization by dumping the expressions in a file (in SMT 2.0 format). To deserialize, we just read the file back. Note that, this solution can already be implemented using the current API if you keep track of the assertions you asserted into the logical context.

That being said, I've seen the following approach used in many projects that use Z3. They have their own representation for formulas. When they invoke Z3, they translate their representation into Z3's representation. In most cases the performance overhead is minimal. This approach gives them a lot of flexibility. Serialization is a good example. Some programming environment (e.g., Python) already provide some built-in support for serialization.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53