Remove alternate versions of mbqi (#2742)

18 files changed, 14 insertions, 2804 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9e93bd953..91c06ddd9 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -475,8 +475,6 @@ libcvc4_add_sources(
   theory/quantifiers/extended_rewrite.h
   theory/quantifiers/first_order_model.cpp
   theory/quantifiers/first_order_model.h
-  theory/quantifiers/fmf/ambqi_builder.cpp
-  theory/quantifiers/fmf/ambqi_builder.h
   theory/quantifiers/fmf/bounded_integers.cpp
   theory/quantifiers/fmf/bounded_integers.h
   theory/quantifiers/fmf/full_model_check.cpp
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 420396452..36144e70e 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -267,7 +267,8 @@ agg \n\
 \n\
 ";
 
-const std::string OptionsHandler::s_mbqiModeHelp = "\
+const std::string OptionsHandler::s_mbqiModeHelp =
+    "\
 Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
 \n\
 default \n\
@@ -277,12 +278,8 @@ default \n\
 none \n\
 + Disable model-based quantifier instantiation.\n\
 \n\
-gen-ev \n\
-+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper based on generalizing evaluations.\n\
-\n\
-abs \n\
-+ Use abstract MBQI algorithm (uses disjoint sets). \n\
+trust \n\
++ Do not instantiate quantified formulas (incomplete technique).\n\
 \n\
 ";
 
@@ -660,14 +657,11 @@ void OptionsHandler::checkLiteralMatchMode(
 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
     std::string option, std::string optarg)
 {
-  if(optarg == "gen-ev") {
-    return theory::quantifiers::MBQI_GEN_EVAL;
-  } else if(optarg == "none") {
+  if (optarg == "none")
+  {
     return theory::quantifiers::MBQI_NONE;
   } else if(optarg == "default" || optarg ==  "fmc") {
     return theory::quantifiers::MBQI_FMC;
-  } else if(optarg == "abs") {
-    return theory::quantifiers::MBQI_ABS;
   } else if(optarg == "trust") {
     return theory::quantifiers::MBQI_TRUST;
   } else if(optarg == "help") {
diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index 1814a363d..b08f71c2e 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -64,18 +64,12 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
 
 std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
   switch(mode) {
-  case theory::quantifiers::MBQI_GEN_EVAL:
-    out << "MBQI_GEN_EVAL";
-    break;
   case theory::quantifiers::MBQI_NONE:
     out << "MBQI_NONE";
     break;
   case theory::quantifiers::MBQI_FMC:
     out << "MBQI_FMC";
     break;
-  case theory::quantifiers::MBQI_ABS:
-    out << "MBQI_ABS";
-    break;
   case theory::quantifiers::MBQI_TRUST:
     out << "MBQI_TRUST";
     break;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 41378d2cd..eea043865 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -53,14 +53,10 @@ enum LiteralMatchMode {
 };
 
 enum MbqiMode {
-  /** mbqi from CADE 24 paper */
-  MBQI_GEN_EVAL,
   /** no mbqi */
   MBQI_NONE,
   /** default, mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
-  /** abstract mbqi algorithm */
-  MBQI_ABS,
   /** mbqi trust (produce no instantiations) */
   MBQI_TRUST,
 };
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7abfd8273..ae20fa156 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1809,12 +1809,6 @@ void SmtEngine::setDefaults() {
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
   }
-  if( options::mbqiMode()==quantifiers::MBQI_ABS ){
-    if( !d_logic.isPure(THEORY_UF) ){
-      //MBQI_ABS is only supported in pure quantified UF
-      options::mbqiMode.set( quantifiers::MBQI_FMC );
-    }
-  }
   if( options::fmfFunWellDefinedRelevant() ){
     if( !options::fmfFunWellDefined.wasSetByUser() ){
       options::fmfFunWellDefined.set( true );
@@ -1852,17 +1846,6 @@ void SmtEngine::setDefaults() {
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }
-    if( options::mbqiMode()==quantifiers::MBQI_ABS ){
-      if( !options::preSkolemQuant.wasSetByUser() ){
-        options::preSkolemQuant.set( true );
-      }
-      if( !options::preSkolemQuantNested.wasSetByUser() ){
-        options::preSkolemQuantNested.set( true );
-      }
-      if( !options::fmfOneInstPerRound.wasSetByUser() ){
-        options::fmfOneInstPerRound.set( true );
-      }
-    }
   }
 
   //apply counterexample guided instantiation options
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 0eec40de2..5eb65ed21 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/fmf/ambqi_builder.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_engine.h"
@@ -414,473 +413,6 @@ unsigned FirstOrderModel::getModelBasisArg(Node n)
   return n.getAttribute(ModelBasisArgAttribute());
 }
 
-Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m,
-                                                              Node n1,
-                                                              Node n2,
-                                                              bool& isGround)
-{
-  isGround = true;
-  std::vector<Node> children;
-  children.push_back(n1.getOperator());
-  for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
-  {
-    if (n1[i] == n2[i])
-    {
-      if (n1[i].getAttribute(ModelBasisAttribute()))
-      {
-        isGround = false;
-      }
-      children.push_back(n1[i]);
-    }
-    else if (n1[i].getAttribute(ModelBasisAttribute()))
-    {
-      children.push_back(n2[i]);
-    }
-    else if (n2[i].getAttribute(ModelBasisAttribute()))
-    {
-      children.push_back(n1[i]);
-    }
-    else if (m->areEqual(n1[i], n2[i]))
-    {
-      children.push_back(n1[i]);
-    }
-    else
-    {
-      return Node::null();
-    }
-  }
-  return NodeManager::currentNM()->mkNode(APPLY_UF, children);
-}
-
-void FirstOrderModelIG::UfModelTreeGenerator::setValue(
-    TheoryModel* m, Node n, Node v, bool ground, bool isReq)
-{
-  Assert(!n.isNull());
-  Assert(!v.isNull());
-  d_set_values[isReq ? 1 : 0][ground ? 1 : 0][n] = v;
-  if (!ground)
-  {
-    for (unsigned i = 0, defSize = d_defaults.size(); i < defSize; i++)
-    {
-      // for correctness, to allow variable order-independent function
-      // interpretations, we must ensure that the intersection of all default
-      // terms is also defined.
-      // for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
-      // then we must define f( b, a ).
-      bool isGround;
-      Node ni = getIntersection(m, n, d_defaults[i], isGround);
-      if (!ni.isNull())
-      {
-        // if the intersection exists, and is not already defined
-        if (d_set_values[0][isGround ? 1 : 0].find(ni)
-                == d_set_values[0][isGround ? 1 : 0].end()
-            && d_set_values[1][isGround ? 1 : 0].find(ni)
-                   == d_set_values[1][isGround ? 1 : 0].end())
-        {
-          // use the current value
-          setValue(m, ni, v, isGround, false);
-        }
-      }
-    }
-    d_defaults.push_back(n);
-  }
-  if (isReq
-      && d_set_values[0][ground ? 1 : 0].find(n)
-             != d_set_values[0][ground ? 1 : 0].end())
-  {
-    d_set_values[0][ground ? 1 : 0].erase(n);
-  }
-}
-
-void FirstOrderModelIG::UfModelTreeGenerator::makeModel(TheoryModel* m,
-                                                        uf::UfModelTree& tree)
-{
-  for (int j = 0; j < 2; j++)
-  {
-    for (int k = 0; k < 2; k++)
-    {
-      for (std::map<Node, Node>::iterator it = d_set_values[j][k].begin();
-           it != d_set_values[j][k].end();
-           ++it)
-      {
-        tree.setValue(m, it->first, it->second, k == 1);
-      }
-    }
-  }
-  if (!d_default_value.isNull())
-  {
-    tree.setDefaultValue(m, d_default_value);
-  }
-  tree.simplify();
-}
-
-void FirstOrderModelIG::UfModelTreeGenerator::clear()
-{
-  d_default_value = Node::null();
-  for (int j = 0; j < 2; j++)
-  {
-    for (int k = 0; k < 2; k++)
-    {
-      d_set_values[j][k].clear();
-    }
-  }
-  d_defaults.clear();
-}
-
-FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(qe, c,name) {
-
-}
-
-void FirstOrderModelIG::processInitialize( bool ispre ){
-  if( ispre ){
-    //rebuild models
-    d_uf_model_tree.clear();
-    d_uf_model_gen.clear();
-  }
-}
-
-void FirstOrderModelIG::processInitializeModelForTerm( Node n ){
-  if( n.getKind()==APPLY_UF ){
-    Node op = n.getOperator();
-    if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){
-      TypeNode tn = op.getType();
-      tn = tn[ (int)tn.getNumChildren()-1 ];
-      //only generate models for predicates and functions with uninterpreted range types
-      //if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){
-        d_uf_model_tree[ op ] = uf::UfModelTree( op );
-        d_uf_model_gen[ op ].clear();
-      //}
-    }
-  }
-  /*
-  if( n.getType().isArray() ){
-    while( n.getKind()==STORE ){
-      n = n[0];
-    }
-    Node nn = getRepresentative( n );
-    if( d_array_model.find( nn )==d_array_model.end() ){
-      d_array_model[nn] = arrays::ArrayModel( nn, this );
-    }
-  }
-  */
-}
-
-//for evaluation of quantifier bodies
-
-void FirstOrderModelIG::resetEvaluate(){
-  d_eval_uf_use_default.clear();
-  d_eval_uf_model.clear();
-  d_eval_term_index_order.clear();
-}
-
-//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 FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
-  Debug("fmf-eval-debug2") << "Evaluate " << n << 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 ){
-    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 = 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()==EQUAL && n[0].getType().isBoolean() ){
-    int depIndex1;
-    int eVal = evaluate( n[0], depIndex1, ri );
-    if( eVal!=0 ){
-      int depIndex2;
-      int eVal2 = evaluate( 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{
-    //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{
-      Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
-      Trace("fmf-eval-amb") << "   value : " << val << std::endl;
-    }
-    return retVal;
-  }
-}
-
-Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
-  //Message() << "Eval term " << n << std::endl;
-  Node val;
-  depIndex = ri->getNumTerms()-1;
-  //check the type of n
-  if( n.getKind()==INST_CONSTANT ){
-    int v = n.getAttribute(InstVarNumAttribute());
-    depIndex = ri->getIndexOrder( v );
-    val = ri->getCurrentTerm( 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;
-    //default term evaluate : evaluate all children, recreate the value
-    val = evaluateTermDefault( n, depIndex, children_depIndex, ri );
-    Trace("fmf-eval-debug") << "Evaluate term, value from " << n << " is " << val << std::endl;
-    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() ){
-          int argDepIndex = 0;
-          //make the term model specifically for n
-          makeEvalUfModel( n );
-          //now, consult the model
-          if( d_eval_uf_use_default[n] ){
-            Trace("fmf-eval-debug") << "get default" << std::endl;
-            val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex );
-          }else{
-            Trace("fmf-eval-debug") << "get uf model" << std::endl;
-            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{
-          Trace("fmf-eval-debug") << "No model." << std::endl;
-        }
-      }
-      //if not set already, rewrite and consult model for interpretation
-      if( !setVal ){
-        val = Rewriter::rewrite( val );
-        if( !val.isConst() ){
-          return Node::null();
-        }
-      }
-      Trace("fmf-eval-debug") << "Evaluate term " << n << " = ";
-      Trace("fmf-eval-debug") << getRepresentative(val);
-      Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl;
-    }
-  }
-  return val;
-}
-
-Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
-  depIndex = -1;
-  if( n.getNumChildren()==0 ){
-    return n;
-  }else{
-    bool isInterp = n.getKind()!=APPLY_UF;
-    //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{
-        if( childDepIndex[i]>depIndex ){
-          depIndex = childDepIndex[i];
-        }
-        if( isInterp ){
-          if( !nn.isConst() ) {
-            nn = getRepresentative( nn );
-          }
-        }
-        children.push_back( nn );
-      }
-    }
-    //recreate the value
-    Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );
-    return val;
-  }
-}
-
-void FirstOrderModelIG::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( std::cout, d_qe->getModel(), 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( TermUtil::hasInstConstAttr(n) ){
-      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 FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
-  if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-    //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;
-  }
-}
-
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
 FirstOrderModel(qe, c, name){
 
@@ -989,128 +521,6 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
 }
 
-FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(qe, c, name) {
-
-}
-
-FirstOrderModelAbs::~FirstOrderModelAbs()
-{
-  for(std::map<Node, AbsDef*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
-    delete (*i).second;
-  }
-}
-
-void FirstOrderModelAbs::processInitialize( bool ispre ) {
-  if( !ispre ){
-    Trace("ambqi-debug") << "Process initialize" << std::endl;
-    for( std::map<Node, AbsDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) {
-      Node op = it->first;
-      TypeNode tno = op.getType();
-      Trace("ambqi-debug") << "  Init " << op << " " << tno << std::endl;
-      for( unsigned i=0; i<tno.getNumChildren(); i++) {
-        //make sure a representative of the type exists
-        if( !d_rep_set.hasType( tno[i] ) ){
-          Node e = getSomeDomainElement( tno[i] );
-          Trace("ambqi-debug") << "  * Initialize type " << tno[i] << ", add ";
-          Trace("ambqi-debug") << e << " " << e.getType() << std::endl;
-          //d_rep_set.add( e );
-        }
-      }
-    }
-  }
-}
-
-unsigned FirstOrderModelAbs::getRepresentativeId( TNode n ) {
-  TNode r = getUsedRepresentative( n );
-  std::map< TNode, unsigned >::iterator it = d_rep_id.find( r );
-  if( it!=d_rep_id.end() ){
-    return it->second;
-  }else{
-    return 0;
-  }
-}
-
-TNode FirstOrderModelAbs::getUsedRepresentative( TNode n ) {
-  if( hasTerm( n ) ){
-    if( n.getType().isBoolean() ){
-      return areEqual(n, d_true) ? d_true : d_false;
-    }else{
-      return getRepresentative( n );
-    }
-  }else{
-    Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl;
-    Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() );
-    return d_rep_set.d_type_reps[n.getType()][0];
-  }
-}
-
-Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) {
-  if( d_models_valid[op] ){
-    Trace("ambqi-debug") << "Get function value for " << op << std::endl;
-    TypeNode type = op.getType();
-    std::vector< Node > vars;
-    for( size_t i=0; i<type.getNumChildren()-1; i++ ){
-      std::stringstream ss;
-      ss << argPrefix << (i+1);
-      Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] );
-      vars.push_back( b );
-    }
-    Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
-    Node curr = d_models[op]->getFunctionValue( this, op, vars );
-    Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
-    Trace("ambqi-debug") << "Return " << fv << std::endl;
-    return fv;
-  }else{
-
-  }
-  return Node::null();
-}
-
-void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) {
-  if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
-    Node op = n.getKind()==APPLY_UF ? n.getOperator() : n;
-    if( d_models.find(op)==d_models.end()) {
-      Trace("abmqi-debug") << "init model for " << op << std::endl;
-      d_models[op] = new AbsDef;
-      d_models_valid[op] = false;
-    }
-  }
-}
-
-void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ) {
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){
-      int v = getVariableId( q, n[i] );
-      Assert( v>=0 && v<(int)q[0].getNumChildren() );
-      eq_vars[v] = true;
-    }
-    collectEqVars( q, n[i], eq_vars );
-  }
-}
-
-void FirstOrderModelAbs::processInitializeQuantifier( Node q ) {
-  if( d_var_order.find( q )==d_var_order.end() ){
-    std::map< int, bool > eq_vars;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      eq_vars[i] = false;
-    }
-    collectEqVars( q, q[1], eq_vars );
-    for( unsigned r=0; r<2; r++ ){
-      for( std::map< int, bool >::iterator it = eq_vars.begin(); it != eq_vars.end(); ++it ){
-        if( it->second==(r==1) ){
-          d_var_index[q][it->first] = d_var_order[q].size();
-          d_var_order[q].push_back( it->first );
-        }
-      }
-    }
-  }
-}
-
-Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) {
-  return q[0][d_var_order[q][i]];
-}
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 7da5b2088..b96b42dc2 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -42,15 +42,10 @@ namespace quantifiers {
 
 class TermDb;
 
-class FirstOrderModelIG;
-
 namespace fmcheck {
   class FirstOrderModelFmc;
 }/* CVC4::theory::quantifiers::fmcheck namespace */
 
-class FirstOrderModelQInt;
-class FirstOrderModelAbs;
-
 struct IsStarAttributeId {};
 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 
@@ -94,10 +89,7 @@ class FirstOrderModel : public TheoryModel
  public:
   FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
 
-  virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
   virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
-  virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
-  virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; }
   /** assert quantifier */
   void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
@@ -172,11 +164,11 @@ class FirstOrderModel : public TheoryModel
   /** get variable id */
   std::map<Node, std::map<Node, int> > d_quant_var_id;
   /** process initialize model for term */
-  virtual void processInitializeModelForTerm(Node n) = 0;
+  virtual void processInitializeModelForTerm(Node n) {}
   /** process initialize quantifier */
   virtual void processInitializeQuantifier(Node q) {}
   /** process initialize */
-  virtual void processInitialize(bool ispre) = 0;
+  virtual void processInitialize(bool ispre) {}
 
  private:
   // list of inactive quantified formulas
@@ -193,85 +185,6 @@ class FirstOrderModel : public TheoryModel
   void computeModelBasisArgAttribute(Node n);
 };/* class FirstOrderModel */
 
-class FirstOrderModelIG : public FirstOrderModel
-{
- public:  // for Theory UF:
-  /** class for generating models for uninterpreted functions
-   *
-   * This implements the model construction from page 6 of Reynolds et al,
-   * "Quantifier Instantiation Techniques for Finite Model Finding in SMT",
-   * CADE 2013.
-   */
-  class UfModelTreeGenerator
-  {
-   public:
-    UfModelTreeGenerator() {}
-    ~UfModelTreeGenerator() {}
-    /** set default value */
-    void setDefaultValue(Node v) { d_default_value = v; }
-    /** set value */
-    void setValue(
-        TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true);
-    /** make model */
-    void makeModel(TheoryModel* m, uf::UfModelTree& tree);
-    /** reset */
-    void clear();
-
-   public:
-    /** the overall default value */
-    Node d_default_value;
-    /**
-     * Stores (required, ground) values in key, value pairs of the form
-     * ( P( a, b ), c ), which indicates P( a, b ) has value c in the model.
-     * The "non-ground" values indicate that the key has a "model-basis"
-     * variable, for example, ( P( _, b ), c ) indicates that P( x, b ) has the
-     * value b for any value of x.
-     */
-    std::map<Node, Node> d_set_values[2][2];
-    /** stores the set of non-ground keys in the above maps */
-    std::vector<Node> d_defaults;
-    /**
-     * Returns the term corresponding to the intersection of n1 and n2, if it
-     * exists, for example, for P( _, a ) and P( b, _ ), this method returns
-     * P( b, a ), where _ is the "model basis" variable. We take into account
-     * equality between arguments, so if a=b, then the intersection of P( a, a )
-     * and P( b, _ ) is P( a, a ).
-     */
-    Node getIntersection(TheoryModel* m, Node n1, Node n2, bool& isGround);
-  };
-  /** models for each UF operator */
-  std::map<Node, uf::UfModelTree> d_uf_model_tree;
-  /** model generators for each UF operator */
-  std::map<Node, 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 );
-//the following functions are for evaluating quantifier bodies
-public:
-  FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
-
-  FirstOrderModelIG* asFirstOrderModelIG() override { return this; }
-  // initialize the model
-  void processInitialize(bool ispre) override;
-  //for initialize model
-  void processInitializeModelForTerm(Node n) override;
-  /** reset evaluation */
-  void resetEvaluate();
-  /** evaluate functions */
-  int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
-  Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
-private:
-  //default evaluate term function
-  Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
-};/* class FirstOrderModelIG */
-
-
 namespace fmcheck {
 
 class Def;
@@ -301,36 +214,6 @@ class FirstOrderModelFmc : public FirstOrderModel
 
 }/* CVC4::theory::quantifiers::fmcheck namespace */
 
