Skip to content

Commit

Permalink
Merge 44dd291 into 7f2339b
Browse files Browse the repository at this point in the history
  • Loading branch information
Marco Gario committed Oct 10, 2016
2 parents 7f2339b + 44dd291 commit 3f9241d
Show file tree
Hide file tree
Showing 4 changed files with 234 additions and 65 deletions.
79 changes: 75 additions & 4 deletions pysmt/solvers/cvc4.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -378,10 +378,43 @@ def walk_bv_mul(self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_MULT, args[0], args[1])

def walk_bv_udiv(self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_UDIV, args[0], args[1])
# Force deterministic semantics of division by 0
# If the denominator is bv0, then the result is ~0
n,d = args
if d.isConst():
bv = d.getConstBitVector()
v = bv.getValue().toString()
if v == "0":
return self.mkExpr(CVC4.BITVECTOR_NOT, d)
else:
return self.mkExpr(CVC4.BITVECTOR_UDIV, n, d)
else:
# (d == 0) ? ~0 : n bvudiv d
base = self.mkExpr(CVC4.BITVECTOR_UDIV, n, d)
zero = self.mkConst(CVC4.BitVector(formula.bv_width(),
CVC4.Integer("0")))
notzero = self.mkExpr(CVC4.BITVECTOR_NOT, zero)
test = self.mkExpr(CVC4.EQUAL, d, zero)
return self.mkExpr(CVC4.ITE, test, notzero, base)

def walk_bv_urem(self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_UREM, args[0], args[1])
# Force deterministic semantics of reminder by 0
# If the denominator is bv0, then the result is the numerator
n,d = args
if d.isConst():
bv = d.getConstBitVector()
v = bv.getValue().toString()
if v == "0":
return n
else:
return self.mkExpr(CVC4.BITVECTOR_UREM, n, d)
else:
# (d == 0) ? n : n bvurem d
base = self.mkExpr(CVC4.BITVECTOR_UREM, n, d)
zero = self.mkConst(CVC4.BitVector(formula.bv_width(),
CVC4.Integer("0")))
test = self.mkExpr(CVC4.EQUAL, d, zero)
return self.mkExpr(CVC4.ITE, test, n, base)

def walk_bv_lshl(self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_SHL, args[0], args[1])
Expand Down Expand Up @@ -415,10 +448,48 @@ def walk_bv_comp (self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_COMP, args[0], args[1])

def walk_bv_sdiv (self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_SDIV, args[0], args[1])
# Force deterministic semantics of division by 0
# If the denominator is bv0, then the result is:
# * ~0 (if the numerator is signed >= 0)
# * 1 (if the numerator is signed < 0)
n,d = args
# sign_expr : ( 0 s<= n ) ? ~0 : 1 )
zero = self.mkConst(CVC4.BitVector(formula.bv_width(),
CVC4.Integer("0")))
notzero = self.mkExpr(CVC4.BITVECTOR_NOT, zero)
one = self.mkConst(CVC4.BitVector(formula.bv_width(),
CVC4.Integer("1")))
is_gt_zero = self.mkExpr(CVC4.BITVECTOR_SLE, zero, n)
sign_expr = self.mkExpr(CVC4.ITE, is_gt_zero, notzero, one)
base = self.mkExpr(CVC4.BITVECTOR_SDIV, n, d)
if d.isConst():
v = d.getConstBitVector().getValue().toString()
if v == "0":
return sign_expr
else:
return base
else:
# (d == 0) ? sign_expr : base
is_zero = self.mkExpr(CVC4.EQUAL, d, zero)
return self.mkExpr(CVC4.ITE, is_zero, sign_expr, base)

def walk_bv_srem (self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_SREM, args[0], args[1])
# Force deterministic semantics of reminder by 0
# If the denominator is bv0, then the result is the numerator
n,d = args
if d.isConst():
v = d.getConstBitVector().getValue().toString()
if v == "0":
return n
else:
return self.mkExpr(CVC4.BITVECTOR_SREM, n, d)
else:
# (d == 0) ? n : n bvurem d
base = self.mkExpr(CVC4.BITVECTOR_SREM, n, d)
zero = self.mkConst(CVC4.BitVector(formula.bv_width(),
CVC4.Integer("0")))
test = self.mkExpr(CVC4.EQUAL, d, zero)
return self.mkExpr(CVC4.ITE, test, n, base)

def walk_bv_ashr (self, formula, args, **kwargs):
return self.mkExpr(CVC4.BITVECTOR_ASHR, args[0], args[1])
Expand Down
12 changes: 6 additions & 6 deletions pysmt/solvers/msat.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -699,7 +699,7 @@ def _back_single_term(self, term, mgr, args):

elif mathsat.msat_term_is_bv_neg(self.msat_env(), term):
assert arity == 1
res = mgr.BVSub(args[0])
res = mgr.BVNeg(args[0])

elif mathsat.msat_term_is_bv_srem(self.msat_env(), term):
assert arity == 2
Expand Down Expand Up @@ -742,25 +742,25 @@ def _back_single_term(self, term, mgr, args):
res = mgr.BVComp(args[0], args[1])

elif mathsat.msat_term_is_bv_zext(self.msat_env(), term)[0]:
assert arity == 2
assert arity == 1
res, amount = mathsat.msat_term_is_bv_zext(self.msat_env(), term)
assert res
res = mgr.BVZExt(args[0], amount)

elif mathsat.msat_term_is_bv_sext(self.msat_env(), term)[0]:
assert arity == 2
assert arity == 1
res, amount = mathsat.msat_term_is_bv_sext(self.msat_env(), term)
assert res
res = mgr.BVSExt(args[0], amount)

elif mathsat.msat_term_is_bv_rol(self.msat_env(), term)[0]:
assert arity == 2
res, amount = mathsat.msat_term_is_bv_ror(self.msat_env(), term)
assert arity == 1
res, amount = mathsat.msat_term_is_bv_rol(self.msat_env(), term)
assert res
res = mgr.BVRol(args[0], amount)

elif mathsat.msat_term_is_bv_ror(self.msat_env(), term)[0]:
assert arity == 2
assert arity == 1
res, amount = mathsat.msat_term_is_bv_ror(self.msat_env(), term)
assert res
res = mgr.BVRor(args[0], amount)
Expand Down

0 comments on commit 3f9241d

Please sign in to comment.