mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

expose method for updating python model for constants

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-17 09:09:04 -07:00
parent 34fc0276e9
commit 1884ad5b2f
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/python/z3/z3.py
View file

@ -6561,6 +6561,15 @@ class ModelRef(Z3PPObject):
r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
return r 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): def translate(self, target):
"""Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
""" """