Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 669df055a..5696251ed 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -28,6 +28,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
+using namespace CVC4::theory::inst;
 
 #define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
 //#define MULTI_TRIGGER_FULL_EFFORT_HALF
@@ -83,7 +84,7 @@ void InstStrategyCheckCESolved::calcSolved( Node f ){
     Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
     Node rep = d_th->getInternalRepresentative( i );
     if( !rep.hasAttribute(InstConstantAttribute()) ){
-      d_th->d_baseMatch[f].d_map[ i ] = rep;
+      d_th->d_baseMatch[f].set(i,rep);
     }else{
       d_solved[ f ] = false;
     }