Fix numerous compiler warnings on various platforms

1 files changed, 1398 insertions, 1398 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 4c168acfc..6e7986390 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -1,1398 +1,1398 @@
-

-/*********************                                                        */

-/*! \file full_model_check.cpp

- ** \verbatim

- ** Original author: Andrew Reynolds

- ** 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 full model check class

- **/

-

-#include "theory/quantifiers/full_model_check.h"

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

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

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

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

-  }

-};

-

-

-struct ConstRationalSort

-{

-  std::vector< Node > d_terms;

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

-    return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() );

-  }

-};

-

-

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

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

-    return d_data!=-1;

-  }else{

-    TypeNode tn = c[index].getType();

-    Node st = m->getStar(tn);

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

-      if( d_child[st].hasGeneralization(m, c, index+1) ){

-        return true;

-      }

-    }

-    if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){

-      if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){

-        return true;

-      }

-    }

-    if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){

-      //for star: check if all children are defined and have generalizations

-      if( options::fmfFmcCoverSimplify() && c[index]==st ){

-        //check if all children exist and are complete

-        int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);

-        if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){

-          bool complete = true;

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

-            if( !m->isStar(it->first) ){

-              if( !it->second.hasGeneralization(m, c, index+1) ){

-                complete = false;

-                break;

-              }

-            }

-          }

-          if( complete ){

-            return true;

-          }

-        }

-      }

-    }

-

-    return false;

-  }

-}

-

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

-  Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;

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

-    return d_data;

-  }else{

-    int minIndex = -1;

-    if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){

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

-        if( !m->isInterval( it->first ) ){

-          std::cout << "Not an interval during getGenIndex " << it->first << std::endl;

-          exit( 11 );

-        }

-        //check if it is in the range

-        if( m->isInRange(inst[index], it->first )  ){

-          int gindex = it->second.getGeneralizationIndex(m, inst, index+1);

-          if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){

-            minIndex = gindex;

-          }

-        }

-      }

-    }else{

-      Node st = m->getStar(inst[index].getType());

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

-        minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);

-      }

-      Node cc = inst[index];

-      if( cc!=st && d_child.find( cc )!=d_child.end() ){

-        int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);

-        if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){

-          minIndex = gindex;

-        }

-      }

-    }

-    return minIndex;

-  }

-}

-

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

-    }

-  }

-  else {

-    d_child[ c[index] ].addEntry(m,c,v,data,index+1);

-    if( d_complete==0 ){

-      d_complete = -1;

-    }

-  }

-}

-

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

-        gen.push_back(d_data);

-      }

-      compat.push_back(d_data);

-    }

-  }else{

-    if (m->isStar(c[index])) {

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

-        it->second.getEntries(m, c, compat, gen, index+1, is_gen );

-      }

-    }else{

-      Node st = m->getStar(c[index].getType());

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

-        d_child[st].getEntries(m, c, compat, gen, index+1, false);

-      }

-      if( d_child.find( c[index] )!=d_child.end() ){

-        d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);

-      }

-    }

-

-  }

-}

-

-void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {

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

-    if( d_data!=-1 ){

-      indices.push_back( d_data );

-    }

-  }else{

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

-      it->second.collectIndices(c, index+1, indices );

-    }

-  }

-}

-

-bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) {

-  if( d_complete==-1 ){

-    d_complete = 1;

-    if (index<(int)c.getNumChildren()) {

-      Node st = m->getStar(c[index].getType());

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

-        if (!d_child[st].isComplete(m, c, index+1)) {

-          d_complete = 0;

-        }

-      }else{

-        d_complete = 0;

-      }

-    }

-  }

-  return d_complete==1;

-}

-

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

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

-    Trace("fmc-debug") << "Already has generalization, skip." << std::endl;

-    return false;

-  }

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

-  if (!d_has_simplified) {

-    std::vector<int> compat;

-    std::vector<int> gen;

-    d_et.getEntries(m, c, compat, gen);

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

-      if( d_status[compat[i]]==status_unk ){

-        if( d_value[compat[i]]!=v ){

-          d_status[compat[i]] = status_non_redundant;

-        }

-      }

-    }

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

-      if( d_status[gen[i]]==status_unk ){

-        if( d_value[gen[i]]==v ){

-          d_status[gen[i]] = status_redundant;

-        }

-      }

-    }

-    d_status.push_back( status_unk );

-  }

-  d_et.addEntry(m, c, v, newIndex);

-  d_cond.push_back(c);

-  d_value.push_back(v);

-  return true;

-}

-

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

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

-  if (gindex!=-1) {

-    return d_value[gindex];

-  }else{

-    Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;

-    return Node::null();

-  }

-}

-

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

-  return d_et.getGeneralizationIndex(m, inst);

-}

-

-void Def::basic_simplify( FirstOrderModelFmc * m ) {

-  d_has_simplified = true;

-  std::vector< Node > cond;

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

-  d_cond.clear();

-  std::vector< Node > value;

-  value.insert( value.end(), d_value.begin(), d_value.end() );

-  d_value.clear();

-  d_et.reset();

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

-    if( d_status[i]!=status_redundant ){

-      addEntry(m, cond[i], value[i]);

-    }

-  }

-  d_status.clear();

-}

-

-void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {

-  basic_simplify( m );

-

-  //check if the last entry is not all star, if so, we can make the last entry all stars

-  if( !d_cond.empty() ){

-    bool last_all_stars = true;

-    Node cc = d_cond[d_cond.size()-1];

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

-      if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){

-        last_all_stars = false;

-        break;

-      }

-    }

-    if( !last_all_stars ){

-      Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;

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

-      debugPrint("fmc-cover-simplify",Node::null(), mc);

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

-      std::vector< Node > cond;

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

-      d_cond.clear();

-      std::vector< Node > value;

-      value.insert( value.end(), d_value.begin(), d_value.end() );

-      d_value.clear();

-      d_et.reset();

-      d_has_simplified = false;

-      //change the last to all star

-      std::vector< Node > nc;

-      nc.push_back( cc.getOperator() );

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

-        nc.push_back(m->getStarElement(cc[j].getType()));

-      }

-      cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );

-      //re-add the entries

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

-        addEntry(m, cond[i], value[i]);

-      }

-      Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;

-      basic_simplify( m );

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

-      debugPrint("fmc-cover-simplify",Node::null(), mc);

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

-    }

-  }

-}

-

-void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {

-  if (!op.isNull()) {

-    Trace(tr) << "Model for " << op << " : " << std::endl;

-  }

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

-    //print the condition

-    if (!op.isNull()) {

-      Trace(tr) << op;

-    }

-    m->debugPrintCond(tr, d_cond[i], true);

-    Trace(tr) << " -> ";

-    m->debugPrint(tr, d_value[i]);

-    Trace(tr) << std::endl;

-  }

-}

-

-

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

-QModelBuilder( c, qe ){

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

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

-}

-

-bool FullModelChecker::optBuildAtFullModel() {

-  //need to build after full model has taken effect if we are constructing interval models

-  //  this is because we need to have a constant in all integer equivalence classes

-  return options::fmfFmcInterval();

-}

-

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

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

-  if( fullModel==optBuildAtFullModel() ){

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

-    fm->initialize( d_considerAxioms );

-    d_quant_models.clear();

-    d_rep_ids.clear();

-    d_star_insts.clear();

-    //process representatives

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

-         it != fm->d_rep_set.d_type_reps.end(); ++it ){

-      if( it->first.isSort() ){

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

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

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

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

-          //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";

-          Trace("fmc-model-debug") << " {";

-          //find best selection for representative

-          for( size_t i=0; i<eqc.size(); i++ ){

-            Trace("fmc-model-debug") << eqc[i] << ", ";

-          }

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

-

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

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

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

-            r = mbt;

-            mbt_index = a;

-          }

-          d_rep_ids[it->first][r] = (int)a;

-        }

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

-

-        if (mbt_index==-1) {

-          std::cout << "   WARNING: model basis term is not a representative!" << std::endl;

-          exit(0);

-        }else{

-          Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;

-        }

-      }

-    }

-    //also process non-rep set sorts

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

