mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Added __deepcopy__ operators to ref-counted objects in the Python API
This commit is contained in:
Christoph M. Wintersteiger
parent
a258236229
commit
83e9c40265
1 changed files with 62 additions and 2 deletions
|
|
@ -50,6 +50,7 @@ from fractions import Fraction
|
|||
import sys
|
||||
import io
|
||||
import math
|
||||
import copy
|
||||
|
||||
if sys.version < '3':
|
||||
def _is_int(v):
|
||||
|
|
@ -288,6 +289,9 @@ class AstRef(Z3PPObject):
|
|||
if self.ctx.ref() is not None:
|
||||
Z3_dec_ref(self.ctx.ref(), self.as_ast())
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return _to_ast_ref(self.ast, self.ctx)
|
||||
|
||||
def __str__(self):
|
||||
return obj_to_string(self)
|
||||
|
||||
|
|
@ -4355,6 +4359,11 @@ class Datatype:
|
|||
self.name = name
|
||||
self.constructors = []
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
r = Datatype(self.name, self.ctx)
|
||||
r.constructors = copy.deepcopy(self.constructors)
|
||||
return r
|
||||
|
||||
def declare_core(self, name, rec_name, *args):
|
||||
if __debug__:
|
||||
_z3_assert(isinstance(name, str), "String expected")
|
||||
|
|
@ -4645,11 +4654,17 @@ class ParamsRef:
|
|||
|
||||
Consider using the function `args2params` to create instances of this object.
|
||||
"""
|
||||
def __init__(self, ctx=None):
|
||||
def __init__(self, ctx=None, params=None):
|
||||
self.ctx = _get_ctx(ctx)
|
||||
self.params = Z3_mk_params(self.ctx.ref())
|
||||
if params is None:
|
||||
self.params = Z3_mk_params(self.ctx.ref())
|
||||
else:
|
||||
self.params = params
|
||||
Z3_params_inc_ref(self.ctx.ref(), self.params)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return ParamsRef(self.ctx, self.params)
|
||||
|
||||
def __del__(self):
|
||||
if self.ctx.ref() is not None:
|
||||
Z3_params_dec_ref(self.ctx.ref(), self.params)
|
||||
|
|
@ -4709,6 +4724,9 @@ class ParamDescrsRef:
|
|||
self.descr = descr
|
||||
Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return ParamsDescrsRef(self.descr, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.ctx.ref() is not None:
|
||||
Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
|
||||
|
|
@ -4770,6 +4788,9 @@ class Goal(Z3PPObject):
|
|||
self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
|
||||
Z3_goal_inc_ref(self.ctx.ref(), self.goal)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return Goal(False, False, False, self.ctx, self.goal)
|
||||
|
||||
def __del__(self):
|
||||
if self.goal is not None and self.ctx.ref() is not None:
|
||||
Z3_goal_dec_ref(self.ctx.ref(), self.goal)
|
||||
|
|
@ -5032,6 +5053,9 @@ class AstVector(Z3PPObject):
|
|||
self.ctx = ctx
|
||||
Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return AstVector(self.vector, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.vector is not None and self.ctx.ref() is not None:
|
||||
Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
|
||||
|
|
@ -5167,6 +5191,9 @@ class AstMap:
|
|||
self.ctx = ctx
|
||||
Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return AstMap(self.map, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.map is not None and self.ctx.ref() is not None:
|
||||
Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
|
||||
|
|
@ -5282,6 +5309,9 @@ class FuncEntry:
|
|||
self.ctx = ctx
|
||||
Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return FuncEntry(self.entry, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.ctx.ref() is not None:
|
||||
Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
|
||||
|
|
@ -5388,6 +5418,9 @@ class FuncInterp(Z3PPObject):
|
|||
if self.f is not None:
|
||||
Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return FuncInterp(self.f, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.f is not None and self.ctx.ref() is not None:
|
||||
Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
|
||||
|
|
@ -5498,6 +5531,9 @@ class ModelRef(Z3PPObject):
|
|||
self.ctx = ctx
|
||||
Z3_model_inc_ref(self.ctx.ref(), self.model)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return ModelRef(self.m, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.ctx.ref() is not None:
|
||||
Z3_model_dec_ref(self.ctx.ref(), self.model)
|
||||
|
|
@ -5774,6 +5810,9 @@ class Statistics:
|
|||
self.ctx = ctx
|
||||
Z3_stats_inc_ref(self.ctx.ref(), self.stats)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return Statistics(self.stats, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.ctx.ref() is not None:
|
||||
Z3_stats_dec_ref(self.ctx.ref(), self.stats)
|
||||
|
|
@ -5908,6 +5947,9 @@ class CheckSatResult:
|
|||
def __init__(self, r):
|
||||
self.r = r
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return CheckSatResult(self.r)
|
||||
|
||||
def __eq__(self, other):
|
||||
return isinstance(other, CheckSatResult) and self.r == other.r
|
||||
|
||||
|
|
@ -5947,6 +5989,9 @@ class Solver(Z3PPObject):
|
|||
self.solver = solver
|
||||
Z3_solver_inc_ref(self.ctx.ref(), self.solver)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return Solver(self.solver, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.solver is not None and self.ctx.ref() is not None:
|
||||
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
|
||||
|
|
@ -6367,6 +6412,9 @@ class Fixedpoint(Z3PPObject):
|
|||
Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
|
||||
self.vars = []
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return FixedPoint(self.fixedpoint, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.fixedpoint is not None and self.ctx.ref() is not None:
|
||||
Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
|
||||
|
|
@ -6741,6 +6789,9 @@ class Optimize(Z3PPObject):
|
|||
self.optimize = Z3_mk_optimize(self.ctx.ref())
|
||||
Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return Optimize(self.optimize, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.optimize is not None and self.ctx.ref() is not None:
|
||||
Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
|
||||
|
|
@ -6893,6 +6944,9 @@ class ApplyResult(Z3PPObject):
|
|||
self.ctx = ctx
|
||||
Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return ApplyResult(self.result, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.ctx.ref() is not None:
|
||||
Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
|
||||
|
|
@ -7021,6 +7075,9 @@ class Tactic:
|
|||
raise Z3Exception("unknown tactic '%s'" % tactic)
|
||||
Z3_tactic_inc_ref(self.ctx.ref(), self.tactic)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return Tactic(self.tactic, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.tactic is not None and self.ctx.ref() is not None:
|
||||
Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
|
||||
|
|
@ -7293,6 +7350,9 @@ class Probe:
|
|||
raise Z3Exception("unknown probe '%s'" % probe)
|
||||
Z3_probe_inc_ref(self.ctx.ref(), self.probe)
|
||||
|
||||
def __deepcopy__(self, memo={}):
|
||||
return Probe(self.probe, self.ctx)
|
||||
|
||||
def __del__(self):
|
||||
if self.probe is not None and self.ctx.ref() is not None:
|
||||
Z3_probe_dec_ref(self.ctx.ref(), self.probe)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue