Make cardinality generators iterative so we don't get RecursionErrors

TODO

@@ -8,7 +8,5 @@
 * 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)
-
-* Make cardinality.py generators iterative instead of recursive to avoid RecursionLimit with large formulas
 * Make NumTrue auto-convert to NumFalse and vise-versa when appropriate
 * Add a Formula.WriteBlocker method to write a blocking solution extractor

cnfc/cardinality.py

@@ -4,25 +4,23 @@
 # Generates clauses satisfiable iff at most one of the variables in vs is false.
 # Uses Heule's encoding, see TAOCP 7.2.2.2 exercise 12.
 def at_most_one_false(formula, vs):
-    if len(vs) <= 4:
-        yield from at_most_one_false_exhaustive(vs)
-    else:
+    while len(vs) > 4:
         head, tail = vs[:3], vs[3:]
         v = formula.AddVar()
         yield from at_most_one_false_exhaustive(head + [v])
-        yield from at_most_one_false(formula, [~v] + tail)
+        vs = [~v] + tail
+    yield from at_most_one_false_exhaustive(vs)
 
 def at_most_one_false_exhaustive(vs):
     yield from combinations(vs, 2)
 
 def at_most_one_true(formula, vs):
-    if len(vs) <= 4:
-        yield from at_most_one_true_exhaustive(vs)
-    else:
+    while len(vs) > 4:
         head, tail = vs[:3], vs[3:]
         v = formula.AddVar()
         yield from at_most_one_true_exhaustive(head + [v])
-        yield from at_most_one_true(formula, [~v] + tail)
+        vs = [~v] + tail
+    yield from at_most_one_true_exhaustive(vs)
 
 def at_most_one_true_exhaustive(vs):
     for x,y in combinations(vs, 2):

tests/test_cardinality.py

@@ -316,3 +316,13 @@ def test_eq_boundary(self):
         self.assertSat(f)
 
         # At most n true is a tautology, no way to create an unsat formula.
+
+    # at_most_one_{true,false} used to be implemented recursively, which meant that
+    # you'd need to adjust the recursion limit with sys.setrecursionlimit() to make
+    # larger cardinality constraints work. This test used to generate a RecursionError.
+    def test_many_vars(self):
+        f = Formula()
+        import sys
+        limit = sys.getrecursionlimit() * 2
+        varz = [f.AddVar() for i in range(2 * limit)]
+        f.Add(NumTrue(*varz) >= limit)