From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 9 May 2013 01:02:10 +0000 (-0500)
Subject: Add new method for checking candidate models, --fmf-fmc.  Add infrastructure for... 
X-Git-Tag: cvc5-1.0.0~7287^2~130^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=85377f73a331b334437aa0d50d15c81e905869c1;p=cvc5.git

Add new method for checking candidate models, --fmf-fmc.  Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp).  Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model.  Add option for relational triggers such as x = f(y), --relational-trigger.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0bfc6e634..37ab9cd48 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1018,11 +1018,18 @@ void SmtEngine::setLogicInternal() throw() {
 
   //for finite model finding
   if( ! options::instWhenMode.wasSetByUser()){
+    //instantiate only on last call
     if( options::fmfInstEngine() ){
       Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
       options::instWhenMode.set( INST_WHEN_LAST_CALL );
     }
   }
+  if ( ! options::fmfInstGen.wasSetByUser()) {
+    //if full model checking is on, disable inst-gen techniques
+    if( options::fmfFullModelCheck() ){
+      options::fmfInstGen.set( false );
+    }
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 7fea8cf3a..1a1413ad6 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -44,7 +44,11 @@ libquantifiers_la_SOURCES = \
 	inst_strategy_e_matching.h \
 	inst_strategy_e_matching.cpp \
 	inst_strategy_cbqi.h \
-	inst_strategy_cbqi.cpp
+	inst_strategy_cbqi.cpp \
+	full_model_check.h \
+	full_model_check.cpp \
+	bounded_integers.h \
+	bounded_integers.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
new file mode 100755
index 000000000..7af6456b6
--- /dev/null
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -0,0 +1,98 @@
+/*********************                                                        */
+/*! \file bounded_integers.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 Bounded integers module
+ **
+ ** This class manages integer bounds for quantifiers
+ **/
+
+#include "theory/quantifiers/bounded_integers.h"
+#include "theory/quantifiers/quant_util.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe) : QuantifiersModule(qe){
+
+}
+
+void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
+  if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
+    std::map< Node, Node > msum;
+    if (QuantArith::getMonomialSumLit( lit, msum )){
+      Trace("bound-integers") << "Literal " << lit << " is monomial sum : " << std::endl;
+      for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+        Trace("bound-integers") << "  ";
+        if( !it->second.isNull() ){
+          Trace("bound-integers") << it->second;
+          if( !it->first.isNull() ){
+            Trace("bound-integers") << " * ";
+          }
+        }
+        if( !it->first.isNull() ){
+          Trace("bound-integers") << it->first;
+        }
+        Trace("bound-integers") << std::endl;
+      }
+      Trace("bound-integers") << std::endl;
+      for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+        if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){
+          Node veq;
+          if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){
+            Trace("bound-integers") << "Isolated for " << it->first << " : " << veq << std::endl;
+          }
+        }
+      }
+    }
+  }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
+    std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
+    exit(0);
+  }
+}
+
+void BoundedIntegers::process( Node f, Node n, bool pol ){
+  if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){
+    for( unsigned i=0; i<n.getNumChildren(); i++) {
+      bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;
+      process( f, n[i], newPol );
+    }
+  }else if( n.getKind()==NOT ){
+    process( f, n[0], !pol );
+  }else {
+    processLiteral( f, n, pol );
+  }
+}
+
+void BoundedIntegers::check( Theory::Effort e ) {
+
+}
+
+void BoundedIntegers::registerQuantifier( Node f ) {
+  bool hasIntType = false;
+  for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+    if( f[0][i].getType().isInteger() ){
+      hasIntType = true;
+      break;
+    }
+  }
+  if( hasIntType ){
+    process( f, f[1], true );
+  }
+}
+
+void BoundedIntegers::assertNode( Node n ) {
+
+}
+
+Node BoundedIntegers::getNextDecisionRequest() {
+  return Node::null();
+}
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
new file mode 100755
index 000000000..570e27a10
--- /dev/null
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file bounded_integers.h
+** \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 This class manages integer bounds for quantifiers
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BOUNDED_INTEGERS_H
+#define __CVC4__BOUNDED_INTEGERS_H
+
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class BoundedIntegers : public QuantifiersModule
+{
+private:
+  std::map< Node, std::map< Node, Node > > d_lowers;
+  std::map< Node, std::map< Node, Node > > d_uppers;
+  std::map< Node, std::map< Node, bool > > d_set;
+  void hasFreeVar( Node f, Node n );
+  void process( Node f, Node n, bool pol );
+  void processLiteral( Node f, Node lit, bool pol );
+public:
+  BoundedIntegers( QuantifiersEngine* qe );
+
+  void check( Theory::Effort e );
+  void registerQuantifier( Node f );
+  void assertNode( Node n );
+  Node getNextDecisionRequest();
+};
+
+}
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
new file mode 100755
index 000000000..efd193fc5
--- /dev/null
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -0,0 +1,943 @@
+
+/*********************                                                        */
+/*! \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;
+
+
+bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {
+  if (index==(int)c.getNumChildren()) {
+    return d_data!=-1;
+  }else{
+    Node st = m->getStar(c[index].getType());
+    if(d_child.find(st)!=d_child.end()) {
+      if( d_child[st].hasGeneralization(m, c, index+1) ){
+        return true;
+      }
+    }
+    if( d_child.find( c[index] )!=d_child.end() ){
+      if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
+int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {
+  if (index==(int)inst.size()) {
+    return d_data;
+  }else{
+    int minIndex = -1;
+    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( 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( FullModelChecker * 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);
+  }
+}
+
+void EntryTrie::getEntries( FullModelChecker * 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);
+      }
+    }
+
+  }
+}
+
+bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {
+
+  return false;
+}
+
+
+bool Def::addEntry( FullModelChecker * m, Node c, Node v) {
+  if (!d_et.hasGeneralization(m, c)) {
+    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;
+  }else{
+    return false;
+  }
+}
+
+Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {
+  int gindex = d_et.getGeneralizationIndex(m, inst);
+  if (gindex!=-1) {
+    return d_value[gindex];
+  }else{
+    return Node::null();
+  }
+}
+
+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {
+  return d_et.getGeneralizationIndex(m, inst);
+}
+
+void Def::simplify(FullModelChecker * 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, d_cond[i], d_value[i]);
+    }
+  }
+  d_status.clear();
+}
+
+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(QuantifiersEngine* qe) : d_qe(qe){
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+void FullModelChecker::reset(FirstOrderModel * fm) {
+  Trace("fmc") << "---Full Model Check reset() " << std::endl;
+  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+    it->second->reset();
+  }
+  d_quant_models.clear();
+  d_models_init.clear();
+  d_rep_ids.clear();
+  d_model_basis_rep.clear();
+  d_star_insts.clear();
+  //process representatives
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+    if( it->first.isSort() ){
+      if( d_type_star.find(it->first)==d_type_star.end() ){
+        Node st = NodeManager::currentNM()->mkSkolem( "star_$$", it->first, "skolem created for full-model checking" );
+        d_type_star[it->first] = st;
+      }
+      Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+      Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
+      Node rmbt = fm->getRepresentative(mbt);
+      int mbt_index = -1;
+      Trace("fmc") << "  Model basis term : " << mbt << std::endl;
+      for( size_t a=0; a<it->second.size(); a++ ){
+        //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );
+        //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );
+        Node r = fm->getRepresentative( it->second[a] );
+        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))) {
+          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;
+      }
+    }
+  }
+}
+
+Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {
+  //Assert( fm->hasTerm(n) );
+  TypeNode tn = n.getType();
+  if( tn.isBoolean() ){
+    return fm->areEqual(n, d_true) ? d_true : d_false;
+  }else{
+    Node r = fm->getRepresentative(n);
+    if (r==d_model_basis_rep[tn]) {
+      r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    }
+    return r;
+  }
+}
+
+struct ModelBasisArgSort
+{
+  std::vector< Node > d_terms;
+  bool operator() (int i,int j) {
+    return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
+            d_terms[j].getAttribute(ModelBasisArgAttribute()) );
+  }
+};
+
+void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
+                                 std::vector< Node > & conds,
+                                 std::vector< Node > & values,
+                                 std::vector< Node > & entry_conds ) {
+  std::vector< Node > children;
+  std::vector< Node > entry_children;
+  children.push_back(op);
+  entry_children.push_back(op);
+  bool hasNonStar = false;
+  for( unsigned i=0; i<c.getNumChildren(); i++) {
+    Node ri = getRepresentative(fm, c[i]);
+    children.push_back(ri);
+    if (isModelBasisTerm(ri)) {
+      ri = d_type_star[ri.getType()];
+    }else{
+      hasNonStar = true;
+    }
+    entry_children.push_back(ri);
+  }
+  Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+  Node nv = getRepresentative(fm, v);
+  Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+  if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
+    Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+    conds.push_back(n);
+    values.push_back(nv);
+    entry_conds.push_back(en);
+  }
+}
+
+Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
+  if( d_models_init.find(op)==d_models_init.end() ){
+    if( d_models.find(op)==d_models.end() ){
+      d_models[op] = new Def;
+      //make sure star's are defined
+      TypeNode tn = op.getType();
+      for(unsigned i=0; i<tn.getNumChildren()-1; i++) {
+        if( d_type_star.find(tn[i])==d_type_star.end() ){
+          Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn[i], "skolem created for full-model checking" );
+          d_type_star[tn[i]] = st;
+        }
+      }
+    }
+    //reset the model
+    d_models[op]->reset();
+
+    std::vector< Node > conds;
+    std::vector< Node > values;
+    std::vector< Node > entry_conds;
+    Trace("fmc-model-debug") << "Model values for " << op << " ... " << std::endl;
+    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+      Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);
+      Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
+    }
+    Trace("fmc-model-debug") << std::endl;
+    //initialize the model
+    for( int j=0; j<2; j++ ){
+      for( int k=1; k>=0; k-- ){
+        Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;
+        for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();
+             it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){
+          Trace("fmc-model-debug") << "   process : " << it->first << " -> " << it->second << std::endl;
+          if( j==1 ){
+            addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
+          }
+        }
+      }
+    }
+    //add for default value
+    if (!fm->d_uf_model_gen[op].d_default_value.isNull()) {
+      Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+      addEntry(fm, op, n, fm->d_uf_model_gen[op].d_default_value, conds, values, entry_conds);
+    }
+
+    //find other default values (TODO: figure out why these entries are added to d_uf_model_gen)
+    if( conds.empty() ){
+      //for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[1][0].begin();
+      //     it != fm->d_uf_model_gen[op].d_set_values[1][0].end(); ++it ){
+      //  Trace("fmc-model-debug") << "   process : " << it->first << " -> " << it->second << std::endl;
+      //  addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
+      //}
+      Trace("fmc-warn") << "WARNING: No entries for " << op << ", make default entry." << std::endl;
+      //choose a complete arbitrary term
+      Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+      TypeNode tn = n.getType();
+      Node v = fm->d_rep_set.d_type_reps[tn][0];
+      addEntry(fm, op, n, v, conds, values, entry_conds);
+    }
+
+    //sort based on # default arguments
+    std::vector< int > indices;
+    ModelBasisArgSort mbas;
+    for (int i=0; i<(int)conds.size(); i++) {
+      d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
+      mbas.d_terms.push_back(conds[i]);
+      indices.push_back(i);
+    }
+    std::sort( indices.begin(), indices.end(), mbas );
+
+
+    for (int i=0; i<(int)indices.size(); i++) {
+      d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);
+    }
+    d_models[op]->debugPrint("fmc-model", op, this);
+    Trace("fmc-model") << std::endl;
+
+    d_models[op]->simplify( this );
+    Trace("fmc-model-simplify") << "After simplification : " << std::endl;
+    d_models[op]->debugPrint("fmc-model-simplify", op, this);
+    Trace("fmc-model-simplify") << std::endl;
+
+    d_models_init[op] = true;
+  }
+  return d_models[op];
+}
+
+
+bool FullModelChecker::isStar(Node n) {
+  return n==d_type_star[n.getType()];
+}
+
+bool FullModelChecker::isModelBasisTerm(Node n) {
+  return n==getModelBasisTerm(n.getType());
+}
+
+Node FullModelChecker::getModelBasisTerm(TypeNode tn) {
+  return d_qe->getTermDatabase()->getModelBasisTerm(tn);
+}
+
+void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
+  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) {
+  if( n.isNull() ){
+    Trace(tr) << "null";
+  }
+  else if(isStar(n) && dispStar) {
+    Trace(tr) << "*";
+  }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;
+    }
+  }
+}
+
+
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort) {
+  int addedLemmas = 0;
+  Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
+  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;
+    }
+
+    //model check the quantifier
+    doCheck(fm, 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 false
+    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 (isStar(d_quant_models[f].d_cond[i][j])) {
+            hasStar = true;
+            inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+          }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(this, inst);
+          if (ev==d_true) {
+            addInst = false;
+          }
+        }else{
+          //for debugging
+          if (Trace.isOn("fmc-test-inst")) {
+            Node ev = d_quant_models[f].evaluate(this, inst);
+            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] );
+          }
+          if (isActive()) {
+            if( d_qe->addInstantiation( f, m ) ){
+              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{
+    //TODO
+    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( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
+        int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );
+        if( lem==-1 ){
+          return -1;
+        }else{
+          addedLemmas += lem;
+        }
+      }
+    }
+  }
+  return addedLemmas;
+}
+
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {
+  int addedLemmas = 0;
+  RepSetIterator riter( &(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;
+  if( riter.setQuantifier( f ) ){
+    std::vector< RepDomain > dom;
+    for (unsigned i=0; i<c.getNumChildren(); i++) {
+      TypeNode tn = c[i].getType();
+      if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+        RepDomain rd;
+        if( isStar(c[i]) ){
+          //add the full range
+          for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
+               it != d_rep_ids[tn].end(); ++it ){
+            rd.push_back(it->second);
+          }
+        }else{
+          if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
+            rd.push_back(d_rep_ids[tn][c[i]]);
+          }else{
+            return -1;
+          }
+        }
+        dom.push_back(rd);
+      }else{
+        return -1;
+      }
+    }
+    riter.setDomain(dom);
+    //now do full iteration
+    while( !riter.isFinished() ){
+      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 = getRepresentative( fm, riter.getTerm( i ) );
+        debugPrint("fmc-exh-debug", r);
+        Trace("fmc-exh-debug") << " ";
+        inst.push_back(r);
+      }
+
+      int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);
+      Trace("fmc-exh-debug") << ", index = " << ev_index;
+      Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
+      if (ev!=d_true) {
+        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 ) ){
+          addedLemmas++;
+        }
+      }
+      Trace("fmc-exh-debug") << std::endl;
+      riter.increment();
+    }
+  }
+  return addedLemmas;
+}
+
+void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
+  Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
+  if( n.getKind() == kind::BOUND_VARIABLE ){
+    d.addEntry(this, mkCondDefault(f), n);
+  }
+  else if( n.getNumChildren()==0 ){
+    Node r = n;
+    if( !fm->hasTerm(n) ){
+      if (fm->d_rep_set.hasType(n.getType())) {
+        r = fm->d_rep_set.d_type_reps[n.getType()][0];
+      }else{
+        //should never happen?
+      }
+    }
+    r = getRepresentative(fm, r);
+    d.addEntry(this, mkCondDefault(f), r);
+  }
+  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(this, mkCondDefault(f), Node::null());
+  }
+  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( !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{
+          std::cout << "Don't know how to check " << n << std::endl;
+          exit(0);
+        }
+      }else{
+        Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
+        std::vector< Node > cond;
+        mkCondDefaultVec(f, cond);
+        std::vector< Node > val;
+        //interpreted compose
+        doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
+      }
+    }
+    d.simplify(this);
+  }
+  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( FirstOrderModel * fm, Node f, Def & d, Node eq ) {
+  std::vector<Node> cond;
+  mkCondDefaultVec(f, cond);
+  if (eq[0]==eq[1]){
+    d.addEntry(this, mkCond(cond), d_true);
+  }else{
+    int j = getVariableId(f, eq[0]);
+    int k = getVariableId(f, eq[1]);
+    TypeNode tn = eq[0].getType();
+    for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
+      Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );
+      cond[j+1] = r;
+      cond[k+1] = r;
+      d.addEntry( this, mkCond(cond), d_true);
+    }
+    d.addEntry(this, mkCondDefault(f), d_false);
+  }
+}
+
+void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {
+  int j = getVariableId(f, v);
+  for (unsigned i=0; i<dc.d_cond.size(); i++) {
+    Node val = dc.d_value[i];
+    if( dc.d_cond[i][j]!=val ){
+      if (isStar(dc.d_cond[i][j])) {
+        std::vector<Node> cond;
+        mkCondVec(dc.d_cond[i],cond);
+        cond[j+1] = val;
+        d.addEntry(this, mkCond(cond), d_true);
+        cond[j+1] = d_type_star[val.getType()];
+        d.addEntry(this, mkCond(cond), d_false);
+      }else{
+        d.addEntry( this, dc.d_cond[i], d_false);
+      }
+    }else{
+      d.addEntry( this, dc.d_cond[i], d_true);
+    }
+  }
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
+  Trace("fmc-uf-debug") << "Definition : " << std::endl;
+  d_models[op]->debugPrint("fmc-uf-debug", op, this);
+  Trace("fmc-uf-debug") << std::endl;
+
+  std::vector< Node > cond;
+  mkCondDefaultVec(f, cond);
+  std::vector< Node > val;
+  doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+                                               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, d_models[op]->d_et);
+    //add them to the definition
+    for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){
+      if ( entries.find(e)!=entries.end() ){
+        d.addEntry(this, entries[e], d_models[op]->d_value[e] );
+      }
+    }
+  }else{
+    for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
+      if (isCompat(cond, dc[index].d_cond[i])!=0) {
+        std::vector< Node > new_cond;
+        new_cond.insert(new_cond.end(), cond.begin(), cond.end());
+        if( doMeet(new_cond, dc[index].d_cond[i]) ){
+          Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
+          val.push_back(dc[index].d_value[i]);
+          doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);
+          val.pop_back();
+        }else{
+          Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
+        }
+      }
+    }
+  }
+}
+
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * 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.getKind()==kind::BOUND_VARIABLE ){
+      int j = getVariableId(f, v);
+      Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
+      if (!isStar(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);
+      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] = getStar(v.getType());
+    }else{
+      if (curr.d_child.find(v)!=curr.d_child.end()) {
+        Trace("fmc-uf-process") << "follow value..." << std::endl;
+        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
+      }
+      Node st = d_type_star[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( FirstOrderModel * fm, Node f, Def & d, Node n,
+                                             std::vector< Def > & dc, int index,
+                                             std::vector< Node > & cond, std::vector<Node> & val ) {
+  if ( index==(int)dc.size() ){
+    Node c = mkCond(cond);
+    Node v = evaluateInterpreted(n, val);
+    d.addEntry(this, c, v);
+  }
+  else {
+    TypeNode vtn = n.getType();
+    for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
+      if (isCompat(cond, dc[index].d_cond[i])!=0) {
+        std::vector< Node > new_cond;
+        new_cond.insert(new_cond.end(), cond.begin(), cond.end());
+        if( doMeet(new_cond, dc[index].d_cond[i]) ){
+          bool process = true;
+          if (vtn.isBoolean()) {
+            //short circuit
+            if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||
+                (n.getKind()==AND && dc[index].d_value[i]==d_false) ){
+              Node c = mkCond(new_cond);
+              d.addEntry(this, c, dc[index].d_value[i]);
+              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( std::vector< Node > & cond, Node c ) {
+  Assert(cond.size()==c.getNumChildren()+1);
+  for (unsigned i=1; i<cond.size(); i++) {
+    if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {
+      return 0;
+    }
+  }
+  return 1;
+}
+
+bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {
+  Assert(cond.size()==c.getNumChildren()+1);
+  for (unsigned i=1; i<cond.size(); i++) {
+    if( cond[i]!=c[i-1] ) {
+      if( isStar(cond[i]) ){
+        cond[i] = c[i-1];
+      }else if( !isStar(c[i-1]) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
+  return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
+}
+
+Node FullModelChecker::mkCondDefault( Node f) {
+  std::vector< Node > cond;
+  mkCondDefaultVec(f, cond);
+  return mkCond(cond);
+}
+
+void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {
+  //get function symbol for f
+  cond.push_back(d_quant_cond[f]);
+  for (unsigned i=0; i<f[0].getNumChildren(); i++) {
+    cond.push_back(d_type_star[f[0][i].getType()]);
+  }
+}
+
+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::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
+  if( n.getKind()==EQUAL ){
+    return vals[0]==vals[1] ? d_true : d_false;
+  }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;
+  }
+}
+
+bool FullModelChecker::isActive() {
+  return options::fmfFullModelCheck();
+}
+
+bool FullModelChecker::useSimpleModels() {
+  return options::fmfFullModelCheckSimple();
+}
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
new file mode 100755
index 000000000..3f54b0574
--- /dev/null
+++ b/src/theory/quantifiers/full_model_check.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file full_model_check.h
+ ** \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 Full model check class
+ **/
+
+#ifndef FULL_MODEL_CHECK
+#define FULL_MODEL_CHECK
+
+#include "theory/quantifiers/model_builder.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace fmcheck {
+
+
+class FullModelChecker;
+
+class EntryTrie
+{
+public:
+  EntryTrie() : d_data(-1){}
+  std::map<Node,EntryTrie> d_child;
+  int d_data;
+  void reset() { d_data = -1; d_child.clear(); }
+  void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 );
+  bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 );
+  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index = 0 );
+  void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
+  //if possible, get ground instance of c that evaluates to the entry
+  bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index = 0 );
+};
+
+
+class Def
+{
+public:
+  EntryTrie d_et;
+  //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative
+  std::vector< Node > d_cond;
+  //value is returned by FullModelChecker::getRepresentative
+  std::vector< Node > d_value;
+private:
+  enum {
+    status_unk,
+    status_redundant,
+    status_non_redundant
+  };
+  std::vector< int > d_status;
+  bool d_has_simplified;
+public:
+  Def() : d_has_simplified(false){}
+  void reset() {
+    d_et.reset();
+    d_cond.clear();
+    d_value.clear();
+    d_status.clear();
+    d_has_simplified = false;
+  }
+  bool addEntry( FullModelChecker * m, Node c, Node v);
+  Node evaluate( FullModelChecker * m, std::vector<Node> inst );
+  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );
+  void simplify( FullModelChecker * m );
+  void debugPrint(const char * tr, Node op, FullModelChecker * m);
+};
+
+
+class FullModelChecker
+{
+private:
+  Node d_true;
+  Node d_false;
+  QuantifiersEngine* d_qe;
+  std::map<TypeNode, std::map< Node, int > > d_rep_ids;
+  std::map<TypeNode, Node > d_model_basis_rep;
+  std::map<Node, Def * > d_models;
+  std::map<Node, Def > d_quant_models;
+  std::map<Node, bool > d_models_init;
+  std::map<Node, Node > d_quant_cond;
+  std::map<TypeNode, Node > d_type_star;
+  std::map<Node, std::map< Node, int > > d_quant_var_id;
+  std::map<Node, std::vector< int > > d_star_insts;
+  Node getRepresentative(FirstOrderModel * fm, Node n);
+  Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n);
+  void addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
+                 std::vector< Node > & conds,
+                 std::vector< Node > & values,
+                 std::vector< Node > & entry_conds );
+  int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index);
+private:
+  void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n );
+
+  void doNegate( Def & dc );
+  void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq );
+  void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v);
+  void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
+
+  void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+                               std::vector< Def > & dc, int index,
+                               std::vector< Node > & cond, std::vector<Node> & val );
+  void doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+                                std::map< int, Node > & entries, int index,
+                                std::vector< Node > & cond, std::vector< Node > & val,
+                                EntryTrie & curr);
+
+  void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,
+                             std::vector< Def > & dc, int index,
+                             std::vector< Node > & cond, std::vector<Node> & val );
+  int isCompat( std::vector< Node > & cond, Node c );
+  bool doMeet( std::vector< Node > & cond, Node c );
+  Node mkCond( std::vector< Node > & cond );
+  Node mkCondDefault( Node f );
+  void mkCondDefaultVec( Node f, std::vector< Node > & cond );
+  void mkCondVec( Node n, std::vector< Node > & cond );
+  Node evaluateInterpreted( Node n, std::vector< Node > & vals );
+public:
+  FullModelChecker( QuantifiersEngine* qe );
+  ~FullModelChecker(){}
+
+  int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
+  bool isStar(Node n);
+  Node getStar(TypeNode tn) { return d_type_star[tn]; }
+  bool isModelBasisTerm(Node n);
+  Node getModelBasisTerm(TypeNode tn);
+  void reset(FirstOrderModel * fm);
+  Def * getModel(FirstOrderModel * fm, Node op);
+
+  void debugPrintCond(const char * tr, Node n, bool dispStar = false);
+  void debugPrint(const char * tr, Node n, bool dispStar = false);
+
+  int exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort);
+  bool hasStarExceptions( Node f ) { return !d_star_insts[f].empty(); }
+
+  bool isActive();
+  bool useSimpleModels();
+};
+
+}
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index f6a0dad11..d4988f223 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -134,18 +134,27 @@ Node InstMatch::getValue( Node var ) const{
   }
 }
 
+Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) {
+  return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) );
+}
+
 void InstMatch::set(TNode var, TNode n){
   Assert( !var.isNull() );
-  if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-  	//var.getType() == n.getType()
-  	!n.getType().isSubtypeOf( var.getType() ) ){
-    Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
-    Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
-    Assert(false);
+  if (Trace.isOn("inst-match-warn")) {
+    // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
+    if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
+      Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
+      Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
+    }
   }
+  Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) );
   d_map[var] = n;
 }
 
+void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
+  set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n );
+}
+
 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 127f83c60..72447fd66 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -92,8 +92,11 @@ public:
   void erase(Node node){ d_map.erase(node); }
   /** get */
   Node get( TNode var ) { return d_map[var]; }
+  Node get( QuantifiersEngine* qe, Node f, int i );
   /** set */
   void set(TNode var, TNode n);
+  void set( QuantifiersEngine* qe, Node f, int i, TNode n );
+  /** size */
   size_t size(){ return d_map.size(); }
   /* iterator */
   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index de7f2f373..105575c49 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -52,22 +52,28 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       //we want to add the children of the NOT
       d_match_pattern = d_pattern[0];
     }
-    if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
-      if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
+    if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
+      if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ||
+          d_match_pattern[0].getKind()==INST_CONSTANT ){
         Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
+        Node mp = d_match_pattern[1];
         //swap sides
         Node pat = d_pattern;
-        d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
-        d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
-        if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
-          d_match_pattern = d_match_pattern[1];
+        if(d_match_pattern.getKind()==GEQ){
+          d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] );
+          d_pattern = d_pattern.negate();
         }else{
-          d_match_pattern = d_pattern[0][0];
+          d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
         }
