Skip to content

Commit

Permalink
Merge pull request #353 from pysmt/tests_fnode
Browse files Browse the repository at this point in the history 
Tests for FNode
  • Loading branch information
@mikand
mikand committed Oct 11, 2016
2 parents de9d8f1 + 1016f75 commit 5bf99c2
Show file tree
Hide file tree
Showing 6 changed files with 143 additions and 56 deletions.
55 changes: 13 additions & 42 deletions pysmt/fnode.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -578,32 +578,12 @@ def array_value_index_type(self):
def array_value_get(self, index):
"""Returns the value of this Array Value at the given index. The
index must be a constant of the correct type.
This function is equivalent (but possibly faster) than the
following code::
m = self.array_value_assigned_values_map()
try:
return m[index]
except KeyError:
return self.array_value_default()
"""
assert index.is_constant()
args = self.args()
start = 0
end = (len(args) - 1) // 2
while end - start > 0:
pivot = (end - start) // 2
i = args[2 * pivot + 1]
if id(i) == id(index):
return args[2 * pivot + 2]
elif id(i) < id(index):
end = pivot
else:
start = pivot + 1
return self.array_value_default()

m = self.array_value_assigned_values_map()
try:
return m[index]
except KeyError:
return self.array_value_default()

def array_value_assigned_values_map(self):
args = self.args()
Expand Down Expand Up @@ -669,8 +649,14 @@ def Iff(self, right):
def Equals(self, right):
return self._apply_infix(right, _mgr().Equals)

def Ite(self, right):
return self._apply_infix(right, _mgr().Ite)
def Ite(self, then_, else_):
if _env().enable_infix_notation:
if isinstance(then_, FNode) and isinstance(else_, FNode):
return _mgr().Ite(self, then_, else_)
else:
raise Exception("Cannot infix ITE with implicit argument types.")
else:
raise Exception("Cannot use infix notation")

def And(self, right):
return self._apply_infix(right, _mgr().And)
Expand Down Expand Up @@ -807,21 +793,6 @@ def __invert__(self):
return _mgr().BVNot(self)
return _mgr().Not(self)

def __int__(self):
if self.is_int_constant():
return self.constant_value()
raise NotImplementedError("Cannot convert `%s` to integer" % str(self))

def __long__(self):
if self.is_int_constant():
return self.constant_value()
raise NotImplementedError("Cannot convert `%s` to integer" % str(self))

def __float__(self):
if self.is_int_constant() or self.is_real_constant():
return float(self.constant_value())
raise NotImplementedError("Cannot convert `%s` to float" % str(self))

def __getitem__(self, idx):
if not _env().enable_infix_notation:
raise Exception("Cannot use infix notation")
Expand Down
2 changes: 2 additions & 0 deletions pysmt/formula.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -800,6 +800,8 @@ def BVSRem(self, left, right):
def BVAShr(self, left, right):
"""Returns the RIGHT arithmetic rotation of the left BV by the number
of steps specified by the right BV."""
if is_python_integer(right):
right = self.BV(right, left.bv_width())
return self.create_node(node_type=op.BV_ASHR,
args=(left, right),
payload=(left.bv_width(),))
Expand Down
33 changes: 33 additions & 0 deletions pysmt/test/test_array.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,39 @@ def test_is_array_op(self):
select_ = Select(store_, Int(100))
self.assertTrue(store_.is_array_op())
self.assertTrue(select_.is_array_op())
self.assertTrue(store_.is_store())
self.assertTrue(select_.is_select())
self.assertFalse(select_.is_store())
self.assertFalse(store_.is_select())

def test_array_value_get(self):
ax = Array(REAL, Real(0),
{Real(1): Real(2),
Real(2): Real(3),
Real(3): Real(4),
Real(4): Real(5),
})
self.assertEqual(ax.array_value_get(Real(1)), Real(2))
self.assertEqual(ax.array_value_get(Real(2)), Real(3))
self.assertEqual(ax.array_value_get(Real(3)), Real(4))
self.assertEqual(ax.array_value_get(Real(4)), Real(5))
self.assertEqual(ax.array_value_get(Real(-1)), Real(0))
self.assertEqual(ax.array_value_get(Real(5)), Real(0))

def test_array_value_is_constant(self):
r = Symbol("r", REAL)
ax1 = Array(REAL, Real(0), {Real(1): r})
ax2 = Array(REAL, r, {Real(1): Real(2)})
ax3 = Array(REAL, Real(0), {Real(1): Real(2)})
self.assertFalse(ax1.is_constant())
self.assertFalse(ax2.is_constant())
self.assertTrue(ax3.is_constant())

with self.assertRaises(ValueError):
self.assertTrue(ax3.is_constant(_type=REAL))

with self.assertRaises(ValueError):
self.assertTrue(ax3.is_constant(value=Real(2)))


if __name__ == "__main__":
Expand Down
52 changes: 51 additions & 1 deletion pysmt/test/test_bv.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,15 +68,19 @@ def test_bv(self):

not_zero32 = mgr.BVNot(zero)
not_b128 = mgr.BVNot(b128)
self.assertTrue(not_b128.is_bv_not())

f1 = Equals(not_zero32, b32)
f2 = Equals(not_b128, big)
self.assertTrue(is_sat(f1, logic=QF_BV))
self.assertTrue(is_sat(f2, logic=QF_BV))

zero_and_one = mgr.BVAnd(zero, one)
self.assertTrue(zero_and_one.is_bv_and())
zero_or_one = mgr.BVOr(zero, one)
self.assertTrue(zero_or_one.is_bv_or())
zero_xor_one = mgr.BVXor(zero, one)
self.assertTrue(zero_xor_one.is_bv_xor())