-class AbsDef;
-
-class FirstOrderModelAbs : public FirstOrderModel
-{
- public:
-  std::map< Node, AbsDef * > d_models;
-  std::map< Node, bool > d_models_valid;
-  std::map< TNode, unsigned > d_rep_id;
-  std::map< TypeNode, unsigned > d_domain;
-  std::map< Node, std::vector< int > > d_var_order;
-  std::map< Node, std::map< int, int > > d_var_index;
-
- private:
-  /** get current model value */
-  void processInitializeModelForTerm(Node n) override;
-  void processInitializeQuantifier(Node q) override;
-  void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
-  TNode getUsedRepresentative( TNode n );
-
- public:
-  FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
-  ~FirstOrderModelAbs() override;
-  FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; }
-  void processInitialize(bool ispre) override;
-  unsigned getRepresentativeId( TNode n );
-  bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
-  Node getFunctionValue(Node op, const char* argPrefix );
-  Node getVariable( Node q, unsigned i );
-};
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp
deleted file mode 100644
index f2b131f21..000000000
--- a/src/theory/quantifiers/fmf/ambqi_builder.cpp
+++ /dev/null
@@ -1,971 +0,0 @@
-/*********************                                                        */
-/*! \file ambqi_builder.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of abstract MBQI builder
- **/
-
-#include "theory/quantifiers/fmf/ambqi_builder.h"
-
-#include "base/cvc4_check.h"
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-
-using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-
-void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {
-  d_def.clear();
-  Assert( !fapps.empty() );
-  if( depth==fapps[0].getNumChildren() ){
-    //if( fapps.size()>1 ){
-    //  for( unsigned i=0; i<fapps.size(); i++ ){
-    //    std::cout << "...." << fapps[i] << " -> " << m->getRepresentativeId( fapps[i] ) << std::endl;
-    //  }
-    //}
-    //get representative in model for this term
-    d_value = m->getRepresentativeId( fapps[0] );
-    Assert( d_value!=val_none );
-  }else{
-    TypeNode tn = fapps[0][depth].getType();
-    std::map< unsigned, std::vector< TNode > > fapp_child;
-
-    //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
-    for( unsigned i=0; i<fapps.size(); i++ ){
-      unsigned r = m->getRepresentativeId( fapps[i][depth] );
-      Assert( r < 32 );
-      fapp_child[r].push_back( fapps[i] );
-    }
-
-    //do completion
-    std::map< unsigned, unsigned > fapp_child_index;
-    unsigned def = m->d_domain[ tn ];
-    unsigned minSize = fapp_child.begin()->second.size();
-    unsigned minSizeIndex = fapp_child.begin()->first;
-    for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
-      fapp_child_index[it->first] = ( 1 << it->first );
-      def = def & ~( 1 << it->first );
-      if( it->second.size()<minSize ){
-        minSize = it->second.size();
-        minSizeIndex = it->first;
-      }
-    }
-    fapp_child_index[minSizeIndex] |= def;
-    d_default = fapp_child_index[minSizeIndex];
-
-    //construct children
-    for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
-      Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : ";
-      const RepSet* rs = m->getRepSet();
-      debugPrintUInt("abs-model-debug",
-                     rs->getNumRepresentatives(tn),
-                     fapp_child_index[it->first]);
-      Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl;
-      d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 );
-    }
-  }
-}
-
-void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {
-  if( d_value==val_none && !d_def.empty() ){
-    //process the default
-    std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );
-    Assert( defd!=d_def.end() );
-    unsigned newDef = d_default;
-    std::vector< unsigned > to_erase;
-    defd->second.simplify( m, q, n, depth+1 );
-    int defVal = defd->second.d_value;
-    bool isConstant = ( defVal!=val_none );
-    //process each child
-    for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
-      if( it->first!=d_default ){
-        it->second.simplify( m, q, n, depth+1 );
-        if( it->second.d_value==defVal && it->second.d_value!=val_none ){
-          newDef = newDef | it->first;
-          to_erase.push_back( it->first );
-        }else{
-          isConstant = false;
-        }
-      }
-    }
-    if( !to_erase.empty() ){
-      //erase old default
-      int defVal = defd->second.d_value;
-      d_def.erase( d_default );
-      //set new default
-      d_default = newDef;
-      d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );
-      //erase redundant entries
-      for( unsigned i=0; i<to_erase.size(); i++ ){
-        d_def.erase( to_erase[i] );
-      }
-    }
-    //if constant, propagate the value upwards
-    if( isConstant ){
-      d_value = defVal;
-    }else{
-      d_value = val_none;
-    }
-  }
-}
-
-void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{
-  for( unsigned i=0; i<dSize; i++ ){
-    Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
-  }
-  //Trace(c) << "(";
-  //for( unsigned i=0; i<32; i++ ){
-  //  Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
-  //}
-  //Trace(c) << ")";
-}
-
-void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{
-  if( Trace.isOn(c) ){
-    if( depth==f.getNumChildren() ){
-      for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
-      Trace(c) << "V[" << d_value << "]" << std::endl;
-    }else{
-      TypeNode tn = f[depth].getType();
-      const RepSet* rs = m->getRepSet();
-      unsigned dSize = rs->getNumRepresentatives(tn);
-      Assert( dSize<32 );
-      for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){
-        for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
-        debugPrintUInt( c, dSize, it->first );
-        if( it->first==d_default ){
-          Trace(c) << "*";
-        }
-        if( it->second.d_value!=val_none ){
-          Trace(c) << " -> V[" << it->second.d_value << "]";
-        }
-        Trace(c) << std::endl;
-        it->second.debugPrint( c, m, f, depth+1 );
-      }
-    }
-  }
-}
-
-bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) {
-  if( inst==0 || !options::fmfOneInstPerRound() ){
-    if( d_value==1 ){
-      //instantiations are all true : ignore this
-      return true;
-    }else{
-      if( depth==q[0].getNumChildren() ){
-        if (qe->getInstantiate()->addInstantiation(q, terms, true))
-        {
-          Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
-          inst++;
-          return true;
-        }else{
-          Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;
-          //we are incomplete
-          return false;
-        }
-      }else{
-        bool osuccess = true;
-        TypeNode tn = m->getVariable( q, depth ).getType();
-        for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
-          //get witness term
-          unsigned index = 0;
-          bool success;
-          do {
-            success = false;
-            index = getId( it->first, index );
-            if( index<32 ){
-              const RepSet* rs = m->getRepSet();
-              Assert(index < rs->getNumRepresentatives(tn));
-              terms[m->d_var_order[q][depth]] =
-                  rs->getRepresentative(tn, index);
-              if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){
-                //if we are incomplete, and have not yet added an instantiation, keep trying
-                index++;
-                Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;
-              }else{
-                success = true;
-              }
-            }
-          }while( !qe->inConflict() && !success && index<32 );
-          //mark if we are incomplete
-          osuccess = osuccess && success;
-        }
-        return osuccess;
-      }
-    }
-  }else{
-    return true;
-  }
-}
-
-void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) {
-  if( depth==entry.size() ){
-    d_value = v;
-  }else{
-    d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 );
-    if( entry_def[depth] ){
-      d_default = entry[depth];
-    }
-  }
-}
-
-void AbsDef::get_defs( unsigned u, std::vector< AbsDef * >& defs ) {
-  for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
-    if( ( u & it->first )!=0 ){
-      Assert( (u & it->first)==u );
-      defs.push_back( &it->second );
-    }
-  }
-}
-
-void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth ) {
-  if( depth==q[0].getNumChildren() ){
-    Assert( defs.size()==1 );
-    d_value = defs[0]->d_value;
-  }else{
-    TypeNode tn = m->getVariable( q, depth ).getType();
-    unsigned def = m->d_domain[tn];
-    for( unsigned i=0; i<defs.size(); i++ ){
-      //process each simple child
-      for( std::map< unsigned, AbsDef >::iterator itd = defs[i]->d_def.begin(); itd != defs[i]->d_def.end(); ++itd ){
-        if( isSimple( itd->first ) && ( def & itd->first )!=0 ){
-          def &= ~( itd->first );
-          //process this value
-          std::vector< AbsDef * > cdefs;
-          for( unsigned j=0; j<defs.size(); j++ ){
-            defs[j]->get_defs( itd->first, cdefs );
-          }
-          d_def[itd->first].construct_normalize( m, q, cdefs, depth+1 );
-          if( def==0 ){
-            d_default = itd->first;
-            break;
-          }
-        }
-      }
-      if( def==0 ){
-        break;
-      }
-    }
-    if( def!=0 ){
-      d_default = def;
-      //process the default
-      std::vector< AbsDef * > cdefs;
-      for( unsigned j=0; j<defs.size(); j++ ){
-        defs[j]->get_defs( d_default, cdefs );
-      }
-      d_def[d_default].construct_normalize( m, q, cdefs, depth+1 );
-    }
-  }
-}
-
-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {
-  d_value = v;
-  if( depth<n.getNumChildren() ){
-    TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();
-    unsigned dom = m->d_domain[tn] ;
-    d_def[dom].construct_def_entry( m, q, n, v, depth+1 );
-    d_default = dom;
-  }
-}
-
-void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q,
-                             std::vector< unsigned >& entry, std::vector< bool >& entry_def,
-                             std::vector< int >& terms, std::map< unsigned, int >& vchildren,
-                             AbsDef * a, unsigned depth ) {
-  if( depth==terms.size() ){
-    if( Trace.isOn("ambqi-check-debug2") ){
-      Trace("ambqi-check-debug2") << "Add entry ( ";
-      const RepSet* rs = m->getRepSet();
-      for( unsigned i=0; i<entry.size(); i++ ){
-        unsigned dSize =
-            rs->getNumRepresentatives(m->getVariable(q, i).getType());
-        debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );
-        Trace("ambqi-check-debug2") << " ";
-      }
-      Trace("ambqi-check-debug2") << ")" << std::endl;
-    }
-    a->construct_entry( entry, entry_def, d_value );
-  }else{
-    unsigned id;
-    if( terms[depth]==val_none ){
-      //a variable
-      std::map< unsigned, int >::iterator itv = vchildren.find( depth );
-      Assert( itv!=vchildren.end() );
-      unsigned prev_v = entry[itv->second];
-      bool prev_vd = entry_def[itv->second];
-      for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
-        entry[itv->second] = it->first & prev_v;
-        entry_def[itv->second] = ( it->first==d_default ) && prev_vd;
-        if( entry[itv->second]!=0 ){
-          it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );
-        }
-      }
-      entry[itv->second] = prev_v;
-      entry_def[itv->second] = prev_vd;
-    }else{
-      id = (unsigned)terms[depth];
-      Assert( id<32 );
-      unsigned fid = 1 << id;
-      std::map< unsigned, AbsDef >::iterator it = d_def.find( fid );
-      if( it!=d_def.end() ){
-        it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );
-      }else{
-        d_def[d_default].apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );
-      }
-    }
-  }
-}
-
-void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) {
-  if( depth==q[0].getNumChildren() ){
-    Assert( currv!=val_none );
-    d_value = currv;
-  }else{
-    TypeNode tn = m->getVariable( q, depth ).getType();
-    unsigned dom = m->d_domain[tn];
-    int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none );
-    if( vindex==val_none ){
-      d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
-      d_default = dom;
-    }else{
-      Assert( currv==val_none );
-      if( curr==val_none ){
-        unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
-        Assert( numReps < 32 );
-        for( unsigned i=0; i<numReps; i++ ){
-          curr = 1 << i;
-          d_def[curr].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
-        }
-        d_default = curr;
-      }else{
-        d_def[curr].construct_var_eq( m, q, v1, v2, curr, 1, depth+1 );
-        dom = dom & ~curr;
-        d_def[dom].construct_var_eq( m, q, v1, v2, curr, 0, depth+1 );
-        d_default = dom;
-      }
-    }
-  }
-}
-
-void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth ) {
-  if( depth==q[0].getNumChildren() ){
-    Assert( currv!=val_none );
-    d_value = currv;
-  }else{
-    TypeNode tn = m->getVariable( q, depth ).getType();
-    if( v==depth ){
-      const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
-      CVC4_CHECK(numReps > 0 && numReps < 32);
-      for( unsigned i=0; i<numReps; i++ ){
-        d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
-      }
-      d_default = 1 << (numReps - 1);
-    }else{
-      unsigned dom = m->d_domain[tn];
-      d_def[dom].construct_var( m, q, v, currv, depth+1 );
-      d_default = dom;
-    }
-  }
-}
-
-void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
-                                std::map< unsigned, AbsDef * >& children,
-                                std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
-                                std::vector< unsigned >& entry, std::vector< bool >& entry_def ) {
-  const RepSet* rs = m->getRepSet();
-  if( n.getKind()==OR || n.getKind()==AND ){
-    // short circuiting
-    for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
-      if( ( it->second->d_value==0 && n.getKind()==AND ) ||
-          ( it->second->d_value==1 && n.getKind()==OR ) ){
-        //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl;
-        unsigned count = q[0].getNumChildren() - entry.size();
-        for( unsigned i=0; i<count; i++ ){
-          entry.push_back( m->d_domain[m->getVariable( q, entry.size() ).getType()] );
-          entry_def.push_back( true );
-        }
-        construct_entry( entry, entry_def, it->second->d_value );
-        for( unsigned i=0; i<count; i++ ){
-          entry.pop_back();
-          entry_def.pop_back();
-        }
-        return;
-      }
-    }
-  }
-  if( entry.size()==q[0].getNumChildren() ){
-    if( f ){
-      if( Trace.isOn("ambqi-check-debug2") ){
-        for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
-        Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl;
-      }
-      //we are composing with an uninterpreted function
-      std::vector< int > values;
-      values.resize( n.getNumChildren(), val_none );
-      for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
-        values[it->first] = it->second->d_value;
-      }
-      for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
-        values[it->first] = it->second;
-      }
-      //look up value(s)
-      f->apply_ucompose( m, q, entry, entry_def, values, vchildren, this );
-    }else{
-      bool incomplete = false;
-      //we are composing with an interpreted function
-      std::vector< TNode > values;
-      values.resize( n.getNumChildren(), TNode::null() );
-      for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
-        Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value;
-        if( it->second->d_value>=0 ){
-          if (it->second->d_value
-              >= (int)rs->getNumRepresentatives(n[it->first].getType()))
-          {
-            std::cout << it->second->d_value << " " << n[it->first] << " "
-                      << n[it->first].getType() << " "
-                      << rs->getNumRepresentatives(n[it->first].getType())
-                      << std::endl;
-          }
-          Assert(it->second->d_value
-                 < (int)rs->getNumRepresentatives(n[it->first].getType()));
-          values[it->first] = rs->getRepresentative(n[it->first].getType(),
-                                                    it->second->d_value);
-        }else{
-          incomplete = true;
-        }
-        Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl;
-      }
-      for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
-        Trace("ambqi-check-debug2") << "   basic :  " << it->first << " : " << it->second;
-        if( it->second>=0 ){
-          Assert(it->second
-                 < (int)rs->getNumRepresentatives(n[it->first].getType()));
-          values[it->first] =
-              rs->getRepresentative(n[it->first].getType(), it->second);
-        }else{
-          incomplete = true;
-        }
-        Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl;
-      }
-      Assert( vchildren.empty() );
-      if( incomplete ){
-        Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl;
-
-        //if a child is unknown, we must return unknown
-        construct_entry( entry, entry_def, val_unk );
-      }else{
-        if( Trace.isOn("ambqi-check-debug2") ){
-          for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
-          Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";
-          for( unsigned i=0; i<values.size(); i++ ){
-            Assert( !values[i].isNull() );
-            Trace("ambqi-check-debug2") << values[i] << " ";
-          }
-          Trace("ambqi-check-debug2") << ")..." << std::endl;
-        }
-        //evaluate
-        Node vv = NodeManager::currentNM()->mkNode( n.getKind(), values );
-        vv = Rewriter::rewrite( vv );
-        int v = m->getRepresentativeId( vv );
-        construct_entry( entry, entry_def, v );
-      }
-    }
-  }else{
-    //take product of arguments
-    TypeNode tn = m->getVariable( q, entry.size() ).getType();
-    Assert( m->isValidType( tn ) );
-    unsigned def = m->d_domain[tn];
-    if( Trace.isOn("ambqi-check-debug2") ){
-      for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
-      Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;
-    }
-    for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
-      Assert( it->second!=NULL );
-      //process each child
-      for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){
-        if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){
-          def &= ~( itd->first );
-          //process this value
-          std::map< unsigned, AbsDef * > cchildren;
-          for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){
-            Assert( it2->second!=NULL );
-            std::map< unsigned, AbsDef >::iterator itdf = it2->second->d_def.find( itd->first );
-            if( itdf!=it2->second->d_def.end() ){
-              cchildren[it2->first] = &itdf->second;
-            }else{
-              Assert( it2->second->getDefault()!=NULL );
-              cchildren[it2->first] = it2->second->getDefault();
-            }
-          }
-          if( Trace.isOn("ambqi-check-debug2") ){
-            for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
-            Trace("ambqi-check-debug2") << "...process : ";
-            debugPrintUInt("ambqi-check-debug2",
-                           rs->getNumRepresentatives(tn),
-                           itd->first);
-            Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl;
-          }
-          entry.push_back( itd->first );
-          entry_def.push_back( def==0 );
-          construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def );
-          entry_def.pop_back();
-          entry.pop_back();
-          if( def==0 ){
-            break;
-          }
-        }
-      }
-      if( def==0 ){
-        break;
-      }
-    }
-    if( def!=0 ){
-      if( Trace.isOn("ambqi-check-debug2") ){
-        for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
-        Trace("ambqi-check-debug2") << "Make default argument" << std::endl;
-      }
-      std::map< unsigned, AbsDef * > cdchildren;
-      for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
-        Assert( it->second->getDefault()!=NULL );
-        cdchildren[it->first] = it->second->getDefault();
-      }
-      if( Trace.isOn("ambqi-check-debug2") ){
-        for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
-        Trace("ambqi-check-debug2") << "...process default : ";
-        debugPrintUInt(
-            "ambqi-check-debug2", rs->getNumRepresentatives(tn), def);
-        Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl;
-      }
-      entry.push_back( def );
-      entry_def.push_back( true );
-      construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def );
-      entry_def.pop_back();
-      entry.pop_back();
-    }
-  }
-}
-
-bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
-                        std::map< unsigned, AbsDef * >& children,
-                        std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
-                        int varChCount ) {
-  if( Trace.isOn("ambqi-check-debug3") ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Trace("ambqi-check-debug3") << i << " : ";
-      Trace("ambqi-check-debug3") << ((children.find( i )!=children.end()) ? "X" : ".");
-      if( bchildren.find( i )!=bchildren.end() ){
-        Trace("ambqi-check-debug3") << bchildren[i];
-      }else{
-        Trace("ambqi-check-debug3") << ".";
-      }
-      if( vchildren.find( i )!=vchildren.end() ){
-        Trace("ambqi-check-debug3") << vchildren[i];
-      }else{
-        Trace("ambqi-check-debug3") << ".";
-      }
-      Trace("ambqi-check-debug3") << std::endl;
-    }
-    Trace("ambqi-check-debug3") << "varChCount : " << varChCount << std::endl;
-  }
-  if( varChCount==0 || f ){
-    //short-circuit
-    if( n.getKind()==AND || n.getKind()==OR ){
-      for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){
-        if( ( it->second==0 && n.getKind()==AND ) ||
-            ( it->second==1 && n.getKind()==OR ) ){
-          construct_def_entry( m, q, q[0], it->second );
-          return true;
-        }
-      }
-    }
-    Trace("ambqi-check-debug2") << "Construct compose..." << std::endl;
-    std::vector< unsigned > entry;
-    std::vector< bool > entry_def;
-    if( f && varChCount>0 ){
-      AbsDef unorm;
-      unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
-      //normalize
-      std::vector< AbsDef* > defs;
-      defs.push_back( &unorm );
-      construct_normalize( m, q, defs );
-    }else{
-      construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
-    }
-    Assert( is_normalized() );
-    return true;
-  }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
-    Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;
-    //expand the variable based on its finite domain
-    AbsDef a;
-    a.construct_var( m, q, vchildren.begin()->second, val_none );
-    children[vchildren.begin()->first] = &a;
-    vchildren.clear();
-    std::vector< unsigned > entry;
-    std::vector< bool > entry_def;
-    Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl;
-    construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
-    return true;
-  }else if( varChCount==2 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
-    Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl;
-    //efficient expansion of the equality
-    construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none );
-    return true;
-  }else{
-    return false;
-  }
-}
-
-void AbsDef::negate() {
-  for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
-    it->second.negate();
-  }
-  if( d_value==0 ){
-    d_value = 1;
-  }else if( d_value==1 ){
-    d_value = 0;
-  }
-}
-
-Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {
-  const RepSet* rs = m->getRepSet();
-  if( depth==vars.size() ){
-    TypeNode tn = op.getType();
-    if( tn.getNumChildren()>0 ){
-      tn = tn[tn.getNumChildren() - 1];
-    }
-    if( d_value>=0 ){
-      Assert(d_value < (int)rs->getNumRepresentatives(tn));
-      if( tn.isBoolean() ){
-        return NodeManager::currentNM()->mkConst( d_value==1 );
-      }else{
-        return rs->getRepresentative(tn, d_value);
-      }
-    }else{
-      return Node::null();
-    }
-  }else{
-    TypeNode tn = vars[depth].getType();
-    Node curr;
-    curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 );
-    for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
-      if( it->first!=d_default ){
-        unsigned id = getId( it->first );
-        Assert(id < rs->getNumRepresentatives(tn));
-        TNode n = rs->getRepresentative(tn, id);
-        Node fv = it->second.getFunctionValue( m, op, vars, depth+1 );
-        if( !curr.isNull() && !fv.isNull() ){
-          curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr );
-        }else{
-          curr = Node::null();
-        }
-      }
-    }
-    return curr;
-  }
-}
-
-bool AbsDef::isSimple( unsigned n ) {
-  return (n & (n - 1))==0;
-}
-
-unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {
-  Assert( n!=0 );
-  while( (n & ( 1 << start )) == 0 ){
-    start++;
-    if( start==end ){
-      return start;
-    }
-  }
-  return start;
-}
-
-Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) {
-  std::vector< unsigned > iargs;
-  for( unsigned i=0; i<args.size(); i++ ){
-    unsigned v = 1 << m->getRepresentativeId( args[i] );
-    iargs.push_back( v );
-  }
-  return evaluate( m, retTyp, iargs, 0 );
-}
-
-Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) {
-  if( d_value!=val_none ){
-    if( d_value==val_unk ){
-      return Node::null();
-    }else{
-      const RepSet* rs = m->getRepSet();
-      Assert(d_value >= 0 && d_value < (int)rs->getNumRepresentatives(retTyp));
-      return rs->getRepresentative(retTyp, d_value);
-    }
-  }else{
-    std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );
-    if( it==d_def.end() ){
-      return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 );
-    }else{
-      return it->second.evaluate( m, retTyp, iargs, depth+1 );
-    }
-  }
-}
-
-bool AbsDef::is_normalized() {
-  for( std::map< unsigned, AbsDef >::iterator it1 = d_def.begin(); it1 != d_def.end(); ++it1 ){
-    if( !it1->second.is_normalized() ){
-      return false;
-    }
-    for( std::map< unsigned, AbsDef >::iterator it2 = d_def.begin(); it2 != d_def.end(); ++it2 ){
-      if( it1->first!=it2->first && (( it1->first & it2->first )!=0) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) :
-QModelBuilder( c, qe ){
-  d_true = NodeManager::currentNM()->mkConst( true );
-  d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-
-//------------------------model construction----------------------------
-
-bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
-  if (!m->areFunctionValuesEnabled())
-  {
-    // nothing to do if no functions
-    return true;
-  }
-  Trace("ambqi-debug") << "process build model " << std::endl;
-  FirstOrderModel* f = (FirstOrderModel*)m;
-  FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
-  RepSet* rs = m->getRepSetPtr();
-  fm->initialize();
-  //process representatives
-  fm->d_rep_id.clear();
-  fm->d_domain.clear();
-
-  //initialize boolean sort
-  TypeNode b = d_true.getType();
-  rs->d_type_reps[b].clear();
-  rs->d_type_reps[b].push_back(d_false);
-  rs->d_type_reps[b].push_back(d_true);
-  fm->d_rep_id[d_false] = 0;
-  fm->d_rep_id[d_true] = 1;
-
-  //initialize unintpreted sorts
-  Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
-  for (std::map<TypeNode, std::vector<Node> >::iterator it =
-           rs->d_type_reps.begin();
-       it != rs->d_type_reps.end();
-       ++it)
-  {
-    if( it->first.isSort() ){
-      Assert( !it->second.empty() );
-      //set the domain
-      fm->d_domain[it->first] = 0;
-      Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        if( i<32 ){
-          fm->d_domain[it->first] |= ( 1 << i );
-        }
-        Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
-        fm->d_rep_id[it->second[i]] = i;
-      }
-      if( it->second.size()>=32 ){
-        fm->d_domain.erase( it->first );
-      }
-    }
-  }
-
-  Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
-  //construct the models for functions
-  for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-    Node f = it->first;
-    Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
-    //reset the model
-    it->second->clear();
-    //get all (non-redundant) f-applications
-    std::vector< TNode > fapps;
-    Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
-    std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f );
-    if( itut!=fm->d_uf_terms.end() ){
-      for( size_t i=0; i<itut->second.size(); i++ ){
-        Node n = itut->second[i];
-        // only consider unique up to congruence (in model equality engine)?
-        Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
-        fapps.push_back( n );
-      }
-    }
-    if( fapps.empty() ){
-      //choose arbitrary value
-      Node mbt = fm->getModelBasisOpTerm(f);
-      Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
-      fapps.push_back( mbt );
-    }
-    bool fValid = true;
-    for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
-      if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
-        Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
-        Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
-        fValid = false;
-        break;
-      }
-    }
-    fm->d_models_valid[f] = fValid;
-    if( fValid ){
-      //construct the ambqi model
-      it->second->construct_func( fm, fapps );
-      Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
-      it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
-      Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
-      it->second->simplify( fm, TNode::null(), fapps[0] );
-      Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
-      it->second->debugPrint("ambqi-model", fm, fapps[0] );
-
-/*
-      if( Debug.isOn("ambqi-model-debug") ){
-        for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
-          Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
-          Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
-          Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
-        }
-      }
-*/
-    }
-  }
-  Trace("ambqi-model") << "Construct model representation..." << std::endl;
-  //make function values
-  for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-    if( it->first.getType().getNumChildren()>1 ){
-      Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
-      Node f_def = fm->getFunctionValue( it->first, "$x" );
-      m->assignFunctionDefinition( it->first, f_def );
-    }
-  }
-  Assert( d_addedLemmas==0 );
-  return TheoryEngineModelBuilder::processBuildModel( m );
-}
-
-
-//--------------------model checking---------------------------------------
-
-//do exhaustive instantiation
-int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
-  Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
-  if (effort==0) {
-    FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
-    bool quantValid = true;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      if( !fma->isValidType( q[0][i].getType() ) ){
-        quantValid = false;
-        Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl;
-        break;
-      }
-    }
-    if( quantValid ){
-      Trace("ambqi-check") << "Compute interpretation..." << std::endl;
-      AbsDef ad;
-      doCheck( fma, q, ad, q[1] );
-      //now process entries
-      Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas << std::endl;
-      Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;
-      ad.debugPrint( "ambqi-inst", fma, q[0] );
-      Trace("ambqi-inst") << std::endl;
-      Trace("ambqi-check") << "Add instantiations..." << std::endl;
-      int lem = 0;
-      quantValid = ad.addInstantiations( fma, d_qe, q, lem );
-      Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;
-      if( lem>0 ){
-        //if we were incomplete but added at least one lemma, we are ok
-        quantValid = true;
-      }
-      d_addedLemmas += lem;
-      Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl;
-    }
-    return quantValid ? 1 : 0;
-  }else{
-    return 1;
-  }
-}
-
-bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
-  Assert( n.getKind()!=FORALL );
-  if( n.getKind()==NOT && n[0].getKind()!=FORALL ){
-    doCheck( m, q, ad, n[0] );
-    ad.negate();
-    return true;
-  }else{
-    std::map< unsigned, AbsDef > children;
-    std::map< unsigned, int > bchildren;
-    std::map< unsigned, int > vchildren;
-    int varChCount = 0;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( n[i].getKind()==FORALL ){
-        bchildren[i] = AbsDef::val_unk;
-      }else if( n[i].getKind() == BOUND_VARIABLE ){
-        varChCount++;
-        vchildren[i] = m->d_var_index[q][ m->getVariableId( q, n[i] ) ];
-        //vchildren[i] = m->getVariableId( q, n[i] );
-      }else if( m->hasTerm( n[i] ) ){
-        bchildren[i] = m->getRepresentativeId( n[i] );
-      }else{
-        if( !doCheck( m, q, children[i], n[i] ) ){
-          bchildren[i] = AbsDef::val_unk;
-          children.erase( i );
-        }
-      }
-    }
-    //convert to pointers
-    std::map< unsigned, AbsDef * > pchildren;
-    for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){
-      pchildren[it->first] = &it->second;
-    }
-    //construct the interpretation
-    Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
-    if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
-      Node op;
-      if( n.getKind() == APPLY_UF ){
-        op = n.getOperator();
-      }else{
-        op = n;
-      }
-      //uninterpreted compose
-      if( m->d_models_valid[op] ){
-        ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount );
-      }else{
-        Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl;
-        return false;
-      }
-    }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){
-      Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl;
-      return false;
-    }
-    Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;
-    ad.debugPrint("ambqi-check-try", m, q[0] );
-    ad.simplify( m, q, q[0] );
-    Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;
-    ad.debugPrint("ambqi-check-debug", m, q[0] );
-    Trace("ambqi-check-debug") << std::endl;
-    return true;
-  }
-}
-
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h
deleted file mode 100644
index b052e0985..000000000
--- a/src/theory/quantifiers/fmf/ambqi_builder.h
+++ /dev/null
@@ -1,105 +0,0 @@
-/*********************                                                        */
-/*! \file ambqi_builder.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Abstract MBQI model builder class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef ABSTRACT_MBQI_BUILDER
-#define ABSTRACT_MBQI_BUILDER
-
-#include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class FirstOrderModelAbs;
-
-//representiation of function and term interpretations
-class AbsDef
-{
-private:
-  bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth );
-  void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
-                          std::map< unsigned, AbsDef * >& children,
-                          std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
-                          std::vector< unsigned >& entry, std::vector< bool >& entry_def );
-  void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
-  void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
-  void apply_ucompose( FirstOrderModelAbs * m, TNode q,
-                       std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
-                       std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
-  void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 );
-  void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 );
-  void get_defs( unsigned u, std::vector< AbsDef * >& defs );
-  void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 );
-public:
-  enum {
-    val_none = -1,
-    val_unk = -2,
-  };
-  AbsDef() : d_default( 0 ), d_value( -1 ){}
-  std::map< unsigned, AbsDef > d_def;
-  unsigned d_default;
-  int d_value;
-
-  void clear() { d_def.clear(); d_default = 0; d_value = -1; }
-  AbsDef * getDefault() { return &d_def[d_default]; }
-  void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
-  void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
-  void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
-  void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
-  int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
-    std::vector< Node > terms;
-    terms.resize( q[0].getNumChildren() );
-    return addInstantiations( m, qe, q, terms, inst, 0 );
-  }
-  bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
-                  std::map< unsigned, AbsDef * >& children,
-                  std::map< unsigned, int >& bchildren,
-                  std::map< unsigned, int >& vchildren,
-                  int varChCount );
-  void negate();
-  Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
-  static bool isSimple( unsigned n );
-  static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
-  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
-  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
-  //for debugging
-  bool is_normalized();
-};
-
-class AbsMbqiBuilder : public QModelBuilder
-{
-  friend class AbsDef;
-private:
-  Node d_true;
-  Node d_false;
-  bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
-public:
-  AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
-
-  //process build model
-  bool processBuildModel(TheoryModel* m) override;
-  //do exhaustive instantiation
-  int doExhaustiveInstantiation(FirstOrderModel* fm,
-                                Node q,
-                                int effort) override;
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index c03fc7a32..8ef30fc4d 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -143,687 +143,3 @@ void QModelBuilder::debugModel( TheoryModel* m ){
     }
   }
 }
-
-bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
-{
-  if (argIndex < n.getNumChildren())
-  {
-    Node r;
-    if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
-      r = n[ argIndex ];
-    }else{
-      r = fm->getRepresentative( n[ argIndex ] );
-    }
-    std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
-    if( it==d_data.end() ){
-      d_data[r].addTerm(fm, n, argIndex + 1);
-      return true;
-    }else{
-      return it->second.addTerm(fm, n, argIndex + 1);
-    }
-  }else{
-    return false;
-  }
-}
-
-void QModelBuilderIG::UfModelPreferenceData::setValuePreference(Node q,
-                                                                Node r,
-                                                                bool isPro)
-{
-  if (std::find(d_values.begin(), d_values.end(), r) == d_values.end())
-  {
-    d_values.push_back(r);
-  }
-  int index = isPro ? 0 : 1;
-  if (std::find(
-          d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), q)
-      == d_value_pro_con[index][r].end())
-  {
-    d_value_pro_con[index][r].push_back(q);
-  }
-}
-
-Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue(
-    Node defaultTerm, TheoryModel* m)
-{
-  Node defaultVal;
-  double maxScore = -1;
-  for (size_t i = 0, size = d_values.size(); i < size; i++)
-  {
-    Node v = d_values[i];
-    double score = (1.0 + static_cast<double>(d_value_pro_con[0][v].size()))
-                   / (1.0 + static_cast<double>(d_value_pro_con[1][v].size()));
-    Debug("fmf-model-cons-debug") << "  - score( ";
-    Debug("fmf-model-cons-debug") << m->getRepresentative(v);
-    Debug("fmf-model-cons-debug") << " ) = " << score << std::endl;
-    if (score > maxScore)
-    {
-      defaultVal = v;
-      maxScore = score;
-    }
-  }
-  if (maxScore < 1.0)
-  {
-    // consider finding another value, if possible
-    Debug("fmf-model-cons-debug")
-        << "Poor choice for default value, score = " << maxScore << std::endl;
-    TypeNode tn = defaultTerm.getType();
-    Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values);
-    if (!newDefaultVal.isNull())
-    {
-      defaultVal = newDefaultVal;
-      Debug("fmf-model-cons-debug") << "-> Change default value to ";
-      Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
-      Debug("fmf-model-cons-debug") << std::endl;
-    }
-    else
-    {
-      Debug("fmf-model-cons-debug")
-          << "-> Could not find arbitrary element of type "
-          << tn[tn.getNumChildren() - 1] << std::endl;
-      Debug("fmf-model-cons-debug") << "      Excluding: " << d_values;
-      Debug("fmf-model-cons-debug") << std::endl;
-    }
-  }
-  // get the default term (this term must be defined non-ground in model)
-  Debug("fmf-model-cons-debug") << "  Choose ";
-  Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
-  Debug("fmf-model-cons-debug")
-      << " as default value (" << defaultTerm << ")" << std::endl;
-  Debug("fmf-model-cons-debug")
-      << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size()
-      << std::endl;
-  Debug("fmf-model-cons-debug")
-      << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size()
-      << std::endl;
-  return defaultVal;
-}
-
-QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
-    : QModelBuilder(c, qe),
-      d_didInstGen(false),
-      d_numQuantSat(0),
-      d_numQuantInstGen(0),
-      d_numQuantNoInstGen(0),
-      d_numQuantNoSelForm(0),
-      d_instGenMatches(0) {}
-
-/*
-Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
-  return n;
-}
-*/
-
-bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
-  if (!m->areFunctionValuesEnabled())
-  {
-    // nothing to do if no functions
-    return true;
-  }
-  FirstOrderModel* f = (FirstOrderModel*)m;
-  FirstOrderModelIG* fm = f->asFirstOrderModelIG();
-  Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
-  d_didInstGen = false;
-  //reset the internal information
-  reset( fm );
-  //only construct first order model if optUseModel() is true
-  if( optUseModel() ){
-    Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
-    //check if any quantifiers are un-initialized
-    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node q = fm->getAssertedQuantifier( i );
-      if( d_qe->getModel()->isQuantifierActive( q ) ){
-        int lems = initializeQuantifier(q, q, f);
-        d_statistics.d_init_inst_gen_lemmas += lems;
-        d_addedLemmas += lems;
-        if( d_qe->inConflict() ){
-          break;
-        }
-      }
-    }
-    if( d_addedLemmas>0 ){
-      Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
-      return false;
-    }else{
-      Assert( !d_qe->inConflict() );
-      //initialize model
-      fm->initialize();
-      //analyze the functions
-      Trace("model-engine-debug") << "Analyzing model..." << std::endl;
-      analyzeModel( fm );
-      //analyze the quantifiers
-      Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
-      d_uf_prefs.clear();
-      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node q = fm->getAssertedQuantifier( i );
-        analyzeQuantifier( fm, q );
-      }
-
-      //if applicable, find exceptions to model via inst-gen
-      if( options::fmfInstGen() ){
-        d_didInstGen = true;
-        d_instGenMatches = 0;
-        d_numQuantSat = 0;
-        d_numQuantInstGen = 0;
-        d_numQuantNoInstGen = 0;
-        d_numQuantNoSelForm = 0;
-        //now, see if we know that any exceptions via InstGen exist
-        Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
-        for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-          Node f = fm->getAssertedQuantifier( i );
-          if( d_qe->getModel()->isQuantifierActive( f ) ){
-            int lems = doInstGen( fm, f );
-            d_statistics.d_inst_gen_lemmas += lems;
-            d_addedLemmas += lems;
-            //temporary
-            if( lems>0 ){
-              d_numQuantInstGen++;
-            }else if( hasInstGen( f ) ){
-              d_numQuantNoInstGen++;
-            }else{
-              d_numQuantNoSelForm++;
-            }
-            if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
-              break;
-            }
-          }else{
-            d_numQuantSat++;
-          }
-        }
-        Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
-        Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
-        Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
-        if( Trace.isOn("model-engine") ){
-          if( d_addedLemmas>0 ){
-            Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
-          }else{
-            Trace("model-engine") << "No InstGen lemmas..." << std::endl;
-          }
-        }
-      }
-      //construct the model if necessary
-      if( d_addedLemmas==0 ){
-        //if no immediate exceptions, build the model
-        //  this model will be an approximation that will need to be tested via exhaustive instantiation
-        Trace("model-engine-debug") << "Building model..." << std::endl;
-        //build model for UF
-        for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-          Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
-          constructModelUf( fm, it->first );
-        }
-        Trace("model-engine-debug") << "Done building models." << std::endl;
-      }else{
-        return false;
-      }
-    }
-  }
-  //update models
-  for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-    it->second.update( fm );
-    Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
-    //construct function values
-    Node f_def = it->second.getFunctionValue( "$x" );
-    fm->assignFunctionDefinition( it->first, f_def );
-  }
-  Assert( d_addedLemmas==0 );
-  return TheoryEngineModelBuilder::processBuildModel( m );
-}
-
-int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
-{
-  if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
-    //create the basis match if necessary
-    if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
-      Trace("inst-fmf-init") << "Initialize " << f << std::endl;
-      //add the model basis instantiation
-      // This will help produce the necessary information for model completion.
-      // We do this by extending distinguish ground assertions (those
-      //   containing terms with "model basis" attribute) to hold for all cases.
-
-      ////first, check if any variables are required to be equal
-      //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
-      //    it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
-      //  Node n = it->first;
-      //  if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){
-      //    Notice() << "Unhandled phase req: " << n << std::endl;
-      //  }
-      //}
-      d_quant_basis_match[f] = InstMatch( f );
-      for (unsigned j = 0; j < f[0].getNumChildren(); j++)
-      {
-        Node t = fm->getModelBasisTerm(f[0][j].getType());
-        //calculate the basis match for f
-        d_quant_basis_match[f].setValue( j, t );
-      }
-      ++(d_statistics.d_num_quants_init);
-    }
-    //try to add it
-    Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
-    //add model basis instantiation
-    if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f]))
-    {
-      d_quant_basis_match_added[f] = true;
-      return 1;
-    }else{
-      //shouldn't happen usually, but will occur if x != y is a required literal for f.
-      //Notice() << "No model basis for " << f << std::endl;
-      d_quant_basis_match_added[f] = false;
-    }
-  }
-  return 0;
-}
-
-void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
-  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
-  d_uf_model_constructed.clear();
-  //determine if any functions are constant
-  for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
-    Node op = it->first;
-    std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
-    if( itut!=fmig->d_uf_terms.end() ){
-      for( size_t i=0; i<itut->second.size(); i++ ){
-        Node n = fmig->d_uf_terms[op][i];
-        //for calculating if op is constant
-        Node v = fmig->getRepresentative( n );
-        if( i==0 ){
-          d_uf_prefs[op].d_const_val = v;
-        }else if( v!=d_uf_prefs[op].d_const_val ){
-          d_uf_prefs[op].d_const_val = Node::null();
-          break;
-        }
-      }
-    }
-    if( !d_uf_prefs[op].d_const_val.isNull() ){
-      fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
-      fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
-      Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
-      Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val;
-      Debug("fmf-model-cons") << std::endl;
-      d_uf_model_constructed[op] = true;
-    }else{
-      d_uf_model_constructed[op] = false;
-    }
-  }
-}
-
-bool QModelBuilderIG::hasConstantDefinition( Node n ){
-  Node lit = n.getKind()==NOT ? n[0] : n;
-  if( lit.getKind()==APPLY_UF ){
-    Node op = lit.getOperator();
-    if( !d_uf_prefs[op].d_const_val.isNull() ){
-      return true;
-    }
-  }
-  return false;
-}
-
-QModelBuilderIG::Statistics::Statistics()
-    : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
-      d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers",
-                                0),
-      d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0),
-      d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0)
-{
-  smtStatisticsRegistry()->registerStat(&d_num_quants_init);
-  smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
-  smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
-}
-
-QModelBuilderIG::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_num_quants_init);
-  smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
-  smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
-}
-
-//do exhaustive instantiation
-int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
-  if( optUseModel() ){
-    QRepBoundExt qrbe(d_qe);
-    RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
-    if( riter.setQuantifier( f ) ){
-      FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
-      Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
-      fmig->resetEvaluate();
-      Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
-      EqualityQuery* qy = d_qe->getEqualityQuery();
-      Instantiate* inst = d_qe->getInstantiate();
-      TermUtil* util = d_qe->getTermUtil();
-      while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
-        d_triedLemmas++;
-        if( Debug.isOn("inst-fmf-ei-debug") ){
-          for( int i=0; i<(int)riter.d_index.size(); i++ ){
-            Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl;
-          }
-        }
-        int eval = 0;
-        int depIndex;
-        //see if instantiation is already true in current model
-        if( Debug.isOn("fmf-model-eval") ){
-          Debug("fmf-model-eval") << "Evaluating ";
-          riter.debugPrintSmall("fmf-model-eval");
-          Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
-        }
-        //if evaluate(...)==1, then the instantiation is already true in the model
-        //  depIndex is the index of the least significant variable that this evaluation relies upon
-        depIndex = riter.getNumTerms()-1;
-        Debug("fmf-model-eval") << "We will evaluate "
-                                << util->getInstConstantBody(f) << std::endl;
-        eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter);
-        if( eval==1 ){
-          Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
-        }else{
-          Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
-        }
-        if( eval==1 ){
-          //instantiation is already true -> skip
-          riter.incrementAtIndex(depIndex);
-        }else{
-          //instantiation was not shown to be true, construct the match
-          InstMatch m( f );
-          for (unsigned i = 0; i < riter.getNumTerms(); i++)
-          {
-            m.set(qy, i, riter.getCurrentTerm(i));
-          }
-          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
-          //add as instantiation
-          if (inst->addInstantiation(f, m, true))
-          {
-            d_addedLemmas++;
-            if( d_qe->inConflict() ){
-              break;
-            }
-            //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
-            if( eval==-1 ){
-              riter.incrementAtIndex(depIndex);
-            }else{
-              riter.increment();
-            }
-          }else{
-            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
-            riter.increment();
-          }
-        }
-      }
-      //print debugging information
-      Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
-      if( d_addedLemmas>1000 ){
-        Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-        Trace("model-engine-warn") << "   Inst Tried: " << d_triedLemmas << std::endl;
-        Trace("model-engine-warn") << "   Inst Added: " << d_addedLemmas << std::endl;
-        Trace("model-engine-warn") << std::endl;
-      }
-    }
-    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    return riter.isIncomplete() ? -1 : 1;
-  }else{
-    return 0;
-  }
-}
-
-
-
-void QModelBuilderDefault::reset( FirstOrderModel* fm ){
-  d_quant_selection_lit.clear();
-  d_quant_selection_lit_candidates.clear();
-  d_quant_selection_lit_terms.clear();
-  d_term_selection_lit.clear();
-  d_op_selection_terms.clear();
-}
-
-
-int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
-  /*
-  size_t maxChildren = 0;
-  for( size_t i=0; i<uf_terms.size(); i++ ){
-    if( uf_terms[i].getNumChildren()>maxChildren ){
-      maxChildren = uf_terms[i].getNumChildren();
-    }
-  }
-  //TODO: look at how many entries they have?
-  return (int)maxChildren;
-  */
-  return 0;
-}
-
-void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
-  if( d_qe->getModel()->isQuantifierActive( f ) ){
-    FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
-    Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
-    //the pro/con preferences for this quantifier
-    std::vector< Node > pro_con[2];
-    //the terms in the selection literal we choose
-    std::vector< Node > selectionLitTerms;
-    Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl;
-    //for each asserted quantifier f,
-    // - determine selection literals
-    // - check which function/predicates have good and bad definitions for satisfying f
-    if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
-      d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true );
-    }
-    int selectLitScore = -1;
-    for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
-      //the literal n is phase-required for quantifier f
-      Node n = it->first;
-      Node gn = fm->getModelBasis(f, n);
-      Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
-      bool value;
-      //if the corresponding ground abstraction literal has a SAT value
-      if( d_qe->getValuation().hasSatValue( gn, value ) ){
-        //collect the non-ground uf terms that this literal contains
-        //  and compute if all of the symbols in this literal have
-        //  constant definitions.
-        bool isConst = true;
-        std::vector< Node > uf_terms;
-        if( TermUtil::hasInstConstAttr(n) ){
-          isConst = false;
-          if( gn.getKind()==APPLY_UF ){
-            uf_terms.push_back( gn );
-            isConst = hasConstantDefinition( gn );
-          }else if( gn.getKind()==EQUAL ){
-            isConst = true;
-            for( int j=0; j<2; j++ ){
-              if( TermUtil::hasInstConstAttr(n[j]) ){
-                if( n[j].getKind()==APPLY_UF &&
-                    fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
-                  uf_terms.push_back( gn[j] );
-                  isConst = isConst && hasConstantDefinition( gn[j] );
-                }else{
-                  isConst = false;
-                }
-              }
-            }
-          }
-        }
-        //check if the value in the SAT solver matches the preference according to the quantifier
-        int pref = 0;
-        if( value!=it->second ){
-          //we have a possible selection literal
-          bool selectLit = d_quant_selection_lit[f].isNull();
-          bool selectLitConstraints = true;
-          //it is a constantly defined selection literal : the quantifier is sat
-          if( isConst ){
-            selectLit = selectLit || d_qe->getModel()->isQuantifierActive( f );
-            d_qe->getModel()->setQuantifierActive( f, false );
-            //check if choosing this literal would add any additional constraints to default definitions
-            selectLitConstraints = false;
-            selectLit = true;
-          }
-          //also check if it is naturally a better literal
-          if( !selectLit ){
-            int score = getSelectionScore( uf_terms );
-            //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
-            selectLit = score<selectLitScore;
-          }
-          //see if we wish to choose this as a selection literal
-          d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
-          if( selectLit ){
-            selectLitScore = getSelectionScore( uf_terms );
-            Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
-            Trace("inst-gen-debug") << "  flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
-            d_quant_selection_lit[f] = value ? n : n.notNode();
-            selectionLitTerms.clear();
-            selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
-            if( !selectLitConstraints ){
-              break;
-            }
-          }
-          pref = 1;
-        }else{
-          pref = -1;
-        }
-        //if we are not yet SAT, so we will add to preferences
-        if( d_qe->getModel()->isQuantifierActive( f ) ){
-          Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
-          Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
-          for( int j=0; j<(int)uf_terms.size(); j++ ){
-            pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
-          }
-        }
-      }
-    }
-    //process information about selection literal for f
-    if( !d_quant_selection_lit[f].isNull() ){
-      d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
-      for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
-        d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
-        d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
-      }
-    }else{
-      Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
-    }
-    //process information about requirements and preferences of quantifier f
-    if( !d_qe->getModel()->isQuantifierActive( f ) ){
-      Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
-      for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
-        Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
-      }
-      Debug("fmf-model-prefs") << std::endl;
-    }else{
-      //note quantifier's value preferences to models
-      for( int k=0; k<2; k++ ){
-        for( int j=0; j<(int)pro_con[k].size(); j++ ){
-          Node op = pro_con[k][j].getOperator();
-          Node r = fmig->getRepresentative( pro_con[k][j] );
-          d_uf_prefs[op].setValuePreference(f, r, k == 0);
-        }
-      }
-    }
-  }
-}
-
-int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
-  int addedLemmas = 0;
-  //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
-  //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
-  //  effectively acting as partial instantiations instead of pointwise instantiations.
-  if( !d_quant_selection_lit[f].isNull() ){
-    Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
-    for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
-      bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
-      Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
-      Assert( TermUtil::hasInstConstAttr(lit) );
-      std::vector< Node > tr_terms;
-      if( lit.getKind()==APPLY_UF ){
-        //only match predicates that are contrary to this one, use literal matching
-        Node eq = NodeManager::currentNM()->mkNode(
-            EQUAL, lit, NodeManager::currentNM()->mkConst(!phase));
-        tr_terms.push_back( eq );
-      }else if( lit.getKind()==EQUAL ){
-        //collect trigger terms
-        for( int j=0; j<2; j++ ){
-          if( TermUtil::hasInstConstAttr(lit[j]) ){
-            if( lit[j].getKind()==APPLY_UF ){
-              tr_terms.push_back( lit[j] );
-            }else{
-              tr_terms.clear();
-              break;
-            }
-          }
-        }
-        if( tr_terms.size()==1 && !phase ){
-          //equality between a function and a ground term, use literal matching
-          tr_terms.clear();
-          tr_terms.push_back( lit );
-        }
-      }
-      //if applicable, try to add exceptions here
-      if( !tr_terms.empty() ){
-        //make a trigger for these terms, add instantiations
-        inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW );
-        //Notice() << "Trigger = " << (*tr) << std::endl;
-        tr->resetInstantiationRound();
-        tr->reset( Node::null() );
-        //d_qe->d_optInstMakeRepresentative = false;
-        //d_qe->d_optMatchIgnoreModelBasis = true;
-        addedLemmas += tr->addInstantiations();
-      }
-    }
-  }
-  return addedLemmas;
-}
-
-void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
-  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
-  if( !d_uf_model_constructed[op] ){
-    //construct the model for the uninterpretted function/predicate
-    bool setDefaultVal = true;
-    Node defaultTerm = fmig->getModelBasisOpTerm(op);
-    Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
-    //set the values in the model
-    std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
-    if( itut!=fmig->d_uf_terms.end() ){
-      for( size_t i=0; i<itut->second.size(); i++ ){
-        Node n = itut->second[i];
-        // only consider unique up to congruence (in model equality engine)?
-        Node v = fmig->getRepresentative( n );
-        Trace("fmf-model-cons") << "Set term " << n << " : "
-                                << fmig->getRepSet()->getIndexFor(v) << " " << v
-                                << std::endl;
-        //if this assertion did not help the model, just consider it ground
-        //set n = v in the model tree
-        //set it as ground value
-        fmig->d_uf_model_gen[op].setValue( fm, n, v );
-        // also set as default value if necessary
-        if (n.hasAttribute(ModelBasisArgAttribute())
-            && n.getAttribute(ModelBasisArgAttribute()) != 0)
-        {
-          Trace("fmf-model-cons") << "  Set as default." << std::endl;
-          fmig->d_uf_model_gen[op].setValue(fm, n, v, false);
-          if( n==defaultTerm ){
-            //incidentally already set, we will not need to find a default value
-            setDefaultVal = false;
-          }
-        }
-      }
-    }
-    //set the overall default value if not set already  (is this necessary??)
-    if( setDefaultVal ){
-      Trace("fmf-model-cons") << "  Choose default value..." << std::endl;
-      //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
-      Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
-      if( defaultVal.isNull() ){
-        if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
-        {
-          Node mbt = fmig->getModelBasisTerm(defaultTerm.getType());
-          fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
-              mbt);
-        }
-        defaultVal =
-            fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0);
-      }
-      Assert( !defaultVal.isNull() );
-      Trace("fmf-model-cons")
-          << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal)
-          << std::endl;
-      fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
-    }
-    Debug("fmf-model-cons") << "  Making model...";
-    fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
-    d_uf_model_constructed[op] = true;
-    Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
-  }
-}
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index b34f1e580..b73716169 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -56,163 +56,6 @@ public:
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
 };
 
