Permalink
Browse files

Tests for reification of Or.

  • Loading branch information...
1 parent b25bcce commit 815c7efec42ff1c91c7c2f23e57abab8ef885a44 @9thbit 9thbit committed Feb 10, 2014
Showing with 20 additions and 1 deletion.
  1. +20 −1 tests/SATEncodingTest.py
@@ -674,7 +674,26 @@ def testReifOrTrue(self):
s = SATEncodingTest.solver(m, encoding=SATEncodingTest.encoding)
s.solve()
self.assertTrue(s.is_sat())
- self.assertTrue((v1.get_value() + 1 == v2.get_value()) or (v1.get_value() == 9 or v2.get_value() == 9))
+ self.assertTrue((v1.get_value() + 1 == v2.get_value()) or
+ (v1.get_value() == 9 or v2.get_value() == 9))
+
+ def testOr(self):
+ v1 = Variable(10)
+ v2 = Variable(10)
+ m = Model((v1 == 2) | (v2 == 2))
+ s = SATEncodingTest.solver(m, encoding=SATEncodingTest.encoding)
+ s.solve()
+ self.assertTrue(s.is_sat())
+ self.assertTrue(v1.get_value() == 2 or v2.get_value() == 2)
+
+ def testOr2(self):
+ v1 = Variable(10)
+ v2 = Variable(10)
+ m = Model((v1 == 2) | False)
+ s = SATEncodingTest.solver(m, encoding=SATEncodingTest.encoding)
+ s.solve()
+ self.assertTrue(s.is_sat())
+ self.assertTrue(v1.get_value() == 2 or v2.get_value() == 2)
# ---------------- Reification of inequalities between two expressions ----------------

0 comments on commit 815c7ef

Please sign in to comment.