merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

26 files changed, 1234 insertions, 1246 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 2b16c9af3..3a19ff9c6 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -25,20 +25,18 @@ libquantifiers_la_SOURCES = \
 	inst_match.cpp \
 	model_engine.h \
 	model_engine.cpp \
-	inst_when_mode.cpp \
-	inst_when_mode.h \
-	literal_match_mode.cpp \
-	literal_match_mode.h \
+	modes.cpp \
+	modes.h \
 	relevant_domain.h \
 	relevant_domain.cpp \
-	rep_set_iterator.h \
-	rep_set_iterator.cpp \
 	term_database.h \
 	term_database.cpp \
 	first_order_model.h \
 	first_order_model.cpp \
 	model_builder.h \
-	model_builder.cpp
+	model_builder.cpp \
+	quantifiers_attributes.h \
+	quantifiers_attributes.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index fd616948c..c3be1cdaf 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -15,9 +15,11 @@
  **/
 
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/rep_set_iterator.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+
+#define USE_INDEX_ORDERING
 
 using namespace std;
 using namespace CVC4;
@@ -26,39 +28,38 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ),
-d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){
+FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : DefaultModel( c, name, true ),
+d_axiom_asserted( c, false ), d_forall_asserts( c ){
 
 }
 
+void FirstOrderModel::assertQuantifier( Node n ){
+  d_forall_asserts.push_back( n );
+  if( n.getAttribute(AxiomAttribute()) ){
+    d_axiom_asserted = true;
+  }
+}
+
 void FirstOrderModel::reset(){
-  //rebuild models
-  d_uf_model_tree.clear();
-  d_uf_model_gen.clear();
-  d_array_model.clear();
   DefaultModel::reset();
 }
 
 void FirstOrderModel::addTerm( Node n ){
-  //std::vector< Node > added;
-  //d_term_db->addTerm( n, added, false );
   DefaultModel::addTerm( n );
 }
 
-void FirstOrderModel::initialize(){
+void FirstOrderModel::initialize( bool considerAxioms ){
+  //rebuild models
+  d_uf_model_tree.clear();
+  d_uf_model_gen.clear();
+  d_array_model.clear();
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
   for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
     Node f = getAssertedQuantifier( i );
-    //initialize relevant models within bodies of all quantifiers
-    initializeModelForTerm( f[1] );
-  }
-  //for debugging
-  if( Trace.isOn("model-engine") ){
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-      }
+    if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){
+      //initialize relevant models within bodies of all quantifiers
+      initializeModelForTerm( f[1] );
     }
   }
 }
@@ -92,33 +93,16 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
   }
 }
 
-void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){
-  /*
-  if( d_uf_model.find( n )!=d_uf_model.end() ){
-    //d_uf_model[n].toStream( out );
-    Node value = d_uf_model[n].getFunctionValue();
-    out << "(" << n << " " << value << ")";
-  }else if( d_array_model.find( n )!=d_array_model.end() ){
-    Node value = d_array_model[n].getArrayValue();
-    out << "(" << n << " " << value << ")" << std::endl;
-  }
-  */
-  DefaultModel::toStreamFunction( n, out );
-}
-
-void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){
-  DefaultModel::toStreamType( tn, out );
-}
-
 Node FirstOrderModel::getInterpretedValue( TNode n ){
   Debug("fo-model") << "get interpreted value " << n << std::endl;
   TypeNode type = n.getType();
   if( type.isFunction() || type.isPredicate() ){
-    if( d_uf_models.find( n )==d_uf_models.end() ){
-      //use the model tree to generate the model
-      Node fn = d_uf_model_tree[n].getFunctionValue();
-      d_uf_models[n] = fn;
-      return fn;
+    if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){
+      if( d_uf_models.find( n )==d_uf_models.end() ){
+        //use the model tree to generate the model
+        d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
+      }
+      return d_uf_models[n];
     }
   /*
   }else if( type.isArray() ){
@@ -141,44 +125,387 @@ Node FirstOrderModel::getInterpretedValue( TNode n ){
   return DefaultModel::getInterpretedValue( n );
 }
 
-TermDb* FirstOrderModel::getTermDatabase(){
-  return d_term_db;
+void FirstOrderModel::toStream(std::ostream& out){
+
 }
 
 
-void FirstOrderModel::toStream(std::ostream& out){
-  DefaultModel::toStream( out );
+//for evaluation of quantifier bodies
+
+void FirstOrderModel::resetEvaluate(){
+  d_eval_uf_use_default.clear();
+  d_eval_uf_model.clear();
+  d_eval_term_index_order.clear();
+  d_eval_failed.clear();
+  d_eval_failed_lits.clear();
+  d_eval_formulas = 0;
+  d_eval_uf_terms = 0;
+  d_eval_lits = 0;
+  d_eval_lits_unknown = 0;
+}
+
+//if evaluate( n ) = eVal,
+// let n' = ri * n be the formula n instantiated with the current values in r_iter
+// if eVal = 1, then n' is true, if eVal = -1, then n' is false,
+// if eVal = 0, then n' cannot be proven to be equal to phaseReq
+// if eVal is not 0, then
+//   each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
+int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
+  ++d_eval_formulas;
+  //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
+  //Notice() << "Eval " << n << std::endl;
+  if( n.getKind()==NOT ){
+    int val = evaluate( n[0], depIndex, ri );
+    return val==1 ? -1 : ( val==-1 ? 1 : 0 );
+  }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
+    int baseVal = n.getKind()==AND ? 1 : -1;
+    int eVal = baseVal;
+    int posDepIndex = ri->getNumTerms();
+    int negDepIndex = -1;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      //evaluate subterm
+      int childDepIndex;
+      Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
+      int eValT = evaluate( nn, childDepIndex, ri );
+      if( eValT==baseVal ){
+        if( eVal==baseVal ){
+          if( childDepIndex>negDepIndex ){
+            negDepIndex = childDepIndex;
+          }
+        }
+      }else if( eValT==-baseVal ){
+        eVal = -baseVal;
+        if( childDepIndex<posDepIndex ){
+          posDepIndex = childDepIndex;
+          if( posDepIndex==-1 ){
+            break;
+          }
+        }
+      }else if( eValT==0 ){
+        if( eVal==baseVal ){
+          eVal = 0;
+        }
+      }
+    }
+    if( eVal!=0 ){
+      depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
+      return eVal;
+    }else{
+      return 0;
+    }
+  }else if( n.getKind()==IFF || n.getKind()==XOR ){
+    int depIndex1;
+    int eVal = evaluate( n[0], depIndex1, ri );
+    if( eVal!=0 ){
+      int depIndex2;
+      int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2, ri );
+      if( eVal2!=0 ){
+        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+        return eVal==eVal2 ? 1 : -1;
+      }
+    }
+    return 0;
+  }else if( n.getKind()==ITE ){
+    int depIndex1, depIndex2;
+    int eVal = evaluate( n[0], depIndex1, ri );
+    if( eVal==0 ){
+      //evaluate children to see if they are the same value
+      int eval1 = evaluate( n[1], depIndex1, ri );
+      if( eval1!=0 ){
+        int eval2 = evaluate( n[1], depIndex2, ri );
+        if( eval1==eval2 ){
+          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+          return eval1;
+        }
+      }
+    }else{
+      int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2, ri );
+      depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+      return eValT;
+    }
+    return 0;
+  }else if( n.getKind()==FORALL ){
+    return 0;
+  }else{
+    ++d_eval_lits;
+    ////if we know we will fail again, immediately return
+    //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
+    //  if( d_eval_failed[n] ){
+    //    return -1;
+    //  }
+    //}
+    //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
+    int retVal = 0;
+    depIndex = ri->getNumTerms()-1;
+    Node val = evaluateTerm( n, depIndex, ri );
+    if( !val.isNull() ){
+      if( areEqual( val, d_true ) ){
+        retVal = 1;
+      }else if( areEqual( val, d_false ) ){
+        retVal = -1;
+      }else{
+        if( val.getKind()==EQUAL ){
+          if( areEqual( val[0], val[1] ) ){
+            retVal = 1;
+          }else if( areDisequal( val[0], val[1] ) ){
+            retVal = -1;
+          }
+        }
+      }
+    }
+    if( retVal!=0 ){
+      Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
+    }else{
+      ++d_eval_lits_unknown;
+      Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
+      Trace("fmf-eval-amb") << "   value : " << val << std::endl;
+      //std::cout << "Neither true nor false : " << n << std::endl;
+      //std::cout << "  Value : " << val << std::endl;
+      //for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      //  std::cout << "   " << i << " : " << n[i].getType() << std::endl;
+      //}
+    }
+    return retVal;
+  }
+}
+
+Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
+  //Message() << "Eval term " << n << std::endl;
+  if( !n.hasAttribute(InstConstantAttribute()) ){
+    //if evaluating a ground term, just consult the standard getValue functionality
+    depIndex = -1;
+    return getValue( n );
+  }else{
+    Node val;
+    depIndex = ri->getNumTerms()-1;
+    //check the type of n
+    if( n.getKind()==INST_CONSTANT ){
+      int v = n.getAttribute(InstVarNumAttribute());
+      depIndex = ri->d_var_order[ v ];
+      val = ri->getTerm( v );
+    }else if( n.getKind()==ITE ){
+      int depIndex1, depIndex2;
+      int eval = evaluate( n[0], depIndex1, ri );
+      if( eval==0 ){
+        //evaluate children to see if they are the same
+        Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri );
+        Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri );
+        if( val1==val2 ){
+          val = val1;
+          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+        }else{
+          return Node::null();
+        }
+      }else{
+        val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri );
+        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+      }
+    }else{
+      std::vector< int > children_depIndex;
+      //for select, pre-process read over writes
+      if( n.getKind()==SELECT ){
 #if 0
-  out << "---Current Model---" << std::endl;
-  out << "Representatives: " << std::endl;
-  d_rep_set.toStream( out );
-  out << "Functions: " << std::endl;
-  for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
-    it->second.toStream( out );
-    out << std::endl;
+        //std::cout << "Evaluate " << n << std::endl;
+        Node sel = evaluateTerm( n[1], depIndex, ri );
+        if( sel.isNull() ){
+          depIndex = ri->getNumTerms()-1;
+          return Node::null();
+        }
+        Node arr = getRepresentative( n[0] );
+        //if( n[0]!=getRepresentative( n[0] ) ){
+        //  std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl;
+        //}
+        int tempIndex;
+        int eval = 1;
+        while( arr.getKind()==STORE && eval!=0 ){
+          eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri );
+          depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+          if( eval==1 ){
+            val = evaluateTerm( arr[2], tempIndex, ri );
+            depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+            return val;
+          }else if( eval==-1 ){
+            arr = arr[0];
+          }
+        }
+        arr = evaluateTerm( arr, tempIndex, ri );
+        depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+        val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
+#else
+        val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
+#endif
+      }else{
+        //default term evaluate : evaluate all children, recreate the value
+        val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
+      }
+      if( !val.isNull() ){
+        bool setVal = false;
+        //custom ways of evaluating terms
+        if( n.getKind()==APPLY_UF ){
+          Node op = n.getOperator();
+          //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+          //if it is a defined UF, then consult the interpretation
+          if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
+            ++d_eval_uf_terms;
+            int argDepIndex = 0;
+            //make the term model specifically for n
+            makeEvalUfModel( n );
+            //now, consult the model
+            if( d_eval_uf_use_default[n] ){
+              val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex );
+            }else{
+              val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex );
+            }
+            //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+            //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
+            Assert( !val.isNull() );
+            //recalculate the depIndex
+            depIndex = -1;
+            for( int i=0; i<argDepIndex; i++ ){
+              int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
+              Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
+              if( children_depIndex[index]>depIndex ){
+                depIndex = children_depIndex[index];
+              }
+            }
+            setVal = true;
+          }
+        }else if( n.getKind()==SELECT ){
+          //we are free to interpret this term however we want
+        }
+        //if not set already, rewrite and consult model for interpretation
+        if( !setVal ){
+          val = Rewriter::rewrite( val );
+          if( val.getMetaKind()!=kind::metakind::CONSTANT ){
+            //FIXME: we cannot do this until we trust all theories collectModelInfo!
+            //val = getInterpretedValue( val );
+            //val = getRepresentative( val );
+          }
+        }
+        Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
+        printRepresentativeDebug( "fmf-eval-debug", val );
+        Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
+      }
+    }
+    return val;
+  }
+}
+
+Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
+  depIndex = -1;
+  if( n.getNumChildren()==0 ){
+    return n;
+  }else{
+    //first we must evaluate the arguments
+    std::vector< Node > children;
+    if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
+      children.push_back( n.getOperator() );
+    }
+    //for each argument, calculate its value, and the variables its value depends upon
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      childDepIndex.push_back( -1 );
+      Node nn = evaluateTerm( n[i], childDepIndex[i], ri );
+      if( nn.isNull() ){
+        depIndex = ri->getNumTerms()-1;
+        return nn;
+      }else{
+        children.push_back( nn );
+        if( childDepIndex[i]>depIndex ){
+          depIndex = childDepIndex[i];
+        }
+      }
+    }
+    //recreate the value
+    Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );
+    return val;
+  }
+}
+
+void FirstOrderModel::clearEvalFailed( int index ){
+  for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
+    d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
+  }
+  d_eval_failed_lits[index].clear();
+}
+
+void FirstOrderModel::makeEvalUfModel( Node n ){
+  if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
+    makeEvalUfIndexOrder( n );
+    if( !d_eval_uf_use_default[n] ){
+      Node op = n.getOperator();
+      d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
+      d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] );
+      //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
+      //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
+    }
   }
-#elif 0
-  d_rep_set.toStream( out );
-  //print everything not related to UF in equality engine
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    Node rep = getRepresentative( eqc );
-    TypeNode type = rep.getType();
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      //do not print things that have interpretations in model
-      if( !(*eqc_i).isConst() && !hasInterpretedValue( *eqc_i ) ){
-        out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;
+}
+
+struct sortGetMaxVariableNum {
+  std::map< Node, int > d_max_var_num;
+  int computeMaxVariableNum( Node n ){
+    if( n.getKind()==INST_CONSTANT ){
+      return n.getAttribute(InstVarNumAttribute());
+    }else if( n.hasAttribute(InstConstantAttribute()) ){
+      int maxVal = -1;
+      for( int i=0; i<(int)n.getNumChildren(); i++ ){
+        int val = getMaxVariableNum( n[i] );
+        if( val>maxVal ){
+          maxVal = val;
+        }
       }
-      ++eqc_i;
+      return maxVal;
+    }else{
+      return -1;
     }
-    ++eqcs_i;
   }
-  //print functions
-  for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
-    it->second.toStream( out );
-    out << std::endl;
+  int getMaxVariableNum( Node n ){
+    std::map< Node, int >::iterator it = d_max_var_num.find( n );
+    if( it==d_max_var_num.end() ){
+      int num = computeMaxVariableNum( n );
+      d_max_var_num[n] = num;
+      return num;
+    }else{
+      return it->second;
+    }
   }
+  bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
+};
+
+void FirstOrderModel::makeEvalUfIndexOrder( Node n ){
+  if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
+#ifdef USE_INDEX_ORDERING
+    //sort arguments in order of least significant vs. most significant variable in default ordering
+    std::map< Node, std::vector< int > > argIndex;
+    std::vector< Node > args;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( argIndex.find( n[i] )==argIndex.end() ){
+        args.push_back( n[i] );
+      }
+      argIndex[n[i]].push_back( i );
+    }
+    sortGetMaxVariableNum sgmvn;
+    std::sort( args.begin(), args.end(), sgmvn );
+    for( int i=0; i<(int)args.size(); i++ ){
+      for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
+        d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
+      }
+    }
+    bool useDefault = true;
+    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
+      if( i!=d_eval_term_index_order[n][i] ){
+        useDefault = false;
+        break;
+      }
+    }
+    d_eval_uf_use_default[n] = useDefault;
+    Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
+    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
+      Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
+    }
+    Debug("fmf-index-order") << std::endl;
+#else
+    d_eval_uf_use_default[n] = true;
 #endif
+  }
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 8ad911452..e66bf8040 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -42,32 +42,41 @@ class TermDb;
 class FirstOrderModel : public DefaultModel
 {
 private:
-  //pointer to term database
-  TermDb* d_term_db;
   //add term function
   void addTerm( Node n );
   //for initialize model
   void initializeModelForTerm( Node n );
-  /** to stream functions */
-  void toStreamFunction( Node n, std::ostream& out );
-  void toStreamType( TypeNode tn, std::ostream& out );
+  /** whether an axiom is asserted */
+  context::CDO< bool > d_axiom_asserted;
+  /** list of quantifiers asserted in the current context */
+  context::CDList<Node> d_forall_asserts;
 public: //for Theory UF:
   //models for each UF operator
   std::map< Node, uf::UfModelTree > d_uf_model_tree;
   //model generators
   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
+private:
+  //map from terms to the models used to calculate their value
+  std::map< Node, bool > d_eval_uf_use_default;
+  std::map< Node, uf::UfModelTree > d_eval_uf_model;
+  void makeEvalUfModel( Node n );
+  //index ordering to use for each term
+  std::map< Node, std::vector< int > > d_eval_term_index_order;
+  void makeEvalUfIndexOrder( Node n );
 public: //for Theory Arrays:
   //default value for each non-store array
   std::map< Node, arrays::ArrayModel > d_array_model;
 public: //for Theory Quantifiers:
-  /** list of quantifiers asserted in the current context */
-  context::CDList<Node> d_forall_asserts;
+  /** assert quantifier */
+  void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
   /** get asserted quantifier */
   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+  /** bool axiom asserted */
+  bool isAxiomAsserted() { return d_axiom_asserted; }
 public:
-  FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
+  FirstOrderModel( context::Context* c, std::string name );
   virtual ~FirstOrderModel(){}
   // reset the model
   void reset();
@@ -75,11 +84,30 @@ public:
   Node getInterpretedValue( TNode n );
 public:
   // initialize the model
-  void initialize();
-  /** get term database */
-  TermDb* getTermDatabase();
+  void initialize( bool considerAxioms = true );
   /** to stream function */
   void toStream( std::ostream& out );
+
+//the following functions are for evaluating quantifier bodies
+public:
+  /** reset evaluation */
+  void resetEvaluate();
+  /** evaluate functions */
+  int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
+  Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
+public:
+  //statistics
+  int d_eval_formulas;
+  int d_eval_uf_terms;
+  int d_eval_lits;
+  int d_eval_lits_unknown;
+private:
+  //default evaluate term function
+  Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
+  //temporary storing which literals have failed
+  void clearEvalFailed( int index );
+  std::map< Node, bool > d_eval_failed;
+  std::map< int, std::vector< Node > > d_eval_failed_lits;
 };/* class FirstOrderModel */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index ce35607d4..d2083ef3d 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -148,7 +148,9 @@ void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >
 }
 void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){
   for( int i=0; i<(int)vars.size(); i++ ){
-    match.push_back( d_map[ vars[i] ] );
+    if( d_map.find( vars[i] )!=d_map.end() && !d_map[ vars[i] ].isNull() ){
+      match.push_back( d_map[ vars[i] ] );
+    }
   }
 }
 
