fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup

11 files changed, 226 insertions, 145 deletions

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 386834385..5484e25e9 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -144,6 +144,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
     return false;
   }else{
     EqualityQuery* q = qe->getEqualityQuery();
+    bool success = true;
     //save previous match
     InstMatch prev( &m );
     //if t is null
@@ -162,33 +163,36 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
                                     << m.get(d_match_pattern[i])
                                     << std::endl;
             Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl;
-            return false;
+            success = false;
+            break;
           }
         }
       }else{
         if( !q->areEqual( d_match_pattern[i], t[i] ) ){
           Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
           //ground arguments are not equal
-          return false;
+          success = false;
+          break;
         }
       }
     }
-    //now, fit children into match
-    //we will be requesting candidates for matching terms for each child
-    std::vector< Node > reps;
-    for( int i=0; i<(int)d_children.size(); i++ ){
-      Node rep = q->getRepresentative( t[ d_children_index[i] ] );
-      reps.push_back( rep );
-      d_children[i]->reset( rep, qe );
-    }
-    bool success = true;
-    if( d_next!=NULL ){
-      success = d_next->getNextMatch( f, m, qe );
-    }else{
-      if( d_active_add ){
-        Trace("active-add") << "Active Adding instantiation " << m << std::endl;
-        success = qe->addInstantiation( f, m );
-        Trace("active-add") << "Success = " << success << std::endl;
+    if( success ){
+      //now, fit children into match
+      //we will be requesting candidates for matching terms for each child
+      std::vector< Node > reps;
+      for( int i=0; i<(int)d_children.size(); i++ ){
+        Node rep = q->getRepresentative( t[ d_children_index[i] ] );
+        reps.push_back( rep );
+        d_children[i]->reset( rep, qe );
+      }
+      if( d_next!=NULL ){
+        success = d_next->getNextMatch( f, m, qe );
+      }else{
+        if( d_active_add ){
+          Trace("active-add") << "Active Adding instantiation " << m << std::endl;
+          success = qe->addInstantiation( f, m );
+          Trace("active-add") << "Success = " << success << std::endl;
+        }
       }
     }
     if( !success ){
@@ -317,10 +321,10 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
           return addedLemmas;
         }
       }
-      m.clear();
     }else{
       addedLemmas++;
     }
+    m.clear();
   }
   //return number of lemmas added
   return addedLemmas;
@@ -463,10 +467,11 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu
     std::vector< InstMatch > newMatches;
     InstMatch m;
     while( d_children[i]->getNextMatch( f, m, qe ) ){
-      m.makeRepresentative( qe );
+      //m.makeRepresentative( qe );
       newMatches.push_back( InstMatch( &m ) );
       m.clear();
     }
+    Debug("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
     for( int j=0; j<(int)newMatches.size(); j++ ){
       processNewMatch( qe, newMatches[j], i, addedLemmas );
     }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index d1c04ceab..d8b154b95 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -368,15 +368,32 @@ void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){
   d_op_selection_terms.clear();
 }
 
+
+int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
+  /*
+  size_t maxChildren = 0;
+  for( size_t i=0; i<uf_terms.size(); i++ ){
+    if( uf_terms[i].getNumChildren()>maxChildren ){
+      maxChildren = uf_terms[i].getNumChildren();
+    }
+  }
+  //TODO: look at how many entries they have?
+  return (int)maxChildren;
+  */
+  return 0;
+}
+
 void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
   Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
   //the pro/con preferences for this quantifier
   std::vector< Node > pro_con[2];
   //the terms in the selection literal we choose
   std::vector< Node > selectionLitTerms;
+  Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl;
   //for each asserted quantifier f,
   // - determine selection literals
   // - check which function/predicates have good and bad definitions for satisfying f
+  int selectLitScore = -1;
   QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f );
   for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){
     //the literal n is phase-required for quantifier f
@@ -433,10 +450,18 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
             selectLit = true;
           }
         }