zero_xor_one.simplify()
self.assertTrue(zero_xor_one.is_bv_op())
Expand Down Expand Up @@ -104,6 +108,8 @@ def test_bv(self):
zero_one_64 = mgr.BVConcat(zero, one)
one_zero_64 = mgr.BVConcat(one, zero)
one_one_64 = mgr.BVConcat(one, one)
self.assertTrue(one_one_64.is_bv_concat())
self.assertFalse(one_one_64.is_bv_and())

self.assertTrue(zero_one_64.bv_width() == 64)
f1 = Equals(mgr.BVXor(one_zero_64, zero_one_64),
Expand All @@ -117,42 +123,60 @@ def test_bv(self):
self.assertTrue(is_valid(Equals(extraction, zero)))

ult = mgr.BVULT(zero, one)
self.assertTrue(ult.is_bv_ult())
neg = mgr.BVNeg(one)
self.assertTrue(neg.is_bv_neg())
self.assertTrue(is_valid(ult, logic=QF_BV), ult)
test_eq = Equals(neg, one)
self.assertTrue(is_unsat(test_eq, logic=QF_BV))

f = zero
addition = mgr.BVAdd(f, one)
self.assertTrue(addition.is_bv_add())
multiplication = mgr.BVMul(f, one)
self.assertTrue(multiplication.is_bv_mul())
udiv = mgr.BVUDiv(f, one)
self.assertTrue(udiv.is_bv_udiv())

self.assertTrue(is_valid(Equals(addition, one), logic=QF_BV), addition)
self.assertTrue(is_valid(Equals(multiplication, zero), logic=QF_BV), multiplication)
self.assertTrue(is_valid(Equals(udiv, zero), logic=QF_BV), udiv)

three = mgr.BV(3, 32)
two = mgr.BV(2, 32)
self.assertEqual(3, three.bv2nat())

reminder = mgr.BVURem(three, two)
self.assertTrue(reminder.is_bv_urem())
shift_l_a = mgr.BVLShl(one, one)
self.assertTrue(shift_l_a.is_bv_lshl())
shift_l_b = mgr.BVLShl(one, 1)

self.assertTrue(is_valid(Equals(reminder, one)), reminder)
self.assertEqual(shift_l_a, shift_l_b)
self.assertTrue(is_valid(Equals(shift_l_a, two)))

shift_r_a = mgr.BVLShr(one, one)
self.assertTrue(shift_r_a.is_bv_lshr())
shift_r_b = mgr.BVLShr(one, 1)
self.assertEqual(shift_r_a, shift_r_b)
self.assertTrue(is_valid(Equals(shift_r_a, zero)))

ashift_r_a = mgr.BVAShr(one, one)
ashift_r_b = mgr.BVAShr(one, 1)
self.assertEqual(ashift_r_a, ashift_r_b)
self.assertTrue(ashift_r_a.is_bv_ashr())

rotate_l = mgr.BVRol(one, 3)
self.assertTrue(rotate_l.is_bv_rol())
rotate_r = mgr.BVRor(rotate_l, 3)
self.assertTrue(rotate_r.is_bv_ror())
self.assertTrue(is_valid(Equals(one, rotate_r)))

zero_ext = mgr.BVZExt(one, 64)
self.assertTrue(zero_ext.is_bv_zext())
signed_ext = mgr.BVSExt(one, 64)
self.assertTrue(signed_ext.is_bv_sext())
signed_ext2 = mgr.BVSExt(mgr.BVNeg(one), 64)

self.assertNotEqual(signed_ext2, signed_ext)
Expand Down Expand Up @@ -207,7 +231,22 @@ def test_bv(self):
# SBV should behave as BV for positive numbers
self.assertEqual(mgr.SBV(10, 16), mgr.BV(10, 16))

return
# Additional is_bv_* tests
f = mgr.BVSub(one, one)
self.assertTrue(f.is_bv_sub())

f = mgr.BVSLT(one, one)
self.assertTrue(f.is_bv_slt())
f = mgr.BVSLE(one, one)
self.assertTrue(f.is_bv_sle())
f = mgr.BVComp(one, one)
self.assertTrue(f.is_bv_comp())
f = mgr.BVSDiv(one, one)
self.assertTrue(f.is_bv_sdiv())
f = mgr.BVSRem(one, one)
self.assertTrue(f.is_bv_srem())
f = mgr.BVULE(one, one)
self.assertTrue(f.is_bv_ule())

@skipIfNoSolverForLogic(QF_BV)
def test_bv_div_by_zero(self):
Expand Down Expand Up @@ -256,6 +295,17 @@ def test_bv_div_by_zero(self):
bvx))
self.assertValid(fsrem)

def test_is_bv_constant(self):
mgr = self.env.formula_manager
bvconst = mgr.BV(4, 8)
self.assertTrue(bvconst.is_bv_constant())
self.assertTrue(bvconst.is_bv_constant(value=4))
self.assertTrue(bvconst.is_bv_constant(width=8))
self.assertTrue(bvconst.is_bv_constant(value=4, width=8))
self.assertFalse(bvconst.is_bv_constant(value=4, width=9))
self.assertFalse(bvconst.is_bv_constant(value=5, width=8))
self.assertFalse(bvconst.is_bv_constant(3,9))
self.assertFalse(bvconst.is_bv_constant(3))

if __name__ == "__main__":
main()

0 comments on commit 5bf99c2

Please sign in to comment.