@@ -177,7 +179,7 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m
     }
     if( modEq ){
       //check modulo equality if any other instantiation match exists
-      if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
                                  qe->getEqualityQuery()->getEngine() );
         while( !eqc.isFinished() ){
@@ -193,13 +195,6 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m
           ++eqc;
         }
       }
-      //for( std::map< Node, InstMatchTrie >::iterator itc = d_data.begin(); itc != d_data.end(); ++itc ){
-      //  if( itc->first!=n && qe->getEqualityQuery()->areEqual( n, itc->first ) ){
-      //    if( itc->second.existsInstMatch( qe, f, m, modEq, index+1 ) ){
-      //      return true;
-      //    }
-      //  }
-      //}
     }
     return false;
   }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 0fa4fad12..727f568c5 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -386,3 +386,16 @@ void InstantiationEngine::propagate( Theory::Effort level ){
     }
   }
 }
+
+Node InstantiationEngine::getNextDecisionRequest(){
+  //propagate as decision all counterexample literals that are not asserted
+  for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){
+    bool value;
+    if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){
+      //if not already set, propagate as decision
+      Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl;
+      return it->second;
+    }
+  }
+  return Node::null();
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 37ee6d801..19dac736c 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -66,6 +66,7 @@ public:
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
   void propagate( Theory::Effort level );
+  Node getNextDecisionRequest();
 public:
   /** get the corresponding counterexample literal for quantified formula node n */
   Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; }
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 106d95cef..c81816528 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -8,7 +8,7 @@ theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory
 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
 instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h"
 
-properties check propagate presolve
+properties check propagate presolve getNextDecisionRequest
 
 rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
 
@@ -30,6 +30,9 @@ sort INST_PATTERN_TYPE \
     not-well-founded \
     "Instantiation pattern type"
 
+# Instantiation pattern, also called trigger.
+# This node is used for specifying hints for quantifier instantiation.
+# An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger.
 operator INST_PATTERN 1: "instantiation pattern"
 
 sort INST_PATTERN_LIST_TYPE \
@@ -37,6 +40,7 @@ sort INST_PATTERN_LIST_TYPE \
     not-well-founded \
     "Instantiation pattern list type"
 
+# a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "instantiation pattern list"
 
 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
