Improvements for CBQI (#1478)

Includes:

- Basic rewriting for choice functions in the builtin rewriter,
- Do not consider more than one equal term in ceg instantiator (helps cases where we have a 
  repeated pattern of duplicate instantiations),
- Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat
  equalities suffice).
- Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass.

4 files changed, 36 insertions, 21 deletions

diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index edc934d0d..b0e3aeb6f 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -94,6 +94,20 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
       Trace("builtin-rewrite-debug") << "...failed to get array representation." << std::endl;
     }
     return RewriteResponse(REWRITE_DONE, node);
+  }
+  else if (node.getKind() == kind::CHOICE)
+  {
+    if (node[1].getKind() == kind::EQUAL)
+    {
+      for (unsigned i = 0; i < 2; i++)
+      {
+        if (node[1][i] == node[0][0])
+        {
+          return RewriteResponse(REWRITE_DONE, node[1][1 - i]);
+        }
+      }
+    }
+    return RewriteResponse(REWRITE_DONE, node);
   }else{ 
     return doRewrite(node);
   }
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index e14ae78fc..0e8b229a3 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -335,6 +335,10 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
                 {
                   return true;
                 }
+                // Do not consider more than one equal term,
+                // this helps non-monotonic strategies that may encounter
+                // duplicate instantiations.
+                break;
               }
             }
           }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 4b326ede6..2c71de666 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -1920,9 +1920,6 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
             nm->mkSkolem("ek",
                          ex.getType(),
                          "variable to represent disjoint extract region");
-        Node ceq_lem = var.eqNode(ex);
-        Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl;
-        new_lems.push_back(ceq_lem);
         children.push_back(var);
         vars.push_back(var);
       }
@@ -1967,15 +1964,17 @@ void BvInstantiatorPreprocess::collectExtracts(
     if (visited.find(cur) == visited.end())
     {
       visited.insert(cur);
-
-      if (cur.getKind() == BITVECTOR_EXTRACT)
+      if (cur.getKind() != FORALL)
       {
-        extract_map[cur[0]].push_back(cur);
-      }
+        if (cur.getKind() == BITVECTOR_EXTRACT)
+        {
+          extract_map[cur[0]].push_back(cur);
+        }
 
-      for (const Node& nc : cur)
-      {
-        visit.push_back(nc);
+        for (const Node& nc : cur)
+        {
+          visit.push_back(nc);
+        }
       }
     }
   } while (!visit.empty());
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 0648942e8..a607909cc 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -284,27 +284,25 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
   virtual ~BvInstantiatorPreprocess() {}
   /** register counterexample lemma
    *
-   * This method modifies the contents of lems based on removing extract terms
-   * when the option --cbqi-bv-rm-extract is enabled.
+   * This method modifies the contents of lems based on the extract terms
+   * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces
+   * a dummy equality so that segments of terms t under extracts can be solved
+   * independently.
    *
    * For example:
    *   P[ ((extract 7 4) t), ((extract 3 0) t)]
    *     becomes:
    *   P[((extract 7 4) t), ((extract 3 0) t)] ^
-   *   t = concat( x74, x30 ) ^
-   *   x74 = ((extract 7 4) t) ^
-   *   x30 = ((extract 3 0) t)
-   * where x74 and x30 are fresh variables.
+   *   t = concat( x74, x30 )
+   * where x74 and x30 are fresh variables of type BV_4.
    *
    * Another example:
    *   P[ ((extract 7 3) t), ((extract 4 0) t)]
    *     becomes:
    *   P[((extract 7 4) t), ((extract 3 0) t)] ^
-   *   t = concat( x75, x44, x30 ) ^
-   *   x75 = ((extract 7 5) t) ^
-   *   x44 = ((extract 4 4) t) ^
-   *   x30 = ((extract 3 0) t)
-   * where x75, x44 and x30 are fresh variables.
+   *   t = concat( x75, x44, x30 )
+   * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4
+   * respectively.
    *
    * Notice we leave the original conjecture alone. This is done for performance
    * since the added equalities ensure we are able to construct the proper