Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.

18 files changed, 548 insertions, 870 deletions

diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index ec834522f..77f102cf8 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -16,9 +16,7 @@ libarrays_la_SOURCES = \
 	array_info.h \
 	array_info.cpp \
 	static_fact_manager.h \
-	static_fact_manager.cpp \
-	theory_arrays_model.h \
-	theory_arrays_model.cpp
+	static_fact_manager.cpp
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 89f1dbf2c..98346d0e3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,7 +21,6 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
-#include "theory/arrays/theory_arrays_model.h"
 #include "theory/model.h"
 #include "theory/arrays/options.h"
 #include "smt/logic_exception.h"
@@ -495,7 +494,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   }
   case kind::STORE_ALL: {
     throw LogicException("Array theory solver does not yet support assertions using constant array value");
-  }    
+  }
   default:
     // Variables etc
     if (node.getType().isArray()) {
@@ -1082,7 +1081,7 @@ void TheoryArrays::checkModel(Effort e)
     if (constraintIdx == d_modelConstraints.size()) {
       break;
     }
-    
+
     if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) {
       assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false);
       if (assertionToCheck.getKind() == kind::AND &&
@@ -1429,7 +1428,7 @@ Node TheoryArrays::getModelValRec(TNode node)
             }
             ++d_numGetModelValConflicts;
             getSatContext()->pop();
-          } 
+          }
           ++te;
           if (te.isFinished()) {
             Assert(false);
@@ -1466,7 +1465,7 @@ bool TheoryArrays::hasLoop(TNode node, TNode target)
       return true;
     }
   }
-  
+
   return false;
 }
 
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
deleted file mode 100644
index b5c81ef69..000000000
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_arrays_model class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_model.h"
-#include "theory/model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-ArrayModel::ArrayModel( Node arr, TheoryModel* m ) : d_arr( arr ){
-  d_base_arr = arr;
-  while( d_base_arr.getKind()==STORE ){
-    Node ri = m->getRepresentative( d_base_arr[1] );
-    if( d_values.find( ri )==d_values.end() ){
-      d_values[ ri ] = m->getRepresentative( d_base_arr[2] );
-    }
-    d_base_arr = d_base_arr[0];
-  }
-}
-
-Node ArrayModel::getValue( TheoryModel* m, Node i ){
-  i = m->getRepresentative( i );
-  std::map< Node, Node >::iterator it = d_values.find( i );
-  if( it!=d_values.end() ){
-    return it->second;
-  }else{
-    return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
-    //return d_default_value;   //TODO: guarantee I can return this here
-  }
-}
-
-void ArrayModel::setValue( TheoryModel* m, Node i, Node e ){
-  Node ri = m->getRepresentative( i );
-  if( d_values.find( ri )==d_values.end() ){
-    d_values[ ri ] = m->getRepresentative( e );
-  }
-}
-
-void ArrayModel::setDefaultArray( Node arr ){
-  d_base_arr = arr;
-}
-
-Node ArrayModel::getArrayValue(){
-  Node curr = d_base_arr;
-  for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
-    curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
-  }
-  return curr;
-}
diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h
deleted file mode 100644
index 66dc80568..000000000
--- a/src/theory/arrays/theory_arrays_model.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_model.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief MODEL for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
-#define __CVC4__THEORY_ARRAYS_MODEL_H
-
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class TheoryModel;
-
-namespace arrays {
-
-class ArrayModel{
-protected:
-  /** the array this model is for */
-  Node d_arr;
-public:
-  ArrayModel(){}
-  ArrayModel( Node arr, TheoryModel* m );
-  ~ArrayModel() {}
-public:
-  /** pre-defined values */
-  std::map< Node, Node > d_values;
-  /** base array */
-  Node d_base_arr;
-  /** get value, return arguments that the value depends on */
-  Node getValue( TheoryModel* m, Node i );
-  /** set value */
-  void setValue( TheoryModel* m, Node i, Node e );
-  /** set default */
-  void setDefaultArray( Node arr );
-public:
-  /** get array value */
-  Node getArrayValue();
-};/* class ArrayModel */
-
-}
-}
-}
-
-#endif
\ No newline at end of file
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 92d780be4..60f2ee7f7 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -23,8 +23,6 @@ libquantifiers_la_SOURCES = \
 	model_engine.cpp \
 	modes.cpp \
 	modes.h \
-	relevant_domain.h \
-	relevant_domain.cpp \
 	term_database.h \
 	term_database.cpp \
 	first_order_model.h \
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 4492e6d2d..e33cd2131 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -355,8 +355,8 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
     }

   }

   Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;

-  l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l );

-  u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u );

+  l = d_quantEngine->getModel()->getCurrentModelValue( l );

+  u = d_quantEngine->getModel()->getCurrentModelValue( u );

   Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;

   return;

 }

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a11729519..cf4381c02 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -38,15 +38,34 @@ void FirstOrderModel::assertQuantifier( Node n ){
   }
 }
 
-void FirstOrderModel::reset(){
-  TheoryModel::reset();
+Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
+  std::vector< Node > children;
+  if( n.getNumChildren()>0 ){
+    if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.push_back( n.getOperator() );
+    }
+    for (unsigned i=0; i<n.getNumChildren(); i++) {
+      Node nc = getCurrentModelValue( n[i], partial );
+      if (nc.isNull()) {
+        return Node::null();
+      }else{
+        children.push_back( nc );
+      }
+    }
+    if( n.getKind()==APPLY_UF ){
+      return getCurrentUfModelValue( n, children, partial );
+    }else{
+      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      nn = Rewriter::rewrite( nn );
+      return nn;
+    }
+  }else{
+    return getRepresentative(n);
+  }
 }
 
-void FirstOrderModel::initialize( bool considerAxioms ){
-  //rebuild models
-  d_uf_model_tree.clear();
-  d_uf_model_gen.clear();
-  d_array_model.clear();
+void FirstOrderModel::initialize( bool considerAxioms ) {
+  processInitialize();
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
   for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
@@ -59,6 +78,23 @@ void FirstOrderModel::initialize( bool considerAxioms ){
 }
 
 void FirstOrderModel::initializeModelForTerm( Node n ){
+  processInitializeModelForTerm( n );
+  for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    initializeModelForTerm( n[i] );
+  }
+}
+
+FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) {
+
+}
+
+void FirstOrderModelIG::processInitialize(){
+  //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() ){
@@ -82,14 +118,11 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
     }
   }
   */
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    initializeModelForTerm( n[i] );
-  }
 }
 
 //for evaluation of quantifier bodies
 
-void FirstOrderModel::resetEvaluate(){
+void FirstOrderModelIG::resetEvaluate(){
   d_eval_uf_use_default.clear();
   d_eval_uf_model.clear();
   d_eval_term_index_order.clear();
@@ -107,7 +140,7 @@ void FirstOrderModel::resetEvaluate(){
 // if eVal = 0, then n' cannot be proven to be equal to phaseReq
 // if eVal is not 0, then
 //   each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
-int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
+int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   ++d_eval_formulas;
   //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
   //Notice() << "Eval " << n << std::endl;
@@ -226,7 +259,7 @@ int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   }
 }
 
-Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
+Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
   //Message() << "Eval term " << n << std::endl;
   Node val;
   depIndex = ri->getNumTerms()-1;
@@ -342,7 +375,7 @@ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){
   return val;
 }
 
-Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
+Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){
   depIndex = -1;
   if( n.getNumChildren()==0 ){
     return n;
@@ -372,14 +405,14 @@ Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< i
   }
 }
 
-void FirstOrderModel::clearEvalFailed( int index ){
+void FirstOrderModelIG::clearEvalFailed( int index ){
   for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
     d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
   }
   d_eval_failed_lits[index].clear();
 }
 
-void FirstOrderModel::makeEvalUfModel( Node n ){
+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] ){
@@ -423,7 +456,7 @@ struct sortGetMaxVariableNum {
   bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
 };
 
-void FirstOrderModel::makeEvalUfIndexOrder( Node n ){
+void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
   if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
 #ifdef USE_INDEX_ORDERING
     //sort arguments in order of least significant vs. most significant variable in default ordering
@@ -460,3 +493,18 @@ void FirstOrderModel::makeEvalUfIndexOrder( Node n ){
 #endif
   }
 }
+
+Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
+  std::vector< Node > children;
+  children.push_back(n.getOperator());
+  children.insert(children.end(), args.begin(), args.end());
+  Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children);
+  //make the term model specifically for nv
+  makeEvalUfModel( nv );
+  int argDepIndex;
+  if( d_eval_uf_use_default[nv] ){
+    return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex );
+  }else{
+    return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
+  }
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 76f21e19c..491e97097 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,7 +19,6 @@
 
 #include "theory/model.h"
 #include "theory/uf/theory_uf_model.h"
-#include "theory/arrays/theory_arrays_model.h"
 
 namespace CVC4 {
 namespace theory {
@@ -30,33 +29,22 @@ namespace quantifiers{
 
 class TermDb;
 
+class FirstOrderModelIG;
+namespace fmcheck {
+  class FirstOrderModelFmc;
+}
+
 class FirstOrderModel : public TheoryModel
 {
 private:
-  //for initialize model
-  void initializeModelForTerm( Node n );
   /** whether an axiom is asserted */
   context::CDO< bool > d_axiom_asserted;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** is model set */
   context::CDO< bool > d_isModelSet;
-public: //for Theory UF:
-  //models for each UF operator
-  std::map< Node, uf::UfModelTree > d_uf_model_tree;
-  //model generators
-  std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
-private:
-  //map from terms to the models used to calculate their value
-  std::map< Node, bool > d_eval_uf_use_default;
-  std::map< Node, uf::UfModelTree > d_eval_uf_model;
-  void makeEvalUfModel( Node n );
-  //index ordering to use for each term
-  std::map< Node, std::vector< int > > d_eval_term_index_order;
-  void makeEvalUfIndexOrder( Node n );
-public: //for Theory Arrays:
-  //default value for each non-store array
-  std::map< Node, arrays::ArrayModel > d_array_model;
+  /** get current model value */
+  virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
   /** assert quantifier */
   void assertQuantifier( Node n );
@@ -66,19 +54,51 @@ public: //for Theory Quantifiers:
   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
   /** bool axiom asserted */
   bool isAxiomAsserted() { return d_axiom_asserted; }
+  /** initialize model for term */
+  void initializeModelForTerm( Node n );
+  virtual void processInitializeModelForTerm( Node n ) = 0;
 public:
   FirstOrderModel( context::Context* c, std::string name );
   virtual ~FirstOrderModel(){}
-  // reset the model
-  void reset();
+  virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
+  virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
   // initialize the model
   void initialize( bool considerAxioms = true );
+  virtual void processInitialize() = 0;
   /** mark model set */
   void markModelSet() { d_isModelSet = true; }
   /** is model set */
   bool isModelSet() { return d_isModelSet; }
+  /** get current model value */
+  Node getCurrentModelValue( Node n, bool partial = false );
+};/* class FirstOrderModel */
+
+
+class FirstOrderModelIG : public FirstOrderModel
+{
+public: //for Theory UF:
+  //models for each UF operator
+  std::map< Node, uf::UfModelTree > d_uf_model_tree;
+  //model generators
+  std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
+private:
+  //map from terms to the models used to calculate their value
+  std::map< Node, bool > d_eval_uf_use_default;
+  std::map< Node, uf::UfModelTree > d_eval_uf_model;
+  void makeEvalUfModel( Node n );
+  //index ordering to use for each term
+  std::map< Node, std::vector< int > > d_eval_term_index_order;
+  void makeEvalUfIndexOrder( Node n );
+  /** get current model value */
+  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 //the following functions are for evaluating quantifier bodies
 public:
+  FirstOrderModelIG(context::Context* c, std::string name);
+  FirstOrderModelIG * asFirstOrderModelIG() { return this; }
+  // initialize the model
+  void processInitialize();
+  //for initialize model
+  void processInitializeModelForTerm( Node n );
   /** reset evaluation */
   void resetEvaluate();
   /** evaluate functions */
@@ -97,7 +117,8 @@ private:
   void clearEvalFailed( int index );
   std::map< Node, bool > d_eval_failed;
   std::map< int, std::vector< Node > > d_eval_failed_lits;
-};/* class FirstOrderModel */
+};
+
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index b5d4648a1..2513cb08e 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -24,8 +24,17 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;

 using namespace CVC4::theory::quantifiers::fmcheck;

 

+struct ModelBasisArgSort

+{

+  std::vector< Node > d_terms;

+  bool operator() (int i,int j) {

+    return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <

+            d_terms[j].getAttribute(ModelBasisArgAttribute()) );

+  }

+};

 

-bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {

+

+bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {

   if (index==(int)c.getNumChildren()) {

     return d_data!=-1;

   }else{

@@ -44,7 +53,7 @@ bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {
   }

 }

 

-int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {

+int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {

   if (index==(int)inst.size()) {

     return d_data;

   }else{

@@ -64,7 +73,7 @@ int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> &
   }

 }

 

-void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {

+void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {

   if (index==(int)c.getNumChildren()) {

     if(d_data==-1) {

       d_data = data;

@@ -75,7 +84,7 @@ void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int in
   }

 }

 

-void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {

+void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {

   if (index==(int)c.getNumChildren()) {

     if( d_data!=-1) {

       if( is_gen ){

@@ -101,13 +110,8 @@ void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & com
   }

 }

 

-bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {

-

-  return false;

-}

-

 

-bool Def::addEntry( FullModelChecker * m, Node c, Node v) {

+bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {

   if (!d_et.hasGeneralization(m, c)) {

     int newIndex = (int)d_cond.size();

     if (!d_has_simplified) {

@@ -139,7 +143,7 @@ bool Def::addEntry( FullModelChecker * m, Node c, Node v) {
   }

 }

 

-Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {

+Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {

   int gindex = d_et.getGeneralizationIndex(m, inst);

   if (gindex!=-1) {

     return d_value[gindex];

@@ -148,11 +152,11 @@ Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {
   }

 }

 

-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {

+int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {

   return d_et.getGeneralizationIndex(m, inst);

 }

 

-void Def::simplify(FullModelChecker * m) {

+void Def::simplify(FirstOrderModelFmc * m) {

   d_has_simplified = true;

   std::vector< Node > cond;

   cond.insert( cond.end(), d_cond.begin(), d_cond.end() );

@@ -186,16 +190,128 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
 }

 

 

+

+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :

+FirstOrderModel(c, name), d_qe(qe){

+

+}

+

+Node FirstOrderModelFmc::getUsedRepresentative(Node n) {

+  //Assert( fm->hasTerm(n) );

+  TypeNode tn = n.getType();

+  if( tn.isBoolean() ){

+    return areEqual(n, d_true) ? d_true : d_false;

+  }else{

+    Node r = getRepresentative(n);

+    if (r==d_model_basis_rep[tn]) {

+      r = d_qe->getTermDatabase()->getModelBasisTerm(tn);

+    }

+    return r;

+  }

+}

+

+Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {

+  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;

+  for(unsigned i=0; i<args.size(); i++) {

+    args[i] = getUsedRepresentative(args[i]);

+  }

+  Assert( n.getKind()==APPLY_UF );

+  return d_models[n.getOperator()]->evaluate(this, args);

+}

+

+void FirstOrderModelFmc::processInitialize() {

+  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){

+    it->second->reset();

+  }

+  d_model_basis_rep.clear();

+}

+

+void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {

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

+    if( d_models.find(n.getOperator())==d_models.end()) {

+      d_models[n.getOperator()] = new Def;

+    }

+  }

+}

+

+Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){

+  //check if there is even any domain elements at all

+  if (!d_rep_set.hasType(tn)) {

+    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;

+    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);

+    d_rep_set.d_type_reps[tn].push_back(mbt);

+  }else if( d_rep_set.d_type_reps[tn].size()==0 ){

+    Message() << "empty reps" << std::endl;

+    exit(0);

+  }

+  return d_rep_set.d_type_reps[tn][0];

+}

+

+

+bool FirstOrderModelFmc::isStar(Node n) {

+  return n==getStar(n.getType());

+}

+

+Node FirstOrderModelFmc::getStar(TypeNode tn) {

+  if( d_type_star.find(tn)==d_type_star.end() ){

+    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );

+    d_type_star[tn] = st;

+  }

+  return d_type_star[tn];

+}

+

+bool FirstOrderModelFmc::isModelBasisTerm(Node n) {

+  return n==getModelBasisTerm(n.getType());

+}

+

+Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {

+  return d_qe->getTermDatabase()->getModelBasisTerm(tn);

+}

+

+Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {

+  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);

+    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );

+  }

+  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);

+  Node curr;

+  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {

+    Node v = getUsedRepresentative( d_models[op]->d_value[i] );

+    if( curr.isNull() ){

+      curr = v;

+    }else{

+      //make the condition

+      Node cond = d_models[op]->d_cond[i];

+      std::vector< Node > children;

+      for( unsigned j=0; j<cond.getNumChildren(); j++) {

+        if (!isStar(cond[j])){

+          Node c = getUsedRepresentative( cond[j] );

+          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );

+        }

+      }

+      Assert( !children.empty() );

+      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );

+      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );

+    }

+  }

+  curr = Rewriter::rewrite( curr );

+  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);

+}

+

+

+

 FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :

 QModelBuilder( c, qe ){

   d_true = NodeManager::currentNM()->mkConst(true);

   d_false = NodeManager::currentNM()->mkConst(false);

 }

 

-

 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){

   d_addedLemmas = 0;

-  FirstOrderModel* fm = (FirstOrderModel*)m;

+  FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();

   if( fullModel ){

     //make function values

     for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){

@@ -204,15 +320,13 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
     TheoryEngineModelBuilder::processBuildModel( m, fullModel );

     //mark that the model has been set

     fm->markModelSet();

+    //debug the model

+    debugModel( fm );

   }else{

     Trace("fmc") << "---Full Model Check reset() " << std::endl;

-    for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){

-      it->second->reset();

-    }

+    fm->initialize( d_considerAxioms );

     d_quant_models.clear();

-    d_models_init.clear();

     d_rep_ids.clear();

-    d_model_basis_rep.clear();

     d_star_insts.clear();

     //process representatives

     for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();

@@ -220,13 +334,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       if( it->first.isSort() ){

         Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;

         Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);

-        Node rmbt = fm->getRepresentative(mbt);

+        Node rmbt = fm->getUsedRepresentative( mbt);

         int mbt_index = -1;

         Trace("fmc") << "  Model basis term : " << mbt << std::endl;

         for( size_t a=0; a<it->second.size(); a++ ){

-          //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );

-          //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );

-          Node r = fm->getRepresentative( it->second[a] );

+          Node r = fm->getUsedRepresentative( it->second[a] );

           std::vector< Node > eqc;

           ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );

           Trace("fmc-model-debug") << "   " << (it->second[a]==r) << (r==mbt);

@@ -241,7 +353,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
 

           //if this is the model basis eqc, replace with actual model basis term

           if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {

-            d_model_basis_rep[it->first] = r;

+            fm->d_model_basis_rep[it->first] = r;

             r = mbt;

             mbt_index = a;

           }

@@ -257,150 +369,63 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         }

       }

     }

-  }

-}

-

-Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {

-  //Assert( fm->hasTerm(n) );

-  TypeNode tn = n.getType();

-  if( tn.isBoolean() ){

-    return fm->areEqual(n, d_true) ? d_true : d_false;

-  }else{

-    Node r = fm->getRepresentative(n);

-    if (r==d_model_basis_rep[tn]) {

-      r = d_qe->getTermDatabase()->getModelBasisTerm(tn);

-    }

-    return r;

-  }

-}

-

-struct ModelBasisArgSort

-{

-  std::vector< Node > d_terms;

-  bool operator() (int i,int j) {

-    return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <

-            d_terms[j].getAttribute(ModelBasisArgAttribute()) );

-  }

-};

-

-void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,

-                                 std::vector< Node > & conds,

-                                 std::vector< Node > & values,

-                                 std::vector< Node > & entry_conds ) {

-  std::vector< Node > children;

-  std::vector< Node > entry_children;

-  children.push_back(op);

-  entry_children.push_back(op);

-  bool hasNonStar = false;

-  for( unsigned i=0; i<c.getNumChildren(); i++) {

-    Node ri = getRepresentative(fm, c[i]);

-    children.push_back(ri);

-    if (isModelBasisTerm(ri)) {

-      ri = getStar( ri.getType() );

-    }else{

-      hasNonStar = true;

-    }

-    entry_children.push_back(ri);

-  }

-  Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );

-  Node nv = getRepresentative(fm, v);

-  Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );

-  if( std::find(conds.begin(), conds.end(), n )==conds.end() ){

-    Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

-    conds.push_back(n);

-    values.push_back(nv);

-    entry_conds.push_back(en);

-  }

-}

-

-Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {

-  if( d_models_init.find(op)==d_models_init.end() ){

-    if( d_models.find(op)==d_models.end() ){

-      d_models[op] = new Def;

-    }

-    //reset the model

-    d_models[op]->reset();

-

-    std::vector< Node > conds;

-    std::vector< Node > values;

-    std::vector< Node > entry_conds;

-    Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;

-    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){

-      Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);

-      Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;

-    }

-    Trace("fmc-model-debug") << std::endl;

-    //initialize the model

-    /*

-    for( int j=0; j<2; j++ ){

-      for( int k=1; k>=0; k-- ){

-        Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;

-        for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();

-             it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){

-          Trace("fmc-model-debug") << "   process : " << it->first << " -> " << it->second << std::endl;

-          if( j==1 ){

-            addEntry(fm, op, it->first, it->second, conds, values, entry_conds);

-          }

+    //now, make models

+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {

+      Node op = it->first;

+      //reset the model

+      fm->d_models[op]->reset();

+

+      std::vector< Node > conds;

+      std::vector< Node > values;

+      std::vector< Node > entry_conds;

+      Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;

+      for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){

+        Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);

+        Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;

+      }

+      Trace("fmc-model-debug") << std::endl;

+      //initialize the model

+      for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){

+        Node n = fm->d_uf_terms[op][i];

+        if( !n.getAttribute(NoMatchAttribute()) ){

+          addEntry(fm, op, n, n, conds, values, entry_conds);

         }

       }

-    }

-    */

-    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){

-      Node n = fm->d_uf_terms[op][i];

-      if( !n.getAttribute(NoMatchAttribute()) ){

-        addEntry(fm, op, n, n, conds, values, entry_conds);

+      Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);

+      //add default value

+      if( fm->hasTerm( nmb ) ){

+        Trace("fmc-model-debug") << "Add default " << nmb << std::endl;

+        addEntry(fm, op, nmb, nmb, conds, values, entry_conds);

+      }else{

+        Node vmb = fm->getSomeDomainElement(nmb.getType());

+        Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";

+        Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;

+        addEntry(fm, op, nmb, vmb, conds, values, entry_conds);

       }

-    }

-    Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);

-    //add default value

-    if( fm->hasTerm( nmb ) ){

-      Trace("fmc-model-debug") << "Add default " << nmb << std::endl;

-      addEntry(fm, op, nmb, nmb, conds, values, entry_conds);

-    }else{

-      Node vmb = getSomeDomainElement( fm, nmb.getType() );

-      Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";

-      Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;

-      addEntry(fm, op, nmb, vmb, conds, values, entry_conds);

-    }

-

-    //sort based on # default arguments

-    std::vector< int > indices;

-    ModelBasisArgSort mbas;

-    for (int i=0; i<(int)conds.size(); i++) {

-      d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );

-      mbas.d_terms.push_back(conds[i]);

-      indices.push_back(i);

-    }

-    std::sort( indices.begin(), indices.end(), mbas );

 

+      //sort based on # default arguments

+      std::vector< int > indices;

+      ModelBasisArgSort mbas;

+      for (int i=0; i<(int)conds.size(); i++) {

+        d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );

+        mbas.d_terms.push_back(conds[i]);

+        indices.push_back(i);

+      }

+      std::sort( indices.begin(), indices.end(), mbas );

 

-    for (int i=0; i<(int)indices.size(); i++) {

-      d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);

-    }

-    d_models[op]->debugPrint("fmc-model", op, this);

-    Trace("fmc-model") << std::endl;

 

-    d_models[op]->simplify( this );

-    Trace("fmc-model-simplify") << "After simplification : " << std::endl;