diff --git a/src/theory/quantifiers/literal_match_mode.cpp b/src/theory/quantifiers/literal_match_mode.cpp
deleted file mode 100644
index 87b4b94fe..000000000
--- a/src/theory/quantifiers/literal_match_mode.cpp
+++ /dev/null
@@ -1,43 +0,0 @@
-/*********************                                                        */
-/*! \file literal_match_mode.cpp
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include <iostream>
-#include "theory/quantifiers/literal_match_mode.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) {
-  switch(mode) {
-  case theory::quantifiers::LITERAL_MATCH_NONE:
-    out << "LITERAL_MATCH_NONE";
-    break;
-  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
-    out << "LITERAL_MATCH_PREDICATE";
-    break;
-  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
-    out << "LITERAL_MATCH_EQUALITY";
-    break;
-  default:
-    out << "LiteralMatchMode!UNKNOWN";
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/literal_match_mode.h b/src/theory/quantifiers/literal_match_mode.h
deleted file mode 100644
index 189f0a235..000000000
--- a/src/theory/quantifiers/literal_match_mode.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*********************                                                        */
-/*! \file literal_match_mode.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H
-#define __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H
-
-#include <iostream>
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-typedef enum {
-  /** Do not consider polarity of patterns */
-  LITERAL_MATCH_NONE,
-  /** Consider polarity of boolean predicates only */
-  LITERAL_MATCH_PREDICATE,
-  /** Consider polarity of boolean predicates, as well as equalities */
-  LITERAL_MATCH_EQUALITY,
-} LiteralMatchMode;
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 5d49c914f..c09346f35 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -20,15 +20,14 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_model.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/model_builder.h"
-
-//#define ME_PRINT_WARNINGS
+#include "theory/quantifiers/quantifiers_attributes.h"
 
 #define RECONSIDER_FUNC_CONSTANT
-//#define ONE_QUANT_PER_ROUND_INST_GEN
 
 using namespace std;
 using namespace CVC4;
@@ -37,78 +36,95 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
+ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) :
 TheoryEngineModelBuilder( qe->getTheoryEngine() ),
-d_qe( qe ){
-
+d_qe( qe ), d_curr_model( c, NULL ){
+  d_considerAxioms = true;
 }
 
-Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){
-  Assert( m->d_equalityEngine.hasTerm( eqc ) );
-  Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc );
-  //avoid interpreted symbols
-  if( isBadRepresentative( eqc ) ){
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      if( !isBadRepresentative( *eqc_i ) ){
-        return *eqc_i;
+Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
+  if( fullModel ){
+    return TheoryEngineModelBuilder::chooseRepresentative( m, eqc, fullModel );
+  }else{
+    Assert( m->d_equalityEngine.hasTerm( eqc ) );
+    Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc );
+    //avoid bad representatives
+    if( isBadRepresentative( eqc ) ){
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine );
+      while( !eqc_i.isFinished() ){
+        if( !isBadRepresentative( *eqc_i ) ){
+          return *eqc_i;
+        }
+        ++eqc_i;
       }
-      ++eqc_i;
+      //otherwise, make new value?
+      //Message() << "Warning: Bad rep " << eqc << std::endl;
     }
-    //otherwise, make new value?
-    //Message() << "Warning: Bad rep " << eqc << std::endl;
+    return eqc;
   }
-  return eqc;
 }
 
 bool ModelEngineBuilder::isBadRepresentative( Node n ){
+  //avoid interpreted symbols
   return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR;
 }
 
-void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
-  d_addedLemmas = 0;
-  //only construct first order model if optUseModel() is true
-  if( optUseModel() ){
-    FirstOrderModel* fm = (FirstOrderModel*)m;
-    //initialize model
-    fm->initialize();
-    //analyze the functions
-    analyzeModel( fm );
-    //analyze the quantifiers
-    Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
-    analyzeQuantifiers( fm );
-    //if applicable, find exceptions
-    if( optInstGen() ){
-      //now, see if we know that any exceptions via InstGen exist
-      Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node f = fm->getAssertedQuantifier( i );
-        if( d_quant_sat.find( f )==d_quant_sat.end() ){
-          d_addedLemmas += doInstGen( fm, f );
-          if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
-            break;
+void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
+  FirstOrderModel* fm = (FirstOrderModel*)m;
+  if( fullModel ){
+    Assert( d_curr_model==fm );
+    //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 );
+    }
+
+  }else{
+    d_curr_model = fm;
+    //build model for relevant symbols contained in quantified formulas
+    d_addedLemmas = 0;
+    //only construct first order model if optUseModel() is true
+    if( optUseModel() ){
+      //initialize model
+      fm->initialize( d_considerAxioms );
+      //analyze the functions
+      Trace("model-engine-debug") << "Analyzing model..." << std::endl;
+      analyzeModel( fm );
+      //analyze the quantifiers
+      Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
+      analyzeQuantifiers( fm );
+      //if applicable, find exceptions
+      if( optInstGen() ){
+        //now, see if we know that any exceptions via InstGen exist
+        Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+        for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+          Node f = fm->getAssertedQuantifier( i );
+          if( isQuantifierActive( f ) ){
+            d_addedLemmas += doInstGen( fm, f );
+            if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
+              break;
+            }
           }
         }
-      }
-      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;
+        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;
+          }
         }
       }
-      Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
-    }
-    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
-      Debug("fmf-model-debug") << "Building model..." << std::endl;
-      finishBuildModel( fm );
+      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;
+        constructModel( fm );
+      }
     }
   }
 }
 
 void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
+  d_uf_model_constructed.clear();
   //determine if any functions are constant
   for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
     Node op = it->first;
@@ -138,108 +154,138 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
 }
 
 void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
-  d_quant_selection_lits.clear();
   d_quant_sat.clear();
+  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();
   d_uf_prefs.clear();
   int quantSatInit = 0;
   int nquantSatInit = 0;
   //analyze the preferences of each quantifier
   for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
     Node f = fm->getAssertedQuantifier( i );
-    Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
-    std::vector< Node > pro_con[2];
-    std::vector< Node > constantSatOps;
-    bool constantSatReconsider;
-    //for each asserted quantifier f,
-    // - determine which literals form model basis for each quantifier
-    // - check which function/predicates have good and bad definitions according to f
-    for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
-         it != d_qe->d_phase_reqs[f].end(); ++it ){
-      Node n = it->first;
-      Node gn = d_qe->getTermDatabase()->getModelBasis( n );
-      Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
-      //calculate preference
-      int pref = 0;
-      bool value;
-      if( d_qe->getValuation().hasSatValue( gn, value ) ){
-        if( value!=it->second ){
-          //store this literal as a model basis literal
-          //  this literal will force a default values in model that (modulo exceptions) shows
-          //  that f is satisfied by the model
-          d_quant_selection_lits[f].push_back( value ? n : n.notNode() );
-          pref = 1;
-        }else{
-          pref = -1;
-        }
-      }
-      if( pref!=0 ){
-        //Store preferences for UF
-        bool isConst = !n.hasAttribute(InstConstantAttribute());
-        std::vector< Node > uf_terms;
-        if( gn.getKind()==APPLY_UF ){
-          uf_terms.push_back( gn );
-          isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
-        }else if( gn.getKind()==EQUAL ){
-          isConst = true;
-          for( int j=0; j<2; j++ ){
-            if( n[j].hasAttribute(InstConstantAttribute()) ){
-              if( n[j].getKind()==APPLY_UF ){
-                Node op = gn[j].getOperator();
-                if( fm->d_uf_model_tree.find( op )!=fm->d_uf_model_tree.end() ){
-                  uf_terms.push_back( gn[j] );
-                  isConst = isConst && !d_uf_prefs[op].d_const_val.isNull();
-                }else{
-                  isConst = false;
+    if( isQuantifierActive( 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;
+      //for each asserted quantifier f,
+      // - determine selection literals
+      // - check which function/predicates have good and bad definitions for satisfying f
+      for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
+           it != d_qe->d_phase_reqs[f].end(); ++it ){
+        //the literal n is phase-required for quantifier f
+        Node n = it->first;
+        Node gn = d_qe->getTermDatabase()->getModelBasis( 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( n.hasAttribute(InstConstantAttribute()) ){
+            isConst = false;
+            if( gn.getKind()==APPLY_UF ){
+              uf_terms.push_back( gn );
+              isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
+            }else if( gn.getKind()==EQUAL ){
+              isConst = true;
+              for( int j=0; j<2; j++ ){
+                if( n[j].hasAttribute(InstConstantAttribute()) ){
+                  if( n[j].getKind()==APPLY_UF &&
+                      fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
+                    uf_terms.push_back( gn[j] );
+                    isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull();
+                  }else{
+                    isConst = false;
+                  }
                 }
-              }else{
-                isConst = false;
               }
             }
           }
-        }
-        Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
-        Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
-        if( pref==1 && isConst ){
-          d_quant_sat[f] = true;
-          //instead, just note to the model for each uf term that f is pro its definition
-          constantSatReconsider = false;
-          constantSatOps.clear();
-          for( int j=0; j<(int)uf_terms.size(); j++ ){
-            Node op = uf_terms[j].getOperator();
-            constantSatOps.push_back( op );
-            if( d_uf_prefs[op].d_reconsiderModel ){
-              constantSatReconsider = true;
+          //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_quant_sat.find( f )==d_quant_sat.end();
+              d_quant_sat[f] = true;
+              //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;
+              }
             }
+            //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 ){
+              Trace("inst-gen-debug") << "Choose selection literal " << gn << 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( !constantSatReconsider ){
-            break;
-          }
-        }else{
-          int pcIndex = pref==1 ? 0 : 1;
-          for( int j=0; j<(int)uf_terms.size(); j++ ){
-            pro_con[pcIndex].push_back( uf_terms[j] );
+          //if we are not yet SAT, so we will add to preferences
+          if( d_quant_sat.find( f )==d_quant_sat.end() ){
+            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] );
+            }
           }
         }
       }
-    }
-    if( d_quant_sat.find( f )!=d_quant_sat.end() ){
-      Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
-      for( int i=0; i<(int)constantSatOps.size(); i++ ){
-        Debug("fmf-model-prefs") << constantSatOps[i] << " ";
-        d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false;
+      //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 (is the body of f clausified?)" << std::endl;
       }
-      Debug("fmf-model-prefs") << std::endl;
-      quantSatInit++;
-      d_statistics.d_pre_sat_quant += quantSatInit;
-    }else{
-      nquantSatInit++;
-      d_statistics.d_pre_nsat_quant += quantSatInit;
-      //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 = fm->getRepresentative( pro_con[k][j] );
-          d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+      //process information about requirements and preferences of quantifier f
+      if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+        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;
+        quantSatInit++;
+        ++(d_statistics.d_pre_sat_quant);
+      }else{
+        nquantSatInit++;
+        ++(d_statistics.d_pre_nsat_quant);
+        //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 = fm->getRepresentative( pro_con[k][j] );
+            d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+          }
         }
       }
     }
@@ -248,58 +294,87 @@ void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
 }
 
 int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
-  //we wish to add all known exceptions to our model basis literal(s)
-  //  this will help to refine our current model.
+  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.
-  int addedLemmas = 0;
-  for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){
-    bool phase = d_quant_selection_lits[f][i].getKind()!=NOT;
-    Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i];
+  if( !d_quant_selection_lit[f].isNull() ){
+#if 0
+    bool phase = d_quant_selection_lit[f].getKind()!=NOT;
+    Node lit = d_quant_selection_lit[f].getKind()==NOT ? d_quant_selection_lit[f][0] : d_quant_selection_lit[f];
     Assert( lit.hasAttribute(InstConstantAttribute()) );
-    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( IFF, lit, !phase ? fm->d_true : fm->d_false );
-      fm->getTermDatabase()->setInstantiationConstantAttr( eq, f );
-      tr_terms.push_back( eq );
-    }else if( lit.getKind()==EQUAL ){
-      //collect trigger terms
-      for( int j=0; j<2; j++ ){
-        if( lit[j].hasAttribute(InstConstantAttribute()) ){
-          if( lit[j].getKind()==APPLY_UF ){
-            tr_terms.push_back( lit[j] );
-          }else{
-            tr_terms.clear();
-            break;
-          }
+    for( size_t i=0; i<d_quant_selection_lit_terms[f].size(); i++ ){
+      Node n1 = d_quant_selection_lit_terms[f][i];
+      Node op = d_quant_selection_lit_terms[f][i].getOperator();
+      //check all other selection literals involving "op"
+      for( size_t i=0; i<d_op_selection_terms[op].size(); i++ ){
+        Node n2 = d_op_selection_terms[op][i];
+        Node n2_lit = d_term_selection_lit[ n2 ];
+        if( n2_lit!=d_quant_selection_lit[f] ){
+          //match n1 and n2
         }
       }
-      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( addedLemmas==0 ){
+        //check all ground terms involving "op"
+        for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+          Node n2 = fm->d_uf_terms[op][i];
+          if( n1!=n2 ){
+            //match n1 and n2
+          }
+        }
       }
     }
-    //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 );
-      //Notice() << "Trigger = " << (*tr) << std::endl;
-      tr->resetInstantiationRound();
-      tr->reset( Node::null() );
-      //d_qe->d_optInstMakeRepresentative = false;
-      //d_qe->d_optMatchIgnoreModelBasis = true;
-      addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
+#else
+    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( lit.hasAttribute(InstConstantAttribute()) );
+      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( IFF, lit, !phase ? fm->d_true : fm->d_false );
+        d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
+        tr_terms.push_back( eq );
+      }else if( lit.getKind()==EQUAL ){
+        //collect trigger terms
+        for( int j=0; j<2; j++ ){
+          if( lit[j].hasAttribute(InstConstantAttribute()) ){
+            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 );
+        //Notice() << "Trigger = " << (*tr) << std::endl;
+        tr->resetInstantiationRound();
+        tr->reset( Node::null() );
+        //d_qe->d_optInstMakeRepresentative = false;
+        //d_qe->d_optMatchIgnoreModelBasis = true;
+        addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
+      }
     }
+#endif
   }
   return addedLemmas;
 }
 
