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, 4 insertions, 0 deletions

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;
               }
             }
           }