+        //also check if it is naturally a better literal
+        if( !selectLit ){
+          int score = getSelectionScore( uf_terms );
+          //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
+          selectLit = score<selectLitScore;
+        }
         //see if we wish to choose this as a selection literal
         d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
         if( selectLit ){
+          selectLitScore = getSelectionScore( uf_terms );
           Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
+          Trace("inst-gen-debug") << "  flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
           d_quant_selection_lit[f] = value ? n : n.notNode();
           selectionLitTerms.clear();
           selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
@@ -466,7 +491,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
       d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
     }
   }else{
-    Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl;
+    Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
   }
   //process information about requirements and preferences of quantifier f
   if( d_quant_sat.find( f )!=d_quant_sat.end() ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 908cfca2b..5490d17dd 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -155,6 +155,8 @@ private:    ///information for (old) InstGen
   std::map< Node, Node > d_term_selection_lit;
   //map from operators to terms that appear in selection literals
   std::map< Node, std::vector< Node > > d_op_selection_terms;
+  //get selection score
+  int getSelectionScore( std::vector< Node >& uf_terms );
 protected:
   //reset
   void reset( FirstOrderModel* fm );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 39377d11c..1522d0828 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -224,7 +224,7 @@ int ModelEngine::checkModel( int checkOption ){
 
 int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
   int addedLemmas = 0;
-  Debug("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl;
+  Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl;
   Debug("inst-fmf-ei") << "   Instantiation Constants: ";
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
@@ -298,12 +298,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
       relevantInst = relevantInst * (int)riter.d_domain[i].size();
     }
     d_relevantLemmas += relevantInst;
-    Debug("inst-fmf-ei") << "Finished: " << std::endl;
+    Trace("inst-fmf-ei") << "Finished: " << std::endl;
     //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
-    Debug("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
-    Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
-    Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-    Debug("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
+    Trace("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
+    Trace("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
+    Trace("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
+    Trace("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
     if( addedLemmas>1000 ){
       Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
       //Trace("model-engine-warn") << "   Inst Total: " << totalInst << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 6b204eb60..7a3687dd5 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -37,6 +37,9 @@ option cnfQuant --cnf-quant bool :default false
 option preSkolemQuant --pre-skolem-quant bool :default false
  apply skolemization eagerly to bodies of quantified formulas
 
+# Whether to perform agressive miniscoping
+option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
+ perform aggressive miniscoping for quantifiers
 # Whether to perform quantifier macro expansion
 option macrosQuant --macros-quant bool :default false
  perform quantifiers macro expansions
@@ -65,6 +68,7 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false
  turns on counterexample-based quantifier instantiation [off by default]
 /turns off counterexample-based quantifier instantiation
 
+
 option userPatternsQuant /--ignore-user-patterns bool :default true
  ignore user-provided patterns for quantifier instantiation
 
@@ -94,6 +98,8 @@ option fmfInstGen /--disable-fmf-inst-gen bool :default true
  disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
+option fmfFreshDistConst --fmf-fresh-dc bool :default false
+ use fresh distinguished representative when applying Inst-Gen techniques
 
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index dabaa2188..bf6a025f8 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -90,29 +90,15 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
   }
 }
 
-void QuantifiersRewriter::computeArgs( std::map< Node, bool >& active, Node n ){
-  if( active.find( n )!=active.end() ){
-    active[n] = true;
+void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ){
+  if( n.getKind()==BOUND_VARIABLE ){
+    if( std::find( args.begin(), args.end(), n )!=args.end() &&
+        std::find( activeArgs.begin(), activeArgs.end(), n )==activeArgs.end() ){
+      activeArgs.push_back( n );
+    }
   }else{
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      computeArgs( active, n[i] );
-    }
-  }
-}
-
-void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ){
-  std::map< Node, bool > active;
-  for( int i=0; i<(int)args.size(); i++ ){
-    active[ args[i] ] = false;
-  }
-  //Notice() << "For " << n << " : " << std::endl;
-  computeArgs( active, n );
-  activeArgs.clear();
-  for( std::map< Node, bool >::iterator it = active.begin(); it != active.end(); ++it ){
-    Node n = it->first;
-    //Notice() << "   " << it->first << " is " << it->second << std::endl;
-    if( it->second ){ //only add bound variables that occur in body
-      activeArgs.push_back( it->first );
+      computeArgs( args, activeArgs, n[i] );
     }
   }
 }
@@ -468,37 +454,19 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
   }
 }
 
-Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq ){
+Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
   if( body.getKind()==FORALL ){
-    if( pol==polReq ){
+    if( pol ){
       std::vector< Node > terms;
       std::vector< Node > subs;
-      if( polReq ){
-        //for doing prenexing of same-signed quantifiers
-        //must rename each variable that already exists
-        for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
-          terms.push_back( body[0][i] );
-          subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
-        }
-        args.insert( args.end(), subs.begin(), subs.end() );
-      }else{
-        std::vector< TypeNode > argTypes;
-        for( int i=0; i<(int)args.size(); i++ ){
-          argTypes.push_back( args[i].getType() );
-        }
-        //for doing pre-skolemization of opposite-signed quantifiers
-        for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          terms.push_back( body[0][i] );
-          //make the new function symbol
-          TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, body[0][i].getType() );
-          Node op = NodeManager::currentNM()->mkSkolem( "op_$$", typ, "was created by the quantifiers rewriter" );
-          std::vector< Node > funcArgs;
-          funcArgs.push_back( op );
-          funcArgs.insert( funcArgs.end(), args.begin(), args.end() );
-          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, funcArgs ) );
-        }
+      //for doing prenexing of same-signed quantifiers
+      //must rename each variable that already exists
+      for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+        //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
+        terms.push_back( body[0][i] );
+        subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
       }
+      args.insert( args.end(), subs.begin(), subs.end() );
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
       Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl;
@@ -514,7 +482,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
     std::vector< Node > newChildren;
     for( int i=0; i<(int)body.getNumChildren(); i++ ){
       bool newPol = ( body.getKind()==NOT || ( body.getKind()==IMPLIES && i==0 ) ) ? !pol : pol;
-      Node n = computePrenex( body[i], args, newPol, polReq );
+      Node n = computePrenex( body[i], args, newPol );
       newChildren.push_back( n );
       if( n!=body[i] ){
         childrenChanged = true;
@@ -549,10 +517,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
     if( computeOption==COMPUTE_MINISCOPING ){
       //return directly
       return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
+    }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
+      return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) );
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
-    }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
-      n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
+    }else if( computeOption==COMPUTE_PRENEX ){
+      n = computePrenex( n, args, true );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
       Node prev;
       do{
@@ -670,42 +640,113 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
   }
   return mkForAll( args, body, ipl );
 }