-      Node op = it->first;

-      TypeNode tno = op.getType();

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

-        initializeType( fm, tno[i] );

-      }

-    }

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

-

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

-

-

-      std::vector< Node > add_conds;

-      std::vector< Node > add_values;

-      bool needsDefault = true;

-      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()) ){

-          add_conds.push_back( n );

-          add_values.push_back( n );

-        }

-      }

-      //possibly get default

-      if( needsDefault ){

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

-        //add default value if necessary

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

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

-          add_conds.push_back( nmb );

-          add_values.push_back( nmb );

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

-          add_conds.push_back( nmb );

-          add_values.push_back( vmb );

-        }

-      }

-

-      std::vector< Node > conds;

-      std::vector< Node > values;

-      std::vector< Node > entry_conds;

-      //get the entries for the mdoel

-      for( size_t i=0; i<add_conds.size(); i++ ){

-        Node c = add_conds[i];

-        Node v = add_values[i];

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

-          if( !ri.getType().isSort() && !ri.isConst() ){

-            Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;

-          }

-          children.push_back(ri);

-          if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){

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

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

-            }else{

-              hasNonStar = true;

-            }

-          }

-          entry_children.push_back(ri);

-        }

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

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

-        if( !nv.getType().isSort() && !nv.isConst() ){

-          Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;

-        }

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

-        }

-        else {

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

-        }

-      }

-

-

-      //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++) {

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

-      }

-

-

-      if( options::fmfFmcInterval() ){

-        Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;

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

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

-        std::vector< int > indices;

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

-          indices.push_back( i );

-        }

-        std::map< int, std::map< int, Node > > changed_vals;

-        makeIntervalModel( fm, op, indices, 0, changed_vals );

-

-        std::vector< Node > conds;

-        std::vector< Node > values;

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

-          if( changed_vals.find(i)==changed_vals.end() ){

-            conds.push_back( fm->d_models[op]->d_cond[i] );

-          }else{

-            std::vector< Node > children;

-            children.push_back( op );

-            for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){

-              if( changed_vals[i].find(j)==changed_vals[i].end() ){

-                children.push_back( fm->d_models[op]->d_cond[i][j] );

-              }else{

-                children.push_back( changed_vals[i][j] );

-              }

-            }

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

-            conds.push_back( nc );

-            Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";

-            debugPrintCond("fmc-interval-model", nc, true );

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

-          }

-          values.push_back( fm->d_models[op]->d_value[i] );

-        }

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

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

-          fm->d_models[op]->addEntry(fm, conds[i], values[i] );

-        }

-      }

-

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

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

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

-

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

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

-

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

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

-    }

-  }

-  if( fullModel ){

-    //make function values

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

-      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );

-    }

-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );

-    //mark that the model has been set

-    fm->markModelSet();

-    //debug the model

-    debugModel( fm );

-  }

-}

-

-void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){

-  if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){

-    Trace("fmc") << "Initialize type " << tn << std::endl;

-    Node mbn;

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

-      mbn = fm->getSomeDomainElement(tn);

-    }else{

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

-    }

-    Node mbnr = fm->getUsedRepresentative( mbn );

-    fm->d_model_basis_rep[tn] = mbnr;

-    Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;

-  }

-}

-

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

-  Trace(tr) << "(";

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

-    if( j>0 ) Trace(tr) << ", ";

-    debugPrint(tr, n[j], dispStar);

-  }

-  Trace(tr) << ")";

-}

-

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

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

-  if( n.isNull() ){

-    Trace(tr) << "null";

-  }

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

-    Trace(tr) << "*";

-  }

-  else if(fm->isInterval(n)) {

-    debugPrint(tr, n[0], dispStar );

-    Trace(tr) << "...";

-    debugPrint(tr, n[1], dispStar );

-  }else{

-    TypeNode tn = n.getType();

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

-      if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {

-        Trace(tr) << d_rep_ids[tn][n];

-      }else{

-        Trace(tr) << n;

-      }

-    }else{

-      Trace(tr) << n;

-    }

-  }

-}

-

-

-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {

-  Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;

-  if( optUseModel() ){

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

-    if (effort==0) {

-      //register the quantifier

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

-        std::vector< TypeNode > types;

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

-          types.push_back(f[0][i].getType());

-          d_quant_var_id[f][f[0][i]] = i;

-        }

-        TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );

-        Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );

-        d_quant_cond[f] = op;

-      }

-      //make sure all types are set

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

-        initializeType( fmfmc, f[0][i].getType() );

-      }

-

-      //model check the quantifier

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

-

-      //consider all entries going to non-true

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

-        if( d_quant_models[f].d_value[i]!=d_true) {

-          Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;

-          bool hasStar = false;

-          std::vector< Node > inst;

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

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

-              hasStar = true;

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

-            }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){

-              hasStar = true;

-              //if interval, find a sample point

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

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

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

-                }else{

-                  Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],

-                                                              NodeManager::currentNM()->mkConst( Rational(1) ) );

-                  nn = Rewriter::rewrite( nn );

-                  inst.push_back( nn );

-                }

-              }else{

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

-              }

-            }else{

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

-            }

-          }

-          bool addInst = true;

-          if( hasStar ){

-            //try obvious (specified by 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(fmfmc, inst);

-              if( ev==d_true ){

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

-                exit(0);

-              }else{

-                Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;

-              }

-            }

-          }

-          if( addInst ){

-            InstMatch m;

-            for( unsigned j=0; j<inst.size(); j++) {

-              m.set( d_qe, f, j, inst[j] );

-            }

-            d_triedLemmas++;

-            if( d_qe->addInstantiation( f, m ) ){

-              d_addedLemmas++;

-            }else{

-              //this can happen if evaluation is unknown

-              //might try it next effort level

-              d_star_insts[f].push_back(i);

-            }

-          }else{

-            //might try it next effort level

-            d_star_insts[f].push_back(i);

-          }

-        }

-      }

-    }else{

-      if (!d_star_insts[f].empty()) {

-        Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;

-        Trace("fmc-exh") << "Definition was : " << std::endl;

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

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

-        Def temp;

-        //simplify the exceptions?

-        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(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){

-            if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){

-              //something went wrong, resort to exhaustive instantiation

-              return false;

-            }

-          }

-        }

-      }

-    }

-    return true;

-  }else{

-    return false;

-  }

-}

-

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

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

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

-  debugPrintCond("fmc-exh", c, true);

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

-  Trace("fmc-exh-debug") << "Set interval domains..." << std::endl;

-  //set the bounds on the iterator based on intervals

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

-    if( c[i].getType().isInteger() ){

-      if( fm->isInterval(c[i]) ){

-        for( unsigned b=0; b<2; b++ ){

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

-            riter.d_bounds[b][i] = c[i][b];

-          }

-        }

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

-        riter.d_bounds[0][i] = c[i];

-        riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );

-      }

-    }

-  }

-  Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;

-  //initialize

-  if( riter.setQuantifier( f ) ){

-    Trace("fmc-exh-debug") << "Set element domains..." << std::endl;

-    //set the domains based on the entry

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

-      if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {

-        TypeNode tn = c[i].getType();

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

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

-            //add the full range

-          }else{

-            if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {

-              riter.d_domain[i].clear();

-              riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);

-            }else{

-              return false;

-            }

-          }

-        }else{

-          return false;

-        }

-      }

-    }

-    int addedLemmas = 0;

-    //now do full iteration

-    while( !riter.isFinished() ){

-      d_triedLemmas++;

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

-      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 = 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(fm, inst);

-      Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();

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

-      if (ev!=d_true) {

-        InstMatch m;

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

-          m.set( d_qe, f, i, riter.getTerm( i ) );

-        }

-        Trace("fmc-exh-debug") << ", add!";

-        //add as instantiation

-        if( d_qe->addInstantiation( f, m ) ){

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

-          addedLemmas++;

-        }

-      }else{

-        Trace("fmc-exh-debug") << ", already true";

-      }

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

-      int index = riter.increment();

-      Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;

-      if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {

-        Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;

-        riter.increment2( index-1 );

-      }

-    }

-    d_addedLemmas += addedLemmas;