-    d_models[op]->debugPrint("fmc-model-simplify", op, this);

-    Trace("fmc-model-simplify") << std::endl;

+      for (int i=0; i<(int)indices.size(); i++) {

+        fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);

+      }

+      fm->d_models[op]->debugPrint("fmc-model", op, this);

+      Trace("fmc-model") << std::endl;

 

-    d_models_init[op] = true;

+      fm->d_models[op]->simplify( fm );

+      Trace("fmc-model-simplify") << "After simplification : " << std::endl;

+      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);

+      Trace("fmc-model-simplify") << std::endl;

+    }

   }

-  return d_models[op];

-}

-

-

-bool FullModelChecker::isStar(Node n) {

-  return n==getStar(n.getType());

-}

-

-bool FullModelChecker::isModelBasisTerm(Node n) {

-  return n==getModelBasisTerm(n.getType());

-}

-

-Node FullModelChecker::getModelBasisTerm(TypeNode tn) {

-  return d_qe->getTermDatabase()->getModelBasisTerm(tn);

 }

 

 void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {

@@ -413,10 +438,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
 }

 

 void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {

+  FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();

   if( n.isNull() ){

     Trace(tr) << "null";

   }

-  else if(isStar(n) && dispStar) {

+  else if(fm->isStar(n) && dispStar) {

     Trace(tr) << "*";

   }else{

     TypeNode tn = n.getType();

@@ -438,6 +464,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
   if (!options::fmfModelBasedInst()) {

     return false;

   }else{

+    FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();

     if (effort==0) {

       //register the quantifier

       if (d_quant_cond.find(f)==d_quant_cond.end()) {

@@ -452,7 +479,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
       }

 

       //model check the quantifier

-      doCheck(fm, f, d_quant_models[f], f[1]);

+      doCheck(fmfmc, f, d_quant_models[f], f[1]);

       Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;

       d_quant_models[f].debugPrint("fmc", Node::null(), this);

       Trace("fmc") << std::endl;

@@ -463,9 +490,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           bool hasStar = false;

           std::vector< Node > inst;

           for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {

-            if (isStar(d_quant_models[f].d_cond[i][j])) {

+            if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {

               hasStar = true;

-              inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));

+              inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));

             }else{

               inst.push_back(d_quant_models[f].d_cond[i][j]);

             }

@@ -473,14 +500,14 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           bool addInst = true;

           if( hasStar ){

             //try obvious (specified by inst)

-            Node ev = d_quant_models[f].evaluate(this, inst);

+            Node ev = d_quant_models[f].evaluate(fmfmc, inst);

             if (ev==d_true) {

               addInst = false;

             }

           }else{

             //for debugging

             if (Trace.isOn("fmc-test-inst")) {

-              Node ev = d_quant_models[f].evaluate(this, inst);

+              Node ev = d_quant_models[f].evaluate(fmfmc, inst);

               if( ev==d_true ){

                 std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;

                 exit(0);

@@ -518,8 +545,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         for( int i=(d_star_insts[f].size()-1); i>=0; i--) {

           //get witness for d_star_insts[f][i]

           int j = d_star_insts[f][i];

-          if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){

-            int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );

+          if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){

+            int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j );

             if( lem==-1 ){

               //something went wrong, resort to exhaustive instantiation

               return false;

@@ -534,7 +561,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
   }

 }

 

-int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {

+int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {

   int addedLemmas = 0;

   RepSetIterator riter( d_qe, &(fm->d_rep_set) );

   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";

@@ -546,7 +573,7 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c
       TypeNode tn = c[i].getType();

       if( d_rep_ids.find(tn)!=d_rep_ids.end() ){

         //RepDomain rd;

-        if( isStar(c[i]) ){

+        if( fm->isStar(c[i]) ){

           //add the full range

           //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();

           //     it != d_rep_ids[tn].end(); ++it ){

@@ -573,13 +600,13 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c
       std::vector< Node > inst;

       for( int i=0; i<riter.getNumTerms(); i++ ){

         //m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );

-        Node r = getRepresentative( fm, riter.getTerm( i ) );

+        Node r = fm->getUsedRepresentative( riter.getTerm( i ) );

         debugPrint("fmc-exh-debug", r);

         Trace("fmc-exh-debug") << " ";

         inst.push_back(r);

       }

 

-      int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);

+      int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);

       Trace("fmc-exh-debug") << ", index = " << ev_index;

       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];

       if (ev!=d_true) {

@@ -600,19 +627,19 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c
   return addedLemmas;

 }

 

-void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {

+void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {

   Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;

   if( n.getKind() == kind::BOUND_VARIABLE ){

-    d.addEntry(this, mkCondDefault(f), n);

+    d.addEntry(fm, mkCondDefault(fm, f), n);

     Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;

   }

   else if( n.getNumChildren()==0 ){

     Node r = n;

     if( !fm->hasTerm(n) ){

-      r = getSomeDomainElement( fm, n.getType() );

+      r = fm->getSomeDomainElement(n.getType() );

     }

-    r = getRepresentative(fm, r);

-    d.addEntry(this, mkCondDefault(f), r);

+    r = fm->getUsedRepresentative( r);

+    d.addEntry(fm, mkCondDefault(fm, f), r);

   }

   else if( n.getKind() == kind::NOT ){

     //just do directly

@@ -620,7 +647,7 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
     doNegate( d );

   }

   else if( n.getKind() == kind::FORALL ){

-    d.addEntry(this, mkCondDefault(f), Node::null());

+    d.addEntry(fm, mkCondDefault(fm, f), Node::null());

   }

   else{

     std::vector< int > var_ch;

@@ -655,13 +682,13 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
       }else{

         Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;

         std::vector< Node > cond;

-        mkCondDefaultVec(f, cond);

+        mkCondDefaultVec(fm, f, cond);

         std::vector< Node > val;

         //interpreted compose

         doInterpretedCompose( fm, f, d, n, children, 0, cond, val );

       }

     }

-    d.simplify(this);

+    d.simplify(fm);

   }

   Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;

   d.debugPrint("fmc-debug", Node::null(), this);

@@ -676,62 +703,61 @@ void FullModelChecker::doNegate( Def & dc ) {
   }

 }

 

-void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {

+void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {

   std::vector<Node> cond;

-  mkCondDefaultVec(f, cond);

+  mkCondDefaultVec(fm, f, cond);

   if (eq[0]==eq[1]){

-    d.addEntry(this, mkCond(cond), d_true);

+    d.addEntry(fm, mkCond(cond), d_true);

   }else{

     int j = getVariableId(f, eq[0]);

     int k = getVariableId(f, eq[1]);

     TypeNode tn = eq[0].getType();

     if( !fm->d_rep_set.hasType( tn ) ){

-      getSomeDomainElement( fm, tn );  //to verify the type is initialized

+      fm->getSomeDomainElement( tn );  //to verify the type is initialized

     }

     for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {

-      Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );

+      Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );

       cond[j+1] = r;

       cond[k+1] = r;

-      d.addEntry( this, mkCond(cond), d_true);

+      d.addEntry( fm, mkCond(cond), d_true);

     }

-    d.addEntry(this, mkCondDefault(f), d_false);

+    d.addEntry( fm, mkCondDefault(fm, f), d_false);

   }

 }

 

-void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {

+void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {

   int j = getVariableId(f, v);

   for (unsigned i=0; i<dc.d_cond.size(); i++) {

     Node val = dc.d_value[i];

     if( dc.d_cond[i][j]!=val ){

-      if (isStar(dc.d_cond[i][j])) {

+      if (fm->isStar(dc.d_cond[i][j])) {

         std::vector<Node> cond;

         mkCondVec(dc.d_cond[i],cond);

         cond[j+1] = val;

-        d.addEntry(this, mkCond(cond), d_true);

-        cond[j+1] = getStar(val.getType());

-        d.addEntry(this, mkCond(cond), d_false);

+        d.addEntry(fm, mkCond(cond), d_true);

+        cond[j+1] = fm->getStar(val.getType());

+        d.addEntry(fm, mkCond(cond), d_false);

       }else{

-        d.addEntry( this, dc.d_cond[i], d_false);

+        d.addEntry( fm, dc.d_cond[i], d_false);

       }

     }else{

-      d.addEntry( this, dc.d_cond[i], d_true);

+      d.addEntry( fm, dc.d_cond[i], d_true);

     }

   }

 }

 

-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {

-  getModel(fm, op);

+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {

   Trace("fmc-uf-debug") << "Definition : " << std::endl;

-  d_models[op]->debugPrint("fmc-uf-debug", op, this);

+  fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);

   Trace("fmc-uf-debug") << std::endl;

 

   std::vector< Node > cond;

-  mkCondDefaultVec(f, cond);

+  mkCondDefaultVec(fm, f, cond);

   std::vector< Node > val;

   doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);

 }

 

-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,

+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,

                                                std::vector< Def > & dc, int index,

                                                std::vector< Node > & cond, std::vector<Node> & val ) {

   Trace("fmc-uf-process") << "process at " << index << std::endl;

@@ -743,19 +769,19 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod
   if (index==(int)dc.size()) {

     //we have an entry, now do actual compose

     std::map< int, Node > entries;

-    doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et);

+    doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et);

     //add them to the definition

-    for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){

+    for( unsigned e=0; e<fm->d_models[op]->d_cond.size(); e++ ){

       if ( entries.find(e)!=entries.end() ){

-        d.addEntry(this, entries[e], d_models[op]->d_value[e] );

+        d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] );

       }

     }

   }else{

     for (unsigned i=0; i<dc[index].d_cond.size(); i++) {

-      if (isCompat(cond, dc[index].d_cond[i])!=0) {

+      if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {

         std::vector< Node > new_cond;

         new_cond.insert(new_cond.end(), cond.begin(), cond.end());

-        if( doMeet(new_cond, dc[index].d_cond[i]) ){

+        if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){

           Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;

           val.push_back(dc[index].d_value[i]);

           doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);

@@ -768,7 +794,7 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod
   }

 }

 

-void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,

+void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,

                                                 std::map< int, Node > & entries, int index,

                                                 std::vector< Node > & cond, std::vector< Node > & val,

                                                 EntryTrie & curr ) {

@@ -788,7 +814,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
     if( v.getKind()==kind::BOUND_VARIABLE ){

       int j = getVariableId(f, v);

       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;

-      if (!isStar(cond[j+1])) {

+      if (!fm->isStar(cond[j+1])) {

         v = cond[j+1];

       }else{

         bind_var = true;

@@ -801,13 +827,13 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
         cond[j+1] = it->first;

         doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);

       }

-      cond[j+1] = getStar(v.getType());

+      cond[j+1] = fm->getStar(v.getType());

     }else{

       if (curr.d_child.find(v)!=curr.d_child.end()) {

         Trace("fmc-uf-process") << "follow value..." << std::endl;

         doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);

       }

-      Node st = getStar(v.getType());

+      Node st = fm->getStar(v.getType());

       if (curr.d_child.find(st)!=curr.d_child.end()) {

         Trace("fmc-uf-process") << "follow star..." << std::endl;

         doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);

@@ -816,28 +842,28 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
   }

 }

 

-void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,

+void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,

                                              std::vector< Def > & dc, int index,

                                              std::vector< Node > & cond, std::vector<Node> & val ) {

   if ( index==(int)dc.size() ){

     Node c = mkCond(cond);

     Node v = evaluateInterpreted(n, val);

-    d.addEntry(this, c, v);

+    d.addEntry(fm, c, v);

   }

   else {

     TypeNode vtn = n.getType();

     for (unsigned i=0; i<dc[index].d_cond.size(); i++) {

-      if (isCompat(cond, dc[index].d_cond[i])!=0) {

+      if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {

         std::vector< Node > new_cond;

         new_cond.insert(new_cond.end(), cond.begin(), cond.end());

-        if( doMeet(new_cond, dc[index].d_cond[i]) ){

+        if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){

           bool process = true;

           if (vtn.isBoolean()) {

             //short circuit

             if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||

                 (n.getKind()==AND && dc[index].d_value[i]==d_false) ){

               Node c = mkCond(new_cond);

-              d.addEntry(this, c, dc[index].d_value[i]);

+              d.addEntry(fm, c, dc[index].d_value[i]);

               process = false;

             }

           }

@@ -852,23 +878,23 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def &
   }

 }

 

-int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) {

+int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {

   Assert(cond.size()==c.getNumChildren()+1);

   for (unsigned i=1; i<cond.size(); i++) {

-    if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {

+    if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {

       return 0;

     }

   }

   return 1;

 }

 

-bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {

+bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {

   Assert(cond.size()==c.getNumChildren()+1);

   for (unsigned i=1; i<cond.size(); i++) {

     if( cond[i]!=c[i-1] ) {

-      if( isStar(cond[i]) ){

+      if( fm->isStar(cond[i]) ){

         cond[i] = c[i-1];

-      }else if( !isStar(c[i-1]) ){

+      }else if( !fm->isStar(c[i-1]) ){

         return false;

       }

     }

@@ -880,38 +906,17 @@ Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
   return NodeManager::currentNM()->mkNode(APPLY_UF, cond);

 }

 

-Node FullModelChecker::mkCondDefault( Node f) {

+Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {

   std::vector< Node > cond;

-  mkCondDefaultVec(f, cond);

+  mkCondDefaultVec(fm, f, cond);

   return mkCond(cond);

 }

 

-Node FullModelChecker::getStar(TypeNode tn) {

-  if( d_type_star.find(tn)==d_type_star.end() ){

-    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );

-    d_type_star[tn] = st;

-  }

-  return d_type_star[tn];

-}

-

-Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){

-  //check if there is even any domain elements at all

-  if (!fm->d_rep_set.hasType(tn)) {

-    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;

-    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);

-    fm->d_rep_set.d_type_reps[tn].push_back(mbt);

-  }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){

-    Message() << "empty reps" << std::endl;

-    exit(0);

-  }

-  return fm->d_rep_set.d_type_reps[tn][0];

-}

-

-void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {

+void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {

   //get function symbol for f

   cond.push_back(d_quant_cond[f]);

   for (unsigned i=0; i<f[0].getNumChildren(); i++) {

-    Node ts = getStar( f[0][i].getType() );

+    Node ts = fm->getStar( f[0][i].getType() );

     cond.push_back(ts);

   }

 }

@@ -964,56 +969,42 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals )
   }

 }

 

-bool FullModelChecker::useSimpleModels() {

-  return options::fmfFullModelCheckSimple();

+Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {

+  return fm->getFunctionValue(op, argPrefix);

 }

 

-Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {

-  getModel( fm, op );

-  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);

-    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );

-  }

-  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);