-void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
+void ModelEngineBuilder::constructModel( FirstOrderModel* fm ){
   //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 ){
-    finishBuildModelUf( fm, it->first );
+    constructModelUf( fm, it->first );
   }
   /*
   //build model for arrays
@@ -311,10 +386,10 @@ void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
     it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) );
   }
   */
-  Debug("fmf-model-debug") << "Done building models." << std::endl;
+  Trace("model-engine-debug") << "Done building models." << std::endl;
 }
 
-void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){
+void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){
 #ifdef RECONSIDER_FUNC_CONSTANT
   if( d_uf_model_constructed[op] ){
     if( d_uf_prefs[op].d_reconsiderModel ){
@@ -337,7 +412,7 @@ void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){
     //set the values in the model
     for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
       Node n = fm->d_uf_terms[op][i];
-      fm->getTermDatabase()->computeModelBasisArgAttribute( n );
+      d_qe->getTermDatabase()->computeModelBasisArgAttribute( n );
       if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
         Node v = fm->getRepresentative( n );
         //if this assertion did not help the model, just consider it ground
@@ -381,12 +456,6 @@ void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){
   }
 }
 
-void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){
-  for( std::map< Node, Node >::iterator it = m->d_reps.begin(); it != m->d_reps.end(); ++it ){
-    //build proper representatives (TODO)
-  }
-}
-
 bool ModelEngineBuilder::optUseModel() {
   return options::fmfModelBasedInst();
 }
@@ -396,11 +465,11 @@ bool ModelEngineBuilder::optInstGen(){
 }
 
 bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
-#ifdef ONE_QUANT_PER_ROUND_INST_GEN
-  return true;
-#else
-  return false;
-#endif
+  return options::fmfInstGenOneQuantPerRound();
+}
+
+void ModelEngineBuilder::setEffort( int effort ){
+  d_considerAxioms = effort>=1;
 }
 
 ModelEngineBuilder::Statistics::Statistics():
@@ -415,3 +484,7 @@ ModelEngineBuilder::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
   StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
 }
+
+bool ModelEngineBuilder::isQuantifierActive( Node f ){
+  return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && 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 344b731e0..1366a7650 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -27,20 +27,29 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-//the model builder
+/** model builder class
+  *  This class is capable of building candidate models based on the current quantified formulas
+  *  that are asserted.  Use:
+  *  (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel
+  *  (2) if candidate model is determined to be a real model,
+           then call ModelEngineBuilder::buildModel( m, true );
+  */
 class ModelEngineBuilder : public TheoryEngineModelBuilder
 {
 protected:
   //quantifiers engine
   QuantifiersEngine* d_qe;
+  //the model we are working with
+  context::CDO< FirstOrderModel* > d_curr_model;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
   //built model uf
   std::map< Node, bool > d_uf_model_constructed;
+protected:
   /** process build model */
-  void processBuildModel( TheoryModel* m );
+  void processBuildModel( TheoryModel* m, bool fullModel );
   /** choose representative for unconstrained equivalence class */
-  Node chooseRepresentative( TheoryModel* m, Node eqc );
+  Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
   /** bad representative */
   bool isBadRepresentative( Node n );
 protected:
@@ -49,23 +58,30 @@ protected:
   //analyze quantifiers
   void analyzeQuantifiers( FirstOrderModel* fm );
   //build model
-  void finishBuildModel( FirstOrderModel* fm );
+  void constructModel( FirstOrderModel* fm );
   //theory-specific build models
-  void finishBuildModelUf( FirstOrderModel* fm, Node op );
+  void constructModelUf( FirstOrderModel* fm, Node op );
   //do InstGen techniques for quantifier, return number of lemmas produced
   int doInstGen( FirstOrderModel* fm, Node f );
 public:
-  ModelEngineBuilder( QuantifiersEngine* qe );
+  ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~ModelEngineBuilder(){}
-  /** finish model */
-  void finishProcessBuildModel( TheoryModel* m );
-public:
   /** number of lemmas generated while building model */
   int d_addedLemmas;
+  //consider axioms
+  bool d_considerAxioms;
+private:    ///information for InstGen
   //map from quantifiers to if are constant SAT
   std::map< Node, bool > d_quant_sat;
-  //map from quantifiers to the instantiation literals that their model is dependent upon
-  std::map< Node, std::vector< Node > > d_quant_selection_lits;
+  //map from quantifiers to their selection literals
+  std::map< Node, Node > d_quant_selection_lit;
+  std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
+  //map from quantifiers to their selection literal terms
+  std::map< Node, std::vector< Node > > d_quant_selection_lit_terms;
+  //map from terms to the selection literals they exist in
+  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;
 public:
   //map from quantifiers to model basis match
   std::map< Node, InstMatch > d_quant_basis_match;
@@ -73,6 +89,8 @@ public:
   bool optUseModel();
   bool optInstGen();
   bool optOneQuantPerRoundInstGen();
+  // set effort
+  void setEffort( int effort );
   /** statistics class */
   class Statistics {
   public:
@@ -82,6 +100,8 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
+  // is quantifier active?
+  bool isQuantifierActive( Node f );
 };/* class ModelEngineBuilder */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index cbeeed8d0..b5a9ee74c 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -15,7 +15,6 @@
  **/
 
 #include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/rep_set_iterator.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -25,11 +24,11 @@
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 
 //#define ME_PRINT_WARNINGS
 
 #define EVAL_FAIL_SKIP_MULTIPLE
-//#define ONE_QUANT_PER_ROUND
 
 using namespace std;
 using namespace CVC4;
@@ -40,96 +39,97 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 //Model Engine constructor
-ModelEngine::ModelEngine( QuantifiersEngine* qe ) :
+ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ),
-d_builder( qe ),
-d_rel_domain( qe->getModel() ){
+d_builder( c, qe ),
+d_rel_domain( qe, qe->getModel() ){
 
 }
 
 void ModelEngine::check( Theory::Effort e ){
   if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
-    //first, check if we can minimize the model further
-    if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
-      return;
-    }
+    FirstOrderModel* fm = d_quantEngine->getModel();
     //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
     int addedLemmas = 0;
+    Trace("model-engine") << "---Model Engine Round---" << std::endl;
     if( d_builder.optUseModel() ){
       //check if any quantifiers are un-initialized
-      for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-        Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node f = fm->getAssertedQuantifier( i );
         addedLemmas += initializeQuantifier( f );
       }
     }
-    if( addedLemmas==0 ){
-      //quantifiers are initialized, we begin an instantiation round
-      double clSet = 0;
-      if( Trace.isOn("model-engine") ){
-        clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("model-engine") << "---Model Engine Round---" << std::endl;
-      }
-      Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl;
-      ++(d_statistics.d_inst_rounds);
-      //reset the quantifiers engine
-      d_quantEngine->resetInstantiationRound( e );
-      //initialize the model
-      Debug("fmf-model-debug") << "Build model..." << std::endl;
-      d_builder.buildModel( d_quantEngine->getModel() );
-      d_quantEngine->d_model_set = true;
-      //if builder has lemmas, add and return
-      if( d_builder.d_addedLemmas>0 ){
-        addedLemmas += (int)d_builder.d_addedLemmas;
-      }else{
-        //print debug
-        Debug("fmf-model-complete") << std::endl;
-        debugPrint("fmf-model-complete");
-        //verify we are SAT by trying exhaustive instantiation
-        if( optUseRelevantDomain() ){
-          d_rel_domain.compute();
+    if( addedLemmas>0 ){
+      Trace("model-engine") << "Initialize, Added Lemmas = " << addedLemmas << std::endl;
+    }
+    //two effort levels: first try exhaustive instantiation without axioms, then with.
+    int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
+    for( int effort=startEffort; effort<2; effort++ ){
+      // for effort = 0, we only instantiate non-axioms
+      // for effort = 1, we instantiate everything
+      if( addedLemmas==0 ){
+        //quantifiers are initialized, we begin an instantiation round
+        double clSet = 0;
+        if( Trace.isOn("model-engine") ){
+          clSet = double(clock())/double(CLOCKS_PER_SEC);
         }
-        d_triedLemmas = 0;
-        d_testLemmas = 0;
-        d_relevantLemmas = 0;
-        d_totalLemmas = 0;
-        Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
-        for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-          Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-          if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){
-            addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
-            if( optOneQuantPerRound() && addedLemmas>0 ){
-              break;
-            }
-          }
-#ifdef ME_PRINT_WARNINGS
-          if( addedLemmas>10000 ){
-            break;
+        ++(d_statistics.d_inst_rounds);
+        //reset the quantifiers engine
+        d_quantEngine->resetInstantiationRound( e );
+        //initialize the model
+        Trace("model-engine-debug") << "Build model..." << std::endl;
+        d_builder.setEffort( effort );
+        d_builder.buildModel( fm, false );
+        //if builder has lemmas, add and return
+        if( d_builder.d_addedLemmas>0 ){
+          addedLemmas += (int)d_builder.d_addedLemmas;
+        }else{
+          Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
+          //let the strong solver verify that the model is minimal
+          uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
+          //for debugging, this will if there are terms in the model that the strong solver was not notified of
+          uf_ss->debugModel( fm );
+          Trace("model-engine-debug") << "Check model..." << std::endl;
+          //print debug
+          Debug("fmf-model-complete") << std::endl;
+          debugPrint("fmf-model-complete");
+          //successfully built an acceptable model, now check it
+          checkModel( addedLemmas );
+          //print debug information
+          if( Trace.isOn("model-engine") ){
+            Trace("model-engine") << "Instantiate axioms : " << ( d_builder.d_considerAxioms ? "yes" : "no" ) << std::endl;
+            Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+            Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+            double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+            Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
           }
-#endif
-        }
-        Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-        Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
-        if( Trace.isOn("model-engine") ){
-          Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-          Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
-          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-          Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
         }
-#ifdef ME_PRINT_WARNINGS
-        if( addedLemmas>10000 ){
-          Debug("fmf-exit") << std::endl;
-          debugPrint("fmf-exit");
-          exit( 0 );
+      }
+      if( addedLemmas==0 ){
+        //if we have not added lemmas yet and axiomInstMode=trust, then we are done
+        if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
+          //we must return unknown if an axiom is asserted
+          if( effort==0 ){
+            d_incomplete_check = true;
+          }
+          break;
         }
-#endif
       }
     }
     if( addedLemmas==0 ){
-      //CVC4 will answer SAT
-      Debug("fmf-consistent") << std::endl;
+      Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
+      //CVC4 will answer SAT or unknown
+      Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-      // finish building the model in the standard way
-      d_builder.finishProcessBuildModel( d_quantEngine->getModel() );
+      if( options::produceModels() ){
+        // finish building the model in the standard way
+        d_builder.buildModel( fm, true );
+        d_quantEngine->d_model_set = true;
+      }
+      //if the check was incomplete, we must set incomplete flag
+      if( d_incomplete_check ){
+        d_quantEngine->getOutputChannel().setIncomplete();
+      }
     }else{
       //otherwise, the search will continue
       d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
@@ -154,11 +154,7 @@ bool ModelEngine::optUseRelevantDomain(){
 }
 
 bool ModelEngine::optOneQuantPerRound(){
-#ifdef ONE_QUANT_PER_ROUND
-  return true;
-#else
-  return false;
-#endif
+  return options::fmfOneQuantPerRound();
 }
 
 int ModelEngine::initializeQuantifier( Node f ){
@@ -178,11 +174,13 @@ int ModelEngine::initializeQuantifier( Node f ){
     //    Notice() << "Unhandled phase req: " << n << std::endl;
     //  }
     //}
+    std::vector< Node > vars;
     std::vector< Node > ics;
     std::vector< Node > terms;
     for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
       Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
       Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() );
+      vars.push_back( f[0][j] );
       ics.push_back( ic );
       terms.push_back( t );
       //calculate the basis match for f
@@ -193,67 +191,137 @@ int ModelEngine::initializeQuantifier( Node f ){
     Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
     Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() );
     d_quantEngine->getTermDatabase()->registerModelBasis( n, gn );
-    //add model basis instantiation
-    if( d_quantEngine->addInstantiation( f, terms ) ){
-      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_statistics.d_num_quants_init_fail);
+    if( d_builder.optInstGen() ){
+      //add model basis instantiation
+      if( d_quantEngine->addInstantiation( f, vars, terms ) ){
+        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_statistics.d_num_quants_init_fail);
+      }
     }
   }
   return 0;
 }
 
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
-  int tests = 0;
-  int addedLemmas = 0;
-  int triedLemmas = 0;
-  Debug("inst-fmf-ei") << "Add matches for " << 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 ) << " ";
+void ModelEngine::checkModel( int& addedLemmas ){
+  FirstOrderModel* fm = d_quantEngine->getModel();
+  //for debugging
+  if( Trace.isOn("model-engine") ){
+    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); it != fm->d_rep_set.d_type_reps.end(); ++it ){
+      if( it->first.isSort() ){
+        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+        Trace("model-engine-debug") << "   ";
+        for( size_t i=0; i<it->second.size(); i++ ){
+          Trace("model-engine-debug") << it->second[i] << "  ";
+        }
+        Trace("model-engine-debug") << std::endl;
+      }
+    }
+  }
+  //verify we are SAT by trying exhaustive instantiation
+  d_incomplete_check = false;
+  if( optUseRelevantDomain() ){
+    d_rel_domain.compute();
   }
-  Debug("inst-fmf-ei") << std::endl;
-  if( d_builder.d_quant_selection_lits[f].empty() ){
-    Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
+  d_triedLemmas = 0;
+  d_testLemmas = 0;
+  d_relevantLemmas = 0;
+  d_totalLemmas = 0;
+  Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
+  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+    Node f = fm->getAssertedQuantifier( i );
+    addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
 #ifdef ME_PRINT_WARNINGS
-    Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
+    if( addedLemmas>10000 ){
+      Debug("fmf-exit") << std::endl;
+      debugPrint("fmf-exit");
+      exit( 0 );
+    }
 #endif
-  }else{
-    Debug("inst-fmf-ei") << "  Model literal definitions:" << std::endl;
-    for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
-      Debug("inst-fmf-ei") << "    " << d_builder.d_quant_selection_lits[f][i] << std::endl;
+    if( optOneQuantPerRound() && addedLemmas>0 ){
+      break;
     }
   }
-  RepSetIterator riter( f, d_quantEngine->getModel() );
-  //set the domain for the iterator (the sufficient set of instantiations to try)
-  if( useRelInstDomain ){
-    riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+  Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+  Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+}
+
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+  int addedLemmas = 0;
+  //keep track of total instantiations for statistics
+  int totalInst = 1;
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    TypeNode tn = f[0][i].getType();
+    if( d_quantEngine->getModel()->d_rep_set.hasType( tn ) ){
+      totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ tn ].size();
+    }
   }