-      }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
+        d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
+        d_match_pattern = mp;
+      }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ||
+                d_match_pattern[1].getKind()==INST_CONSTANT ){
         Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
         if( d_pattern.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
           d_match_pattern = d_match_pattern[0];
+        }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){
+          d_match_pattern = d_match_pattern[0];
         }
       }
     }
@@ -96,17 +102,23 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
         //candidates will be all disequalities
         d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
       }
-    }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
+    }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF ||
+              d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){
       Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
       if( d_pattern.getKind()==NOT ){
-        Unimplemented("Disequal generator unimplemented");
+        if (d_pattern[0][1].getKind()!=INST_CONSTANT) {
+          Unimplemented("Disequal generator unimplemented");
+        }else{
+          d_eq_class = d_pattern[0][1];
+        }
       }else{
-        Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
-        //we are matching only in a particular equivalence class
-        d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
         //store the equivalence class that we will call d_cg->reset( ... ) on
         d_eq_class = d_pattern[1];
       }
+      Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
+      //we are matching only in a particular equivalence class
+      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
+
     }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
       //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
         //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
@@ -134,7 +146,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
 /** get match (not modulo equality) */
 bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){
   Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
-                    << m << ")" << ", " << d_children.size() << std::endl;
+                    << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
   Assert( !d_match_pattern.isNull() );
   if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
     return true;
@@ -182,6 +194,36 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
         }
       }
     }
+    //for relational matching
+    if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){
+      //also must fit match to equivalence class
+      bool pol = d_pattern.getKind()!=NOT;
+      Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
+      Node t_match;
+      if( pol ){
+        if (pat.getKind()==GT) {
+          Node r = NodeManager::currentNM()->mkConst( Rational(-1) );
+          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+        }else{
+          t_match = t;
+        }
+      }else{
+        if(pat.getKind()==EQUAL) {
+          Node r = NodeManager::currentNM()->mkConst( Rational(1) );
+          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+        }else if( pat.getKind()==IFF ){
+          t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) );
+        }else if( pat.getKind()==GEQ ){
+          Node r = NodeManager::currentNM()->mkConst( Rational(1) );
+          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+        }else if( pat.getKind()==GT ){
+          t_match = t;
+        }
+      }
+      if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){
+        success = false;
+      }
+    }
     if( success ){
       //now, fit children into match
       //we will be requesting candidates for matching terms for each child
@@ -286,7 +328,7 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
   //we have a specific equivalence class in mind
   //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
   //just look in equivalence class of the RHS
-  d_cg->reset( d_eq_class );
+  d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class );
 }
 
 bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
@@ -306,7 +348,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
   if( !success ){
     //Debug("matching") << this << " failed, reset " << d_eq_class << std::endl;
     //we failed, must reset
-    reset( d_eq_class, qe );
+    reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe );
   }
   return success;
 }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 0e1266e0d..ef81d55a1 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -144,7 +144,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
     }
     if( gen ){
       generateTriggers( f, effort, e, status );
+      if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){
+        Trace("no-trigger") << "Could not find trigger for " << f << std::endl;
+      }
     }
+
     //if( e==4 ){
     //  d_processed_trigger.clear();
     //  d_quantEngine->getEqualityQuery()->setLiberal( true );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 0b74cfc5e..059c76b21 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -192,6 +192,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
           Trace("model-engine-debug") << "Building model..." << std::endl;
           //build model for UF
           for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+            Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
             constructModelUf( fm, it->first );
           }
           /*
@@ -273,7 +274,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
         }
       }
       //for calculating terms that we don't need to consider
-      if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+      if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
         if( !n.getAttribute(BasisNoMatchAttribute()) ){
           //need to consider if it is not congruent modulo model basis
           if( !tabt.addTerm( fm, n ) ){
@@ -352,7 +353,7 @@ bool ModelEngineBuilder::isQuantifierActive( Node f ){
 
 bool ModelEngineBuilder::isTermActive( Node n ){
   return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
-         ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
+         ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
                                                                                                       //and is not congruent modulo model basis
                                                                                                       //to another active term
 }
@@ -597,7 +598,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op )
         fm->d_uf_model_gen[op].setValue( fm, n, v );
         if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){
           //also set as default value if necessary
-          if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
+          if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
             Trace("fmf-model-cons") << "  Set as default." << std::endl;
             fm->d_uf_model_gen[op].setValue( fm, n, v, false );
             if( n==defaultTerm ){
@@ -619,6 +620,13 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op )
       Trace("fmf-model-cons") << "  Choose default value..." << std::endl;
       //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
       Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
+      if( defaultVal.isNull() ){
+        if (!fm->d_rep_set.hasType(defaultTerm.getType())) {
+          Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
+          fm->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
+        }
+        defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0];
+      }
       Assert( !defaultVal.isNull() );
       Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl;
       fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
@@ -935,7 +943,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
   if( s.getKind()==APPLY_UF ){
     Assert( s.hasAttribute(ModelBasisArgAttribute()) );
     if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl;
-    if( s.getAttribute(ModelBasisArgAttribute())==1 ){
+    if( s.getAttribute(ModelBasisArgAttribute())!=0 ){
       d_term_selected[ s ] = true;
       Trace("sel-form-term") << "  " << s << " is a selected term." << std::endl;
     }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index a69b278c0..90b8c62ba 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -36,7 +36,8 @@ using namespace CVC4::theory::inst;
 //Model Engine constructor
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ){
+d_rel_domain( qe, qe->getModel() ),
+d_fmc( qe ){
 
   if( options::fmfNewInstGen() ){
     d_builder = new ModelEngineBuilderInstGen( c, qe );
@@ -75,6 +76,11 @@ void ModelEngine::check( Theory::Effort e ){
           //let the strong solver verify that the model is minimal
           //for debugging, this will if there are terms in the model that the strong solver was not notified of
           ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
+          //for full model checking
+          if( d_fmc.isActive() ){
+            Trace("model-engine-debug") << "Reset full model checker..." << std::endl;
+            d_fmc.reset( fm );
+          }
           Trace("model-engine-debug") << "Check model..." << std::endl;
           d_incomplete_check = false;
           //print debug
@@ -161,15 +167,23 @@ int ModelEngine::checkModel( int checkOption ){
       if( it->first.isSort() ){
         Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
         Trace("model-engine-debug") << "   ";
+        Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
         for( size_t i=0; i<it->second.size(); i++ ){
           //Trace("model-engine-debug") << it->second[i] << "  ";
           Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
           Trace("model-engine-debug") << r << " ";
         }
         Trace("model-engine-debug") << std::endl;
+        Trace("model-engine-debug") << "  Model basis term : " << mbt << std::endl;
       }
     }
   }
+  //full model checking: construct models for all functions
+  if( d_fmc.isActive() ){
+    for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
+      d_fmc.getModel(fm, it->first);
+    }
+  }
   //compute the relevant domain if necessary
   if( optUseRelevantDomain() ){
     d_rel_domain.compute();
@@ -179,36 +193,41 @@ int ModelEngine::checkModel( int checkOption ){
   d_relevantLemmas = 0;
   d_totalLemmas = 0;
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-    Node f = fm->getAssertedQuantifier( i );
-    //keep track of total instantiations for statistics
-    int totalInst = 1;
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      TypeNode tn = f[0][i].getType();
-      if( fm->d_rep_set.hasType( tn ) ){
-        totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
-      }
-    }
-    d_totalLemmas += totalInst;
-    //determine if we should check this quantifiers
-    bool checkQuant = false;
-    if( checkOption==check_model_full ){
-      checkQuant = d_builder->isQuantifierActive( f );
-    }else if( checkOption==check_model_no_inst_gen ){
-      checkQuant = !d_builder->hasInstGen( f );
-    }
-    //if we need to consider this quantifier on this iteration
-    if( checkQuant ){
-      addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
-      if( Trace.isOn("model-engine-warn") ){
-        if( addedLemmas>10000 ){
-          Debug("fmf-exit") << std::endl;
-          debugPrint("fmf-exit");
-          exit( 0 );
+  int e_max = d_fmc.isActive() ? 2 : 1;
+  for( int e=0; e<e_max; e++) {
+    if (addedLemmas==0) {
+      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node f = fm->getAssertedQuantifier( i );
+        //keep track of total instantiations for statistics
+        int totalInst = 1;
+        for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+          TypeNode tn = f[0][i].getType();
+          if( fm->d_rep_set.hasType( tn ) ){
+            totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+          }
+        }
+        d_totalLemmas += totalInst;
+        //determine if we should check this quantifiers
+        bool checkQuant = false;
+        if( checkOption==check_model_full ){
+          checkQuant = d_builder->isQuantifierActive( f );
+        }else if( checkOption==check_model_no_inst_gen ){
+          checkQuant = !d_builder->hasInstGen( f );
+        }
+        //if we need to consider this quantifier on this iteration
+        if( checkQuant ){
+          addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain(), e );
+          if( Trace.isOn("model-engine-warn") ){
+            if( addedLemmas>10000 ){
+              Debug("fmf-exit") << std::endl;
+              debugPrint("fmf-exit");
+              exit( 0 );
+            }
+          }
+          if( optOneQuantPerRound() && addedLemmas>0 ){
+            break;
+          }
         }
-      }
-      if( optOneQuantPerRound() && addedLemmas>0 ){
-        break;
       }
     }
   }
@@ -222,100 +241,115 @@ int ModelEngine::checkModel( int checkOption ){
   return addedLemmas;
 }
 
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effort ){
   int addedLemmas = 0;
-  Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl;
-  Debug("inst-fmf-ei") << "   Instantiation Constants: ";
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
-  }
-  Debug("inst-fmf-ei") << std::endl;
 
-  //create a rep set iterator and iterate over the (relevant) domain of the quantifier
-  RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
-  if( riter.setQuantifier( f ) ){
-    //set the domain for the iterator (the sufficient set of instantiations to try)
-    if( useRelInstDomain ){
-      riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+  bool useModel = d_builder->optUseModel();
+  if (d_fmc.isActive() && effort==0) {
+    addedLemmas = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
+  }else if( !d_fmc.isActive() || (effort==1 && d_fmc.hasStarExceptions(f)) ) {
+    if(d_fmc.isActive()){
+      useModel = false;
+      int lem = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
+      if( lem!=-1 ){
+        return lem;
+      }
     }
-    d_quantEngine->getModel()->resetEvaluate();
-    int tests = 0;
-    int triedLemmas = 0;
-    while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
-      d_testLemmas++;
-      int eval = 0;
-      int depIndex;
-      if( d_builder->optUseModel() ){
-        //see if instantiation is already true in current model
-        Debug("fmf-model-eval") << "Evaluating ";
-        riter.debugPrintSmall("fmf-model-eval");
-        Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
-        tests++;
-        //if evaluate(...)==1, then the instantiation is already true in the model
-        //  depIndex is the index of the least significant variable that this evaluation relies upon
-        depIndex = riter.getNumTerms()-1;
-        eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
-        if( eval==1 ){
-          Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
-        }else{
-          Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
-        }
+    Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
+    Debug("inst-fmf-ei") << "   Instantiation Constants: ";
+    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+    }
+    Debug("inst-fmf-ei") << std::endl;
+    //create a rep set iterator and iterate over the (relevant) domain of the quantifier
+    RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
+    if( riter.setQuantifier( f ) ){
+      Debug("inst-fmf-ei") << "Set domain..." << std::endl;
+      //set the domain for the iterator (the sufficient set of instantiations to try)
+      if( useRelInstDomain ){
+        riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
       }
-      if( eval==1 ){
-        //instantiation is already true -> skip
-        riter.increment2( depIndex );
-      }else{
-        //instantiation was not shown to be true, construct the match
-        InstMatch m;
-        for( int i=0; i<riter.getNumTerms(); i++ ){
-          m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+      Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+      d_quantEngine->getModel()->resetEvaluate();
+      Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+      int tests = 0;
+      int triedLemmas = 0;
+      while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+        d_testLemmas++;
+        int eval = 0;
+        int depIndex;
+        if( useModel ){
+          //see if instantiation is already true in current model
+          Debug("fmf-model-eval") << "Evaluating ";
+          riter.debugPrintSmall("fmf-model-eval");
+          Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+          tests++;
+          //if evaluate(...)==1, then the instantiation is already true in the model
+          //  depIndex is the index of the least significant variable that this evaluation relies upon
+          depIndex = riter.getNumTerms()-1;
+          eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+          if( eval==1 ){
+            Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+          }else{
+            Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+          }
         }
-        Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
-        triedLemmas++;
-        d_triedLemmas++;
-        //add as instantiation
-        if( d_quantEngine->addInstantiation( f, m ) ){
-          addedLemmas++;
-          //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
-          if( eval==-1 && optExhInstEvalSkipMultiple() ){
-            riter.increment2( depIndex );
+        if( eval==1 ){
+          //instantiation is already true -> skip
+          riter.increment2( depIndex );
+        }else{
+          //instantiation was not shown to be true, construct the match
+          InstMatch m;
+          for( int i=0; i<riter.getNumTerms(); i++ ){
+            m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
+          }
+          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+          triedLemmas++;
+          d_triedLemmas++;
+          //add as instantiation
+          if( d_quantEngine->addInstantiation( f, m ) ){
+            addedLemmas++;
+            //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+            if( eval==-1 && optExhInstEvalSkipMultiple() ){
+              riter.increment2( depIndex );
+            }else{
+              riter.increment();
+            }
           }else{
+            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
             riter.increment();
           }
-        }else{
-          Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
-          riter.increment();
         }
       }
+      //print debugging information
+      d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
+      d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
+      d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
+      d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+      int relevantInst = 1;
+      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+        relevantInst = relevantInst * (int)riter.d_domain[i].size();
+      }
+      d_relevantLemmas += relevantInst;
+      Trace("inst-fmf-ei") << "Finished: " << std::endl;
+      //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
+      Trace("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
+      Trace("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
+      Trace("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
+      Trace("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
+      if( addedLemmas>1000 ){
+        Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+        //Trace("model-engine-warn") << "   Inst Total: " << totalInst << std::endl;
+        Trace("model-engine-warn") << "   Inst Relevant: " << relevantInst << std::endl;
+        Trace("model-engine-warn") << "   Inst Tried: " << triedLemmas << std::endl;
+        Trace("model-engine-warn") << "   Inst Added: " << addedLemmas << std::endl;
+        Trace("model-engine-warn") << "   # Tests: " << tests << std::endl;
+        Trace("model-engine-warn") << std::endl;
+      }
     }
-    //print debugging information
-    d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
-    d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
-    d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
-    d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
-    int relevantInst = 1;
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      relevantInst = relevantInst * (int)riter.d_domain[i].size();
-    }
-    d_relevantLemmas += relevantInst;
-    Trace("inst-fmf-ei") << "Finished: " << std::endl;
-    //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
-    Trace("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
-    Trace("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
-    Trace("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-    Trace("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
-    if( addedLemmas>1000 ){
-      Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-      //Trace("model-engine-warn") << "   Inst Total: " << totalInst << std::endl;
-      Trace("model-engine-warn") << "   Inst Relevant: " << relevantInst << std::endl;
-      Trace("model-engine-warn") << "   Inst Tried: " << triedLemmas << std::endl;
-      Trace("model-engine-warn") << "   Inst Added: " << addedLemmas << std::endl;
-      Trace("model-engine-warn") << "   # Tests: " << tests << std::endl;
-      Trace("model-engine-warn") << std::endl;
-    }
+     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    d_incomplete_check = d_incomplete_check || riter.d_incomplete;
   }
-   //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-  d_incomplete_check = d_incomplete_check || riter.d_incomplete;
   return addedLemmas;
 }
 
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 386864164..d2cd8807a 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/model_builder.h"
 #include "theory/model.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/full_model_check.h"
 
 namespace CVC4 {
 namespace theory {
@@ -35,6 +36,8 @@ private:
 private:    //analysis of current model:
   //relevant domain
   RelevantDomain d_rel_domain;
+  //full model checker
+  fmcheck::FullModelChecker d_fmc;
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
 private:
@@ -51,7 +54,7 @@ private:
   //check model
   int checkModel( int checkOption );
   //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
-  int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
+  int exhaustiveInstantiate( Node f, bool useRelInstDomain = false, int effort = 0 );
 private:
   //temporary statistics
   int d_triedLemmas;
@@ -63,6 +66,7 @@ public:
   ~ModelEngine(){}
   //get the builder
   ModelEngineBuilder* getModelBuilder() { return d_builder; }
+  fmcheck::FullModelChecker* getFullModelChecker() { return &d_fmc; }
 public:
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 60f5a171d..a9b7f269f 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -54,6 +54,8 @@ option smartTriggers /--disable-smart-triggers bool :default true
 # Whether to use relevent triggers
 option relevantTriggers /--disable-relevant-triggers bool :default true
  prefer triggers that are more relevant based on SInE style analysis
+option relationalTriggers --relational-triggers bool :default false
+ choose relational triggers such as x = f(y), x >= f(y)
 
 # Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
@@ -88,6 +90,11 @@ option finiteModelFind --finite-model-find bool :default false
 option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
  disable model-based quantifier instantiation for finite model finding
 
+option fmfFullModelCheck --fmf-fmc bool :default false
+ enable full model check for finite model finding
+option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true
+ disable simple models in full model check for finite model finding
+
 option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for fmf
 option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
@@ -98,8 +105,8 @@ option fmfRelevantDomain --fmf-relevant-domain bool :default false
  use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
 option fmfNewInstGen --fmf-new-inst-gen bool :default false
  use new inst gen technique for answering sat without exhaustive instantiation
-option fmfInstGen /--disable-fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
+option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
+ enable/disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
 option fmfFreshDistConst --fmf-fresh-dc bool :default false
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 36db56d0d..6b07a87e0 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -22,6 +22,96 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 
+
+bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
+  if ( n.getKind()==MULT ){
+    if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){
+      msum[n[1]] = n[0];
+      return true;
+    }
+  }else{
+    if( msum.find(n)==msum.end() ){
+      msum[n] = Node::null();
+      return true;
+    }
+  }
+  return false;
+}
+
+bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) {
+  if ( n.getKind()==PLUS ){
+    for( unsigned i=0; i<n.getNumChildren(); i++) {
+      if (!getMonomial( n[i], msum )){
+        return false;
+      }
+    }
+    return true;
+  }else{
+    return getMonomial( n, msum );
+  }
+}
+
+bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
+  if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){
+    if( getMonomialSum( lit[0], msum ) ){
+      if( lit[1].isConst() ){
+        if( !lit[1].getConst<Rational>().isZero() ){
+          msum[Node::null()] = negate( lit[1] );
+        }
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ) {
+  if( msum.find(v)!=msum.end() ){
+    std::vector< Node > children;
+    Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>();
+    if ( r.sgn()!=0 ){
+      for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+        if( it->first!=v ){
+          Node m;
+          if( !it->first.isNull() ){
+            if ( !it->second.isNull() ){
+              m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
+            }else{
+              m = it->first;
+            }
+          }else{
+            m = it->second;
+          }
+          children.push_back(m);
+        }
+      }
+      veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
+                                (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
+      if( !r.isNegativeOne() ){
+        if( r.isOne() ){
+          veq = negate(veq);
+        }else{
+          //TODO
+          return false;
+        }
+      }
+      veq = Rewriter::rewrite( veq );
+      veq = NodeManager::currentNM()->mkNode( k, r.sgn()==1 ? v : veq, r.sgn()==1 ? veq : v );
+      return true;
+    }
+    return false;
+  }else{
+    return false;
+  }
+}
+
+Node QuantArith::negate( Node t ) {
+  Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
+  tt = Rewriter::rewrite( tt );
+  return tt;
+}
+
+
 void QuantRelevance::registerQuantifier( Node f ){
   //compute symbols in f
   std::vector< Node > syms;
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 6a5726cc7..d248a8999 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -28,6 +28,17 @@ namespace CVC4 {
 namespace theory {
 
 
+class QuantArith
+{
+public:
+  static bool getMonomial( Node n, std::map< Node, Node >& msum );
+  static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
+  static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
+  static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
+  static Node negate( Node t );
+};
+
+
 class QuantRelevance
 {
 private:
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3153a3c64..417b4ae3a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -254,8 +254,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
     //determine if it has model basis attribute
     for( int j=0; j<(int)n.getNumChildren(); j++ ){
       if( n[j].getAttribute(ModelBasisAttribute()) ){
-        val = 1;
-        break;
+        val++;
       }
     }
     ModelBasisArgAttribute mbaa;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 231d0ee9e..e5154476a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -83,10 +83,15 @@ public:
 };/* class TermArgTrie */
 
 
+namespace fmcheck {
+  class FullModelChecker;
+}
+
 class TermDb {
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class ::CVC4::theory::inst::Trigger;
   friend class ::CVC4::theory::rrinst::Trigger;
+  friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index cab94fb5c..1f1667522 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -28,8 +28,6 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-//#define NESTED_PATTERN_SELECTION
-
 /** trigger class constructor */
 Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) :
 d_quantEngine( qe ), d_f( f ){
@@ -249,11 +247,75 @@ bool Trigger::isUsable( Node n, Node f ){
   }
 }
 
-bool Trigger::isUsableTrigger( Node n, Node f ){
-  //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF;
+bool nodeContainsVar( Node n, Node v ){
+  if( n==v) {
+    return true;
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++) {
+      if( nodeContainsVar(n[i], v) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
+Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
+  if( options::relationalTriggers() ){
+    if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+      Node rtr;
+      for( unsigned i=0; i<2; i++) {
+        unsigned j = (i==0) ? 1 : 0;
+        if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) {
+          rtr = n;
+          break;
+        }
+      }
+      if( n[0].getType().isInteger() ){
+        //try to rearrange?
+        std::map< Node, Node > m;
+        if (QuantArith::getMonomialSumLit(n, m) ){
+          for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
+            if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
+              Node veq;
+              if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){
+                int vti = veq[0]==it->first ? 1 : 0;
+                if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){
+                  rtr = veq;
+                  InstConstantAttribute ica;
+                  rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) );
+                }
+              }
+            }
+          }
+        }
+      }
+      if( !rtr.isNull() ){
+        Trace("relational-trigger") << "Relational trigger : " << std::endl;
+        Trace("relational-trigger") << "    " << rtr << " (from " << n << ")" << std::endl;
+        Trace("relational-trigger") << "    in quantifier " << f << std::endl;
+        if( hasPol ){
+          Trace("relational-trigger") << "    polarity : " << pol << std::endl;
+        }
+        Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr;
+        InstConstantAttribute ica;
+        rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) );
+        return rtr2;
+      }
+    }
+  }
   bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
   Trace("usable") << n << " usable : " << usable << std::endl;
-  return usable;
+  if( usable ){
+    return n;
+  }else{
+    return Node::null();
+  }
+}
+
+bool Trigger::isUsableTrigger( Node n, Node f ){
+  Node nu = getIsUsableTrigger(n,f);
+  return !nu.isNull();
 }
 
 bool Trigger::isAtomicTrigger( Node n ){
@@ -274,55 +336,51 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
+bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){
   if( patMap.find( n )==patMap.end() ){
     patMap[ n ] = false;
+    bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol;
+    bool newPol = n.getKind()==NOT ? !pol : pol;
     if( tstrt==TS_MIN_TRIGGER ){
       if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
-        //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );
-        return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );
-#else
         return false;
-#endif
       }else{
         bool retVal = false;
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+          bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol;
+          bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
+          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){
             retVal = true;
           }
         }
         if( retVal ){
           return true;
-        }else if( isUsableTrigger( n, f ) ){
-          patMap[ n ] = true;
-          return true;
         }else{
-          return false;
+          Node nu = getIsUsableTrigger( n, f, pol, hasPol );
+          if( !nu.isNull() ){
+            patMap[ nu ] = true;
+            return true;
+          }else{
+            return false;
+          }
         }
       }
     }else{
       bool retVal = false;
-      if( isUsableTrigger( n, f ) ){
-        patMap[ n ] = true;
+      Node nu = getIsUsableTrigger( n, f, pol, hasPol );
+      if( !nu.isNull() ){
+        patMap[ nu ] = true;
         if( tstrt==TS_MAX_TRIGGER ){
           return true;
         }else{
           retVal = true;
         }
       }
-      if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
-        //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){
-        //  retVal = true;
-        //}
-        if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){
-          retVal = true;
-        }
-#endif
-      }else{
+      if( n.getKind()!=FORALL ){
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+          bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol;
+          bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
+          if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){
             retVal = true;
           }
         }
@@ -367,7 +425,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
       }
     }
   }
-  collectPatTerms2( qe, f, n, patMap, tstrt );
+  collectPatTerms2( qe, f, n, patMap, tstrt, true, true );
   for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
     if( it->second ){
       patTerms.push_back( it->first );
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index ca9124751..28fb2acda 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -92,8 +92,9 @@ public:
 private:
   /** is subterm of trigger usable */
   static bool isUsable( Node n, Node f );
+  static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt );
+  static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol );
 public:
   //different strategies for choosing trigger terms
   enum {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0bb0f1f79..5c24f89b7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/trigger.h"
 #include "theory/rewriterules/efficient_e_matching.h"
 #include "theory/rewriterules/rr_trigger.h"
+#include "theory/quantifiers/bounded_integers.h"
 
 using namespace std;
 using namespace CVC4;
@@ -60,8 +61,12 @@ d_lemmas_produced_c(u){
   if( options::finiteModelFind() ){
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
+
+    d_bint = new quantifiers::BoundedIntegers( this );
+    d_modules.push_back( d_bint );
   }else{
     d_model_engine = NULL;
+    d_bint = NULL;
   }
 
   //options
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bfa19bb98..85da53087 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -56,7 +56,7 @@ public:
   virtual void assertNode( Node n ) = 0;
   virtual void propagate( Theory::Effort level ){}
   virtual Node getNextDecisionRequest() { return TNode::null(); }
-  virtual Node explain(TNode n) = 0;
+  virtual Node explain(TNode n) { return TNode::null(); }
 };/* class QuantifiersModule */
 
 namespace quantifiers {
@@ -64,6 +64,7 @@ namespace quantifiers {
   class ModelEngine;
   class TermDb;
   class FirstOrderModel;
+  class BoundedIntegers;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -99,6 +100,8 @@ private:
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
   /** efficient e-matcher */
   EfficientEMatcher* d_eem;
+  /** bounded integers utility */
+  quantifiers::BoundedIntegers * d_bint;
 private:
   /** list of all quantifiers seen */
   std::vector< Node > d_quants;
diff --git a/src/theory/uf/options b/src/theory/uf/options
index 33d1255ef..bea11621a 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -30,5 +30,7 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
  always use simple clique lemmas for uf strong solver
 option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
  eagerly propagate disequalities for uf strong solver
+option ufssMinimalModel /--disable-uf-ss-min-model bool :default true
+ disable finding a minimal model in uf strong solver
 
 endmodule
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 228cfd2c4..2c853a4fa 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -17,6 +17,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/options.h"
 
 #define RECONSIDER_FUNC_DEFAULT_VALUE
 #define USE_PARTIAL_DEFAULT_VALUES
@@ -309,19 +310,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground
     if( !ground ){
       int defSize = (int)d_defaults.size();
       for( int i=0; i<defSize; i++ ){
-        bool isGround;
         //for soundness, to allow variable order-independent function interpretations,
         //  we must ensure that the intersection of all default terms
         //  is also defined.
         //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
         //  then we must define f( b, a ).
-        Node ni = getIntersection( m, n, d_defaults[i], isGround );
-        if( !ni.isNull() ){
-          //if the intersection exists, and is not already defined
-          if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
-              d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
-            //use the current value
-            setValue( m, ni, v, isGround, false );
+        if (!options::fmfFullModelCheck()) {
+          bool isGround;
+          Node ni = getIntersection( m, n, d_defaults[i], isGround );
+          if( !ni.isNull() ){
+            //if the intersection exists, and is not already defined
+            if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
+                d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
+              //use the current value
+              setValue( m, ni, v, isGround, false );
+            }
           }
         }
       }
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 12c1cf244..9140806ec 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -153,9 +153,10 @@ public:
   static Node toIte( TypeNode type, Node fm_node, const char* argPrefix );
 };
 
+
 class UfModelTreeGenerator
 {
-private:
+public:
   //store for set values
   Node d_default_value;
   std::map< Node, Node > d_set_values[2][2];
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d64f7df60..e868460f8 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -595,9 +595,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           if( d_regions[i]->d_valid ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
-              //add clique lemma
-              addCliqueLemma( clique, out );
-              return;
+              if( options::ufssMinimalModel() ){
+                //add clique lemma
+                addCliqueLemma( clique, out );
+                return;
+              }
             }else{
               Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
             }
@@ -659,13 +661,17 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
               //naive strategy, force region combination involving the first valid region
               for( int i=0; i<(int)d_regions_index; i++ ){
                 if( d_regions[i]->d_valid ){
-                  forceCombineRegion( i, false );
-                  recheck = true;
-                  break;
+                  int fcr = forceCombineRegion( i, false );
+                  Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
+                  if( options::ufssMinimalModel() || fcr!=-1 ){
+                    recheck = true;
+                    break;
+                  }
                 }
               }
             }
             if( recheck ){
+              Trace("uf-ss-debug") << "Must recheck." << std::endl;
               check( level, out );
             }
           }
@@ -869,8 +875,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
     //now check if region is in conflict
     std::vector< Node > clique;
     if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
-      //explain clique
-      addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      if( options::ufssMinimalModel() ){
+        //explain clique
+        addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      }
     }
   }
 }
@@ -1013,8 +1021,8 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 }
 
 bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
+  Node s;
   if( r->hasSplits() ){
-    Node s;
     if( !options::ufssSmartSplits() ){
       //take the first split you find
       for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
@@ -1038,8 +1046,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
         }
       }
     }
+    Assert( s!=Node::null() );
+  }else{
+    if( !options::ufssMinimalModel() ){
+      //since candidate clique is not reported, we may need to find splits manually
+      for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
+        if ( it->second->d_valid ){
+          for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){
+            if ( it->second!=it2->second && it2->second->d_valid ){
+              if( !r->isDisequal( it->first, it2->first, 1 ) ){
+                s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first );
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  if (!s.isNull() ){
     //add lemma to output channel
-    Assert( s!=Node::null() && s.getKind()==EQUAL );
+    Assert( s.getKind()==EQUAL );
     s = Rewriter::rewrite( s );
     Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
     if( options::sortInference()) {