support restricted integer subtraction

README.md

@@ -163,7 +163,8 @@ Arbitrary clauses can be built, composed, and added to formulas with:
 
    * Familiar boolean operators `And`, `Or`, `Not`, `If`, `Eq`, `Neq`.
    * `Tuple`s that can be compared for equality, inequality, or lexicographic order.
-   * `Integer`s that can be added, multiplied, or compared as `Tuple`s (see [examples/prime](examples/prime)).
+   * Non-negative `Integer`s that can be added, multiplied, or compared (see [examples/prime](examples/prime)). `%`, `//`, and `**` are also supported. Subtraction is
+     supported as long as the result is non-negative (e.g., `Integer(1) - Integer(2) == x` is unsolvable.
    * `NumTrue` and `NumFalse` for cardinality constraints (see [examples/nqueens](examples/nqueens)).
    * `RegexMatch` to apply binary regular expressions to `Tuple`s (see [examples/nonagram](examples/nonagram)).
 

TODO

@@ -3,6 +3,7 @@
 * Rename generate_var, generate_cnf to evaluate*
 * Implement very simple clause caching/suppressing duplicate clauses
 * Support integer division/subtraction by re-arranging parse tree into addition/multiplication
+  instead of solving for the result.
 * Generate a bash script for sat generation/solving/extracting
 * Implement IsPrime predicate using Pratt certificates, drop into jane st. number cross 4
 * Implement Formula.WriteCubedCnf(fd, vars)
@@ -14,3 +15,4 @@
   generate a selection network, but it's not clear if that's more efficient that just computing the
   sum of the varz. Test and remove all the selection network code if it isn't dramatically more
   efficient.
+* Support negative integers with twos-complement representation.

cnfc/model.py

@@ -271,22 +271,22 @@ class TupleExpr:
     def __len__(self):
         return len(self.exprs)
 
-    def __eq__(self, other: 'TupleExpr'):
+    def __eq__(self, other):
         return TupleEq(self, other)
 
-    def __ne__(self, other: 'TupleExpr'):
+    def __ne__(self, other):
         return TupleNeq(self, other)
 
-    def __lt__(self, other: 'TupleExpr'):
+    def __lt__(self, other):
         return TupleLt(self, other)
 
-    def __le__(self, other: 'TupleExpr'):
+    def __le__(self, other):
         return TupleLe(self, other)
 
-    def __gt__(self, other: 'TupleExpr'):
+    def __gt__(self, other):
         return TupleGt(self, other)
 
-    def __ge__(self, other: 'TupleExpr'):
+    def __ge__(self, other):
         return TupleGe(self, other)
 
     def __add__(self, other):
@@ -295,6 +295,12 @@ def __add__(self, other):
     def __radd__(self, other):
         return TupleAdd(other, self)
 
+    def __sub__(self, other):
+        return TupleSub(self, other)
+
+    def __rsub__(self, other):
+        return TupleSub(other, self)
+
     def __mul__(self, other):
         return TupleMul(self, other)
 
@@ -348,6 +354,18 @@ def evaluate(self, formula):
     def __len__(self):
         return max(len(self.args[0]), len(self.args[1])) + 1
 
+class TupleSub(TupleCompositeExpr):
+    def evaluate(self, formula):
+        t1, t2 = self.args
+        # if t1 - t2 == y, then t2 + y == t1
+        ys = [formula.AddVar() for i in range(len(self))]
+        y = Tuple(*ys)
+        formula.Add(t2 + y == t1)
+        return ys
+
+    def __len__(self):
+        return max(len(self.args[0]), len(self.args[1]))
+
 class TupleMul(TupleCompositeExpr):
     def evaluate(self, formula):
         t1 = self.args[0].evaluate(formula)

tests/test_formula.py

@@ -860,6 +860,21 @@ def test_integer_arithmetic(self):
         self.assertSat(f)
         f.PopCheckpoint()
 
+    def test_integer_subtraction(self):
+        f = Formula()
+        bits = 8
+        x = [f.AddVar('x{}'.format(i)) for i in range(bits)]
+
+        # x = 00001010 (== 10). Does this equal 5 + 5?
+
+        f.Add(~x[0]); f.Add(~x[1]); f.Add(~x[2]); f.Add(~x[3])
+        f.Add(x[4]);  f.Add(~x[5]); f.Add(x[6]);  f.Add(~x[7])
+
+        f.PushCheckpoint()
+        f.Add(Integer(*x) - Integer(5) == Integer(5))
+        self.assertSat(f)
+        f.PopCheckpoint()
+
     def test_addition_exhaustive(self):
         f = Formula()
         # Test addition of all numbers x + y where x,y < 8
@@ -882,6 +897,31 @@ def test_addition_exhaustive(self):
                     self.assertUnsat(f)
                     f.PopCheckpoint()
 
+    def test_subtraction_exhaustive(self):
+        f = Formula()
+        # Test addition of all numbers x + y where x,y < 8
+        # Currently, we only support subtraction that yields a non-negative
+        # integer, so a result that would be negative will be UNSAT. This test
+        # should change when we support twos complement integers.
+        limit = 8
+        for x in range(limit):
+            for y in range(limit):
+                f.PushCheckpoint()
+                f.Add(Integer(x) == Integer(x+y) - Integer(y))
+                self.assertSat(f)
+                f.PopCheckpoint()
+
+                f.PushCheckpoint()
+                f.Add(Integer(x) == Integer(x+y+1) - Integer(y))
+                self.assertUnsat(f)
+                f.PopCheckpoint()
+
+                if x > 0 and y > 0:
+                    f.PushCheckpoint()
+                    f.Add(Integer(x) == Integer(x+y-1) - Integer(y))
+                    self.assertUnsat(f)
+                    f.PopCheckpoint()
+
     def test_integer_multiplication_basic(self):
         f = Formula()
         x2, x1, x0 = f.AddVars('x2 x1 x0')