-  RepSetEvaluator reval( d_quantEngine->getModel(), &riter );
-  while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
-    d_testLemmas++;
-    if( d_builder.optUseModel() ){
-      //see if instantiation is already true in current model
-      Debug("fmf-model-eval") << "Evaluating ";
-      riter.debugPrintSmall("fmf-model-eval");
-      Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
-      tests++;
-      //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
-      int depIndex = riter.getNumTerms()-1;
-      int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex );
+  d_totalLemmas += totalInst;
+  //if we need to consider this quantifier on this iteration
+  if( d_builder.isQuantifierActive( f ) ){
+    Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
+    if( useRelInstDomain ){
+      Trace("rel-dom") << "Relevant domain : " << std::endl;
+      for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){
+        Trace("rel-dom") << "   " << i << " : ";
+        for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){
+          Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " ";
+        }
+        Trace("rel-dom") << std::endl;
+      }
+    }
+    int tests = 0;
+    int triedLemmas = 0;
+    Debug("inst-fmf-ei") << "Add matches for " << 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 ) << " ";
+    }
+    Debug("inst-fmf-ei") << std::endl;
+    RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
+    riter.setQuantifier( f );
+    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    d_incomplete_check = d_incomplete_check || riter.d_incomplete;
+    //set the domain for the iterator (the sufficient set of instantiations to try)
+    if( useRelInstDomain ){
+      riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+    }
+    d_quantEngine->getModel()->resetEvaluate();
+    while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+      d_testLemmas++;
+      int eval = 0;
+      int depIndex;
+      if( d_builder.optUseModel() ){
+        //see if instantiation is already true in current model
+        Debug("fmf-model-eval") << "Evaluating ";
+        riter.debugPrintSmall("fmf-model-eval");
+        Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+        tests++;
+        //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;
+        eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( 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 ){
-        Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+        //instantiation is already true -> skip
         riter.increment2( depIndex );
       }else{
-        Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+        //instantiation was not shown to be true, construct the match
         InstMatch m;
-        riter.getMatch( d_quantEngine, m );
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+        }
         Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
         triedLemmas++;
         d_triedLemmas++;
+        //add as instantiation
         if( d_quantEngine->addInstantiation( f, m ) ){
           addedLemmas++;
 #ifdef EVAL_FAIL_SKIP_MULTIPLE
@@ -270,70 +338,48 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
           riter.increment();
         }
       }
-    }else{
-      InstMatch m;
-      riter.getMatch( d_quantEngine, m );
-      Debug("fmf-model-eval") << "* Add instantiation " << std::endl;
-      triedLemmas++;
-      d_triedLemmas++;
-      if( d_quantEngine->addInstantiation( f, m ) ){
-        addedLemmas++;
-      }
-      riter.increment();
     }
-  }
-  d_statistics.d_eval_formulas += reval.d_eval_formulas;
-  d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms;
-  d_statistics.d_eval_lits += reval.d_eval_lits;
-  d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown;
-  int totalInst = 1;
-  int relevantInst = 1;
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size();
-    relevantInst = relevantInst * (int)riter.d_domain[i].size();
-  }
-  d_totalLemmas += totalInst;
-  d_relevantLemmas += relevantInst;
-  Debug("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;
-///-----------
+    d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
+    d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
+    d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
+    d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+    int relevantInst = 1;
+    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      relevantInst = relevantInst * (int)riter.d_domain[i].size();
+    }
+    d_relevantLemmas += relevantInst;
+    Debug("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;
 #ifdef ME_PRINT_WARNINGS
-  if( addedLemmas>1000 ){
-    Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-    Notice() << "   Inst Total: " << totalInst << std::endl;
-    Notice() << "   Inst Relevant: " << totalRelevant << std::endl;
-    Notice() << "   Inst Tried: " << triedLemmas << std::endl;
-    Notice() << "   Inst Added: " << addedLemmas << std::endl;
-    Notice() << "   # Tests: " << tests << std::endl;
-    Notice() << std::endl;
-    if( !d_builder.d_quant_selection_lits[f].empty() ){
-      Notice() << "  Model literal definitions:" << std::endl;
-      for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
-        Notice() << "    " << d_builder.d_quant_selection_lits[f][i] << std::endl;
-      }
+    if( addedLemmas>1000 ){
+      Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+      Notice() << "   Inst Total: " << totalInst << std::endl;
+      Notice() << "   Inst Relevant: " << totalRelevant << std::endl;
+      Notice() << "   Inst Tried: " << triedLemmas << std::endl;
+      Notice() << "   Inst Added: " << addedLemmas << std::endl;
+      Notice() << "   # Tests: " << tests << std::endl;
       Notice() << std::endl;
     }
-  }
 #endif
-///-----------
+  }
   return addedLemmas;
 }
 
 void ModelEngine::debugPrint( const char* c ){
-  Debug( c ) << "Quantifiers: " << std::endl;
+  Trace( c ) << "Quantifiers: " << std::endl;
   for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-    Debug( c ) << "   ";
-    if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){
-      Debug( c ) << "*SAT* ";
+    Trace( c ) << "   ";
+    if( !d_builder.isQuantifierActive( f ) ){
+      Trace( c ) << "*Inactive* ";
     }else{
-      Debug( c ) << "      ";
+      Trace( c ) << "           ";
     }
-    Debug( c ) << f << std::endl;
+    Trace( c ) << f << std::endl;
   }
   //d_quantEngine->getModel()->debugPrint( c );
 }
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index f5d1db736..a292eb5f8 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -40,6 +40,8 @@ private:    //data maintained globally:
 private:    //analysis of current model:
   //relevant domain
   RelevantDomain d_rel_domain;
