From 1884ad5b2f119fa21ea5fb1295af0c0662687f8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Aug 2021 09:09:04 -0700 Subject: [PATCH] expose method for updating python model for constants Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index fe711d4f0..dc9c427ce 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6561,6 +6561,15 @@ class ModelRef(Z3PPObject): r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) return r + def update_value(self, x, value): + """Update the interpretation of a constant""" + if is_expr(x): + x = x.decl() + if not is_func_decl(x) or x.arity() != 0: + raise Z3Exception(f"Expecting 0-ary function or constant expression {x}") + value = _py2expr(value) + Z3_add_const_interp(x.ctx_ref(), self.model, x.ast, value.ast) + def translate(self, target): """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. """