Quantifiers subdirectories (#1608)

1 files changed, 808 insertions, 0 deletions

diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
new file mode 100644
index 000000000..9e7961172
--- /dev/null
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -0,0 +1,808 @@
+/*********************                                                        */
+/*! \file model_builder.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of model builder class
+ **/
+
+#include "theory/quantifiers/fmf/model_builder.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/fmf/model_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/uf/theory_uf_strong_solver.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
+    : TheoryEngineModelBuilder(qe->getTheoryEngine()),
+      d_qe(qe),
+      d_addedLemmas(0),
+      d_triedLemmas(0) {}
+
+bool QModelBuilder::optUseModel() {
+  return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
+}
+
+bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
+  return preProcessBuildModelStd( m );
+}
+
+bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
+  d_addedLemmas = 0;
+  d_triedLemmas = 0;
+  if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
+    FirstOrderModel * fm = (FirstOrderModel*)m;
+    //traverse equality engine
+    std::map< TypeNode, bool > eqc_usort;
+    eq::EqClassesIterator eqcs_i =
+        eq::EqClassesIterator(fm->getEqualityEngine());
+    while( !eqcs_i.isFinished() ){
+      TypeNode tr = (*eqcs_i).getType();
+      eqc_usort[tr] = true;
+      ++eqcs_i;
+    }
+    //look at quantified formulas
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node q = fm->getAssertedQuantifier( i, true );
+      if( fm->isQuantifierActive( q ) ){
+        //check if any of these quantified formulas can be set inactive
+        if( options::fmfEmptySorts() ){
+          for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+            TypeNode tn = q[0][i].getType();
+            //we are allowed to assume the type is empty
+            if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
+              Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
+              fm->setQuantifierActive( q, false );
+            }
+          }
+        }else if( options::fmfFunWellDefinedRelevant() ){
+          if( q[0].getNumChildren()==1 ){
+            TypeNode tn = q[0][0].getType();
+            if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
+              //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
+              //we are allowed to assume the introduced type is empty
+              if( eqc_usort.find( tn )==eqc_usort.end() ){
+                Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
+                fm->setQuantifierActive( q, false );
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  return true;
+}
+
+void QModelBuilder::debugModel( TheoryModel* m ){
+  //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
+  if( Trace.isOn("quant-check-model") ){
+    FirstOrderModel* fm = (FirstOrderModel*)m;
+    Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
+    int tests = 0;
+    int bad = 0;
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      std::vector< Node > vars;
+      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
+        vars.push_back( f[0][j] );
+      }
+      QRepBoundExt qrbe(d_qe);
+      RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
+      if( riter.setQuantifier( f ) ){
+        while( !riter.isFinished() ){
+          tests++;
+          std::vector< Node > terms;
+          for (unsigned k = 0; k < riter.getNumTerms(); k++)
+          {
+            terms.push_back( riter.getCurrentTerm( k ) );
+          }
+          Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
+          Node val = fm->getValue( n );
+          if (val != d_qe->getTermUtil()->d_true)
+          {
+            Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
+            Trace("quant-check-model") << "         " << f << std::endl;
+            Trace("quant-check-model") << "         Evaluates to " << val << std::endl;
+            bad++;
+          }
+          riter.increment();
+        }
+        Trace("quant-check-model") << "Tested " << tests << " instantiations";
+        if( bad>0 ){
+          Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
+        }
+        Trace("quant-check-model") << "." << std::endl;
+      }else{
+        if( riter.isIncomplete() ){
+          Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
+        }
+      }
+    }
+  }
+}
+
+bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
+{
+  if (argIndex < n.getNumChildren())
+  {
+    Node r;
+    if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
+      r = n[ argIndex ];
+    }else{
+      r = fm->getRepresentative( n[ argIndex ] );
+    }
+    std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
+    if( it==d_data.end() ){
+      d_data[r].addTerm(fm, n, argIndex + 1);
+      return true;
+    }else{
+      return it->second.addTerm(fm, n, argIndex + 1);
+    }
+  }else{
+    return false;
+  }
+}
+
+QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
+    : QModelBuilder(c, qe),
+      d_basisNoMatch(c),
+      d_didInstGen(false),
+      d_numQuantSat(0),
+      d_numQuantInstGen(0),
+      d_numQuantNoInstGen(0),
+      d_numQuantNoSelForm(0),
+      d_instGenMatches(0) {}
+
+/*
+Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
+  return n;
+}
+*/
+
+bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
+  FirstOrderModel* f = (FirstOrderModel*)m;
+  FirstOrderModelIG* fm = f->asFirstOrderModelIG();
+  Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
+  d_didInstGen = false;
+  //reset the internal information
+  reset( fm );
+  //only construct first order model if optUseModel() is true
+  if( optUseModel() ){
+    Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
+    //check if any quantifiers are un-initialized
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node q = fm->getAssertedQuantifier( i );
+      if( d_qe->getModel()->isQuantifierActive( q ) ){
+        int lems = initializeQuantifier(q, q, f);
+        d_statistics.d_init_inst_gen_lemmas += lems;
+        d_addedLemmas += lems;
+        if( d_qe->inConflict() ){
+          break;
+        }
+      }
+    }
+    if( d_addedLemmas>0 ){
+      Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
+      return false;
+    }else{
+      Assert( !d_qe->inConflict() );
+      //initialize model
+      fm->initialize();
+      //analyze the functions
+      Trace("model-engine-debug") << "Analyzing model..." << std::endl;
+      analyzeModel( fm );
+      //analyze the quantifiers
+      Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
+      d_uf_prefs.clear();
+      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node q = fm->getAssertedQuantifier( i );
+        analyzeQuantifier( fm, q );
+      }
+
+      //if applicable, find exceptions to model via inst-gen
+      if( options::fmfInstGen() ){
+        d_didInstGen = true;
+        d_instGenMatches = 0;
+        d_numQuantSat = 0;
+        d_numQuantInstGen = 0;
+        d_numQuantNoInstGen = 0;
+        d_numQuantNoSelForm = 0;
+        //now, see if we know that any exceptions via InstGen exist
+        Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+        for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+          Node f = fm->getAssertedQuantifier( i );
+          if( d_qe->getModel()->isQuantifierActive( f ) ){
+            int lems = doInstGen( fm, f );
+            d_statistics.d_inst_gen_lemmas += lems;
+            d_addedLemmas += lems;
+            //temporary
+            if( lems>0 ){
+              d_numQuantInstGen++;
+            }else if( hasInstGen( f ) ){
+              d_numQuantNoInstGen++;
+            }else{
+              d_numQuantNoSelForm++;
+            }
+            if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
+              break;
+            }
+          }else{
+            d_numQuantSat++;
+          }
+        }
+        Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
+        Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
+        Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
+        if( Trace.isOn("model-engine") ){
+          if( d_addedLemmas>0 ){
+            Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+          }else{
+            Trace("model-engine") << "No InstGen lemmas..." << std::endl;
+          }
+        }
+      }
+      //construct the model if necessary
+      if( d_addedLemmas==0 ){
+        //if no immediate exceptions, build the model
+        //  this model will be an approximation that will need to be tested via exhaustive instantiation
+        Trace("model-engine-debug") << "Building model..." << std::endl;
+        //build model for UF
+        for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+          Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
+          constructModelUf( fm, it->first );
+        }
+        Trace("model-engine-debug") << "Done building models." << std::endl;
+      }else{
+        return false;
+      }
+    }
+  }
+  //update models
+  for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+    it->second.update( fm );
+    Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
+    //construct function values
+    Node f_def = it->second.getFunctionValue( "$x" );
+    fm->assignFunctionDefinition( it->first, f_def );
+  }
+  Assert( d_addedLemmas==0 );
+  return TheoryEngineModelBuilder::processBuildModel( m );
+}
+
+int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
+{
+  if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
+    //create the basis match if necessary
+    if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
+      Trace("inst-fmf-init") << "Initialize " << f << std::endl;
+      //add the model basis instantiation
+      // This will help produce the necessary information for model completion.
+      // We do this by extending distinguish ground assertions (those
+      //   containing terms with "model basis" attribute) to hold for all cases.
+
+      ////first, check if any variables are required to be equal
+      //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
+      //    it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
+      //  Node n = it->first;
+      //  if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
+      //    Notice() << "Unhandled phase req: " << n << std::endl;
+      //  }
+      //}
+      d_quant_basis_match[f] = InstMatch( f );
+      for (unsigned j = 0; j < f[0].getNumChildren(); j++)
+      {
+        Node t = fm->getModelBasisTerm(f[0][j].getType());
+        //calculate the basis match for f
+        d_quant_basis_match[f].setValue( j, t );
+      }
+      ++(d_statistics.d_num_quants_init);
+    }
+    //try to add it
+    Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
+    //add model basis instantiation
+    if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f]))
+    {
+      d_quant_basis_match_added[f] = true;
+      return 1;
+    }else{
+      //shouldn't happen usually, but will occur if x != y is a required literal for f.
+      //Notice() << "No model basis for " << f << std::endl;
+      d_quant_basis_match_added[f] = false;
+    }
+  }
+  return 0;
+}
+
+void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
+  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
+  d_uf_model_constructed.clear();
+  //determine if any functions are constant
+  for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
+    Node op = it->first;
+    TermArgBasisTrie tabt;
+    std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
+    if( itut!=fmig->d_uf_terms.end() ){
+      for( size_t i=0; i<itut->second.size(); i++ ){
+        Node n = fmig->d_uf_terms[op][i];
+        //for calculating if op is constant
+        Node v = fmig->getRepresentative( n );
+        if( i==0 ){
+          d_uf_prefs[op].d_const_val = v;
+        }else if( v!=d_uf_prefs[op].d_const_val ){
+          d_uf_prefs[op].d_const_val = Node::null();
+          break;
+        }
+        //for calculating terms that we don't need to consider
+        //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
+        if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
+          //need to consider if it is not congruent modulo model basis
+          if( !tabt.addTerm( fmig, n ) ){
+            d_basisNoMatch[n] = true;
+          }
+        }
+      }
+    }
+    if( !d_uf_prefs[op].d_const_val.isNull() ){
+      fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
+      fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
+      Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
+      fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+      Debug("fmf-model-cons") << std::endl;
+      d_uf_model_constructed[op] = true;
+    }else{
+      d_uf_model_constructed[op] = false;
+    }
+  }
+}
+
+bool QModelBuilderIG::hasConstantDefinition( Node n ){
+  Node lit = n.getKind()==NOT ? n[0] : n;
+  if( lit.getKind()==APPLY_UF ){
+    Node op = lit.getOperator();
+    if( !d_uf_prefs[op].d_const_val.isNull() ){
+      return true;
+    }
+  }
+  return false;
+}
+
+QModelBuilderIG::Statistics::Statistics():
+  d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+  d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
+  d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
+  d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
+  d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
+  d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
+  d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
+  d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
+{
+  smtStatisticsRegistry()->registerStat(&d_num_quants_init);
+  smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
+  smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_eval_formulas);
+  smtStatisticsRegistry()->registerStat(&d_eval_uf_terms);
+  smtStatisticsRegistry()->registerStat(&d_eval_lits);
+  smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown);
+}
+
+QModelBuilderIG::Statistics::~Statistics(){
+  smtStatisticsRegistry()->unregisterStat(&d_num_quants_init);
+  smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
+  smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_eval_formulas);
+  smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms);
+  smtStatisticsRegistry()->unregisterStat(&d_eval_lits);
+  smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
+}
+
+//do exhaustive instantiation
+int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+  if( optUseModel() ){
+    QRepBoundExt qrbe(d_qe);
+    RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
+    if( riter.setQuantifier( f ) ){
+      FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
+      Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+      fmig->resetEvaluate();
+      Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+      EqualityQuery* qy = d_qe->getEqualityQuery();
+      Instantiate* inst = d_qe->getInstantiate();
+      TermUtil* util = d_qe->getTermUtil();
+      while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+        d_triedLemmas++;
+        if( Debug.isOn("inst-fmf-ei-debug") ){
+          for( int i=0; i<(int)riter.d_index.size(); i++ ){
+            Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl;
+          }
+        }
+        int eval = 0;
+        int depIndex;
+        //see if instantiation is already true in current model
+        if( Debug.isOn("fmf-model-eval") ){
+          Debug("fmf-model-eval") << "Evaluating ";
+          riter.debugPrintSmall("fmf-model-eval");
+          Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+        }
+        //if evaluate(...)==1, then the instantiation is already true in the model
+        //  depIndex is the index of the least significant variable that this evaluation relies upon
+        depIndex = riter.getNumTerms()-1;
+        Debug("fmf-model-eval") << "We will evaluate "
+                                << util->getInstConstantBody(f) << std::endl;
+        eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter);
+        if( eval==1 ){
+          Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+        }else{
+          Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+        }
+        if( eval==1 ){
+          //instantiation is already true -> skip
+          riter.incrementAtIndex(depIndex);
+        }else{
+          //instantiation was not shown to be true, construct the match
+          InstMatch m( f );
+          for (unsigned i = 0; i < riter.getNumTerms(); i++)
+          {
+            m.set(qy, i, riter.getCurrentTerm(i));
+          }
+          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+          //add as instantiation
+          if (inst->addInstantiation(f, m, true))
+          {
+            d_addedLemmas++;
+            if( d_qe->inConflict() ){
+              break;
+            }
+            //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+            if( eval==-1 ){
+              riter.incrementAtIndex(depIndex);
+            }else{
+              riter.increment();
+            }
+          }else{
+            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+            riter.increment();
+          }
+        }
+      }
+      //print debugging information
+      if( fmig ){
+        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
+        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
+        d_statistics.d_eval_lits += fmig->d_eval_lits;
+        d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
+      }
+      Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
+      Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
+      Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
+      if( d_addedLemmas>1000 ){
+        Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+        Trace("model-engine-warn") << "   Inst Tried: " << d_triedLemmas << std::endl;
+        Trace("model-engine-warn") << "   Inst Added: " << d_addedLemmas << std::endl;
+        Trace("model-engine-warn") << std::endl;
+      }
+    }
+    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    return riter.isIncomplete() ? -1 : 1;
+  }else{
+    return 0;
+  }
+}
+
+
+
+void QModelBuilderDefault::reset( FirstOrderModel* fm ){
+  d_quant_selection_lit.clear();
+  d_quant_selection_lit_candidates.clear();
+  d_quant_selection_lit_terms.clear();
+  d_term_selection_lit.clear();
+  d_op_selection_terms.clear();
+}
+
+
+int QModelBuilderDefault::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 QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+  if( d_qe->getModel()->isQuantifierActive( f ) ){
+    FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
+    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
+    if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
+      d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true );
+    }
+    int selectLitScore = -1;
+    for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
+      //the literal n is phase-required for quantifier f
+      Node n = it->first;
+      Node gn = fm->getModelBasis(f, n);
+      Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
+      bool value;
+      //if the corresponding ground abstraction literal has a SAT value
+      if( d_qe->getValuation().hasSatValue( gn, value ) ){
+        //collect the non-ground uf terms that this literal contains
+        //  and compute if all of the symbols in this literal have
+        //  constant definitions.
+        bool isConst = true;
+        std::vector< Node > uf_terms;
+        if( TermUtil::hasInstConstAttr(n) ){
+          isConst = false;
+          if( gn.getKind()==APPLY_UF ){
+            uf_terms.push_back( gn );
+            isConst = hasConstantDefinition( gn );
+          }else if( gn.getKind()==EQUAL ){
+            isConst = true;
+            for( int j=0; j<2; j++ ){
+              if( TermUtil::hasInstConstAttr(n[j]) ){
+                if( n[j].getKind()==APPLY_UF &&
+                    fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
+                  uf_terms.push_back( gn[j] );
+                  isConst = isConst && hasConstantDefinition( gn[j] );
+                }else{
+                  isConst = false;
+                }
+              }
+            }
+          }
+        }
+        //check if the value in the SAT solver matches the preference according to the quantifier
+        int pref = 0;
+        if( value!=it->second ){
+          //we have a possible selection literal
+          bool selectLit = d_quant_selection_lit[f].isNull();
+          bool selectLitConstraints = true;
+          //it is a constantly defined selection literal : the quantifier is sat
+          if( isConst ){
+            selectLit = selectLit || d_qe->getModel()->isQuantifierActive( f );
+            d_qe->getModel()->setQuantifierActive( f, false );
+            //check if choosing this literal would add any additional constraints to default definitions
+            selectLitConstraints = false;
+            for( int j=0; j<(int)uf_terms.size(); j++ ){
+              Node op = uf_terms[j].getOperator();
+              if( d_uf_prefs[op].d_reconsiderModel ){
+                selectLitConstraints = true;
+              }
+            }
+            if( !selectLitConstraints ){
+              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() );
+            if( !selectLitConstraints ){
+              break;
+            }
+          }
+          pref = 1;
+        }else{
+          pref = -1;
+        }
+        //if we are not yet SAT, so we will add to preferences
+        if( d_qe->getModel()->isQuantifierActive( f ) ){
+          Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
+          Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
+          for( int j=0; j<(int)uf_terms.size(); j++ ){
+            pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
+          }
+        }
+      }
+    }
+    //process information about selection literal for f
+    if( !d_quant_selection_lit[f].isNull() ){
+      d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
+      for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
+        d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
+        d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
+      }
+    }else{
+      Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
+    }
+    //process information about requirements and preferences of quantifier f
+    if( !d_qe->getModel()->isQuantifierActive( f ) ){
+      Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
+      for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
+        Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
+        d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
+      }
+      Debug("fmf-model-prefs") << std::endl;
+    }else{
+      //note quantifier's value preferences to models
+      for( int k=0; k<2; k++ ){
+        for( int j=0; j<(int)pro_con[k].size(); j++ ){
+          Node op = pro_con[k][j].getOperator();
+          Node r = fmig->getRepresentative( pro_con[k][j] );
+          d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+        }
+      }
+    }
+  }
+}
+
+int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
+  int addedLemmas = 0;
+  //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
+  //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+  //  effectively acting as partial instantiations instead of pointwise instantiations.
+  if( !d_quant_selection_lit[f].isNull() ){
+    Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
+    for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
+      bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
+      Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
+      Assert( TermUtil::hasInstConstAttr(lit) );
+      std::vector< Node > tr_terms;
+      if( lit.getKind()==APPLY_UF ){
+        //only match predicates that are contrary to this one, use literal matching
+        Node eq = NodeManager::currentNM()->mkNode(
+            EQUAL, lit, NodeManager::currentNM()->mkConst(!phase));
+        tr_terms.push_back( eq );
+      }else if( lit.getKind()==EQUAL ){
+        //collect trigger terms
+        for( int j=0; j<2; j++ ){
+          if( TermUtil::hasInstConstAttr(lit[j]) ){
+            if( lit[j].getKind()==APPLY_UF ){
+              tr_terms.push_back( lit[j] );
+            }else{
+              tr_terms.clear();
+              break;
+            }
+          }
+        }
+        if( tr_terms.size()==1 && !phase ){
+          //equality between a function and a ground term, use literal matching
+          tr_terms.clear();
+          tr_terms.push_back( lit );
+        }
+      }
+      //if applicable, try to add exceptions here
+      if( !tr_terms.empty() ){
+        //make a trigger for these terms, add instantiations
+        inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW );
+        //Notice() << "Trigger = " << (*tr) << std::endl;
+        tr->resetInstantiationRound();
+        tr->reset( Node::null() );
+        //d_qe->d_optInstMakeRepresentative = false;
+        //d_qe->d_optMatchIgnoreModelBasis = true;
+        addedLemmas += tr->addInstantiations();
+      }
+    }
+  }
+  return addedLemmas;
+}
+
+void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
+  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
+  if( optReconsiderFuncConstants() ){
+    //reconsider constant functions that weren't necessary
+    if( d_uf_model_constructed[op] ){
+      if( d_uf_prefs[op].d_reconsiderModel ){
+        //if we are allowed to reconsider default value, then see if the default value can be improved
+        Node v = d_uf_prefs[op].d_const_val;
+        if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
+          Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
+          fmig->d_uf_model_tree[op].clear();
+          fmig->d_uf_model_gen[op].clear();
+          d_uf_model_constructed[op] = false;
+        }
+      }
+    }
+  }
+  if( !d_uf_model_constructed[op] ){
+    //construct the model for the uninterpretted function/predicate
+    bool setDefaultVal = true;
+    Node defaultTerm = fmig->getModelBasisOpTerm(op);
+    Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
+    //set the values in the model
+    std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
+    if( itut!=fmig->d_uf_terms.end() ){
+      for( size_t i=0; i<itut->second.size(); i++ ){
+        Node n = itut->second[i];
+        // only consider unique up to congruence (in model equality engine)?
+        Node v = fmig->getRepresentative( n );
+        Trace("fmf-model-cons") << "Set term " << n << " : "
+                                << fmig->getRepSet()->getIndexFor(v) << " " << v
+                                << std::endl;
+        //if this assertion did not help the model, just consider it ground
+        //set n = v in the model tree
+        //set it as ground value
+        fmig->d_uf_model_gen[op].setValue( fm, n, v );
+        if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
+          //also set as default value if necessary
+          if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
+            Trace("fmf-model-cons") << "  Set as default." << std::endl;
+            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
+            if( n==defaultTerm ){
+              //incidentally already set, we will not need to find a default value
+              setDefaultVal = false;
+            }
+          }
+        }else{
+          if( n==defaultTerm ){
+            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
+            //incidentally already set, we will not need to find a default value
+            setDefaultVal = false;
+          }
+        }
+      }
+    }
+    //set the overall default value if not set already  (is this necessary??)
+    if( setDefaultVal ){
+      Trace("fmf-model-cons") << "  Choose default value..." << std::endl;
+      //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
+      Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
+      if( defaultVal.isNull() ){
+        if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
+        {
+          Node mbt = fmig->getModelBasisTerm(defaultTerm.getType());
+          fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
+              mbt);
+        }
+        defaultVal =
+            fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0);
+      }
+      Assert( !defaultVal.isNull() );
+      Trace("fmf-model-cons")
+          << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal)
+          << std::endl;
+      fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
+    }
+    Debug("fmf-model-cons") << "  Making model...";
+    fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
+    d_uf_model_constructed[op] = true;
+    Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
+  }
+}