-  Node curr;

-  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {

-    Node v = fm->getRepresentative( d_models[op]->d_value[i] );

-    if( curr.isNull() ){

-      curr = v;

+

+

+void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,

+                                   std::vector< Node > & conds,

+                                   std::vector< Node > & values,

+                                   std::vector< Node > & entry_conds ) {

+  std::vector< Node > children;

+  std::vector< Node > entry_children;

+  children.push_back(op);

+  entry_children.push_back(op);

+  bool hasNonStar = false;

+  for( unsigned i=0; i<c.getNumChildren(); i++) {

+    Node ri = fm->getUsedRepresentative( c[i]);

+    children.push_back(ri);

+    if (fm->isModelBasisTerm(ri)) {

+      ri = fm->getStar( ri.getType() );

     }else{

-      //make the condition

-      Node cond = d_models[op]->d_cond[i];

-      std::vector< Node > children;

-      for( unsigned j=0; j<cond.getNumChildren(); j++) {

-        if (!isStar(cond[j])){

-          Node c = fm->getRepresentative( cond[j] );

-          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );

-        }

-      }

-      Assert( !children.empty() );

-      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );

-      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );

+      hasNonStar = true;

     }

+    entry_children.push_back(ri);

+  }

+  Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );

+  Node nv = fm->getUsedRepresentative( v);

+  Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );

+  if( std::find(conds.begin(), conds.end(), n )==conds.end() ){

+    Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

+    conds.push_back(n);

+    values.push_back(nv);

+    entry_conds.push_back(en);

   }

-  curr = Rewriter::rewrite( curr );

-  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);

 }

 

-Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {

-  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;

-  for(unsigned i=0; i<args.size(); i++) {

-    args[i] = getRepresentative(fm, args[i]);

-  }

-  if( n.getKind()==VARIABLE ){

-    Node r = getRepresentative(fm, n);

-    return r;

-  }else if( n.getKind()==APPLY_UF ){

-    getModel(fm, n.getOperator());

-    return d_models[n.getOperator()]->evaluate(this, args);

-  }else{

-    return Node::null();

-  }

-}
\ No newline at end of file
+bool FullModelChecker::useSimpleModels() {

+  return options::fmfFullModelCheckSimple();

+}

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 00a910567..ddf298006 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -14,6 +14,7 @@
 #define FULL_MODEL_CHECK

 

 #include "theory/quantifiers/model_builder.h"

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

 

 namespace CVC4 {

 namespace theory {

@@ -21,6 +22,7 @@ namespace quantifiers {
 namespace fmcheck {

 

 

+class FirstOrderModelFmc;

 class FullModelChecker;

 

 class EntryTrie

@@ -30,12 +32,10 @@ public:
   std::map<Node,EntryTrie> d_child;

   int d_data;

   void reset() { d_data = -1; d_child.clear(); }

-  void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 );

-  bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 );

-  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index = 0 );

-  void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );

-  //if possible, get ground instance of c that evaluates to the entry

-  bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index = 0 );

+  void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );

+  bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );

+  int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );

+  void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );

 };

 

 

@@ -64,13 +64,42 @@ public:
     d_status.clear();

     d_has_simplified = false;

   }

-  bool addEntry( FullModelChecker * m, Node c, Node v);

-  Node evaluate( FullModelChecker * m, std::vector<Node>& inst );

-  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );

-  void simplify( FullModelChecker * m );

+  bool addEntry( FirstOrderModelFmc * m, Node c, Node v);

+  Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );

+  int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );

+  void simplify( FirstOrderModelFmc * m );

   void debugPrint(const char * tr, Node op, FullModelChecker * m);

 };

 

+class FirstOrderModelFmc : public FirstOrderModel

+{

+  friend class FullModelChecker;

+private:

+  /** quant engine */

+  QuantifiersEngine * d_qe;

+  /** models for UF */

+  std::map<Node, Def * > d_models;

+  std::map<TypeNode, Node > d_model_basis_rep;

+  std::map<TypeNode, Node > d_type_star;

+  Node getUsedRepresentative(Node n);

+  /** get current model value */

+  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );

+  void processInitializeModelForTerm(Node n);

+public:

+  FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);

+  FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }

+  // initialize the model

+  void processInitialize();

+

+  Node getFunctionValue(Node op, const char* argPrefix );

+

+  bool isStar(Node n);

+  Node getStar(TypeNode tn);

+  bool isModelBasisTerm(Node n);

+  Node getModelBasisTerm(TypeNode tn);

+  Node getSomeDomainElement(TypeNode tn);

+};

+

 

 class FullModelChecker : public QModelBuilder

 {

@@ -78,45 +107,41 @@ protected:
   Node d_true;

   Node d_false;

   std::map<TypeNode, std::map< Node, int > > d_rep_ids;

-  std::map<TypeNode, Node > d_model_basis_rep;

-  std::map<Node, Def * > d_models;

   std::map<Node, Def > d_quant_models;

-  std::map<Node, bool > d_models_init;

   std::map<Node, Node > d_quant_cond;

-  std::map<TypeNode, Node > d_type_star;

   std::map<Node, std::map< Node, int > > d_quant_var_id;

   std::map<Node, std::vector< int > > d_star_insts;

-  Node getRepresentative(FirstOrderModel * fm, Node n);

-  Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n);

-  void addEntry( FirstOrderModel * fm, Node op, Node c, Node v,

+  Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);

+  int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);

+protected:

+  void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,

                  std::vector< Node > & conds,

                  std::vector< Node > & values,

                  std::vector< Node > & entry_conds );

-  int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index);

 private:

-  void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n );

+  void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );

 

   void doNegate( Def & dc );

-  void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq );

-  void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v);

-  void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc );

+  void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );

+  void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);

+  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );

 

-  void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,

+  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,

                                std::vector< Def > & dc, int index,

                                std::vector< Node > & cond, std::vector<Node> & val );

-  void doUninterpretedCompose2( FirstOrderModel * fm, Node f,

+  void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,

                                 std::map< int, Node > & entries, int index,

                                 std::vector< Node > & cond, std::vector< Node > & val,

                                 EntryTrie & curr);

 

-  void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,

+  void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,

                              std::vector< Def > & dc, int index,

                              std::vector< Node > & cond, std::vector<Node> & val );

-  int isCompat( std::vector< Node > & cond, Node c );

-  bool doMeet( std::vector< Node > & cond, Node c );

+  int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );

+  bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );

   Node mkCond( std::vector< Node > & cond );

-  Node mkCondDefault( Node f );

-  void mkCondDefaultVec( Node f, std::vector< Node > & cond );

+  Node mkCondDefault( FirstOrderModelFmc * fm, Node f );

+  void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );

   void mkCondVec( Node n, std::vector< Node > & cond );

   Node evaluateInterpreted( Node n, std::vector< Node > & vals );

 public:

@@ -124,25 +149,20 @@ public:
   ~FullModelChecker(){}

 

   int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }

-  bool isStar(Node n);

-  Node getStar(TypeNode tn);

-  Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn);

-  bool isModelBasisTerm(Node n);

-  Node getModelBasisTerm(TypeNode tn);

-  Def * getModel(FirstOrderModel * fm, Node op);

 

   void debugPrintCond(const char * tr, Node n, bool dispStar = false);

   void debugPrint(const char * tr, Node n, bool dispStar = false);

 

   bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );

 

-  bool useSimpleModels();

-  Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );

+  Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );

 

   /** process build model */

   void processBuildModel(TheoryModel* m, bool fullModel);

   /** get current model value */

-  Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );

+  Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );

+

+  bool useSimpleModels();

 };

 

 }

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 76e61707e..88fb7cd8f 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -18,7 +18,6 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_model.h"
 #include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/model_builder.h"
@@ -45,38 +44,37 @@ bool QModelBuilder::optUseModel() {
   return options::fmfModelBasedInst();
 }
 
-
-Node QModelBuilder::getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial ) {
-  std::vector< Node > children;
-  if( n.getNumChildren()>0 ){
-    if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.push_back( n.getOperator() );
-    }
-    for (unsigned i=0; i<n.getNumChildren(); i++) {
-      Node nc = getCurrentModelValue( fm, n[i] );
-      if (nc.isNull()) {
-        return Node::null();
-      }else{
-        children.push_back( nc );
+void QModelBuilder::debugModel( FirstOrderModel* fm ){
+  //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
+  if( Trace.isOn("quant-model-warn") ){
+    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      std::vector< Node > vars;
+      for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+        vars.push_back( f[0][j] );
+      }
+      RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+      riter.setQuantifier( f );
+      while( !riter.isFinished() ){
+        std::vector< Node > terms;
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          terms.push_back( riter.getTerm( i ) );
+        }
+        Node n = d_qe->getInstantiation( f, vars, terms );
+        Node val = fm->getValue( n );
+        if( val!=fm->d_true ){
+          Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
+          Trace("quant-model-warn") << "         " << f << std::endl;
+          Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
+        }
+        riter.increment();
       }
-    }
-    if( n.getKind()==APPLY_UF ){
-      return getCurrentUfModelValue( fm, n, children, partial );
-    }else{
-      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      nn = Rewriter::rewrite( nn );
-      return nn;
-    }
-  }else{
-    if( n.getKind()==VARIABLE ){
-      return getCurrentUfModelValue( fm, n, children, partial );
-    }else{
-      return n;
     }
   }
 }
 
 
+
 bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   if( argIndex<(int)n.getNumChildren() ){
     Node r;
@@ -97,6 +95,7 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   }
 }
 
+
 QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
 QModelBuilder( c, qe ) {
 
@@ -106,37 +105,9 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::
   return n;
 }
 
