Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.

9 files changed, 329 insertions, 90 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 85a245a09..be6acd09c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1031,6 +1031,10 @@ void SmtEngine::setLogicInternal() throw() {
       options::fmfInstGen.set( false );
     }
   }
+  if ( options::fmfBoundInt() ){
+    //if bounded integers are set, must use full model check for MBQI
+    options::fmfFullModelCheck.set( true );
+  }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 186444e0a..0bbef1601 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -32,7 +32,7 @@ class DatatypesRewriter {
 public:
 
   static RewriteResponse postRewrite(TNode in) {
-    Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl;
+    Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
 
     if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
       Type t = in.getType().toType();
@@ -41,7 +41,7 @@ public:
       // to ensure a normal form, all parameteric datatype constructors must have a type ascription
       if( dt.isParametric() ){
         if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
-          Trace("datatypes-rewrite") << "Ascribing type to parametric datatype constructor " << in << std::endl;
+          Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
           Node op = in.getOperator();
           //get the constructor object
           const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
@@ -53,7 +53,7 @@ public:
           children.push_back( op_new );
           children.insert( children.end(), in.begin(), in.end() );
           Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-          Trace("datatypes-rewrite") << "Created " << inr << std::endl;
+          Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
           return RewriteResponse(REWRITE_DONE, inr);
         }
       }
@@ -214,7 +214,7 @@ public:
   }
 
   static RewriteResponse preRewrite(TNode in) {
-    Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl;
+    Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
     return RewriteResponse(REWRITE_DONE, in);
   }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index a0651efb4..c827a8f07 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -26,6 +26,8 @@
 #include "smt/options.h"
 #include "smt/boolean_terms.h"
 #include "theory/quantifiers/options.h"
+#include "theory/datatypes/options.h"
+#include "theory/type_enumerator.h"
 
 #include <map>
 
@@ -158,15 +160,18 @@ void TheoryDatatypes::check(Effort e) {
                 }
               }
               if( !needSplit && mustSpecifyAssignment() ){
+                // &&
                 //for the sake of termination, we must choose the constructor of a ground term
                 //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
                 //** TODO: this is probably not good enough, actually need fair enumeration strategy
+                /*
                 Node groundTerm = n.getType().mkGroundTerm();
                 int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
                 if( pcons[index] ){
                   consIndex = index;
                 }
                 needSplit = true;
+                */
               }
               if( needSplit && consIndex!=-1 ) {
                 Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
@@ -179,7 +184,7 @@ void TheoryDatatypes::check(Effort e) {
                 d_out->requirePhase( test, true );
                 return;
               }else{
-                Trace("dt-split") << "Do not split constructor for " << n << std::endl;
+                Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl;
               }
             }
           }else{
@@ -503,6 +508,9 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         trep2 = eqc2->d_constructor.get();
       }
       EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
+
+
+
       if( eqc1 ){
         if( !eqc1->d_constructor.get().isNull() ){
           trep1 = eqc1->d_constructor.get();
@@ -538,6 +546,29 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           eqc1->d_inst = true;
         }
         if( cons1.isNull() && !cons2.isNull() ){
+          Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
+          NodeListMap::iterator lbl_i = d_labels.find( t1 );
+          if( lbl_i != d_labels.end() ){
+            size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr());
+            NodeList* lbl = (*lbl_i).second;
+            for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+              if( (*i).getKind()==NOT ){
+                if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){
+                  Node n = *i;
+                  std::vector< TNode > assumptions;
+                  explain( *i, assumptions );
+                  explain( cons2.eqNode( (*i)[0][0] ), assumptions );
+                  d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
+                  Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+                  Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
+                  d_out->conflict( d_conflictNode );
+                  d_conflict = true;
+                  return;
+                }
+              }
+            }
+          }
+
           checkInst = true;
           eqc1->d_constructor.set( eqc2->d_constructor );
         }
@@ -548,14 +579,18 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         eqc1->d_inst.set( eqc2->d_inst );
         eqc1->d_constructor.set( eqc2->d_constructor );
       }
+
+
+
       //merge labels
-      Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
       NodeListMap::iterator lbl_i = d_labels.find( t2 );
       if( lbl_i != d_labels.end() ){
+        Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
         NodeList* lbl = (*lbl_i).second;
         for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
           addTester( *j, eqc1, t1 );
           if( d_conflict ){
+            Debug("datatypes-debug") << "Conflict!" << std::endl;
             return;
           }
         }
@@ -643,7 +678,7 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
 
 void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
   if( !d_conflict ){
-    Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl;
+    Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
     bool tpolarity = t.getKind()!=NOT;
     Node tt = ( t.getKind() == NOT ) ? t[0] : t;
     int ttindex = Datatype::indexOf( tt.getOperator().toExpr() );
@@ -768,6 +803,28 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
   m->assertEqualityEngine( &d_equalityEngine );
+
+  std::vector< TypeEnumerator > vec;
+  std::map< TypeNode, int > tes;
+  Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl;
+
+  //get all constructors
+  eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
+  std::vector< Node > cons;
+  while( !eqccs_i.isFinished() ){
+    Node eqc = (*eqccs_i);
+    //for all equivalence classes that are datatypes
+    if( DatatypesRewriter::isTermDatatype( eqc ) ){
+      EqcInfo* ei = getOrMakeEqcInfo( eqc );
+      if( ei ){
+        if( !ei->d_constructor.get().isNull() ){
+          cons.push_back( ei->d_constructor.get() );
+        }
+      }
+    }
+    ++eqccs_i;
+  }
+
   //must choose proper representatives
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
@@ -778,10 +835,63 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
       if( ei ){
         if( !ei->d_constructor.get().isNull() ){
           //specify that we should use the constructor as the representative
-          m->assertRepresentative( ei->d_constructor.get() );
+          //m->assertRepresentative( ei->d_constructor.get() );
         }else{
-          Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc << std::endl;
-          Trace("model-warn") << "   Type : " << eqc.getType() << std::endl;
+          Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
+          Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
+
+          std::vector< bool > pcons;
+          getPossibleCons( ei, eqc, pcons );
+          Trace("dt-cmi") << "Possible constructors : ";
+          for( unsigned i=0; i<pcons.size(); i++ ){
+            Trace("dt-cmi") << pcons[i] << " ";
+          }
+          Trace("dt-cmi") << std::endl;
+
+          if( tes.find( eqc.getType() )==tes.end() ){
+            tes[eqc.getType()]=vec.size();
+            vec.push_back( TypeEnumerator( eqc.getType() ) );
+          }
+          bool success;
+          Node n;
+          do {
+            success = true;
+            Assert( !vec[tes[eqc.getType()]].isFinished() );
+            n = *vec[tes[eqc.getType()]];
+            ++vec[tes[eqc.getType()]];
+
+            //applyTypeAscriptions( n, eqc.getType() );
+
+            Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl;
+            //check if it is consistent with labels
+            size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
+            if( constructorIndex<pcons.size() && pcons[constructorIndex] ){
+              for( unsigned i=0; i<cons.size(); i++ ){
+                //check if it is modulo equality the same
+                if( cons[i].getOperator()==n.getOperator() ){
+                  bool diff = false;
+                  for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+                    if( !m->areEqual( cons[i][j], n[j] ) ){
+                      diff = true;
+                      break;
+                    }
+                  }
+                  if( !diff ){
+                    Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
+                    success = false;
+                    break;
+                  }
+                }
+              }
+            }else{
+              Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
+              success = false;
+            }
+          }while( !success );
+          Trace("dt-cmi") << "Assign : " << n << std::endl;
+          //m->assertRepresentative( n );
+          m->assertEquality( eqc, n, true );
+
         }
       }else{
         Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl;
@@ -871,7 +981,38 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
     return n_ic;
   //}
 }
-
+/*
+Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){
+  Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl;
+  if( n.getKind()==APPLY_CONSTRUCTOR ){
+    //add type ascription for ambiguous constructor types
+    if(!n.getType().isComparableTo(tn)) {
+      size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      Assert( dt.isParametric() );
+      Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl;
+      Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl;
+      Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType());
+      Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl;
+      Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                 NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() );
+      std::vector< Node > children;
+      children.push_back( op );
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        children.push_back( applyTypeAscriptions( n[i], TypeNode::fromType( tspec )[i] ) );
+      }
+      n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ) );
+      Assert( n.getType()==tn );
+      return n;
+    }
+  }else{
+    if( n.getType()!=tn ){
+      Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl;
+    }
+  }
+  return n;
+}
+*/
 void TheoryDatatypes::collapseSelectors(){
   //must check incorrect applications of selectors
   for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){
@@ -918,7 +1059,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     int index = getLabelIndex( eqc, n );
     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
     //must be finite or have a selector
-    if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
+    //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
       //instantiate this equivalence class
       eqc->d_inst = true;
       Node tt_cons = getInstantiateCons( tt, dt, index );
@@ -933,7 +1074,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
         d_infer.push_back( eq );
         d_infer_exp.push_back( exp );
       }
-    }
+    //}
+    //else{
+    //  Debug("datatypes-inst") << "Do not instantiate" << std::endl;
+    //}
   }
 }
 
@@ -1094,43 +1238,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
-    if( DatatypesRewriter::isTermDatatype( eqc ) ){
-      Trace( c ) << "DATATYPE : ";
-    }
-    Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
-    Trace( c ) << "   { ";
-    //add terms to model
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      Trace( c ) << (*eqc_i) << " ";
-      ++eqc_i;
-    }
-    Trace( c ) << "}" << std::endl;
-    if( DatatypesRewriter::isTermDatatype( eqc ) ){
-      EqcInfo* ei = getOrMakeEqcInfo( eqc );
-      if( ei ){
-        Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
-        if( ei->d_constructor.get().isNull() ){
-          Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
-          Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
-          Trace( c ) << "   Constructor : " << std::endl;
-          Trace( c ) << "   Labels : ";
-          if( hasLabel( ei, eqc ) ){
-            Trace( c ) << getLabel( eqc );
-          }else{
-            NodeListMap::iterator lbl_i = d_labels.find( eqc );
-            if( lbl_i != d_labels.end() ){
-              NodeList* lbl = (*lbl_i).second;
-              for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
-                Trace( c ) << *j << " ";
+    if( !eqc.getType().isBoolean() ){
+      if( DatatypesRewriter::isTermDatatype( eqc ) ){
+        Trace( c ) << "DATATYPE : ";
+      }
+      Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
+      Trace( c ) << "   { ";
+      //add terms to model
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+      while( !eqc_i.isFinished() ){
+        Trace( c ) << (*eqc_i) << " ";
+        ++eqc_i;
+      }
+      Trace( c ) << "}" << std::endl;
+      if( DatatypesRewriter::isTermDatatype( eqc ) ){
+        EqcInfo* ei = getOrMakeEqcInfo( eqc );
+        if( ei ){
+          Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
+          if( ei->d_constructor.get().isNull() ){
+            Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
+            Trace("debug-model-warn") << "  Type : " << eqc.getType() << std::endl;
+            Trace( c ) << "   Constructor : " << std::endl;
+            Trace( c ) << "   Labels : ";
+            if( hasLabel( ei, eqc ) ){
+              Trace( c ) << getLabel( eqc );
+            }else{
+              NodeListMap::iterator lbl_i = d_labels.find( eqc );
+              if( lbl_i != d_labels.end() ){
+                NodeList* lbl = (*lbl_i).second;
+                for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
+                  Trace( c ) << *j << " ";
+                }
               }
             }
+            Trace( c ) << std::endl;
+          }else{
+            Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
           }
-          Trace( c ) << std::endl;
-        }else{
-          Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
+          Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
         }
-        Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
       }
     }
     ++eqcs_i;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e38c522c5..203782a79 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -226,6 +226,8 @@ private:
   void collectTerms( Node n );
   /** get instantiate cons */
   Node getInstantiateCons( Node n, const Datatype& dt, int index );
+  /** apply type ascriptions */
+  //Node applyTypeAscriptions( Node n, TypeNode tn );
   /** process new term that was created internally */
   void processNewTerm( Node n );
   /** check instantiate */
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 778304f32..cec1dccfc 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -37,6 +37,8 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   size_t d_zeroCtor;
   /** Delegate enumerators for the arguments of the current constructor */
   TypeEnumerator** d_argEnumerators;
+  /** type */
+  TypeNode d_type;
 
   /** Allocate and initialize the delegate enumerators */
   void newEnumerators() {
@@ -65,7 +67,8 @@ public:
     d_datatype(DatatypeType(type.toType()).getDatatype()),
     d_ctor(0),
     d_zeroCtor(0),
-    d_argEnumerators(NULL) {
+    d_argEnumerators(NULL),
+    d_type(type) {
 
     //Assert(type.isDatatype());
     Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl;
@@ -76,8 +79,21 @@ public:
     /* FIXME: this isn't sufficient for mutually-recursive datatypes! */
     while(d_zeroCtor < d_datatype.getNumConstructors()) {
       bool recursive = false;
-      for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
-        recursive = (Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type);
+      if( d_datatype.isParametric() ){
+        TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) );
+        for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
+          if( tn[i]==type ){
+            recursive = true;
+            break;
+          }
+        }
+      }else{
+        for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) {
+          if(Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type) {
+            recursive = true;
+            break;
+          }
+        }
       }
       if(!recursive) {
         break;
@@ -97,7 +113,8 @@ public:
     d_datatype(de.d_datatype),
     d_ctor(de.d_ctor),
     d_zeroCtor(de.d_zeroCtor),
-    d_argEnumerators(NULL) {
+    d_argEnumerators(NULL),
+    d_type(de.d_type) {
 
     if(de.d_argEnumerators != NULL) {
       newEnumerators();
@@ -117,18 +134,33 @@ public:
     if(d_ctor < d_datatype.getNumConstructors()) {
       DatatypeConstructor ctor = d_datatype[d_ctor];
       NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
-      b << ctor.getConstructor();
+      Type typ;
+      if( d_datatype.isParametric() ){
+        typ = d_datatype[d_ctor].getSpecializedConstructorType(d_type.toType());
+        b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                              NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
+      }else{
+        b << ctor.getConstructor();
+      }
       try {
         for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) {
           if(d_argEnumerators[a] == NULL) {
-            d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]);
+            if( d_datatype.isParametric() ){
+              d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType( typ )[a]);
+            }else{
+              d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]);
+            }
           }
           b << **d_argEnumerators[a];
         }
       } catch(NoMoreValuesException&) {
         InternalError();
       }
-      return Node(b);
+      Node nnn = Node(b);
+      //if( nnn.getType()!=d_type || !nnn.getType().isComparableTo(d_type) ){
+      //  Debug("dt-warn") << "WARNING : Enum : " << nnn << " bad type : " << nnn.getType() << " " << d_type << std::endl;
+      //}
+      return nnn;
     } else {
       throw NoMoreValuesException(getType());
     }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index cb8cb8154..b1a0c4ed4 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -139,6 +139,11 @@ bool ModelEngine::optOneQuantPerRound(){
 
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_quantEngine->getModel();
+
+  //flatten the representatives
+  //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
+  //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
+
   //for debugging
   if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
     for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
@@ -149,7 +154,7 @@ int ModelEngine::checkModel(){
         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] );
+          Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
           Trace("model-engine-debug") << r << " ";
         }
         Trace("model-engine-debug") << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 57211ade7..fd114df04 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -98,7 +98,7 @@ 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
+option fmfFullModelCheck --fmf-fmc bool :default false :read-write
  enable full model check for finite model finding
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2ae5edb39..c14ee01ce 100755
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -102,7 +102,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_eq_query;
 }
 
-EqualityQuery* QuantifiersEngine::getEqualityQuery() {
+EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
   return d_eq_query;
 }
 
@@ -594,8 +594,9 @@ Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
   eq::EqualityEngine* ee = getEngine();
   if( ee->hasTerm( a ) ){
     return ee->getRepresentative( a );
+  }else{
+    return a;
   }
-  return a;
 }
 
 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
@@ -631,14 +632,10 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
   if( !options::internalReps() ){
     return r;
   }else{
-    int sortId = 0;
-    if( optInternalRepSortInference() && !f.isNull() ){
-      sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
-    }
-    if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
+    if( d_int_rep.find( r )==d_int_rep.end() ){
       //find best selection for representative
       Node r_best;
-      if( options::fmfRelevantDomain() ){
+      if( options::fmfRelevantDomain() && !f.isNull() ){
         Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
         r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r );
         Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
@@ -656,13 +653,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
           //if cbqi is active, do not choose instantiation constant terms
           if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
             int score = getRepScore( eqc[i], f, index );
-            //base it on sort information as well
-            if( sortId!=0 ){
-              int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i] );
-              if( score>=0 && e_sortId!=sortId ){
-                score += 100;
-              }
-            }
             //score prefers earliest use of this term as a representative
             if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
               r_best = eqc[i];
@@ -671,37 +661,100 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
 		      }
         }
         if( r_best.isNull() ){
-	        Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
-		      r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+          if( !f.isNull() ){
+            Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
+            r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+          }else{
+            r_best = a;
+          }
 		    }
         //now, make sure that no other member of the class is an instance
-        if( !optInternalRepSortInference() ){
-          r_best = getInstance( r_best, eqc );
-        }
+        r_best = getInstance( r_best, eqc );
         //store that this representative was chosen at this point
         if( d_rep_score.find( r_best )==d_rep_score.end() ){
           d_rep_score[ r_best ] = d_reset_count;
         }
         Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
       }
-      d_int_rep[sortId][r] = r_best;
+      d_int_rep[r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
       }
-      if( optInternalRepSortInference() ){
-        int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best );
-        if( sortId!=sortIdBest ){
-          Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl;
-        }
-      }
       return r_best;
     }else{
-      return d_int_rep[sortId][r];
+      return d_int_rep[r];
     }
   }
 }
 
+void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
+  //make sure internal representatives currently exist
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
+    if( it->first.isSort() ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
+      }
+    }
+  }
+  Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
+  for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+    Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+  }
+  //store representatives for newly created terms
+  std::map< Node, Node > temp_rep_map;
+
+  bool success;
+  do {
+    success = false;
+    for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+      if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
+        Node ni = it->second;
+        std::vector< Node > cc;
+        cc.push_back( it->second.getOperator() );
+        bool changed = false;
+        for( unsigned j=0; j<ni.getNumChildren(); j++ ){
+          if( ni[j].getType().isSort() ){
+            Node r = getRepresentative( ni[j] );
+            if( d_int_rep.find( r )==d_int_rep.end() ){
+              Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
+              r = temp_rep_map[r];
+            }
+            if( r==ni ){
+              //found sub-term as instance
+              Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
+              d_int_rep[it->first] = ni[j];
+              changed = false;
+              success = true;
+              break;
+            }else{
+              Node ir = d_int_rep[r];
+              cc.push_back( ir );
+              if( ni[j]!=ir ){
+                changed = true;
+              }
+            }
+          }else{
+            changed = false;
+            break;
+          }
+        }
+        if( changed ){
+          Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
+          Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
+          success = true;
+          d_int_rep[it->first] = n;
+          temp_rep_map[n] = it->first;
+        }
+      }
+    }
+  }while( success );
+  Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
+  for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
+    Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+  }
+}
+
 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
   return d_qe->getMasterEqualityEngine();
 }
@@ -758,6 +811,3 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
   //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 }
 
-bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
-  return false; //shown to be not effective
-}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b075f7be8..8f645afe7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -142,7 +142,7 @@ public:
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
       generic one */
-  EqualityQuery* getEqualityQuery();
+  EqualityQueryQuantifiersEngine* getEqualityQuery();
   /** get instantiation engine */
   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
   /** get model engine */
@@ -277,7 +277,7 @@ private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
   /** internal representatives */
-  std::map< int, std::map< Node, Node > > d_int_rep;
+  std::map< Node, Node > d_int_rep;
   /** rep score */
   std::map< Node, int > d_rep_score;
   /** reset count */
@@ -289,8 +289,6 @@ private:
   Node getInstance( Node n, std::vector< Node >& eqc );
   /** get score */
   int getRepScore( Node n, Node f, int index );
-  /** choose rep based on sort inference */
-  bool optInternalRepSortInference();
 public:
   EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
   ~EqualityQueryQuantifiersEngine(){}
@@ -308,6 +306,8 @@ public:
       not contain instantiation constants, if such a term exists.
    */
   Node getInternalRepresentative( Node a, Node f, int index );
+  /** flatten representatives */
+  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 
   void setLiberal( bool l ) { d_liberal = l; }
 }; /* EqualityQueryQuantifiersEngine */