-    return true;

-  }else{

-    return false;

-  }

-}

-

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

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

-  //first check if it is a bounding literal

-  if( n.hasAttribute(BoundIntLitAttribute()) ){

-    Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;

-    d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );

-  }else if( n.getKind() == kind::BOUND_VARIABLE ){

-    Trace("fmc-debug") << "Add default entry..." << std::endl;

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

-  }

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

-    //just do directly

-    doCheck( fm, f, d, n[0] );

-    doNegate( d );

-  }

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

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

-  }

-  else if( n.getType().isArray() ){

-    //make the definition

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

-    Trace("fmc-debug") << "Representative for array is " << r << std::endl;

-    while( r.getKind() == kind::STORE ){

-      Node i = fm->getUsedRepresentative( r[1] );

-      Node e = fm->getUsedRepresentative( r[2] );

-      d.addEntry(fm, mkArrayCond(i), e );

-      r = r[0];

-    }

-    Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));

-    bool success = false;

-    if( r.getKind() == kind::STORE_ALL ){

-      ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();

-      Node defaultValue = Node::fromExpr(storeAll.getExpr());

-      defaultValue = fm->getUsedRepresentative( defaultValue, true );

-      if( !defaultValue.isNull() ){

-        d.addEntry(fm, defC, defaultValue);

-        success = true;

-      }

-    }

-    if( !success ){

-      Trace("fmc-debug") << "Can't process base array " << r << std::endl;

-      //can't process this array

-      d.reset();

-      d.addEntry(fm, defC, Node::null());

-    }

-  }

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

-    Node r = n;

-    if( !n.isConst() ){

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

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

-      }

-      r = fm->getUsedRepresentative( r );

-    }

-    Trace("fmc-debug") << "Add constant entry..." << std::endl;

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

-  }

-  else{

-    std::vector< int > var_ch;

-    std::vector< Def > children;

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

-      Def dc;

-      doCheck(fm, f, dc, n[i]);

-      children.push_back(dc);

-      if( n[i].getKind() == kind::BOUND_VARIABLE ){

-        var_ch.push_back(i);

-      }

-    }

-

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

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

-      //uninterpreted compose

-      doUninterpretedCompose( fm, f, d, n.getOperator(), children );

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

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

-      std::vector< Def > children2;

-      children2.push_back( children[1] );

-      std::vector< Node > cond;

-      mkCondDefaultVec(fm, f, cond);

-      std::vector< Node > val;

-      doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );

-    } else {

-      if( !var_ch.empty() ){

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

-          if( var_ch.size()==2 ){

-            Trace("fmc-debug") << "Do variable equality " << n << std::endl;

-            doVariableEquality( fm, f, d, n );

-          }else{

-            Trace("fmc-debug") << "Do variable relation " << n << std::endl;

-            doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );

-          }

-        }else{

-          Trace("fmc-warn") << "Don't know how to check " << n << std::endl;

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

-        }

-      }else{

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

-        std::vector< Node > cond;

-        mkCondDefaultVec(fm, f, cond);

-        std::vector< Node > val;

-        //interpreted compose

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

-      }

-    }

-    Trace("fmc-debug") << "Simplify the definition..." << std::endl;

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

-    d.simplify(this, fm);

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

-  }

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

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

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

-}

-

-void FullModelChecker::doNegate( Def & dc ) {

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

-    if (!dc.d_value[i].isNull()) {

-      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;

-    }

-  }

-}

-

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

-  std::vector<Node> cond;

-  mkCondDefaultVec(fm, f, cond);

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

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

-  }else{

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

-    if( tn.isSort() ){

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

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

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

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

-      }

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

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

-        cond[j+1] = r;

-        cond[k+1] = r;

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

-      }

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

-    }else{

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

-    }

-  }

-}

-

-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( val.isNull() ){

-      d.addEntry( fm, dc.d_cond[i], val);

-    }else{

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

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

-          std::vector<Node> cond;

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

-          cond[j+1] = val;

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

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

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

-        }else{

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

-        }

-      }else{

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

-      }

-    }

-  }

-}

-

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

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

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

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

-

-  std::vector< Node > cond;

-  mkCondDefaultVec(fm, f, cond);

-  std::vector< Node > val;

-  doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);

-}

-

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

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

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

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

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

-    debugPrint("fmc-uf-process", cond[i], true);

-    Trace("fmc-uf-process") << " ";

-  }

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

-  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, df.d_et);

-    if( entries.empty() ){

-      d.addEntry(fm, mkCond(cond), Node::null());

-    }else{

-      //add them to the definition

-      for( unsigned e=0; e<df.d_cond.size(); e++ ){

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

-          Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;

-          d.addEntry(fm, entries[e], df.d_value[e] );

-          Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;

-        }

-      }

-    }

-  }else{

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

-      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(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, d, df, dc, index+1, new_cond, val);

-          val.pop_back();

-        }else{

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

-        }

-      }

-    }

-  }

-}

-

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

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

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

-                                                EntryTrie & curr ) {

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

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

-    debugPrint("fmc-uf-process", cond[i], true);

-    Trace("fmc-uf-process") << " ";

-  }

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

-  if (index==(int)val.size()) {

-    Node c = mkCond(cond);

-    Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;

-    entries[curr.d_data] = c;

-  }else{

-    Node v = val[index];

-    bool bind_var = false;

-    if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){

-      int j = getVariableId(f, v);

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

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

-        v = cond[j+1];

-      }else{

-        bind_var = true;

-      }

-    }

-    if (bind_var) {

-      Trace("fmc-uf-process") << "bind variable..." << std::endl;

-      int j = getVariableId(f, v);

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

-        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {

-          cond[j+1] = it->first;

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

-        }

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

-      }else{

-        Node orig = cond[j+1];

-        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {

-          Node nw = doIntervalMeet( fm, it->first, orig );

-          if( !nw.isNull() ){

-            cond[j+1] = nw;

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

-          }

-        }

-        cond[j+1] = orig;

-      }

-    }else{

-      if( !v.isNull() ){

-        if( options::fmfFmcInterval() && v.getType().isInteger() ){

-          for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {

-            if( fm->isInRange( v, it->first ) ){

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

-            }

-          }

-        }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 = fm->getStarElement(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]);

-          }

-        }

-      }

-    }

-  }

-}

-

-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(fm, c, v);

-  }

-  else {

-    TypeNode vtn = n.getType();

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

-      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(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(fm, c, dc[index].d_value[i]);

-              process = false;

-            }

-          }

-          if (process) {

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

-            doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);

-            val.pop_back();

-          }

-        }

-      }

-    }

-  }

-}

-

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

-  Trace("fmc-debug2") << "isCompat " << c << std::endl;

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

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

-    if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){

-      Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );

-      if( iv.isNull() ){

-        return 0;

-      }

-    }else{

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

-        return 0;

-      }

-    }

-  }

-  return 1;

-}

-

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

-  Trace("fmc-debug2") << "doMeet " << c << std::endl;

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

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

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

-      if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){

-        Node iv = doIntervalMeet( fm, cond[i], c[i-1] );

-        if( !iv.isNull() ){

-          cond[i] = iv;

-        }else{

-          return false;

-        }

-      }else{

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

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

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

-          return false;

-        }

-      }

-    }

-  }

-  return true;

-}

-

-Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {

-  if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){

-    std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;

-    exit( 0 );

-  }

-  Node b[2];

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

-    Node b1 = i1[j];

-    Node b2 = i2[j];

-    if( fm->isStar( b1 ) ){

-      b[j] = b2;

-    }else if( fm->isStar( b2 ) ){

-      b[j] = b1;

-    }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){

-      b[j] = j==0 ? b2 : b1;

-    }else{

-      b[j] = j==0 ? b1 : b2;

-    }

-  }

-  if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){

-    return mk ? fm->getInterval( b[0], b[1] ) : i1;

-  }else{

-    return Node::null();

-  }

-}

-

-Node FullModelChecker::mkCond( std::vector< Node > & cond ) {

-  return NodeManager::currentNM()->mkNode(APPLY_UF, cond);

-}

-

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

-  std::vector< Node > cond;

