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

prop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-19 10:39:44 -07:00
parent 5aaa7e0022
commit 79aa3457c1
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10519,7 +10519,7 @@ def user_prop_fixed(ctx, id, value):
def user_prop_fresh(ctx): def user_prop_fresh(ctx):
prop = _user_propagate_bases[ctx] prop = _user_propagate_bases[ctx]
new_prop = prop.copy() new_prop = prop.fresh()
return ctypes.c_void_p(new_prop.id) return ctypes.c_void_p(new_prop.id)
@ -10552,9 +10552,18 @@ class UserPropagateBase:
def fixed(self, id, e): def fixed(self, id, e):
raise Z3Exception("fixed has not been overwritten") raise Z3Exception("fixed has not been overwritten")
def fresh(self):
raise Z3Exception("fresh has not been overwritten")
def add(self, e): def add(self, e):
return Z3_solver_propagate_register(self.ctx.ref(), self.solver.solver, e.ast) return Z3_solver_propagate_register(self.ctx.ref(), self.solver.solver, e.ast)
def propagate(self, ids, e): def propagate(self, ids, e):
Z3_solver_propagate_consequence(self.ctx.ref(), self.solver.solver, ids, e.ast) sz = len(ids)
_ids = (ctypes.c_uint * sz)()
for i in range(sz):
_ids[i] = ids[i]
Z3_solver_propagate_consequence(self.ctx.ref(), self.solver.solver, sz, _ids, e.ast)
def conflict(self, ids):
self.propagate(ids, BoolVal(False, self.ctx))