WIP: make balanced-depth adder trees

src/ast/rewriter/bit_blaster/bit_blaster_adder.cpp

@@ -52,39 +52,102 @@ void bit_blaster_adder::mk_full_adder(expr * a, expr * b, expr * c, expr_ref & o
 void bit_blaster_adder::variable_bits(expr_ref_vector & out_bits) {
     SASSERT(out_bits.empty());
 
-    expr_ref_vector carries(m());
+    // A balanced adder tree is one with roughly the same number of gates
+    // between an output bit and all the input bits which affect it. The
+    // invariant for the following loop is that the bits in a column of
+    // m_variable are all outputs of balanced adder trees of roughly equal
+    // height. Initially the bits in m_variable are the input bits, so they're
+    // all at height 0. At iteration N+1, a column has the sums of triples of
+    // bits that were in that column at N, and carries from the next column to
+    // the right at N. By induction, the number of full adders between any bit
+    // and its inputs is N; aside from a little hand-waving for when the number
+    // of bits in a column isn't divisible by three and the leftovers are
+    // forwarded to the next round unchanged, or when the heights of the
+    // columns are very uneven.
+    //
+    // The loop terminates once all columns have at most two bits in them, at
+    // which point the final sum can be computed with a ripple-carry adder.
+    // This construction resembles a Wallace or Dadda tree adder but is easier
+    // to explain, and uses only full adders during the reduction to minimize
+    // gate count.
+
+    expr_ref_vector carries(m()), last(m());
     expr_ref out(m()), carry(m());
-    expr_ref a(m()), b(m()), c(m());
-
-    for (auto & column : m_variable) {
-        column.append(carries);
-        carries.reset();
-
-        while (column.size() >= 3) {
-            a = column.back();
-            column.pop_back();
-            b = column.back();
-            column.pop_back();
-            c = column.back();
-            column.pop_back();
-
-            mk_full_adder(a, b, c, out, carry);
-            column.push_back(out);
-            carries.push_back(carry);
+    bool too_big;
+    do {
+        too_big = false;
+        SASSERT(last.empty());
+        for (auto & column : m_variable) {
+            SASSERT(carries.empty());
+
+            unsigned src = 0, dst = 0;
+            while (src + 3 <= column.size()) {
+                expr * a = column.get(src + 0);
+                expr * b = column.get(src + 1);
+                expr * c = column.get(src + 2);
+
+                mk_full_adder(a, b, c, out, carry);
+                column.set(dst, out);
+                carries.push_back(carry);
+
+                src += 3;
+                dst += 1;
+            }
+            if (dst > 0) {
+                while (src < column.size()) {
+                    column.set(dst, column.get(src));
+                    ++src;
+                    ++dst;
+                }
+                column.shrink(dst);
+            }
+
+            // The carries from the previous column are trees of the same
+            // height as this column _after_ it's reduced, so to maintain the
+            // loop invariant it's important to add the carries here and not
+            // before the above adder loop.
+            column.append(last);
+            last.reset();
+            carries.swap(last);
+
+            if (column.size() > 2)
+                too_big = true;
         }
 
-        if (column.size() == 2) {
-            a = column.back();
-            column.pop_back();
-            b = column.back();
-            column.pop_back();
+        // discard final carries
+        last.reset();
+    } while (too_big);
 
-            mk_half_adder(a, b, out, carry);
-            column.push_back(out);
-            carries.push_back(carry);
+    carry = m().mk_false();
+    for (auto & column : m_variable) {
+        if (!m().is_false(carry))
+            column.push_back(carry);
+
+        switch (column.size()) {
+            case 0:
+                out = m().mk_false();
+                break;
+
+            case 1:
+                out = column.get(0);
+                carry = m().mk_false();
+                break;
+
+            case 2:
+                mk_half_adder(column.get(0), column.get(1), out, carry);
+                column.reset();
+                column.push_back(out);
+                break;
+
+            case 3:
+                mk_full_adder(column.get(0), column.get(1), column.get(2), out, carry);
+                column.reset();
+                column.push_back(out);
+                break;
+
+            default: UNREACHABLE();
         }
-
-        out_bits.push_back(column.get(0, m().mk_false()));
+        out_bits.push_back(out);
     }
 
     SASSERT(out_bits.size() == size());