-  mkCondDefaultVec(fm, f, cond);

-  return mkCond(cond);

-}

-

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

-  Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;

-  //get function symbol for f

-  cond.push_back(d_quant_cond[f]);

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

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

-    cond.push_back(ts);

-  }

-}

-

-void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {

-  cond.push_back(n.getOperator());

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

-    cond.push_back( n[i] );

-  }

-}

-

-Node FullModelChecker::mkArrayCond( Node a ) {

-  if( d_array_term_cond.find(a)==d_array_term_cond.end() ){

-    if( d_array_cond.find(a.getType())==d_array_cond.end() ){

-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );

-      Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );

-      d_array_cond[a.getType()] = op;

-    }

-    std::vector< Node > cond;

-    cond.push_back(d_array_cond[a.getType()]);

-    cond.push_back(a);

-    d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond );

-  }

-  return d_array_term_cond[a];

-}

-

-Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {

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

-    if (!vals[0].isNull() && !vals[1].isNull()) {

-      return vals[0]==vals[1] ? d_true : d_false;

-    }else{

-      return Node::null();

-    }

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

-    if( vals[0]==d_true ){

-      return vals[1];

-    }else if( vals[0]==d_false ){

-      return vals[2];

-    }else{

-      return vals[1]==vals[2] ? vals[1] : Node::null();

-    }

-  }else if( n.getKind()==AND || n.getKind()==OR ){

-    bool isNull = false;

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

-      if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {

-        return vals[i];

-      }else if( vals[i].isNull() ){

-        isNull = true;

-      }

-    }

-    return isNull ? Node::null() : vals[0];

-  }else{

-    std::vector<Node> children;

-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){

-      children.push_back( n.getOperator() );

-    }

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

-      if( vals[i].isNull() ){

-        return Node::null();

-      }else{

-        children.push_back( vals[i] );

-      }

-    }

-    Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);

-    Trace("fmc-eval") << "Evaluate " << nc << " to ";

-    nc = Rewriter::rewrite(nc);

-    Trace("fmc-eval") << nc << std::endl;

-    return nc;

-  }

-}

-

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

-  bool addRepId = !fm->d_rep_set.hasType( tn );

-  Node de = fm->getSomeDomainElement(tn);

-  if( addRepId ){

-    d_rep_ids[tn][de] = 0;

-  }

-  return de;

-}

-

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

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

-}

-

-

-bool FullModelChecker::useSimpleModels() {

-  return options::fmfFmcSimple();

-}

-

-void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

-                                          std::map< int, std::map< int, Node > >& changed_vals ) {

-  if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){

-    makeIntervalModel2( fm, op, indices, 0, changed_vals );

-  }else{

-    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();

-    if( tn.isInteger() ){

-      makeIntervalModel(fm,op,indices,index+1, changed_vals );

-    }else{

-      std::map< Node, std::vector< int > > new_indices;

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

-        Node v = fm->d_models[op]->d_cond[indices[i]][index];

-        new_indices[v].push_back( indices[i] );

-      }

-

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

-        makeIntervalModel( fm, op, it->second, index+1, changed_vals );

-      }

-    }

-  }

-}

-

-void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

-                                          std::map< int, std::map< int, Node > >& changed_vals ) {

-  Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";

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

-    Debug("fmc-interval-model-debug") << indices[i] << " ";

-  }

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

-

-  if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){

-    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();

-    if( tn.isInteger() ){

-      std::map< Node, std::vector< int > > new_indices;

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

-        Node v = fm->d_models[op]->d_cond[indices[i]][index];

-        new_indices[v].push_back( indices[i] );

-        if( !v.isConst() ){

-          Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;

-          Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;

-        }

-      }

-

-      std::vector< Node > values;

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

-        makeIntervalModel2( fm, op, it->second, index+1, changed_vals );

-        values.push_back( it->first );

-      }

-

-      if( tn.isInteger() ){

-        //sort values by size

-        ConstRationalSort crs;

-        std::vector< int > sindices;

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

-          sindices.push_back( (int)i );

-          crs.d_terms.push_back( values[i] );

-        }

-        std::sort( sindices.begin(), sindices.end(), crs );

-

-        Node ub = fm->getStar( tn );

-        for( int i=(int)(sindices.size()-1); i>=0; i-- ){

-          Node lb = fm->getStar( tn );

-          if( i>0 ){

-            lb = values[sindices[i]];

-          }

-          Node interval = fm->getInterval( lb, ub );

-          for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){

-            Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;

-            changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;

-          }

-          ub = lb;

-        }

-      }

-    }else{

-      makeIntervalModel2( fm, op, indices, index+1, changed_vals );

-    }

-  }

-}
\ No newline at end of file
+
+/*********************                                                        */
+/*! \file full_model_check.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** 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 full model check class
+ **/
+
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+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()) );
+  }
+};
+
+
+struct ConstRationalSort
+{
+  std::vector< Node > d_terms;
+  bool operator() (int i, int j) {
+    return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() );
+  }
+};
+
+
+bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
+  if (index==(int)c.getNumChildren()) {
+    return d_data!=-1;
+  }else{
+    TypeNode tn = c[index].getType();
+    Node st = m->getStar(tn);
+    if(d_child.find(st)!=d_child.end()) {
+      if( d_child[st].hasGeneralization(m, c, index+1) ){
+        return true;
+      }
+    }
+    if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){
+      if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){
+        return true;
+      }
+    }
+    if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){
+      //for star: check if all children are defined and have generalizations
+      if( options::fmfFmcCoverSimplify() && c[index]==st ){
+        //check if all children exist and are complete
+        int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);
+        if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){
+          bool complete = true;
+          for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+            if( !m->isStar(it->first) ){
+              if( !it->second.hasGeneralization(m, c, index+1) ){
+                complete = false;
+                break;
+              }
+            }
+          }
+          if( complete ){
+            return true;
+          }
+        }
+      }
+    }
+
+    return false;
+  }
+}
+
+int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {
+  Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;
+  if (index==(int)inst.size()) {
+    return d_data;
+  }else{
+    int minIndex = -1;
+    if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
+      for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+        if( !m->isInterval( it->first ) ){
+          std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
+          exit( 11 );
+        }
+        //check if it is in the range
+        if( m->isInRange(inst[index], it->first )  ){
+          int gindex = it->second.getGeneralizationIndex(m, inst, index+1);
+          if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+            minIndex = gindex;
+          }
+        }
+      }
+    }else{
+      Node st = m->getStar(inst[index].getType());
+      if(d_child.find(st)!=d_child.end()) {
+        minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
+      }
+      Node cc = inst[index];
+      if( cc!=st && d_child.find( cc )!=d_child.end() ){
+        int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);
+        if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+          minIndex = gindex;
+        }
+      }
+    }
+    return minIndex;
+  }
+}
+
+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;
+    }
+  }
+  else {
+    d_child[ c[index] ].addEntry(m,c,v,data,index+1);
+    if( d_complete==0 ){
+      d_complete = -1;
+    }
+  }
+}
+
+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 ){
+        gen.push_back(d_data);
+      }
+      compat.push_back(d_data);
+    }
+  }else{
+    if (m->isStar(c[index])) {
+      for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+        it->second.getEntries(m, c, compat, gen, index+1, is_gen );
+      }
+    }else{
+      Node st = m->getStar(c[index].getType());
+      if(d_child.find(st)!=d_child.end()) {
+        d_child[st].getEntries(m, c, compat, gen, index+1, false);
+      }
+      if( d_child.find( c[index] )!=d_child.end() ){
+        d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);
+      }
+    }
+
+  }
+}
+
+void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {
+  if (index==(int)c.getNumChildren()) {
+    if( d_data!=-1 ){
+      indices.push_back( d_data );
+    }
+  }else{
+    for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+      it->second.collectIndices(c, index+1, indices );
+    }
+  }
+}
+
+bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) {
+  if( d_complete==-1 ){
+    d_complete = 1;
+    if (index<(int)c.getNumChildren()) {
+      Node st = m->getStar(c[index].getType());
+      if(d_child.find(st)!=d_child.end()) {
+        if (!d_child[st].isComplete(m, c, index+1)) {
+          d_complete = 0;
+        }
+      }else{
+        d_complete = 0;
+      }
+    }
+  }
+  return d_complete==1;
+}
+
+bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
+  if (d_et.hasGeneralization(m, c)) {
+    Trace("fmc-debug") << "Already has generalization, skip." << std::endl;
+    return false;
+  }
+  int newIndex = (int)d_cond.size();
+  if (!d_has_simplified) {
+    std::vector<int> compat;
+    std::vector<int> gen;
+    d_et.getEntries(m, c, compat, gen);
+    for( unsigned i=0; i<compat.size(); i++) {
+      if( d_status[compat[i]]==status_unk ){
+        if( d_value[compat[i]]!=v ){
+          d_status[compat[i]] = status_non_redundant;
+        }
+      }
+    }
+    for( unsigned i=0; i<gen.size(); i++) {
+      if( d_status[gen[i]]==status_unk ){
+        if( d_value[gen[i]]==v ){
+          d_status[gen[i]] = status_redundant;
+        }
+      }
+    }
+    d_status.push_back( status_unk );
+  }
+  d_et.addEntry(m, c, v, newIndex);
+  d_cond.push_back(c);
+  d_value.push_back(v);
+  return true;
+}
+
+Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
+  int gindex = d_et.getGeneralizationIndex(m, inst);
+  if (gindex!=-1) {
+    return d_value[gindex];
+  }else{
+    Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;
+    return Node::null();
+  }
+}
+
+int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
+  return d_et.getGeneralizationIndex(m, inst);
+}
+
+void Def::basic_simplify( FirstOrderModelFmc * m ) {
+  d_has_simplified = true;
+  std::vector< Node > cond;
+  cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
+  d_cond.clear();
+  std::vector< Node > value;
+  value.insert( value.end(), d_value.begin(), d_value.end() );
+  d_value.clear();
+  d_et.reset();
+  for (unsigned i=0; i<d_status.size(); i++) {
+    if( d_status[i]!=status_redundant ){
+      addEntry(m, cond[i], value[i]);
+    }
+  }
+  d_status.clear();
+}
+
+void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
+  basic_simplify( m );
+
+  //check if the last entry is not all star, if so, we can make the last entry all stars
+  if( !d_cond.empty() ){
+    bool last_all_stars = true;
+    Node cc = d_cond[d_cond.size()-1];
+    for( unsigned i=0; i<cc.getNumChildren(); i++ ){
+      if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){
+        last_all_stars = false;
+        break;
+      }
+    }
+    if( !last_all_stars ){
+      Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;
+      Trace("fmc-cover-simplify") << "Before: " << std::endl;
+      debugPrint("fmc-cover-simplify",Node::null(), mc);
+      Trace("fmc-cover-simplify") << std::endl;
+      std::vector< Node > cond;
+      cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
+      d_cond.clear();
+      std::vector< Node > value;
+      value.insert( value.end(), d_value.begin(), d_value.end() );
+      d_value.clear();
+      d_et.reset();
+      d_has_simplified = false;
+      //change the last to all star
+      std::vector< Node > nc;
+      nc.push_back( cc.getOperator() );
+      for( unsigned j=0; j< cc.getNumChildren(); j++){
+        nc.push_back(m->getStarElement(cc[j].getType()));
+      }
+      cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );
+      //re-add the entries
+      for (unsigned i=0; i<cond.size(); i++) {
+        addEntry(m, cond[i], value[i]);
+      }
+      Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;
+      basic_simplify( m );
+      Trace("fmc-cover-simplify") << "After: " << std::endl;
+      debugPrint("fmc-cover-simplify",Node::null(), mc);
+      Trace("fmc-cover-simplify") << std::endl;
+    }
+  }
+}
+
+void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
+  if (!op.isNull()) {
+    Trace(tr) << "Model for " << op << " : " << std::endl;
+  }
+  for( unsigned i=0; i<d_cond.size(); i++) {
+    //print the condition
+    if (!op.isNull()) {
+      Trace(tr) << op;
+    }
+    m->debugPrintCond(tr, d_cond[i], true);
+    Trace(tr) << " -> ";
+    m->debugPrint(tr, d_value[i]);
+    Trace(tr) << std::endl;
+  }
+}
+
+
+FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
+QModelBuilder( c, qe ){
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+bool FullModelChecker::optBuildAtFullModel() {
+  //need to build after full model has taken effect if we are constructing interval models
+  //  this is because we need to have a constant in all integer equivalence classes
+  return options::fmfFmcInterval();
+}
+
+void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
+  FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+  if( fullModel==optBuildAtFullModel() ){
+    Trace("fmc") << "---Full Model Check reset() " << std::endl;
+    fm->initialize( d_considerAxioms );
+    d_quant_models.clear();
+    d_rep_ids.clear();
+    d_star_insts.clear();
+    //process representatives
+    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+         it != fm->d_rep_set.d_type_reps.end(); ++it ){
+      if( it->first.isSort() ){
+        Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+        Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
+        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 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);
+          Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+          //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+          Trace("fmc-model-debug") << " {";
+          //find best selection for representative
+          for( size_t i=0; i<eqc.size(); i++ ){
+            Trace("fmc-model-debug") << eqc[i] << ", ";
+          }
+          Trace("fmc-model-debug") << "}" << std::endl;
+
+          //if this is the model basis eqc, replace with actual model basis term
+          if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
+            fm->d_model_basis_rep[it->first] = r;
+            r = mbt;
+            mbt_index = a;
+          }
+          d_rep_ids[it->first][r] = (int)a;
+        }
+        Trace("fmc-model-debug") << std::endl;
+
+        if (mbt_index==-1) {
+          std::cout << "   WARNING: model basis term is not a representative!" << std::endl;
+          exit(0);
+        }else{
+          Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
+        }
+      }
+    }
+    //also process non-rep set sorts
+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      Node op = it->first;
+      TypeNode tno = op.getType();
+      for( unsigned i=0; i<tno.getNumChildren(); i++) {
+        initializeType( fm, tno[i] );
+      }
+    }
+    //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();
+
+      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;
+
+
+      std::vector< Node > add_conds;
+      std::vector< Node > add_values;
+      bool needsDefault = true;
+      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()) ){
+          add_conds.push_back( n );
+          add_values.push_back( n );
+        }
+      }
+      //possibly get default
+      if( needsDefault ){
+        Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+        //add default value if necessary
+        if( fm->hasTerm( nmb ) ){
+          Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+          add_conds.push_back( nmb );
+          add_values.push_back( nmb );
+        }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;
+          add_conds.push_back( nmb );
+          add_values.push_back( vmb );
+        }
+      }
+
+      std::vector< Node > conds;
+      std::vector< Node > values;
+      std::vector< Node > entry_conds;
+      //get the entries for the mdoel
+      for( size_t i=0; i<add_conds.size(); i++ ){
+        Node c = add_conds[i];
+        Node v = add_values[i];
+        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]);
+          if( !ri.getType().isSort() && !ri.isConst() ){
+            Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
+          }
+          children.push_back(ri);
+          if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){
+            if (fm->isModelBasisTerm(ri) ) {
+              ri = fm->getStar( ri.getType() );
+            }else{
+              hasNonStar = true;
+            }
+          }
+          entry_children.push_back(ri);
+        }
+        Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+        Node nv = fm->getUsedRepresentative( v );
+        if( !nv.getType().isSort() && !nv.isConst() ){
+          Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;
+        }
+        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);
+        }
+        else {
+          Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+        }
+      }
+
+
+      //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++) {
+        fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
+      }
+
+
+      if( options::fmfFmcInterval() ){
+        Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;
+        fm->d_models[op]->debugPrint("fmc-interval-model", op, this);
+        Trace("fmc-interval-model") << std::endl;
+        std::vector< int > indices;
+        for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){
+          indices.push_back( i );
+        }
+        std::map< int, std::map< int, Node > > changed_vals;
+        makeIntervalModel( fm, op, indices, 0, changed_vals );
+
+        std::vector< Node > conds;
+        std::vector< Node > values;
+        for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){
+          if( changed_vals.find(i)==changed_vals.end() ){
+            conds.push_back( fm->d_models[op]->d_cond[i] );
+          }else{
+            std::vector< Node > children;
+            children.push_back( op );
+            for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){
+              if( changed_vals[i].find(j)==changed_vals[i].end() ){
+                children.push_back( fm->d_models[op]->d_cond[i][j] );
+              }else{
+                children.push_back( changed_vals[i][j] );
+              }
+            }
+            Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+            conds.push_back( nc );
+            Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";
+            debugPrintCond("fmc-interval-model", nc, true );
+            Trace("fmc-interval-model") << std::endl;
+          }
+          values.push_back( fm->d_models[op]->d_value[i] );
+        }
+        fm->d_models[op]->reset();
+        for( unsigned i=0; i<conds.size(); i++ ){
+          fm->d_models[op]->addEntry(fm, conds[i], values[i] );
+        }
+      }
+
+      Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
+      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+      Trace("fmc-model-simplify") << std::endl;
+
+      Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
+      fm->d_models[op]->simplify( this, fm );
+
+      fm->d_models[op]->debugPrint("fmc-model", op, this);
+      Trace("fmc-model") << std::endl;
+    }
+  }
+  if( fullModel ){
+    //make function values
+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
+      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
+    }
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+    //mark that the model has been set
+    fm->markModelSet();
+    //debug the model
+    debugModel( fm );
+  }
+}
+
+void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
+  if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
+    Trace("fmc") << "Initialize type " << tn << std::endl;
+    Node mbn;
+    if (!fm->d_rep_set.hasType(tn)) {
+      mbn = fm->getSomeDomainElement(tn);
+    }else{
+      mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    }
+    Node mbnr = fm->getUsedRepresentative( mbn );
+    fm->d_model_basis_rep[tn] = mbnr;
+    Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;
+  }
+}
+
+void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
+  Trace(tr) << "(";
+  for( unsigned j=0; j<n.getNumChildren(); j++) {
+    if( j>0 ) Trace(tr) << ", ";
+    debugPrint(tr, n[j], dispStar);
+  }
+  Trace(tr) << ")";
+}
+
+void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
+  FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();
+  if( n.isNull() ){
+    Trace(tr) << "null";
+  }
+  else if(fm->isStar(n) && dispStar) {
+    Trace(tr) << "*";
+  }
+  else if(fm->isInterval(n)) {
+    debugPrint(tr, n[0], dispStar );
+    Trace(tr) << "...";
+    debugPrint(tr, n[1], dispStar );
+  }else{
+    TypeNode tn = n.getType();
+    if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+      if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
+        Trace(tr) << d_rep_ids[tn][n];
+      }else{
+        Trace(tr) << n;
+      }
+    }else{
+      Trace(tr) << n;
+    }
+  }
+}
+
+
+bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+  Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
+  if( optUseModel() ){
+    FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
+    if (effort==0) {
+      //register the quantifier
+      if (d_quant_cond.find(f)==d_quant_cond.end()) {
+        std::vector< TypeNode > types;
+        for(unsigned i=0; i<f[0].getNumChildren(); i++){
+          types.push_back(f[0][i].getType());
+          d_quant_var_id[f][f[0][i]] = i;
+        }
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
+        Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+        d_quant_cond[f] = op;
+      }
+      //make sure all types are set
+      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+        initializeType( fmfmc, f[0][i].getType() );
+      }
+
+      //model check the quantifier
+      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;
+
+      //consider all entries going to non-true
+      for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
+        if( d_quant_models[f].d_value[i]!=d_true) {
+          Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
+          bool hasStar = false;
+          std::vector< Node > inst;
+          for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
+            if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
+              hasStar = true;
+              inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+            }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){
+              hasStar = true;
+              //if interval, find a sample point
+              if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){
+                if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){
+                  inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));
+                }else{
+                  Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],
+                                                              NodeManager::currentNM()->mkConst( Rational(1) ) );
+                  nn = Rewriter::rewrite( nn );
+                  inst.push_back( nn );
+                }
+              }else{
+                inst.push_back(d_quant_models[f].d_cond[i][j][0]);
+              }
+            }else{
+              inst.push_back(d_quant_models[f].d_cond[i][j]);
+            }
+          }
+          bool addInst = true;
+          if( hasStar ){
+            //try obvious (specified by 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(fmfmc, inst);
+              if( ev==d_true ){
+                std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
+                exit(0);
+              }else{
+                Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+              }
+            }
+          }
+          if( addInst ){
+            InstMatch m;
+            for( unsigned j=0; j<inst.size(); j++) {
+              m.set( d_qe, f, j, inst[j] );
+            }
+            d_triedLemmas++;
+            if( d_qe->addInstantiation( f, m ) ){
+              d_addedLemmas++;
+            }else{
+              //this can happen if evaluation is unknown
+              //might try it next effort level
+              d_star_insts[f].push_back(i);
+            }
+          }else{
+            //might try it next effort level
+            d_star_insts[f].push_back(i);
+          }
+        }
+      }
+    }else{
+      if (!d_star_insts[f].empty()) {
+        Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
+        Trace("fmc-exh") << "Definition was : " << std::endl;
+        d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
+        Trace("fmc-exh") << std::endl;
+        Def temp;
+        //simplify the exceptions?
+        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(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
+            if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){
+              //something went wrong, resort to exhaustive instantiation
+              return false;
+            }
+          }
+        }
+      }
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
+bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
+  RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+  Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
+  debugPrintCond("fmc-exh", c, true);
+  Trace("fmc-exh")<< std::endl;
+  Trace("fmc-exh-debug") << "Set interval domains..." << std::endl;
+  //set the bounds on the iterator based on intervals
+  for( unsigned i=0; i<c.getNumChildren(); i++ ){
+    if( c[i].getType().isInteger() ){
+      if( fm->isInterval(c[i]) ){
+        for( unsigned b=0; b<2; b++ ){
+          if( !fm->isStar(c[i][b]) ){
+            riter.d_bounds[b][i] = c[i][b];
+          }
+        }
+      }else if( !fm->isStar(c[i]) ){
+        riter.d_bounds[0][i] = c[i];
+        riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );
+      }
+    }
+  }
+  Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
+  //initialize
+  if( riter.setQuantifier( f ) ){
+    Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
+    //set the domains based on the entry
+    for (unsigned i=0; i<c.getNumChildren(); i++) {
+      if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
+        TypeNode tn = c[i].getType();
+        if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+          if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
+            //add the full range
+          }else{
+            if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
+              riter.d_domain[i].clear();
+              riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+            }else{
+              return false;
+            }
+          }
+        }else{
+          return false;
+        }
+      }
+    }
+    int addedLemmas = 0;
+    //now do full iteration
+    while( !riter.isFinished() ){
+      d_triedLemmas++;
+      Trace("fmc-exh-debug") << "Inst : ";
+      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 = 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(fm, inst);
+      Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
+      Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
+      if (ev!=d_true) {
+        InstMatch m;
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          m.set( d_qe, f, i, riter.getTerm( i ) );
+        }
+        Trace("fmc-exh-debug") << ", add!";
+        //add as instantiation
+        if( d_qe->addInstantiation( f, m ) ){
+          Trace("fmc-exh-debug")  << " ...success.";
+          addedLemmas++;
+        }
+      }else{
+        Trace("fmc-exh-debug") << ", already true";
+      }
+      Trace("fmc-exh-debug") << std::endl;
+      int index = riter.increment();
+      Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
+      if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
+        Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
+        riter.increment2( index-1 );
+      }
+    }
+    d_addedLemmas += addedLemmas;
+    return true;
+  }else{
+    return false;
+  }
+}
+
+void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
+  Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
+  //first check if it is a bounding literal
+  if( n.hasAttribute(BoundIntLitAttribute()) ){
+    Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;
+    d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );
+  }else if( n.getKind() == kind::BOUND_VARIABLE ){
+    Trace("fmc-debug") << "Add default entry..." << std::endl;
+    d.addEntry(fm, mkCondDefault(fm, f), n);
+  }
+  else if( n.getKind() == kind::NOT ){
+    //just do directly
+    doCheck( fm, f, d, n[0] );
+    doNegate( d );
+  }
+  else if( n.getKind() == kind::FORALL ){
+    d.addEntry(fm, mkCondDefault(fm, f), Node::null());
+  }
+  else if( n.getType().isArray() ){
+    //make the definition
+    Node r = fm->getRepresentative(n);
+    Trace("fmc-debug") << "Representative for array is " << r << std::endl;
+    while( r.getKind() == kind::STORE ){
+      Node i = fm->getUsedRepresentative( r[1] );
+      Node e = fm->getUsedRepresentative( r[2] );
+      d.addEntry(fm, mkArrayCond(i), e );
+      r = r[0];
+    }
+    Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));
+    bool success = false;
+    if( r.getKind() == kind::STORE_ALL ){
+      ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();
+      Node defaultValue = Node::fromExpr(storeAll.getExpr());
+      defaultValue = fm->getUsedRepresentative( defaultValue, true );
+      if( !defaultValue.isNull() ){
+        d.addEntry(fm, defC, defaultValue);
+        success = true;
+      }
+    }
+    if( !success ){
+      Trace("fmc-debug") << "Can't process base array " << r << std::endl;
+      //can't process this array
+      d.reset();
+      d.addEntry(fm, defC, Node::null());
+    }
+  }
+  else if( n.getNumChildren()==0 ){
+    Node r = n;
+    if( !n.isConst() ){
+      if( !fm->hasTerm(n) ){
+        r = getSomeDomainElement(fm, n.getType() );
+      }
+      r = fm->getUsedRepresentative( r );
+    }
+    Trace("fmc-debug") << "Add constant entry..." << std::endl;
+    d.addEntry(fm, mkCondDefault(fm, f), r);
+  }
+  else{
+    std::vector< int > var_ch;
+    std::vector< Def > children;
+    for( int i=0; i<(int)n.getNumChildren(); i++) {
+      Def dc;
+      doCheck(fm, f, dc, n[i]);
+      children.push_back(dc);
+      if( n[i].getKind() == kind::BOUND_VARIABLE ){
+        var_ch.push_back(i);
+      }
+    }
+
+    if( n.getKind()==APPLY_UF ){
+      Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
+      //uninterpreted compose
+      doUninterpretedCompose( fm, f, d, n.getOperator(), children );
+    } else if( n.getKind()==SELECT ){
+      Trace("fmc-debug") << "Do select compose " << n << std::endl;
+      std::vector< Def > children2;
+      children2.push_back( children[1] );
+      std::vector< Node > cond;
+      mkCondDefaultVec(fm, f, cond);
+      std::vector< Node > val;
+      doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );
+    } else {
+      if( !var_ch.empty() ){
+        if( n.getKind()==EQUAL ){
+          if( var_ch.size()==2 ){
+            Trace("fmc-debug") << "Do variable equality " << n << std::endl;
+            doVariableEquality( fm, f, d, n );
+          }else{
+            Trace("fmc-debug") << "Do variable relation " << n << std::endl;
+            doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );
+          }
+        }else{
+          Trace("fmc-warn") << "Don't know how to check " << n << std::endl;
+          d.addEntry(fm, mkCondDefault(fm, f), Node::null());
+        }
+      }else{
+        Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
+        std::vector< Node > cond;
+        mkCondDefaultVec(fm, f, cond);
+        std::vector< Node > val;
+        //interpreted compose
+        doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
+      }
+    }
+    Trace("fmc-debug") << "Simplify the definition..." << std::endl;
+    d.debugPrint("fmc-debug", Node::null(), this);
+    d.simplify(this, fm);
+    Trace("fmc-debug") << "Done simplifying" << std::endl;
+  }
+  Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
+  d.debugPrint("fmc-debug", Node::null(), this);
+  Trace("fmc-debug") << std::endl;
+}
+
+void FullModelChecker::doNegate( Def & dc ) {
+  for (unsigned i=0; i<dc.d_cond.size(); i++) {
+    if (!dc.d_value[i].isNull()) {
+      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;
+    }
+  }
+}
+
+void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {
+  std::vector<Node> cond;
+  mkCondDefaultVec(fm, f, cond);
+  if (eq[0]==eq[1]){
+    d.addEntry(fm, mkCond(cond), d_true);
+  }else{
+    TypeNode tn = eq[0].getType();
+    if( tn.isSort() ){
+      int j = getVariableId(f, eq[0]);
+      int k = getVariableId(f, eq[1]);
+      if( !fm->d_rep_set.hasType( tn ) ){
+        getSomeDomainElement( fm, tn );  //to verify the type is initialized
+      }
+      for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
+        Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
+        cond[j+1] = r;
+        cond[k+1] = r;
+        d.addEntry( fm, mkCond(cond), d_true);
+      }
+      d.addEntry( fm, mkCondDefault(fm, f), d_false);
+    }else{
+      d.addEntry( fm, mkCondDefault(fm, f), Node::null());
+    }
+  }
+}
+
+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( val.isNull() ){
+      d.addEntry( fm, dc.d_cond[i], val);
+    }else{
+      if( dc.d_cond[i][j]!=val ){
+        if (fm->isStar(dc.d_cond[i][j])) {
+          std::vector<Node> cond;
+          mkCondVec(dc.d_cond[i],cond);
+          cond[j+1] = val;
+          d.addEntry(fm, mkCond(cond), d_true);
+          cond[j+1] = fm->getStar(val.getType());
+          d.addEntry(fm, mkCond(cond), d_false);
+        }else{
+          d.addEntry( fm, dc.d_cond[i], d_false);
+        }
+      }else{
+        d.addEntry( fm, dc.d_cond[i], d_true);
+      }
+    }
+  }
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
+  Trace("fmc-uf-debug") << "Definition : " << std::endl;
+  fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);
+  Trace("fmc-uf-debug") << std::endl;
+
+  std::vector< Node > cond;
+  mkCondDefaultVec(fm, f, cond);
+  std::vector< Node > val;
+  doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
+                                               Def & df, std::vector< Def > & dc, int index,
+                                               std::vector< Node > & cond, std::vector<Node> & val ) {
+  Trace("fmc-uf-process") << "process at " << index << std::endl;
+  for( unsigned i=1; i<cond.size(); i++) {
+    debugPrint("fmc-uf-process", cond[i], true);
+    Trace("fmc-uf-process") << " ";
+  }
+  Trace("fmc-uf-process") << std::endl;
+  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, df.d_et);
+    if( entries.empty() ){
+      d.addEntry(fm, mkCond(cond), Node::null());
+    }else{
+      //add them to the definition
+      for( unsigned e=0; e<df.d_cond.size(); e++ ){
+        if ( entries.find(e)!=entries.end() ){
+          Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;
+          d.addEntry(fm, entries[e], df.d_value[e] );
+          Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;
+        }
+      }
+    }
+  }else{
+    for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
+      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(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, d, df, dc, index+1, new_cond, val);
+          val.pop_back();
+        }else{
+          Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
+        }
+      }
+    }
+  }
+}
+
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
+                                                std::map< int, Node > & entries, int index,
+                                                std::vector< Node > & cond, std::vector< Node > & val,
+                                                EntryTrie & curr ) {
+  Trace("fmc-uf-process") << "compose " << index << std::endl;
+  for( unsigned i=1; i<cond.size(); i++) {
+    debugPrint("fmc-uf-process", cond[i], true);
+    Trace("fmc-uf-process") << " ";
+  }
+  Trace("fmc-uf-process") << std::endl;
+  if (index==(int)val.size()) {
+    Node c = mkCond(cond);
+    Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;
+    entries[curr.d_data] = c;
+  }else{
+    Node v = val[index];
+    bool bind_var = false;
+    if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
+      int j = getVariableId(f, v);
+      Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
+      if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {
+        v = cond[j+1];
+      }else{
+        bind_var = true;
+      }
+    }
+    if (bind_var) {
+      Trace("fmc-uf-process") << "bind variable..." << std::endl;
+      int j = getVariableId(f, v);
+      if( fm->isStar(cond[j+1]) ){
+        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+          cond[j+1] = it->first;
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+        }
+        cond[j+1] = fm->getStar(v.getType());
+      }else{
+        Node orig = cond[j+1];
+        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+          Node nw = doIntervalMeet( fm, it->first, orig );
+          if( !nw.isNull() ){
+            cond[j+1] = nw;
+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+          }
+        }
+        cond[j+1] = orig;
+      }
+    }else{
+      if( !v.isNull() ){
+        if( options::fmfFmcInterval() && v.getType().isInteger() ){
+          for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+            if( fm->isInRange( v, it->first ) ){
+              doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+            }
+          }
+        }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 = fm->getStarElement(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]);
+          }
+        }
+      }
+    }
+  }
+}
+
+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(fm, c, v);
+  }
+  else {
+    TypeNode vtn = n.getType();
+    for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
+      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(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(fm, c, dc[index].d_value[i]);
+              process = false;
+            }
+          }
+          if (process) {
+            val.push_back(dc[index].d_value[i]);
+            doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);
+            val.pop_back();
+          }
+        }
+      }
+    }
+  }
+}
+
+int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
+  Trace("fmc-debug2") << "isCompat " << c << std::endl;
+  Assert(cond.size()==c.getNumChildren()+1);
+  for (unsigned i=1; i<cond.size(); i++) {
+    if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+      Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
+      if( iv.isNull() ){
+        return 0;
+      }
+    }else{
+      if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
+        return 0;
+      }
+    }
+  }
+  return 1;
+}
+
+bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
+  Trace("fmc-debug2") << "doMeet " << c << std::endl;
+  Assert(cond.size()==c.getNumChildren()+1);
+  for (unsigned i=1; i<cond.size(); i++) {
+    if( cond[i]!=c[i-1] ) {
+      if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+        Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
+        if( !iv.isNull() ){
+          cond[i] = iv;
+        }else{
+          return false;
+        }
+      }else{
+        if( fm->isStar(cond[i]) ){
+          cond[i] = c[i-1];
+        }else if( !fm->isStar(c[i-1]) ){
+          return false;
+        }
+      }
+    }
+  }
+  return true;
+}
+
+Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {
+  if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){
+    std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;
+    exit( 0 );
+  }
+  Node b[2];
+  for( unsigned j=0; j<2; j++ ){
+    Node b1 = i1[j];
+    Node b2 = i2[j];
+    if( fm->isStar( b1 ) ){
+      b[j] = b2;
+    }else if( fm->isStar( b2 ) ){
+      b[j] = b1;
+    }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){
+      b[j] = j==0 ? b2 : b1;
+    }else{
+      b[j] = j==0 ? b1 : b2;
+    }
+  }
+  if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){
+    return mk ? fm->getInterval( b[0], b[1] ) : i1;
+  }else{
+    return Node::null();
+  }
+}
+
+Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
+  return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
+}
+
+Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
+  std::vector< Node > cond;
+  mkCondDefaultVec(fm, f, cond);
+  return mkCond(cond);
+}
+
+void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
+  Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;
+  //get function symbol for f
+  cond.push_back(d_quant_cond[f]);
+  for (unsigned i=0; i<f[0].getNumChildren(); i++) {
+    Node ts = fm->getStarElement( f[0][i].getType() );
+    cond.push_back(ts);
+  }
+}
+
+void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
+  cond.push_back(n.getOperator());
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    cond.push_back( n[i] );
+  }
+}
+
+Node FullModelChecker::mkArrayCond( Node a ) {
+  if( d_array_term_cond.find(a)==d_array_term_cond.end() ){
+    if( d_array_cond.find(a.getType())==d_array_cond.end() ){
+      TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );
+      Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+      d_array_cond[a.getType()] = op;
+    }
+    std::vector< Node > cond;
+    cond.push_back(d_array_cond[a.getType()]);
+    cond.push_back(a);
+    d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond );
+  }
+  return d_array_term_cond[a];
+}
+
+Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
+  if( n.getKind()==EQUAL ){
+    if (!vals[0].isNull() && !vals[1].isNull()) {
+      return vals[0]==vals[1] ? d_true : d_false;
+    }else{
+      return Node::null();
+    }
+  }else if( n.getKind()==ITE ){
+    if( vals[0]==d_true ){
+      return vals[1];
+    }else if( vals[0]==d_false ){
+      return vals[2];
+    }else{
+      return vals[1]==vals[2] ? vals[1] : Node::null();
+    }
+  }else if( n.getKind()==AND || n.getKind()==OR ){
+    bool isNull = false;
+    for (unsigned i=0; i<vals.size(); i++) {
+      if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {
+        return vals[i];
+      }else if( vals[i].isNull() ){
+        isNull = true;
+      }
+    }
+    return isNull ? Node::null() : vals[0];
+  }else{
+    std::vector<Node> children;
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.push_back( n.getOperator() );
+    }
+    for (unsigned i=0; i<vals.size(); i++) {
+      if( vals[i].isNull() ){
+        return Node::null();
+      }else{
+        children.push_back( vals[i] );
+      }
+    }
+    Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);
+    Trace("fmc-eval") << "Evaluate " << nc << " to ";
+    nc = Rewriter::rewrite(nc);
+    Trace("fmc-eval") << nc << std::endl;
+    return nc;
+  }
+}
+
+Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {
+  bool addRepId = !fm->d_rep_set.hasType( tn );
+  Node de = fm->getSomeDomainElement(tn);
+  if( addRepId ){
+    d_rep_ids[tn][de] = 0;
+  }
+  return de;
+}
+
+Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {
+  return fm->getFunctionValue(op, argPrefix);
+}
+
+
+bool FullModelChecker::useSimpleModels() {
+  return options::fmfFmcSimple();
+}
+
+void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
+                                          std::map< int, std::map< int, Node > >& changed_vals ) {
+  if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){
+    makeIntervalModel2( fm, op, indices, 0, changed_vals );
+  }else{
+    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();
+    if( tn.isInteger() ){
+      makeIntervalModel(fm,op,indices,index+1, changed_vals );
+    }else{
+      std::map< Node, std::vector< int > > new_indices;
+      for( unsigned i=0; i<indices.size(); i++ ){
+        Node v = fm->d_models[op]->d_cond[indices[i]][index];
+        new_indices[v].push_back( indices[i] );
+      }
+
+      for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
+        makeIntervalModel( fm, op, it->second, index+1, changed_vals );
+      }
+    }
+  }
+}
+
+void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
+                                          std::map< int, std::map< int, Node > >& changed_vals ) {
+  Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";
+  for( unsigned i=0; i<indices.size(); i++ ){
+    Debug("fmc-interval-model-debug") << indices[i] << " ";
+  }
+  Debug("fmc-interval-model-debug") << std::endl;
+
+  if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){
+    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();
+    if( tn.isInteger() ){
+      std::map< Node, std::vector< int > > new_indices;
+      for( unsigned i=0; i<indices.size(); i++ ){
+        Node v = fm->d_models[op]->d_cond[indices[i]][index];
+        new_indices[v].push_back( indices[i] );
+        if( !v.isConst() ){
+          Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;
+          Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;
+        }
+      }
+
+      std::vector< Node > values;
+      for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
+        makeIntervalModel2( fm, op, it->second, index+1, changed_vals );
+        values.push_back( it->first );
+      }
+
+      if( tn.isInteger() ){
+        //sort values by size
+        ConstRationalSort crs;
+        std::vector< int > sindices;
+        for( unsigned i=0; i<values.size(); i++ ){
+          sindices.push_back( (int)i );
+          crs.d_terms.push_back( values[i] );
+        }
+        std::sort( sindices.begin(), sindices.end(), crs );
+
+        Node ub = fm->getStar( tn );
+        for( int i=(int)(sindices.size()-1); i>=0; i-- ){
+          Node lb = fm->getStar( tn );
+          if( i>0 ){
+            lb = values[sindices[i]];
+          }
+          Node interval = fm->getInterval( lb, ub );
+          for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){
+            Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;
+            changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;
+          }
+          ub = lb;
+        }
+      }
+    }else{
+      makeIntervalModel2( fm, op, indices, index+1, changed_vals );
+    }
+  }
+}