fixup! WIP: Schoenhage-Strassen debugging

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -2190,7 +2190,7 @@ bvt bv_utilst::unsigned_schoenhage_strassen_multiplier(
   bvt b = a;
   PRECONDITION(a.size() == b.size());
 
-  // Running examples: we want to multiple 213 by 15 as 8- or 9-bit integers.
+  // Running example: we want to multiply 213 by 15 as 8- or 9-bit integers.
   // That is, we seek to multiply 11010101 (011010101) by 00001111 (000001111).
   //                              ^bit 7 ^bit 0
   // The expected result is 123 as both an 8-bit and 9-bit result (001111011).
@@ -2245,8 +2245,10 @@ bvt bv_utilst::unsigned_schoenhage_strassen_multiplier(
   {
     a_rho.emplace_back(
       a_ext.begin() + i * chunk_size, a_ext.begin() + (i + 1) * chunk_size);
+    std::cerr << "a_rho[" << i << "]: " << beautify(a_rho.back()) << std::endl;
     b_sigma.emplace_back(
       b_ext.begin() + i * chunk_size, b_ext.begin() + (i + 1) * chunk_size);
+    std::cerr << "b_sigma[" << i << "]: " << beautify(b_sigma.back()) << std::endl;
   }
   // For our example we now have
   // a_rho = [ 0101, 1101, 0000, ..., 0000 ]
@@ -2268,11 +2270,13 @@ bvt bv_utilst::unsigned_schoenhage_strassen_multiplier(
         ++rho)
     {
       const std::size_t sigma = tau - rho;
+      std::cerr << "Inner multiplication a_" << rho << " * b_" << sigma << std::endl;
       gamma_tau[tau] = add(
         gamma_tau[tau],
+        zero_extension(
         unsigned_multiplier(
-          zero_extension(a_rho[rho], 3 * n + 5),
-          zero_extension(b_sigma[sigma], 3 * n + 5)));
+          zero_extension(a_rho[rho], chunk_size * 2),
+          zero_extension(b_sigma[sigma], chunk_size * 2)), 3 * n + 5));
     }
   }
   // For our example we obtain
@@ -2284,6 +2288,7 @@ bvt bv_utilst::unsigned_schoenhage_strassen_multiplier(
   c_tau.reserve(num_chunks);
   for(std::size_t tau = 0; tau < num_chunks; ++tau)
   {
+    std::cerr << "gamma_tau[" << tau << "]: " << beautify(gamma_tau[tau]) << std::endl;
     c_tau.push_back(add(gamma_tau[tau], gamma_tau[tau + num_chunks]));
     CHECK_RETURN(c_tau.back().size() >= address_bits(num_chunks) + 1);
     c_tau.back().resize(address_bits(num_chunks) + 1);
@@ -2292,6 +2297,10 @@ bvt bv_utilst::unsigned_schoenhage_strassen_multiplier(
   // For our example we obtain
   // c_tau = [ 01011, 00011, 0... ]
 
+  // XXX 19*19 seems ok up to here with
+  // http://malte-leip.net/beschreibung_ssa.pdf,
+  // https://de.wikipedia.org/wiki/Sch%C3%B6nhage-Strassen-Algorithmus
+
   // Compute z_j = c_j - c_{j + 2^n} (mod 2^(n + 2)) (mod 2^(n + 1) and c_{j +
   // 2^(n - 1)} when m is even)
   std::vector<bvt> z_j;