Skip to content

Commit

Permalink
Merge pull request #421 from pysmt/z3_walker
Browse files Browse the repository at this point in the history 
Z3Converter: Remove use of deprecated self.functions
  • Loading branch information
@mikand
mikand committed Aug 1, 2017
2 parents 8d05074 + fde8b42 commit a08c694
Showing 1 changed file with 48 additions and 42 deletions.
90 changes: 48 additions & 42 deletions pysmt/solvers/z3.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -291,37 +291,6 @@ def __init__(self, environment, z3_ctx):
self._get_type = environment.stc.get_type
self._back_memoization = {}
self.ctx = z3_ctx
# Forward conversion
self.set_function(p_(self.walk_nary, z3.Z3_mk_and), op.AND)
self.set_function(p_(self.walk_nary, z3.Z3_mk_or), op.OR)
self.set_function(p_(self.walk_nary, z3.Z3_mk_add), op.PLUS)
self.set_function(p_(self.walk_nary, z3.Z3_mk_mul), op.TIMES)
self.set_function(p_(self.walk_nary, z3.Z3_mk_sub), op.MINUS)
self.set_function(p_(self.walk_binary, z3.Z3_mk_implies), op.IMPLIES)
self.set_function(p_(self.walk_binary, z3.Z3_mk_le), op.LE)
self.set_function(p_(self.walk_binary, z3.Z3_mk_lt), op.LT)
self.set_function(p_(self.walk_binary, z3.Z3_mk_eq), op.EQUALS, op.IFF)
self.set_function(p_(self.walk_binary, z3.Z3_mk_power), op.POW)
self.set_function(p_(self.walk_binary, z3.Z3_mk_div), op.DIV)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvult), op.BV_ULT)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvule), op.BV_ULE)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvslt), op.BV_SLT)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvsle), op.BV_SLE)
self.set_function(p_(self.walk_binary, z3.Z3_mk_concat), op.BV_CONCAT)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvor), op.BV_OR)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvand), op.BV_AND)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvxor), op.BV_XOR)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvadd), op.BV_ADD)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvsub), op.BV_SUB)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvmul), op.BV_MUL)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvudiv), op.BV_UDIV)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvurem), op.BV_UREM)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvshl), op.BV_LSHL)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvlshr), op.BV_LSHR)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvsdiv), op.BV_SDIV)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvsrem), op.BV_SREM)
self.set_function(p_(self.walk_binary, z3.Z3_mk_bvashr), op.BV_ASHR)
self.set_function(self.walk_quantifier, *op.QUANTIFIERS)

# Back Conversion
self._back_fun = {
Expand Down Expand Up @@ -598,17 +567,6 @@ def _to_ast_array(self, args):
_args[i] = arg
return _args, sz

def walk_nary(self, func, formula, args, **kwargs):
_args, sz = self._to_ast_array(args)
z3term = func(self.ctx.ref(), sz, _args)
z3.Z3_inc_ref(self.ctx.ref(), z3term)
return z3term

def walk_binary(self, func, formula, args, **kwargs):
z3term = func(self.ctx.ref(), args[0], args[1])
z3.Z3_inc_ref(self.ctx.ref(), z3term)
return z3term

def walk_not(self, formula, args, **kwargs):
z3term = z3.Z3_mk_not(self.ctx.ref(), args[0])
z3.Z3_inc_ref(self.ctx.ref(), z3term)
Expand Down Expand Up @@ -837,6 +795,54 @@ def _z3_to_type(self, sort):
else:
raise NotImplementedError("Unsupported sort in conversion: %s" % sort)

def make_walk_nary(func):
def walk_nary(self, formula, args, **kwargs):
_args, sz = self._to_ast_array(args)
z3term = func(self.ctx.ref(), sz, _args)
z3.Z3_inc_ref(self.ctx.ref(), z3term)
return z3term
return walk_nary

def make_walk_binary(func):
def walk_binary(self, formula, args, **kwargs):
z3term = func(self.ctx.ref(), args[0], args[1])
z3.Z3_inc_ref(self.ctx.ref(), z3term)
return z3term
return walk_binary

walk_and = make_walk_nary(z3.Z3_mk_and)
walk_or = make_walk_nary(z3.Z3_mk_or)
walk_plus = make_walk_nary(z3.Z3_mk_add)
walk_times = make_walk_nary(z3.Z3_mk_mul)
walk_minus = make_walk_nary(z3.Z3_mk_sub)
walk_implies = make_walk_binary(z3.Z3_mk_implies)
walk_le = make_walk_binary(z3.Z3_mk_le)
walk_lt = make_walk_binary(z3.Z3_mk_lt)
walk_equals = make_walk_binary(z3.Z3_mk_eq)
walk_iff = make_walk_binary(z3.Z3_mk_eq)
walk_pow = make_walk_binary(z3.Z3_mk_power)
walk_div = make_walk_binary(z3.Z3_mk_div)
walk_bv_ult = make_walk_binary(z3.Z3_mk_bvult)
walk_bv_ule = make_walk_binary(z3.Z3_mk_bvule)
walk_bv_slt = make_walk_binary(z3.Z3_mk_bvslt)
walk_bv_sle = make_walk_binary(z3.Z3_mk_bvsle)
walk_bv_concat = make_walk_binary(z3.Z3_mk_concat)
walk_bv_or = make_walk_binary(z3.Z3_mk_bvor)
walk_bv_and = make_walk_binary(z3.Z3_mk_bvand)
walk_bv_xor = make_walk_binary(z3.Z3_mk_bvxor)
walk_bv_add = make_walk_binary(z3.Z3_mk_bvadd)
walk_bv_sub = make_walk_binary(z3.Z3_mk_bvsub)
walk_bv_mul = make_walk_binary(z3.Z3_mk_bvmul)
walk_bv_udiv = make_walk_binary(z3.Z3_mk_bvudiv)
walk_bv_urem = make_walk_binary(z3.Z3_mk_bvurem)
walk_bv_lshl = make_walk_binary(z3.Z3_mk_bvshl)
walk_bv_lshr = make_walk_binary(z3.Z3_mk_bvlshr)
walk_bv_sdiv = make_walk_binary(z3.Z3_mk_bvsdiv)
walk_bv_srem = make_walk_binary(z3.Z3_mk_bvsrem)
walk_bv_ashr = make_walk_binary(z3.Z3_mk_bvashr)
walk_exists = walk_quantifier
walk_forall = walk_quantifier

def _type_to_z3(self, tp):
"""Convert a pySMT type into the corresponding Z3 sort."""
if tp.is_bool_type():
Expand Down

0 comments on commit a08c694

Please sign in to comment.