Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)

Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility
depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks.

1 files changed, 26 insertions, 1 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 3a7568196..cf16efbfa 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -2939,7 +2939,32 @@ Node BvInverter::solveBvLit(Node sv,
     }
     else if (k == BITVECTOR_CONCAT)
     {
-      sc = getScBvConcat(pol, litk, index, x, sv_t, t);
+      if (litk == EQUAL && options::cbqiBvConcInv())
+      {
+        /* Compute inverse for s1 o x, x o s2, s1 o x o s2
+         * (while disregarding that invertibility depends on si)
+         * rather than an invertibility condition (the proper handling).
+         * This improves performance on a considerable number of benchmarks.
+         *
+         * x = t[upper:lower]
+         * where
+         * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
+         * lower = getSize(sv_t[i]) for i > index  */
+        unsigned upper, lower;
+        upper = bv::utils::getSize(t) - 1;
+        lower = 0;
+        NodeBuilder<> nb(BITVECTOR_CONCAT);
+        for (unsigned i = 0; i < nchildren; i++)
+        {
+          if (i < index) { upper -= bv::utils::getSize(sv_t[i]); }
+          else if (i > index) { lower += bv::utils::getSize(sv_t[i]); }
+        }
+        t = bv::utils::mkExtract(t, upper, lower);
+      }
+      else
+      {
+        sc = getScBvConcat(pol, litk, index, x, sv_t, t);
+      }
     }
     else if (k == BITVECTOR_SIGN_EXTEND)
     {