From 9b66d8600bdb527098792efdb00f154f39e1a067 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Apr 2022 07:21:22 +0200 Subject: [PATCH] add shortcut to serialize/deserialize based on question at FV hangout use case ``` from z3 import * x, y = Ints('x y') s = (x + y).serialize() y = deserialize(s) print(y) ``` --- src/api/python/z3/z3.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index ed9c7f0a8..af1d32972 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1101,6 +1101,28 @@ class ExprRef(AstRef): else: return [] + def from_string(self, s): + pass + + def serialize(self): + s = Solver() + f = Function('F', self.sort(), BoolSort(self.ctx)) + s.add(f(self)) + return s.sexpr() + +def deserialize(st): + """inverse function to the serialize method on ExprRef. + It is made available to make it easier for users to serialize expressions back and forth between + strings. Solvers can be serialized using the 'sexpr()' method. + """ + s = Solver() + s.from_string(st) + if len(s.assertions()) != 1: + raise Z3Exception("single assertion expected") + fml = s.assertions()[0] + if fml.num_args() != 1: + raise Z3Exception("dummy function 'F' expected") + return fml.arg(0) def _to_expr_ref(a, ctx): if isinstance(a, Pattern):