-class TermArgBasisTrie {
-public:
-  /** the data */
-  std::map< Node, TermArgBasisTrie > d_data;
-  /** add term to the trie */
-  bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0);
-};/* class TermArgBasisTrie */
-
-/** model builder class
-  *  This class is capable of building candidate models based on the current quantified formulas
-  *  that are asserted.  Use:
-  *  (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel
-  *  (2) if candidate model is determined to be a real model,
-           then call QModelBuilder::buildModel( m, true );
-  */
-class QModelBuilderIG : public QModelBuilder
-{
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-
- protected:
-  /**
-   * This class stores temporary information useful to model engine for
-   * constructing models for uninterpreted functions.
-   */
-  class UfModelPreferenceData
-  {
-   public:
-    UfModelPreferenceData() {}
-    virtual ~UfModelPreferenceData() {}
-    /** any constant value of the type */
-    Node d_const_val;
-    /** list of possible default values */
-    std::vector<Node> d_values;
-    /**
-     * Map from values to the set of quantified formulas that are (pro, con)
-     * that value. A quantified formula may be "pro" a particular default
-     * value of an uninterpreted function if that value is likely to satisfy
-     * many points in its domain. For example, forall x. P( f( x ) ) may be
-     * "pro" the default value true for P.
-     */
-    std::map<Node, std::vector<Node> > d_value_pro_con[2];
-    /** set that quantified formula q is pro/con the default value of r */
-    void setValuePreference(Node q, Node r, bool isPro);
-    /** get best default value */
-    Node getBestDefaultValue(Node defaultTerm, TheoryModel* m);
-  };
-  /** map from operators to model preference data */
-  std::map<Node, UfModelPreferenceData> d_uf_prefs;
-  //built model uf
-  std::map< Node, bool > d_uf_model_constructed;
-  //whether inst gen was done
-  bool d_didInstGen;
-  /** process build model */
-  bool processBuildModel(TheoryModel* m) override;
-
- protected:
-  //reset
-  virtual void reset( FirstOrderModel* fm ) = 0;
-  //initialize quantifiers, return number of lemmas produced
-  virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm);
-  //analyze model
-  virtual void analyzeModel( FirstOrderModel* fm );
-  //analyze quantifiers
-  virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0;
-  //do InstGen techniques for quantifier, return number of lemmas produced
-  virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
-  //theory-specific build models
-  virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
-
- protected:
-  //map from quantifiers to if are SAT
-  //std::map< Node, bool > d_quant_sat;
-  //which quantifiers have been initialized
-  std::map< Node, bool > d_quant_basis_match_added;
-  //map from quantifiers to model basis match
-  std::map< Node, InstMatch > d_quant_basis_match;
-
- protected:  // helper functions
-  /** term has constant definition */
-  bool hasConstantDefinition( Node n );
-
- public:
-  QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
-
- public:
-  /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_num_quants_init;
-    IntStat d_num_partial_quants_init;
-    IntStat d_init_inst_gen_lemmas;
-    IntStat d_inst_gen_lemmas;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-  // is term selected
-  virtual bool isTermSelected( Node n ) { return false; }
-  /** quantifier has inst-gen definition */
-  virtual bool hasInstGen( Node f ) = 0;
-  /** did inst gen this round? */
-  bool didInstGen() { return d_didInstGen; }
-  // is quantifier active?
-  bool isQuantifierActive( Node f );
-  //do exhaustive instantiation
-  int doExhaustiveInstantiation(FirstOrderModel* fm,
-                                Node f,
-                                int effort) override;
-
-  //temporary stats
-  int d_numQuantSat;
-  int d_numQuantInstGen;
-  int d_numQuantNoInstGen;
-  int d_numQuantNoSelForm;
-  //temporary stat
-  int d_instGenMatches;
-};/* class QModelBuilder */
-
-
-class QModelBuilderDefault : public QModelBuilderIG
-{
- private:  /// information for (old) InstGen
-  // 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;
-  //get selection score
-  int getSelectionScore( std::vector< Node >& uf_terms );
-
- protected:
-  //reset
-  void reset(FirstOrderModel* fm) override;
-  //analyze quantifier
-  void analyzeQuantifier(FirstOrderModel* fm, Node f) override;
-  //do InstGen techniques for quantifier, return number of lemmas produced
-  int doInstGen(FirstOrderModel* fm, Node f) override;
-  //theory-specific build models
-  void constructModelUf(FirstOrderModel* fm, Node op) override;
-
- protected:
-  std::map< Node, QuantPhaseReq > d_phase_reqs;
-
- public:
-  QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
-
-  //has inst gen
-  bool hasInstGen(Node f) override
-  {
-    return !d_quant_selection_lit[f].isNull();
-  }
-};
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 81ecf9e77..d2579b4ee 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/fmf/ambqi_builder.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/instantiate.h"
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 320f50afb..433621d31 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,7 +30,6 @@
 #include "theory/quantifiers/equality_infer.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/ambqi_builder.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_engine.h"