-/*
-Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){
-  if( n.getKind()==FORALL ){
-    return rewriteQuant( n, isNested );
-  }else if( isLiteral( n ) ){
-    return n;
-  }else{
-    NodeBuilder<> tt(n.getKind());
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      tt << rewriteQuants( n[i], isNested );
-    }
-    return tt.constructNode();
-  }
-}
 
-Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){
-  Node prev = n;
-  for( int op=0; op<COMPUTE_LAST; op++ ){
-    if( doOperation( n, isNested, op ) ){
-      Node prev2 = n;
-      n = computeOperation( n, op );
-      if( prev2!=n ){
-        Trace("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl;
-        Trace("quantifiers-rewrite-op") << " to " << std::endl;
-        Trace("quantifiers-rewrite-op") << n << std::endl;
+Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){
+  if( !isNested ){
+    std::map< Node, std::vector< Node > > varLits;
+    std::map< Node, std::vector< Node > > litVars;
+    if( body.getKind()==OR ){
+      Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
+      for( size_t i=0; i<body.getNumChildren(); i++ ){
+        std::vector< Node > activeArgs;
+        computeArgs( args, activeArgs, body[i] );
+        for (unsigned j=0; j<activeArgs.size(); j++ ){
+          varLits[activeArgs[j]].push_back( body[i] );
+        }
+        litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+      }
+      //find the variable in the least number of literals
+      Node bestVar;
+      for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
+        if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
+          bestVar = it->first;
+        }
+      }
+      Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
+      if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
+        //we can miniscope
+        Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
+        //make the bodies
+        std::vector< Node > qlit1;
+        qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
+        std::vector< Node > qlitt;
+        //for all literals not containing bestVar
+        for( size_t i=0; i<body.getNumChildren(); i++ ){
+          if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
+            qlitt.push_back( body[i] );
+          }
+        }
+        //make the variable lists
+        std::vector< Node > qvl1;
+        std::vector< Node > qvl2;
+        std::vector< Node > qvsh;
+        for( unsigned i=0; i<args.size(); i++ ){
+          bool found1 = false;
+          bool found2 = false;
+          for( size_t j=0; j<varLits[args[i]].size(); j++ ){
+            if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
+              found1 = true;
+            }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
+              found2 = true;
+            }
+            if( found1 && found2 ){
+              break;
+            }
+          }
+          if( found1 ){
+            if( found2 ){
+              qvsh.push_back( args[i] );
+            }else{
+              qvl1.push_back( args[i] );
+            }
+          }else{
+            Assert(found2);
+            qvl2.push_back( args[i] );
+          }
+        }
+        Assert( !qvl1.empty() );
+        Assert( !qvl2.empty() || !qvsh.empty() );
+        //check for literals that only contain shared variables
+        std::vector< Node > qlitsh;
+        std::vector< Node > qlit2;
+        for( size_t i=0; i<qlitt.size(); i++ ){
+          bool hasVar2 = false;
+          for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
+            if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
+              hasVar2 = true;
+              break;
+            }
+          }
+          if( hasVar2 ){
+            qlit2.push_back( qlitt[i] );
+          }else{
+            qlitsh.push_back( qlitt[i] );
+          }
+        }
+        varLits.clear();
+        litVars.clear();
+        Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
+        Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
+        Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
+        n1 = computeAggressiveMiniscoping( qvl1, n1 );
+        qlitsh.push_back( n1 );
+        if( !qlit2.empty() ){
+          Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
+          n2 = computeAggressiveMiniscoping( qvl2, n2 );
+          qlitsh.push_back( n2 );
+        }
+        Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
+        if( !qvsh.empty() ){
+          Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
+          n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
+        }
+        Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
+        return n;
       }
     }
   }
-  if( prev==n ){
-    return n;
-  }else{
-    //rewrite again until fix point is reached
-    return rewriteQuant( n, isNested );
-  }
+  return mkForAll( args, body, Node::null() );
 }
-*/
 
 bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
   return options::miniscopeQuantFreeVar();
