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.

1 files changed, 14 insertions, 0 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);
   }