@@ -249,20 +248,14 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
           this, c, "FirstOrderModelFmc"));
       d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
-    }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
-      Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
-      d_model.reset(
-          new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs"));
-      d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_model.reset(
-          new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
-      d_builder.reset(new quantifiers::QModelBuilderDefault(c, this));
+          new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
+      d_builder.reset(new quantifiers::QModelBuilder(c, this));
     }
   }else{
-    d_model.reset(
-        new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
+    d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel"));
   }
 }
 
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index a3e058569..42847dfd4 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -37,17 +37,6 @@ void UfModelTreeNode::clear(){
   d_value = Node::null();
 }
 
-bool UfModelTreeNode::hasConcreteArgumentDefinition(){
-  if( d_data.size()>1 ){
-    return true;
-  }else if( d_data.empty() ){
-    return false;
-  }else{
-    Node r;
-    return d_data.find( r )==d_data.end();
-  }
-}
-
 //set value function
 void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
   if( d_data.empty() ){
@@ -67,75 +56,6 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int
   }
 }
 
-//get value function
-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
-  if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
-    //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
-    depIndex = argIndex;
-    return d_value;
-  }else{
-    Node val;
-    int childDepIndex[2] = { argIndex, argIndex };
-    for( int i=0; i<2; i++ ){
-      //first check the argument, then check default
-      Node r;
-      if( i==0 ){
-        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
-      }
-      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
-      if( it!=d_data.end() ){
-        val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );
-        if( !val.isNull() ){
-          break;
-        }
-      }else{
-        //argument is not a defined argument: thus, it depends on this argument
-        childDepIndex[i] = argIndex+1;
-      }
-    }
-    //update depIndex
-    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
-    //Notice() << "Return " << val << ", depIndex = " << depIndex;
-    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
-    return val;
-  }
-}
-
-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){
-  if( argIndex==(int)indexOrder.size() ){
-    return d_value;
-  }else{
-    Node val;
-    bool depArg = false;
-    //will try concrete value first, then default
-    for( int i=0; i<2; i++ ){
-      Node r;
-      if( i==0 ){
-        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
-      }
-      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
-      if( it!=d_data.end() ){
-        val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );
-        //we have found a value
-        if( !val.isNull() ){
-          if( i==0 ){
-            depArg = true;
-          }
-          break;
-        }
-      }
-    }
-    //it depends on this argument if we found it via concrete argument value,
-    // or if found by default/disequal from some concrete argument value(s).
-    if( depArg || hasConcreteArgumentDefinition() ){
-      if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){
-        depIndex.push_back( indexOrder[argIndex] );
-      }
-    }
-    return val;
-  }
-}
-
 Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
   if(!d_data.empty()) {
     Node defaultValue = argDefaultValue;
@@ -264,10 +184,6 @@ bool UfModelTreeNode::isTotal( Node op, int argIndex ){
   }
 }
 
-Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
-  return d_value;
-}
-
 void indent( std::ostream& out, int ind ){
   for( int i=0; i<ind; i++ ){
     out << " ";
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 201faccee..ac57bde27 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -31,8 +31,6 @@ public:
   std::map< Node, UfModelTreeNode > d_data;
   /** the value of this tree node (if all paths lead to same value) */
   Node d_value;
-  /** has concrete argument defintion */
-  bool hasConcreteArgumentDefinition();
 public:
   //is this model tree empty?
   bool isEmpty() { return d_data.empty() && d_value.isNull(); }
@@ -40,11 +38,6 @@ public:
   void clear();
   /** setValue function */
   void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
-  /**  getValue function */
-  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );
-  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex );
-  /** getConstant Value function */
-  Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );
   /** getFunctionValue */
   Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true );
   /** update function */
@@ -92,36 +85,6 @@ public:
   void setDefaultValue( TheoryModel* m, Node v ){
     d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );
   }
-  /**  getValue function
-    *
-    *  returns val, the value of ground term n
-    *  Say n is f( t_0...t_n )
-    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val
-    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,
-    *      then g( a, a, a ) would return b with depIndex = 1
-    *
-    */
-  Node getValue( TheoryModel* m, Node n, int& depIndex ){
-    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
-  }
-  /** -> implementation incomplete */
-  Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){
-    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
-  }
-  /** getConstantValue function
-    *
-    * given term n, where n may contain "all value" arguments, aka model basis arguments
-    *   if n is null, then every argument of n is considered "all value"
-    * if n is constant for the entire domain specified by n, then this function returns the value of its domain
-    * otherwise, it returns null
-    * for example, say the term e represents "all values"
-    *   if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,
-    *     then f( a, e ) would return b, while f( e, a ) would return null
-    *  -> implementation incomplete
-    */
-  Node getConstantValue( TheoryModel* m, Node n ) {
-    return d_tree.getConstantValue( m, n, d_index_order, 0 );
-  }
   /** getFunctionValue
     *   Returns a representation of this function.
     */
@@ -136,8 +99,6 @@ public:
   void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
   /** is this tree total? */
   bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
-  /** is this function constant? */
-  bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); }
   /** is this tree empty? */
   bool isEmpty() { return d_tree.isEmpty(); }
 public:
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
index e8c7949dc..bb2630b93 100644
--- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
+++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
 (benchmark Isabelle
 :status sat
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt
index 4fe592638..97a585090 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smt
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (benchmark Isabelle
 :status sat
diff --git a/test/regress/regress1/fmf/nlp042+1.smt2 b/test/regress/regress1/fmf/nlp042+1.smt2
index 567a3c0b7..6159f0b41 100644
--- a/test/regress/regress1/fmf/nlp042+1.smt2
+++ b/test/regress/regress1/fmf/nlp042+1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --mbqi=abs --no-check-models
+; COMMAND-LINE: --finite-model-find --no-check-models
 ; EXPECT: sat
 (set-logic UF)
 (set-info :status sat)