fixup! Implement Karatsuba's multiplication algorithm

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -1973,14 +1973,17 @@ bvt bv_utilst::unsigned_karatsuba_multiplier(const bvt &_op0, const bvt &_op1)
     return unsigned_multiplier(_op0, _op1);
 
   const std::size_t op_size = _op0.size();
-  // only use this approach for powers of two
-  if(op_size == 0 || (op_size & (op_size - 1)) != 0)
-    return unsigned_multiplier(_op0, _op1);
-
   if(op_size == 1)
     return {prop.land(_op0[0], _op1[0])};
 
-  const std::size_t half_op_size = op_size >> 1;
+  // Make sure we work with operands the length of which are powers of two
+  const std::size_t log2 = address_bits(op_size);
+  PRECONDITION(sizeof(std::size_t) * CHAR_BIT > log2);
+  const std::size_t two_to_log2 = (std::size_t)1 << log2;
+  bvt a = zero_extension(_op0, two_to_log2);
+  bvt b = zero_extension(_op1, two_to_log2);
+
+  const std::size_t half_op_size = two_to_log2 >> 1;
 
   // We split each of the operands in half and treat them as coefficients of a
   // polynomial a * 2^half_op_size + b. Straightforward polynomial
@@ -2012,18 +2015,22 @@ bvt bv_utilst::unsigned_karatsuba_multiplier(const bvt &_op0, const bvt &_op1)
   // Therefore, after adding (dh + cg) the multiplication can safely be added
   // over just 2 bits.
 
-  bvt x0{_op0.begin(), _op0.begin() + half_op_size};
-  bvt x1{_op0.begin() + half_op_size, _op0.end()};
-  bvt y0{_op1.begin(), _op1.begin() + half_op_size};
-  bvt y1{_op1.begin() + half_op_size, _op1.end()};
+  bvt x0{a.begin(), a.begin() + half_op_size};
+  bvt x1{a.begin() + half_op_size, a.end()};
+  bvt y0{b.begin(), b.begin() + half_op_size};
+  bvt y1{b.begin() + half_op_size, b.end()};
 
   bvt z0 = unsigned_karatsuba_full_multiplier(x0, y0);
   bvt z1 = add(
     unsigned_karatsuba_multiplier(x1, y0),
     unsigned_karatsuba_multiplier(x0, y1));
   bvt z1_full = concatenate(zeros(half_op_size), z1);
 
-  return add(z0, z1_full);
+  bvt result = add(z0, z1_full);
+  CHECK_RETURN(result.size() >= op_size);
+  if(result.size() > op_size)
+    result.resize(op_size);
+  return result;
 }
 
 bvt bv_utilst::unsigned_toom_cook_multiplier(const bvt &_op0, const bvt &_op1)