@@ -726,12 +767,12 @@ bool QuantifiersRewriter::doMiniscopingAnd(){
 bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
   if( computeOption==COMPUTE_MINISCOPING ){
     return true;
+  }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
+    return options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
-  }else if( computeOption==COMPUTE_PRE_SKOLEM ){
-    return false;//options::preSkolemQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant();
+    return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return options::varElimQuant();
   }else if( computeOption==COMPUTE_CNF ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 00301c610..75b392e15 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -41,19 +41,19 @@ private:
   static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static bool hasArg( std::vector< Node >& args, Node n );
   static void setNestedQuantifiers( Node n, Node q );
-  static void computeArgs( std::map< Node, bool >& active, Node n );
   static Node computeClause( Node n );
 private:
   static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
+  static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false );
   static Node computeNNF( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
-  static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq );
+  static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
 private:
   enum{
     COMPUTE_MINISCOPING = 0,
+    COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
-    COMPUTE_PRE_SKOLEM,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 65624686a..f6518cfd3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -75,7 +75,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
     //Call the children?
     if( inst::Trigger::isAtomicTrigger( n ) ){
       if( !n.hasAttribute(InstConstantAttribute()) ){
-        Debug("term-db") << "register trigger term " << n << std::endl;
+        Trace("term-db") << "register term in db " << n << std::endl;
         //std::cout << "register trigger term " << n << std::endl;
         Node op = n.getOperator();
         d_op_map[op].push_back( n );
@@ -194,7 +194,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
-    if( d_type_map[ tn ].empty() ){
+    if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
       std::stringstream ss;
       ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c4bc248d3..cff28f243 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -38,7 +38,8 @@ d_quantEngine( qe ), d_f( f ){
   for( int i=0; i<(int)d_nodes.size(); i++ ){
     Trace("trigger") << "   " << d_nodes[i] << std::endl;
   }
-  Trace("trigger") << ", smart triggers = " << smartTriggers << std::endl;
+  Trace("trigger-debug") << ", smart triggers = " << smartTriggers;
+  Trace("trigger") << std::endl;
   if( smartTriggers ){
     if( d_nodes.size()==1 ){
       if( isSimpleTrigger( d_nodes[0] ) ){
@@ -49,6 +50,8 @@ d_quantEngine( qe ), d_f( f ){
       }
     }else{
       d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption );
+      //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
+      //d_mg->setActiveAdd();
     }
   }else{
     d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 50433facd..a11cc85c0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -616,7 +616,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       getEquivalenceClass( r, eqc );
       //find best selection for representative
       Node r_best;
-      int r_best_score;
+      int r_best_score = -1;
       for( size_t i=0; i<eqc.size(); i++ ){
         int score = getRepScore( eqc[i], f, index );
         if( optInternalRepSortInference() ){
@@ -714,5 +714,5 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
 }
 
 bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
-  return false;
+  return false; //shown to be not effective
 }
\ No newline at end of file
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 3e31faedb..25cb8b66c 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -637,38 +637,37 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           if( !addedLemma ){
             Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
             Trace("uf-ss-si")  << "Must combine region" << std::endl;
-            if( true || !options::ufssColoringSat() ){
-              bool recheck = false;
-              //naive strategy, force region combination involving the first valid region
-              if( options::sortInference()){
-                std::map< int, int > sortsFound;
-                for( int i=0; i<(int)d_regions_index; i++ ){
-                  if( d_regions[i]->d_valid ){
-                    Node op = d_regions[i]->d_nodes.begin()->first;
-                    int sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ;
-                    if( sortsFound.find( sort_id )!=sortsFound.end() ){
-                      combineRegions( sortsFound[sort_id], i );
-                      recheck = true;
-                      break;
-                    }else{
-                      sortsFound[sort_id] = i;
-                    }
-                  }
-                }
-              }
-              if( !recheck ) {
-                for( int i=0; i<(int)d_regions_index; i++ ){
-                  if( d_regions[i]->d_valid ){
-                    forceCombineRegion( i, false );
+            bool recheck = false;
+            if( options::sortInference()){
+              //if sort inference is enabled, search for regions with same sort
+              std::map< int, int > sortsFound;
+              for( int i=0; i<(int)d_regions_index; i++ ){
+                if( d_regions[i]->d_valid ){
+                  Node op = d_regions[i]->d_nodes.begin()->first;
+                  int sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op);
+                  if( sortsFound.find( sort_id )!=sortsFound.end() ){
+                    combineRegions( sortsFound[sort_id], i );
                     recheck = true;
                     break;
+                  }else{
+                    sortsFound[sort_id] = i;
                   }
                 }
               }
-              if( recheck ){
-                check( level, out );
+            }
+            if( !recheck ) {
+              //naive strategy, force region combination involving the first valid region
+              for( int i=0; i<(int)d_regions_index; i++ ){
+                if( d_regions[i]->d_valid ){
+                  forceCombineRegion( i, false );
+                  recheck = true;
+                  break;
+                }
               }
             }
+            if( recheck ){
+              check( level, out );
+            }
           }
         }
       }