-void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
-  //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
-  if( Trace.isOn("quant-model-warn") ){
-    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node f = fm->getAssertedQuantifier( i );
-      std::vector< Node > vars;
-      for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
-        vars.push_back( f[0][j] );
-      }
-      RepSetIterator riter( d_qe, &(fm->d_rep_set) );
-      riter.setQuantifier( f );
-      while( !riter.isFinished() ){
-        std::vector< Node > terms;
-        for( int i=0; i<riter.getNumTerms(); i++ ){
-          terms.push_back( riter.getTerm( i ) );
-        }
-        Node n = d_qe->getInstantiation( f, vars, terms );
-        Node val = fm->getValue( n );
-        if( val!=fm->d_true ){
-          Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
-          Trace("quant-model-warn") << "         " << f << std::endl;
-          Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
-        }
-        riter.increment();
-      }
-    }
-  }
-}
-
 void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
-  FirstOrderModel* fm = (FirstOrderModel*)m;
+  FirstOrderModel* f = (FirstOrderModel*)m;
+  FirstOrderModelIG* fm = f->asFirstOrderModelIG();
   if( fullModel ){
     Assert( d_curr_model==fm );
     //update models
@@ -303,16 +274,17 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
 }
 
 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 = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+  for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
     Node op = it->first;
     TermArgBasisTrie tabt;
-    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-      Node n = fm->d_uf_terms[op][i];
+    for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
+      Node n = fmig->d_uf_terms[op][i];
       //for calculating if op is constant
       if( !n.getAttribute(NoMatchAttribute()) ){
-        Node v = fm->getRepresentative( n );
+        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 ){
@@ -324,7 +296,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
       if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
         if( !n.getAttribute(BasisNoMatchAttribute()) ){
           //need to consider if it is not congruent modulo model basis
-          if( !tabt.addTerm( fm, n ) ){
+          if( !tabt.addTerm( fmig, n ) ){
              BasisNoMatchAttribute bnma;
              n.setAttribute(bnma,true);
           }
@@ -332,10 +304,10 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
       }
     }
     if( !d_uf_prefs[op].d_const_val.isNull() ){
-      fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
-      fm->d_uf_model_gen[op].makeModel( fm, it->second );
+      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 ";
-      fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+      fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
       Debug("fmf-model-cons") << std::endl;
       d_uf_model_constructed[op] = true;
     }else{
@@ -420,6 +392,7 @@ int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
 }
 
 void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node 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];
@@ -454,7 +427,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
           for( int j=0; j<2; j++ ){
             if( TermDb::hasInstConstAttr(n[j]) ){
               if( n[j].getKind()==APPLY_UF &&
-                  fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
+                  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{
@@ -542,7 +515,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
     for( int k=0; k<2; k++ ){
       for( int j=0; j<(int)pro_con[k].size(); j++ ){
         Node op = pro_con[k][j].getOperator();
-        Node r = fm->getRepresentative( pro_con[k][j] );
+        Node r = fmig->getRepresentative( pro_con[k][j] );
         d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
       }
     }
@@ -600,6 +573,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
 }
 
 void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
+  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
   if( optReconsiderFuncConstants() ){
     //reconsider constant functions that weren't necessary
     if( d_uf_model_constructed[op] ){
@@ -608,8 +582,8 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
         Node v = d_uf_prefs[op].d_const_val;
         if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
           Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
-          fm->d_uf_model_tree[op].clear();
-          fm->d_uf_model_gen[op].clear();
+          fmig->d_uf_model_tree[op].clear();
+          fmig->d_uf_model_gen[op].clear();
           d_uf_model_constructed[op] = false;
         }
       }
@@ -621,20 +595,20 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
     Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
     Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
     //set the values in the model
-    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-      Node n = fm->d_uf_terms[op][i];
+    for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
+      Node n = fmig->d_uf_terms[op][i];
       if( isTermActive( n ) ){
-        Node v = fm->getRepresentative( n );
-        Trace("fmf-model-cons") << "Set term " << n << " : " << fm->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+        Node v = fmig->getRepresentative( n );
+        Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.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
-        fm->d_uf_model_gen[op].setValue( fm, n, v );
-        if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){
+        fmig->d_uf_model_gen[op].setValue( fm, n, v );
+        if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
           //also set as default value if necessary
           if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
             Trace("fmf-model-cons") << "  Set as default." << std::endl;
-            fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+            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;
@@ -642,7 +616,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
           }
         }else{
           if( n==defaultTerm ){
-            fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
             //incidentally already set, we will not need to find a default value
             setDefaultVal = false;
           }
@@ -655,18 +629,18 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
       //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 (!fm->d_rep_set.hasType(defaultTerm.getType())) {
+        if (!fmig->d_rep_set.hasType(defaultTerm.getType())) {
           Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
-          fm->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
+          fmig->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
         }
-        defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0];
+        defaultVal = fmig->d_rep_set.d_type_reps[defaultTerm.getType()][0];
       }
       Assert( !defaultVal.isNull() );
-      Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl;
-      fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
+      Trace("fmf-model-cons") << "Set default term : " << fmig->d_rep_set.getIndexFor( defaultVal ) << std::endl;
+      fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
     }
     Debug("fmf-model-cons") << "  Making model...";
-    fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] );
+    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;
   }
@@ -1030,19 +1004,20 @@ void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, Ins
 }
 
 void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
+  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
   bool setDefaultVal = true;
   Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
   //set the values in the model
-  for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-    Node n = fm->d_uf_terms[op][i];
+  for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
+    Node n = fmig->d_uf_terms[op][i];
     if( isTermActive( n ) ){
-      Node v = fm->getRepresentative( n );
-      fm->d_uf_model_gen[op].setValue( fm, n, v );
+      Node v = fmig->getRepresentative( n );
+      fmig->d_uf_model_gen[op].setValue( fm, n, v );
     }
     //also possible set as default
     if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){
-      Node v = fm->getRepresentative( n );
-      fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+      Node v = fmig->getRepresentative( n );
+      fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
       if( n==defaultTerm ){
         setDefaultVal = false;
       }
@@ -1051,9 +1026,9 @@ void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
   //set the overall default value if not set already  (is this necessary??)
   if( setDefaultVal ){
     Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
-    fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
+    fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
   }
-  fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] );
+  fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
   d_uf_model_constructed[op] = true;
 }
 
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index f41392eee..715612975 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -33,8 +33,6 @@ protected:
   context::CDO< FirstOrderModel* > d_curr_model;
   //quantifiers engine
   QuantifiersEngine* d_qe;
-  /** get current model value */
-  virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilder(){}
@@ -50,8 +48,8 @@ public:
   bool d_considerAxioms;
   /** exist instantiation ? */
   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
-  /** get current model value */
-  Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false );
+  //debug model
+  void debugModel( FirstOrderModel* fm );
 };
 
 
@@ -123,8 +121,6 @@ protected:  //helper functions
 public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilderIG(){}
-  //debug model
-  void debugModel( FirstOrderModel* fm );
 public:
   //whether to add inst-gen lemmas
   virtual bool optInstGen();
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index c91d9d3ab..32deb9e47 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -18,7 +18,6 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/quantifiers/options.h"
-#include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -35,8 +34,7 @@ using namespace CVC4::theory::inst;
 
 //Model Engine constructor
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
-QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ){
+QuantifiersModule( qe ){
 
   if( options::fmfFullModelCheck() ){
     d_builder = new fmcheck::FullModelChecker( c, qe );
@@ -179,9 +177,8 @@ int ModelEngine::checkModel(){
   }
   */
   //compute the relevant domain if necessary
-  if( optUseRelevantDomain() ){
-    d_rel_domain.compute();
-  }
+  //if( optUseRelevantDomain() ){
+  //}
   d_triedLemmas = 0;
   d_testLemmas = 0;
   d_relevantLemmas = 0;
@@ -240,8 +237,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
-      d_quantEngine->getModel()->resetEvaluate();
+      FirstOrderModelIG * fmig = NULL;
+      if( !options::fmfFullModelCheck() ){
+        fmig = (FirstOrderModelIG*)d_quantEngine->getModel();
+        Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+        fmig->resetEvaluate();
+      }
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
       int tests = 0;
       int triedLemmas = 0;
@@ -252,7 +253,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         d_testLemmas++;
         int eval = 0;
         int depIndex;
-        if( d_builder->optUseModel() ){
+        if( d_builder->optUseModel() && fmig ){
           //see if instantiation is already true in current model
           Debug("fmf-model-eval") << "Evaluating ";
           riter.debugPrintSmall("fmf-model-eval");
@@ -261,7 +262,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           //if evaluate(...)==1, then the instantiation is already true in the model
           //  depIndex is the index of the least significant variable that this evaluation relies upon
           depIndex = riter.getNumTerms()-1;
-          eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+          eval = fmig->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
           if( eval==1 ){
             Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
           }else{
@@ -296,10 +297,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         }
       }
       //print debugging information
-      d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
-      d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
-      d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
-      d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+      if( fmig ){
+        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
+        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
+        d_statistics.d_eval_lits += fmig->d_eval_lits;
+        d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
+      }
       int relevantInst = 1;
       for( size_t i=0; i<f[0].getNumChildren(); i++ ){
         relevantInst = relevantInst * (int)riter.d_domain[i].size();
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 97aa085ed..0f0ab4fe7 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -20,7 +20,6 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/model_builder.h"
 #include "theory/model.h"
-#include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/full_model_check.h"
 
 namespace CVC4 {
@@ -34,8 +33,6 @@ private:
   /** builder class */
   QModelBuilder* d_builder;
 private:    //analysis of current model:
-  //relevant domain
-  RelevantDomain d_rel_domain;
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
 private:
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
deleted file mode 100644
index cf12cf540..000000000
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ /dev/null
@@ -1,198 +0,0 @@
-/*********************                                                        */
-/*! \file relevant_domain.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of relevant domain class
- **/
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/relevant_domain.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
-
-}
-
-void RelevantDomain::compute(){
-  Trace("rel-dom") << "compute relevant domain" << std::endl;
-  d_quant_inst_domain.clear();
-  for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_model->getAssertedQuantifier( i );
-    d_quant_inst_domain[f].resize( f[0].getNumChildren() );
-  }
-  Trace("rel-dom") << "account for ground terms" << std::endl;
-  //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
-  for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();
-       it != d_model->d_uf_model_tree.end(); ++it ){
-    Node op = it->first;
-    for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){
-      Node n = d_model->d_uf_terms[op][i];
-      //add arguments to domain
-      for( int j=0; j<(int)n.getNumChildren(); j++ ){
-        if( d_model->d_rep_set.hasType( n[j].getType() ) ){
-          Node ra = d_model->getRepresentative( n[j] );
-          int raIndex = d_model->d_rep_set.getIndexFor( ra );
-          if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl;
-          Assert( raIndex!=-1 );
-          if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
-            d_active_domain[op][j].push_back( raIndex );
-          }
-        }
-      }
-      //add to range
-      Node r = d_model->getRepresentative( n );
-      int raIndex = d_model->d_rep_set.getIndexFor( r );
-      if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl;
-      Assert( raIndex!=-1 );
-      if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){
-        d_active_range[op].push_back( raIndex );
-      }
-    }
-  }
-  Trace("rel-dom") << "do quantifiers" << std::endl;
-  //find fixed point for relevant domain computation
-  bool success;
-  do{
-    success = true;
-    for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
-      Node f = d_model->getAssertedQuantifier( i );
-      //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
-      if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){
-        success = false;
-      }
-      //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
-      RepDomain range;
-      if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){
-        success = false;
-      }
-    }
-  }while( !success );
-  Trace("rel-dom") << "done compute relevant domain" << std::endl;
-  /*
-  //debug printing
-  Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
-  if( useRelInstDomain ){
-    Trace("rel-dom") << "Relevant domain : " << std::endl;
-    for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){
-      Trace("rel-dom") << "   " << i << " : ";
-      for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){
-        Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " ";
-      }
-      Trace("rel-dom") << std::endl;
-    }
-  }
-  */
-}
-
-bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){
-  bool domainChanged = false;
-  if( n.getKind()==INST_CONSTANT ){
-    bool domainSet = false;
-    int vi = n.getAttribute(InstVarNumAttribute());
-    Assert( !parent.isNull() );
-    if( parent.getKind()==APPLY_UF ){
-      //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument
-      Node op = parent.getOperator();
-      if( d_active_domain.find( op )!=d_active_domain.end() ){
-        for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
-          int d = d_active_domain[op][arg][i];
-          if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )==
-              d_quant_inst_domain[f][vi].end() ){
-            d_quant_inst_domain[f][vi].push_back( d );
-            domainChanged = true;
-          }
-        }
-        domainSet = true;
-      }
-    }
-    if( !domainSet ){
-      //otherwise, we must consider the entire domain
-      TypeNode tn = n.getType();
-      if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){
-        if( d_model->d_rep_set.hasType( tn ) ){
-          //it is the complete domain
-          d_quant_inst_domain[f][vi].clear();
-          for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){
-            d_quant_inst_domain[f][vi].push_back( i );
-          }
-          domainChanged = true;
-        }
-        d_quant_inst_domain_complete[f][vi] = true;
-      }
-    }
-  }else{
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){
-        domainChanged = true;
-      }
-    }
-  }
-  return domainChanged;
-}
-
-bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
-  if( n.getKind()==INST_CONSTANT ){
-    Node f = TermDb::getInstConstAttr(n);
-    int var = n.getAttribute(InstVarNumAttribute());
-    range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
-    return false;
-  }else{
-    Node op;
-    if( n.getKind()==APPLY_UF ){
-      op = n.getOperator();
-    }
-    bool domainChanged = false;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      RepDomain childRange;
-      if( extendFunctionDomains( n[i], childRange ) ){
-        domainChanged = true;
-      }
-      if( n.getKind()==APPLY_UF ){
-        if( d_active_domain.find( op )!=d_active_domain.end() ){
-          for( int j=0; j<(int)childRange.size(); j++ ){
-            int v = childRange[j];
-            if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){
-              d_active_domain[op][i].push_back( v );
-              domainChanged = true;
-            }
-          }
-        }else{
-          //do this?
-        }
-      }
-    }
-    //get the range
-    if( TermDb::hasInstConstAttr(n) ){
-      if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
-        range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
-      }else{
-        //infinite range?
-      }
-    }else{
-      Node r = d_model->getRepresentative( n );
-      int index = d_model->d_rep_set.getIndexFor( r );
-      if( index==-1 ){
-        //we consider all ground terms in bodies of quantifiers to be the first ground representative
-        range.push_back( 0 );
-      }else{
-        range.push_back( index );
-      }
-    }
-    return domainChanged;
-  }
-}
\ No newline at end of file
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
deleted file mode 100644
index 6fc035e8a..000000000
--- a/src/theory/quantifiers/relevant_domain.h
+++ /dev/null
@@ -1,54 +0,0 @@
-/*********************                                                        */
-/*! \file relevant_domain.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief relevant domain class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class RelevantDomain
-{
-private:
-  QuantifiersEngine* d_qe;
-  FirstOrderModel* d_model;
-
-  //the domain of the arguments for each operator
-  std::map< Node, std::map< int, RepDomain > > d_active_domain;
-  //the range for each operator
-  std::map< Node, RepDomain > d_active_range;
-  //for computing relevant instantiation domain, return true if changed
-  bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f );
-  //for computing extended
-  bool extendFunctionDomains( Node n, RepDomain& range );
-public:
-  RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
-  virtual ~RelevantDomain(){}
-  //compute the relevant domain
-  void compute();
-  //relevant instantiation domain for each quantifier
-  std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
-  std::map< Node, std::map< int, bool > > d_quant_inst_domain_complete;
-};/* class RelevantDomain */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 89d1ad55a..c663e1aa2 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -48,7 +48,11 @@ d_lemmas_produced_c(u){
   d_hasAddedLemma = false;
 
   //the model object
-  d_model = new quantifiers::FirstOrderModel( c, "FirstOrderModel" );
+  if( options::fmfFullModelCheck() ){
+    d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
+  }else{
+    d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" );
+  }
 
   //add quantifiers modules
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 6903adda5..99e28714f 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -100,6 +100,7 @@ RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe),
 }
 
 int RepSetIterator::domainSize( int i ) {
+  Assert(i>=0);
   if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
     return d_domain[i].size();
   }else{
@@ -281,7 +282,9 @@ void RepSetIterator::increment2( int counter ){
   counter = (int)d_index.size()-1;
 #endif
   //increment d_index
-  Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+  if( counter>=0){
+    Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+  }
   while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
     counter--;
     if( counter>=0){