+  //is the exhaustive instantiation incomplete?
+  bool d_incomplete_check;
 private:
   //options
   bool optOneInstPerQuantRound();
@@ -48,6 +50,8 @@ private:
 private:
   //initialize quantifiers, return number of lemmas produced
   int initializeQuantifier( Node f );
+  //check model
+  void checkModel( int& addedLemmas );
   //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
   int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
 private:
@@ -57,7 +61,7 @@ private:
   int d_totalLemmas;
   int d_relevantLemmas;
 public:
-  ModelEngine( QuantifiersEngine* qe );
+  ModelEngine( context::Context* c, QuantifiersEngine* qe );
   ~ModelEngine(){}
 public:
   void check( Theory::Effort e );
diff --git a/src/theory/quantifiers/inst_when_mode.cpp b/src/theory/quantifiers/modes.cpp
index b60148c21..b6786d9f0 100644
--- a/src/theory/quantifiers/inst_when_mode.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -2,7 +2,7 @@
 /*! \file inst_when_mode.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: ajreynol
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
@@ -18,7 +18,7 @@
  **/
 
 #include <iostream>
-#include "theory/quantifiers/inst_when_mode.h"
+#include "theory/quantifiers/modes.h"
 
 namespace CVC4 {
 
@@ -43,5 +43,41 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mo
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) {
+  switch(mode) {
+  case theory::quantifiers::LITERAL_MATCH_NONE:
+    out << "LITERAL_MATCH_NONE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
+    out << "LITERAL_MATCH_PREDICATE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
+    out << "LITERAL_MATCH_EQUALITY";
+    break;
+  default:
+    out << "LiteralMatchMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode mode) {
+  switch(mode) {
+  case theory::quantifiers::AXIOM_INST_MODE_DEFAULT:
+    out << "AXIOM_INST_MODE_DEFAULT";
+    break;
+  case theory::quantifiers::AXIOM_INST_MODE_TRUST:
+    out << "AXIOM_INST_MODE_TRUST";
+    break;
+  case theory::quantifiers::AXIOM_INST_MODE_PRIORITY:
+    out << "AXIOM_INST_MODE_PRIORITY";
+    break;
+  default:
+    out << "AxiomInstMode!UNKNOWN";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
 
diff --git a/src/theory/quantifiers/inst_when_mode.h b/src/theory/quantifiers/modes.h
index 2cfba4935..8c56b8f3f 100644
--- a/src/theory/quantifiers/inst_when_mode.h
+++ b/src/theory/quantifiers/modes.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file inst_when_mode.h
+/*! \file modes.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: ajreynol
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
@@ -19,8 +19,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__MODEs_H
+#define __CVC4__THEORY__QUANTIFIERS__MODEs_H
 
 #include <iostream>
 
@@ -39,6 +39,25 @@ typedef enum {
   INST_WHEN_LAST_CALL,
 } InstWhenMode;
 
+typedef enum {
+  /** Do not consider polarity of patterns */
+  LITERAL_MATCH_NONE,
+  /** Consider polarity of boolean predicates only */
+  LITERAL_MATCH_PREDICATE,
+  /** Consider polarity of boolean predicates, as well as equalities */
+  LITERAL_MATCH_EQUALITY,
+} LiteralMatchMode;
+
+typedef enum {
+  /** default, use all methods for axioms */
+  AXIOM_INST_MODE_DEFAULT,
+  /** only use heuristic methods for axioms, return unknown in the case no instantiations are produced */
+  AXIOM_INST_MODE_TRUST,
+  /** only use heuristic methods for axioms, resort to all methods when no instantiations are produced */
+  AXIOM_INST_MODE_PRIORITY,
+} AxiomInstMode;
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 91e831092..a28ccb423 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -45,13 +45,13 @@ option smartTriggers /--disable-smart-triggers bool :default true
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching
 
-option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :include "theory/quantifiers/inst_when_mode.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
-
+ 
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
 
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/literal_match_mode.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode
 
 option cbqi --enable-cbqi/--disable-cbqi bool :default false
@@ -67,23 +67,23 @@ option flipDecision --enable-flip-decision/ bool :default false
 option finiteModelFind --finite-model-find bool :default false
  use finite model finding heuristic for quantifier instantiation
 
-option ufssRegions /--disable-uf-ss-regions bool :default true
- disable region-based method for discovering cliques and splits in uf strong solver
-option ufssEagerSplits --uf-ss-eager-split bool :default false
- add splits eagerly for uf strong solver
-option ufssColoringSat --uf-ss-coloring-sat bool :default false
- use coloring-based SAT heuristic for uf strong solver
-
 option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
  disable model-based quantifier instantiation for finite model finding
 
-option fmfInstGen /--disable-fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
 option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for fmf
+option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
+ only add instantiations for one quantifier per round for fmf 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
 option fmfRelevantDomain --fmf-relevant-domain bool :default false
  use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
+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 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
 
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 24734e8c8..00e91d115 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -58,6 +58,23 @@ predicate\n\
 \n\
 ";
 
+static const std::string axiomInstModeHelp = "\
+Literal match modes currently supported by the --axiom-inst option:\n\
+\n\
+default \n\
++ Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\
+  instantiating axioms.\n\
+\n\
+trust \n\
++ Treat axioms only using heuristic instantiation.  Return unknown if in the case\n\
+  that no instantiations are produced.\n\
+\n\
+priority \n\
++ Treat axioms only using heuristic instantiation.  Resort to using all methods\n\
+  in the case that no instantiations are produced.\n\
+\n\
+";
+
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
     return INST_WHEN_PRE_FULL;
@@ -104,6 +121,22 @@ inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, Smt
   }
 }
 
+inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default") {
+    return AXIOM_INST_MODE_DEFAULT;
+  } else if(optarg ==  "trust") {
+    return AXIOM_INST_MODE_TRUST;
+  } else if(optarg ==  "priority") {
+    return AXIOM_INST_MODE_PRIORITY;
+  } else if(optarg ==  "help") {
+    puts(axiomInstModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --axiom-inst: `") +
+                          optarg + "'.  Try --axiom-inst help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
new file mode 100644
index 000000000..22ee66362
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -0,0 +1,43 @@
+/*********************                                                        */

+/*! \file quantifiers_attributes.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Implementation of QuantifiersAttributes class

+ **/

+

+#include "theory/quantifiers/quantifiers_attributes.h"

+#include "theory/quantifiers/options.h"

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+using namespace CVC4::theory::quantifiers;

+

+void QuantifiersAttributes::setUserAttribute( std::string& attr, Node n ){

+  if( n.getKind()==FORALL ){

+    if( attr=="axiom" ){

+      Trace("quant-attr") << "Set axiom " << n << std::endl;

+      AxiomAttribute aa;

+      n.setAttribute( aa, true );

+    }else if( attr=="conjecture" ){

+      Trace("quant-attr") << "Set conjecture " << n << std::endl;

+      ConjectureAttribute ca;

+      n.setAttribute( ca, true );

+    }

+  }else{

+    for( size_t i=0; i<n.getNumChildren(); i++ ){

+      setUserAttribute( attr, n[i] );

+    }

+  }

+}

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
new file mode 100644
index 000000000..49c374f3e
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -0,0 +1,53 @@
+/*********************                                                        */

+/*! \file quantifiers_attributes.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Attributes for the theory quantifiers

+ **

+ ** Attributes for the theory quantifiers.

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H

+#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H

+

+#include "theory/rewriter.h"

+#include "theory/quantifiers_engine.h"

+

+namespace CVC4 {

+namespace theory {

+namespace quantifiers {

+

+/** Attribute true for quantifiers that are axioms */

+struct AxiomAttributeId {};

+typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;

+

+/** Attribute true for quantifiers that are conjecture */

+struct ConjectureAttributeId {};

+typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;

+

+struct QuantifiersAttributes

+{

+  /** set user attribute

+    *   This function will apply a custom set of attributes to all top-level universal

+    *   quantifiers contained in n

+    */

+  static void setUserAttribute( std::string& attr, Node n );

+};

+

+

+}

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 1563a3d1d..495e0f7a4 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -26,16 +26,18 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){
+RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
 
 }
 
 void RelevantDomain::compute(){
+  Trace("rel-dom") << "compute relevant domain" << std::endl;
   d_quant_inst_domain.clear();
   for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
     Node f = d_model->getAssertedQuantifier( i );
     d_quant_inst_domain[f].resize( f[0].getNumChildren() );
   }
+  Trace("rel-dom") << "account for ground terms" << std::endl;
   //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
   for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();
        it != d_model->d_uf_model_tree.end(); ++it ){
@@ -47,6 +49,7 @@ void RelevantDomain::compute(){
         if( d_model->d_rep_set.hasType( n[j].getType() ) ){
           Node ra = d_model->getRepresentative( n[j] );
           int raIndex = d_model->d_rep_set.getIndexFor( ra );
+          if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl;
           Assert( raIndex!=-1 );
           if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
             d_active_domain[op][j].push_back( raIndex );
@@ -56,12 +59,14 @@ void RelevantDomain::compute(){
       //add to range
       Node r = d_model->getRepresentative( n );
       int raIndex = d_model->d_rep_set.getIndexFor( r );
+      if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl;
       Assert( raIndex!=-1 );
       if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){
         d_active_range[op].push_back( raIndex );
       }
     }
   }
+  Trace("rel-dom") << "do quantifiers" << std::endl;
   //find fixed point for relevant domain computation
   bool success;
   do{
@@ -69,19 +74,20 @@ void RelevantDomain::compute(){
     for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
       Node f = d_model->getAssertedQuantifier( i );
       //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
-      if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){
+      if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, f ) ){
         success = false;
       }
       //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
       RepDomain range;
-      if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){
+      if( extendFunctionDomains( d_qe->getTermDatabase()->getCounterexampleBody( f ), range ) ){
         success = false;
       }
     }
   }while( !success );
+  Trace("rel-dom") << "done compute relevant domain" << std::endl;
 }
 
-bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){
+bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){
   bool domainChanged = false;
   if( n.getKind()==INST_CONSTANT ){
     bool domainSet = false;
@@ -93,8 +99,9 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in
       if( d_active_domain.find( op )!=d_active_domain.end() ){
         for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
           int d = d_active_domain[op][arg][i];
-          if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){
-            rd[vi].push_back( d );
+          if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )==
+              d_quant_inst_domain[f][vi].end() ){
+            d_quant_inst_domain[f][vi].push_back( d );
             domainChanged = true;
           }
         }
@@ -104,21 +111,21 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in
     if( !domainSet ){
       //otherwise, we must consider the entire domain
       TypeNode tn = n.getType();
-      if( d_model->d_rep_set.hasType( tn ) ){
-        if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){
-          rd[vi].clear();
+      if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){
+        if( d_model->d_rep_set.hasType( tn ) ){
+          //it is the complete domain
+          d_quant_inst_domain[f][vi].clear();
           for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){
-            rd[vi].push_back( i );
-            domainChanged = true;
+            d_quant_inst_domain[f][vi].push_back( i );
           }
+          domainChanged = true;
         }
-      }else{
-        //infinite domain?
+        d_quant_inst_domain_complete[f][vi] = true;
       }
     }
   }else{
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){
+      if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){
         domainChanged = true;
       }
     }
@@ -166,7 +173,13 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
       }
     }else{
       Node r = d_model->getRepresentative( n );
-      range.push_back( d_model->d_rep_set.getIndexFor( r ) );
+      int index = d_model->d_rep_set.getIndexFor( r );
+      if( index==-1 ){
+        //we consider all ground terms in bodies of quantifiers to be the first ground representative
+        range.push_back( 0 );
+      }else{
+        range.push_back( index );
+      }
     }
     return domainChanged;
   }
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 6ce47d114..62522812a 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -28,6 +28,7 @@ namespace quantifiers {
 class RelevantDomain
 {
 private:
+  QuantifiersEngine* d_qe;
   FirstOrderModel* d_model;
 
   //the domain of the arguments for each operator
@@ -35,16 +36,17 @@ private:
   //the range for each operator
   std::map< Node, RepDomain > d_active_range;
   //for computing relevant instantiation domain, return true if changed
-  bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
+  bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f );
   //for computing extended
   bool extendFunctionDomains( Node n, RepDomain& range );
 public:
-  RelevantDomain( FirstOrderModel* m );
+  RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
   virtual ~RelevantDomain(){}
   //compute the relevant domain
   void compute();
   //relevant instantiation domain for each quantifier
   std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
+  std::map< Node, std::map< int, bool > > d_quant_inst_domain_complete;
 };/* class RelevantDomain */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp
deleted file mode 100644
index 7461f3477..000000000
--- a/src/theory/quantifiers/rep_set_iterator.cpp
+++ /dev/null
@@ -1,517 +0,0 @@
-/*********************                                                        */
-/*! \file rep_set_iterator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of relevant domain class
- **/
-
-#include "theory/quantifiers/rep_set_iterator.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-
-#define USE_INDEX_ORDERING
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){
-  //store instantiation constants
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    d_index.push_back( 0 );
-  }
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    //store default index order
-    d_index_order.push_back( i );
-    d_var_order[i] = i;
-    //store default domain
-    d_domain.push_back( RepDomain() );
-    TypeNode tn = d_f[0][i].getType();
-    if( tn.isSort() ){
-      if( d_model->d_rep_set.hasType( tn ) ){
-        for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){
-          d_domain[i].push_back( j );
-        }
-      }else{
-        Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort");
-      }
-    }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
-      Unimplemented("Cannot create instantiation iterator for arithmetic quantifier");
-    }else if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      //if finite, then use type enumerator
-      if( dt.isFinite() ){
-        //DO_THIS: use type enumerator
-        Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier");
-      }else{
-        Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier");
-      }
-    }else{
-      Unimplemented("Cannot create instantiation iterator for quantifier");
-    }
-  }
-}
-
-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
-  d_index_order.clear();
-  d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
-  //make the d_var_order mapping
-  for( int i=0; i<(int)d_index_order.size(); i++ ){
-    d_var_order[d_index_order[i]] = i;
-  }
-}
-
-void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
-  d_domain.clear();
-  d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
-  //we are done if a domain is empty
-  for( int i=0; i<(int)d_domain.size(); i++ ){
-    if( d_domain[i].empty() ){
-      d_index.clear();
-    }
-  }
-}
-
-void RepSetIterator::increment2( int counter ){
-  Assert( !isFinished() );
-#ifdef DISABLE_EVAL_SKIP_MULTIPLE
-  counter = (int)d_index.size()-1;
-#endif
-  //increment d_index
-  while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
-    counter--;
-  }
-  if( counter==-1 ){
-    d_index.clear();
-  }else{
-    for( int i=(int)d_index.size()-1; i>counter; i-- ){
-      d_index[i] = 0;
-      //d_model->clearEvalFailed( i );
-    }
-    d_index[counter]++;
-    //d_model->clearEvalFailed( counter );
-  }
-}
-
-void RepSetIterator::increment(){
-  if( !isFinished() ){
-    increment2( (int)d_index.size()-1 );
-  }
-}
-
-bool RepSetIterator::isFinished(){
-  return d_index.empty();
-}
-
-void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
-  for( int i=0; i<(int)d_index.size(); i++ ){
-    m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i ));
-  }
-}
-
-Node RepSetIterator::getTerm( int i ){
-  TypeNode tn = d_f[0][d_index_order[i]].getType();
-  Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() );
-  int index = d_index_order[i];
-  return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];
-}
-
-void RepSetIterator::debugPrint( const char* c ){
-  for( int i=0; i<(int)d_index.size(); i++ ){
-    Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
-  }
-}
-
-void RepSetIterator::debugPrintSmall( const char* c ){
-  Debug( c ) << "RI: ";
-  for( int i=0; i<(int)d_index.size(); i++ ){
-    Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
-  }
-  Debug( c ) << std::endl;
-}
-
-RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){
-  d_eval_formulas = 0;
-  d_eval_uf_terms = 0;
-  d_eval_lits = 0;
-  d_eval_lits_unknown = 0;
-}
-
-//if evaluate( n ) = eVal,
-// let n' = d_riter * n be the formula n instantiated with the current values in r_iter
-// if eVal = 1, then n' is true, if eVal = -1, then n' is false,
-// if eVal = 0, then n' cannot be proven to be equal to phaseReq
-// if eVal is not 0, then
-//   each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
-int RepSetEvaluator::evaluate( Node n, int& depIndex ){
-  ++d_eval_formulas;
-  //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
-  //Notice() << "Eval " << n << std::endl;
-  if( n.getKind()==NOT ){
-    int val = evaluate( n[0], depIndex );
-    return val==1 ? -1 : ( val==-1 ? 1 : 0 );
-  }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
-    int baseVal = n.getKind()==AND ? 1 : -1;
-    int eVal = baseVal;
-    int posDepIndex = d_riter->getNumTerms();
-    int negDepIndex = -1;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      //evaluate subterm
-      int childDepIndex;
-      Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
-      int eValT = evaluate( nn, childDepIndex );
-      if( eValT==baseVal ){
-        if( eVal==baseVal ){
-          if( childDepIndex>negDepIndex ){
-            negDepIndex = childDepIndex;
-          }
-        }
-      }else if( eValT==-baseVal ){
-        eVal = -baseVal;
-        if( childDepIndex<posDepIndex ){
-          posDepIndex = childDepIndex;
-          if( posDepIndex==-1 ){
-            break;
-          }
-        }
-      }else if( eValT==0 ){
-        if( eVal==baseVal ){
-          eVal = 0;
-        }
-      }
-    }
-    if( eVal!=0 ){
-      depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
-      return eVal;
-    }else{
-      return 0;
-    }
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
-    int depIndex1;
-    int eVal = evaluate( n[0], depIndex1 );
-    if( eVal!=0 ){
-      int depIndex2;
-      int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
-      if( eVal2!=0 ){
-        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-        return eVal==eVal2 ? 1 : -1;
-      }
-    }
-    return 0;
-  }else if( n.getKind()==ITE ){
-    int depIndex1, depIndex2;
-    int eVal = evaluate( n[0], depIndex1 );
-    if( eVal==0 ){
-      //evaluate children to see if they are the same value
-      int eval1 = evaluate( n[1], depIndex1 );
-      if( eval1!=0 ){
-        int eval2 = evaluate( n[1], depIndex2 );
-        if( eval1==eval2 ){
-          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-          return eval1;
-        }
-      }
-    }else{
-      int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 );
-      depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-      return eValT;
-    }
-    return 0;
-  }else if( n.getKind()==FORALL ){
-    return 0;
-  }else{
-    ++d_eval_lits;
-    ////if we know we will fail again, immediately return
-    //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
-    //  if( d_eval_failed[n] ){
-    //    return -1;
-    //  }
-    //}
-    //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
-    int retVal = 0;
-    depIndex = d_riter->getNumTerms()-1;
-    Node val = evaluateTerm( n, depIndex );
-    if( !val.isNull() ){
-      if( d_model->areEqual( val, d_model->d_true ) ){
-        retVal = 1;
-      }else if( d_model->areEqual( val, d_model->d_false ) ){
-        retVal = -1;
-      }else{
-        if( val.getKind()==EQUAL ){
-          if( d_model->areEqual( val[0], val[1] ) ){
-            retVal = 1;
-          }else if( d_model->areDisequal( val[0], val[1] ) ){
-            retVal = -1;
-          }
-        }
-      }
-    }
-    if( retVal!=0 ){
-      Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
-    }else{
-      ++d_eval_lits_unknown;
-      Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
-      //std::cout << "Neither true nor false : " << n << std::endl;
-      //std::cout << "  Value : " << val << std::endl;
-      //for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      //  std::cout << "   " << i << " : " << n[i].getType() << std::endl;
-      //}
-    }
-    return retVal;
-  }
-}
-
-Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
-  //Message() << "Eval term " << n << std::endl;
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    //if evaluating a ground term, just consult the standard getValue functionality
-    depIndex = -1;
-    return d_model->getValue( n );
-  }else{
-    Node val;
-    depIndex = d_riter->getNumTerms()-1;
-    //check the type of n
-    if( n.getKind()==INST_CONSTANT ){
-      int v = n.getAttribute(InstVarNumAttribute());
-      depIndex = d_riter->d_var_order[ v ];
-      val = d_riter->getTerm( v );
-    }else if( n.getKind()==ITE ){
-      int depIndex1, depIndex2;
-      int eval = evaluate( n[0], depIndex1 );
-      if( eval==0 ){
-        //evaluate children to see if they are the same
-        Node val1 = evaluateTerm( n[ 1 ], depIndex1 );
-        Node val2 = evaluateTerm( n[ 2 ], depIndex2 );
-        if( val1==val2 ){
-          val = val1;
-          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-        }else{
-          return Node::null();
-        }
-      }else{
-        val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 );
-        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-      }
-    }else{
-      std::vector< int > children_depIndex;
-      //for select, pre-process read over writes
-      if( n.getKind()==SELECT ){
-#if 1
-        //std::cout << "Evaluate " << n << std::endl;
-        Node sel = evaluateTerm( n[1], depIndex );
-        if( sel.isNull() ){
-          depIndex = d_riter->getNumTerms()-1;
-          return Node::null();
-        }
-        Node arr = d_model->getRepresentative( n[0] );
-        //if( n[0]!=d_model->getRepresentative( n[0] ) ){
-        //  std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl;
-        //}
-        int tempIndex;
-        int eval = 1;
-        while( arr.getKind()==STORE && eval!=0 ){
-          eval = evaluate( sel.eqNode( arr[1] ), tempIndex );
-          depIndex = tempIndex > depIndex ? tempIndex : depIndex;
-          if( eval==1 ){
-            val = evaluateTerm( arr[2], tempIndex );
-            depIndex = tempIndex > depIndex ? tempIndex : depIndex;
-            return val;
-          }else if( eval==-1 ){
-            arr = arr[0];
-          }
-        }
-        arr = evaluateTerm( arr, tempIndex );
-        depIndex = tempIndex > depIndex ? tempIndex : depIndex;
-        val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
-#else
-        val = evaluateTermDefault( n, depIndex, children_depIndex );
-#endif
-      }else{
-        //default term evaluate : evaluate all children, recreate the value
-        val = evaluateTermDefault( n, depIndex, children_depIndex );
-      }
-      if( !val.isNull() ){
-        bool setVal = false;
-        //custom ways of evaluating terms
-        if( n.getKind()==APPLY_UF ){
-          Node op = n.getOperator();
-          //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
-          //if it is a defined UF, then consult the interpretation
-          if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){
-            ++d_eval_uf_terms;
-            int argDepIndex = 0;
-            //make the term model specifically for n
-            makeEvalUfModel( n );
-            //now, consult the model
-            if( d_eval_uf_use_default[n] ){
-              val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex );
-            }else{
-              val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );
-            }
-            //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
-            //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
-            Assert( !val.isNull() );
-            //recalculate the depIndex
-            depIndex = -1;
-            for( int i=0; i<argDepIndex; i++ ){
-              int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
-              Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
-              if( children_depIndex[index]>depIndex ){
-                depIndex = children_depIndex[index];
-              }
-            }
-            setVal = true;
-          }
-        }else if( n.getKind()==SELECT ){
-          //we are free to interpret this term however we want
-        }
-        //if not set already, rewrite and consult model for interpretation
-        if( !setVal ){
-          val = Rewriter::rewrite( val );
-          if( !val.isConst() ){
-            //FIXME: we cannot do this until we trust all theories collectModelInfo!
-            //val = d_model->getInterpretedValue( val );
-            //val = d_model->getRepresentative( val );
-          }
-        }
-        Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
-        d_model->printRepresentativeDebug( "fmf-eval-debug", val );
-        Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
-      }
-    }
-    return val;
-  }
-}
-
-Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){
-  depIndex = -1;
-  if( n.getNumChildren()==0 ){
-    return n;
-  }else{
-    //first we must evaluate the arguments
-    std::vector< Node > children;
-    if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
-      children.push_back( n.getOperator() );
-    }
-    //for each argument, calculate its value, and the variables its value depends upon
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      childDepIndex.push_back( -1 );
-      Node nn = evaluateTerm( n[i], childDepIndex[i] );
-      if( nn.isNull() ){
-        depIndex = d_riter->getNumTerms()-1;
-        return nn;
-      }else{
-        children.push_back( nn );
-        if( childDepIndex[i]>depIndex ){
-          depIndex = childDepIndex[i];
-        }
-      }
-    }
-    //recreate the value
-    Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );
-    return val;
-  }
-}
-
-void RepSetEvaluator::clearEvalFailed( int index ){
-  for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
-    d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
-  }
-  d_eval_failed_lits[index].clear();
-}
-
-void RepSetEvaluator::makeEvalUfModel( Node n ){
-  if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
-    makeEvalUfIndexOrder( n );
-    if( !d_eval_uf_use_default[n] ){
-      Node op = n.getOperator();
-      d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
-      d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] );
-      //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
-      //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
-    }
-  }
-}
-
-struct sortGetMaxVariableNum {
-  std::map< Node, int > d_max_var_num;
-  int computeMaxVariableNum( Node n ){
-    if( n.getKind()==INST_CONSTANT ){
-      return n.getAttribute(InstVarNumAttribute());
-    }else if( n.hasAttribute(InstConstantAttribute()) ){
-      int maxVal = -1;
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        int val = getMaxVariableNum( n[i] );
-        if( val>maxVal ){
-          maxVal = val;
-        }
-      }
-      return maxVal;
-    }else{
-      return -1;
-    }
-  }
-  int getMaxVariableNum( Node n ){
-    std::map< Node, int >::iterator it = d_max_var_num.find( n );
-    if( it==d_max_var_num.end() ){
-      int num = computeMaxVariableNum( n );
-      d_max_var_num[n] = num;
-      return num;
-    }else{
-      return it->second;
-    }
-  }
-  bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
-};
-
-void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){
-  if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-#ifdef USE_INDEX_ORDERING
-    //sort arguments in order of least significant vs. most significant variable in default ordering
-    std::map< Node, std::vector< int > > argIndex;
-    std::vector< Node > args;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( argIndex.find( n[i] )==argIndex.end() ){
-        args.push_back( n[i] );
-      }
-      argIndex[n[i]].push_back( i );
-    }
-    sortGetMaxVariableNum sgmvn;
-    std::sort( args.begin(), args.end(), sgmvn );
-    for( int i=0; i<(int)args.size(); i++ ){
-      for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
-        d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
-      }
-    }
-    bool useDefault = true;
-    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
-      if( i!=d_eval_term_index_order[n][i] ){
-        useDefault = false;
-        break;
-      }
-    }
-    d_eval_uf_use_default[n] = useDefault;
-    Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
-    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
-      Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
-    }
-    Debug("fmf-index-order") << std::endl;
-#else
-    d_eval_uf_use_default[n] = true;
-#endif
-  }
-}
-
-
diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h
deleted file mode 100644
index 85a2f3fd2..000000000
--- a/src/theory/quantifiers/rep_set_iterator.h
+++ /dev/null
@@ -1,119 +0,0 @@
-/*********************                                                        */
-/*! \file rep_set_iterator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief rep_set_iterator class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__REP_SET_ITERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__REP_SET_ITERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** this class iterates over a RepSet */
-class RepSetIterator {
-public:
-  RepSetIterator( Node f, FirstOrderModel* model );
-  ~RepSetIterator(){}
-  //pointer to quantifier
-  Node d_f;
-  //pointer to model
-  FirstOrderModel* d_model;
-  //index we are considering
-  std::vector< int > d_index;
-  //domain we are considering
-  std::vector< RepDomain > d_domain;
-  //ordering for variables we are indexing over
-  //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
-  //    then we consider instantiations in this order:
-  //      a/x a/y a/z
-  //      a/x b/y a/z
-  //      b/x a/y a/z
-  //      b/x b/y a/z
-  //      ...
-  std::vector< int > d_index_order;
-  //variables to index they are considered at
-  //  for example, if d_index_order = { 2, 0, 1 }
-  //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
-  std::map< int, int > d_var_order;
-  //the instantiation constants of d_f
-  std::vector< Node > d_ic;
-  //the current terms we are considering
-  std::vector< Node > d_terms;
-public:
-  /** set index order */
-  void setIndexOrder( std::vector< int >& indexOrder );
-  /** set domain */
-  void setDomain( std::vector< RepDomain >& domain );
-  /** increment the iterator */
-  void increment2( int counter );
-  void increment();
-  /** is the iterator finished? */
-  bool isFinished();
-  /** produce the match that this iterator represents */
-  void getMatch( QuantifiersEngine* qe, InstMatch& m );
-  /** get the i_th term we are considering */
-  Node getTerm( int i );
-  /** get the number of terms we are considering */
-  int getNumTerms() { return d_f[0].getNumChildren(); }
-  /** debug print */
-  void debugPrint( const char* c );
-  void debugPrintSmall( const char* c );
-};
-
-class RepSetEvaluator
-{
-private:
-  FirstOrderModel* d_model;
-  RepSetIterator* d_riter;
-private: //for Theory UF:
-  //map from terms to the models used to calculate their value
-  std::map< Node, bool > d_eval_uf_use_default;
-  std::map< Node, uf::UfModelTree > d_eval_uf_model;
-  void makeEvalUfModel( Node n );
-  //index ordering to use for each term
-  std::map< Node, std::vector< int > > d_eval_term_index_order;
-  int getMaxVariableNum( int n );
-  void makeEvalUfIndexOrder( Node n );
-private:
-  //default evaluate term function
-  Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex );
-  //temporary storing which literals have failed
-  void clearEvalFailed( int index );
-  std::map< Node, bool > d_eval_failed;
-  std::map< int, std::vector< Node > > d_eval_failed_lits;
-public:
-  RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri );
-  virtual ~RepSetEvaluator(){}
-  /** evaluate functions */
-  int evaluate( Node n, int& depIndex );
-  Node evaluateTerm( Node n, int& depIndex );
-public:
-  //statistics
-  int d_eval_formulas;
-  int d_eval_uf_terms;
-  int d_eval_lits;
-  int d_eval_lits_unknown;
-};/* class RepSetEvaluator */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a73d42a31..bd6b03a78 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -131,7 +131,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
    //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
      if( !it->second.empty() ){
-       if( it->second[0].getType()==NodeManager::currentNM()->booleanType() ){
+       if( it->second[0].getType().isBoolean() ){
          d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
          d_pred_map_trie[ 1 ][ it->first ].d_data.clear();
        }else{
@@ -199,6 +199,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
       ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;
       mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
+      Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
     }else{
       mbt = d_type_map[ tn ][ 0 ];
     }
@@ -337,12 +338,13 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){
   TypeNode tn = n.getType();
   if( d_free_vars.find( tn )==d_free_vars.end() ){
     //if integer or real, make zero
-    if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+    if( tn.isInteger() || tn.isReal() ){
       Rational z(0);
       d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
     }else{
       if( d_type_map[ tn ].empty() ){
         d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( tn );
+        Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
       }else{
         d_free_vars[tn] = d_type_map[ tn ][ 0 ];
       }
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 3d41d28b7..c45626dd9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -24,11 +24,10 @@
 #include "theory/quantifiers/model_engine.h"
 #include "expr/kind.h"
 #include "util/Assert.h"
-#include <map>
-#include <time.h>
 #include "theory/quantifiers/theory_quantifiers_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 
 using namespace std;
 using namespace CVC4;
@@ -42,6 +41,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   d_numRestarts(0){
   d_numInstantiations = 0;
   d_baseDecLevel = -1;
+  out.handleUserAttribute( "axiom", this );
+  out.handleUserAttribute( "conjecture", this );
 }
 
 
@@ -89,7 +90,7 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
-void TheoryQuantifiers::collectModelInfo( TheoryModel* m ){
+void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
 
 }
 
@@ -126,9 +127,12 @@ void TheoryQuantifiers::check(Effort e) {
 }
 
 void TheoryQuantifiers::propagate(Effort level){
-  CodeTimer codeTimer(d_theoryTime);
+  //CodeTimer codeTimer(d_theoryTime);
+  //getQuantifiersEngine()->propagate( level );
+}
 
-  getQuantifiersEngine()->propagate( level );
+Node TheoryQuantifiers::getNextDecisionRequest(){
+  return getQuantifiersEngine()->getNextDecisionRequest();
 }
 
 void TheoryQuantifiers::assertUniversal( Node n ){
@@ -186,6 +190,6 @@ bool TheoryQuantifiers::restart(){
   }
 }
 
-void TheoryQuantifiers::performCheck(Effort e){
-  getQuantifiersEngine()->check( e );
+void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){
+  QuantifiersAttributes::setUserAttribute( attr, n );
 }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 1e42abd22..bc712955e 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -61,17 +61,17 @@ public:
   void presolve();
   void check(Effort e);
   void propagate(Effort level);
+  Node getNextDecisionRequest();
   Node getValue(TNode n);
-  void collectModelInfo( TheoryModel* m );
+  void collectModelInfo( TheoryModel* m, bool fullModel );
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();
+  void setUserAttribute( std::string& attr, Node n );
 private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
   bool restart();
-public:
-  void performCheck(Effort e);
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */