From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 22 Jan 2018 18:06:26 +0000 (-0800)
Subject: Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)
X-Git-Tag: cvc5-1.0.0~5350
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b12b1e8307295e68cb389eaa7692036fae6e872;p=cvc5.git

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.
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 2376409e0..c6eb1cd5e 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -355,6 +355,8 @@ option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true
   replaces extract terms with variables for counterexample-guided instantiation for bit-vectors
 option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true
   linearize adder chains for variables
+option cbqiBvConcInv cbqi-bv-concat-inv --cbqi-bv-concat-inv bool :read-write :default true
+  compute inverse for concat over equalities rather than producing an invertibility condition
  
 ### local theory extensions options 
 
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)
     {