Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.

16 files changed, 177 insertions, 145 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1ab4ee62a..55e83ee14 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1426,6 +1426,12 @@ void SmtEngine::setDefaults() {
   }
 
   //cbqi options
+  // enable if pure arithmetic quantifiers
+  if( d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) ){
+    if( !options::cbqi.wasSetByUser() && !options::cbqi2.wasSetByUser() ){
+      options::cbqi2.set( true );
+    }
+  }
   if( options::recurseCbqi() || options::cbqi2() ){
     options::cbqi.set( true );
   }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index d08c92dd9..851f97624 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -820,7 +820,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
     Node progr = d_tds->getNormalized( at, prog );
     Node rep_prog;
     std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr );
-    int tsize = d_tds->getTermSize( prog );
+    int tsize = d_tds->getSygusTermSize( prog );
     if( itnp==d_normalized_to_orig[at].end() ){
       d_normalized_to_orig[at][progr] = prog;
       if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 4fbf298f4..631216507 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -66,11 +66,10 @@ void InstantiationEngine::finishInit(){
 
   //counterexample-based quantifier instantiation
   if( options::cbqi() ){
-    if( !options::cbqi2() || options::cbqi.wasSetByUser() ){
+    if( !options::cbqi2() ){
       d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
       d_instStrategies.push_back( d_i_splx );
-    }
-    if( options::cbqi2() ){
+    }else{
       d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
       d_instStrategies.push_back( d_i_cegqi );
     }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 53f55e70b..e297e138c 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -176,7 +176,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
         }
 
         //if applicable, find exceptions to model via inst-gen
-        if( optInstGen() ){
+        if( options::fmfInstGen() ){
           d_didInstGen = true;
           d_instGenMatches = 0;
           d_numQuantSat = 0;
@@ -201,7 +201,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
               }else{
                 d_numQuantNoSelForm++;
               }
-              if( optOneQuantPerRoundInstGen() && lems>0 ){
+              if( options::fmfInstGenOneQuantPerRound() && lems>0 ){
                 break;
               }
             }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
@@ -341,14 +341,6 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){
   return false;
 }
 
-bool QModelBuilderIG::optInstGen(){
-  return options::fmfInstGen();
-}
-
-bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
-  return options::fmfInstGenOneQuantPerRound();
-}
-
 QModelBuilderIG::Statistics::Statistics():
   d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
   d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index d9ed3f092..8e84f15e2 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -123,10 +123,6 @@ public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilderIG() throw() {}
 public:
-  //whether to add inst-gen lemmas
-  virtual bool optInstGen();
-  //whether to only consider only quantifier per round of inst-gen
-  virtual bool optOneQuantPerRoundInstGen();
   /** statistics class */
   class Statistics {
   public:
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index ce780a29b..2ad8be3a1 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -157,15 +157,19 @@ int ModelEngine::checkModel(){
       if( it->first.isSort() ){
         Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
         if( Trace.isOn("model-engine-debug") ){
-          Trace("model-engine-debug") << "   ";
-          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+          Trace("model-engine-debug") << "        Reps : ";
+          for( size_t i=0; i<it->second.size(); i++ ){
+            Trace("model-engine-debug") << it->second[i] << "  ";
+          }
+          Trace("model-engine-debug") << std::endl;
+          Trace("model-engine-debug") << "   Term reps : ";
           for( size_t i=0; i<it->second.size(); i++ ){
-            //Trace("model-engine-debug") << 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;
-          Trace("model-engine-debug") << "  Model basis term : " << mbt << std::endl;
+          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+          Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
         }
       }
     }
@@ -200,6 +204,7 @@ int ModelEngine::checkModel(){
         for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
           Node f = fm->getAssertedQuantifier( i );
           bool isAx = getTermDatabase()->isQAttrAxiom( f );
+          Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
           //determine if we should check this quantifier
           if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){
             exhaustiveInstantiate( f, e );
@@ -214,7 +219,7 @@ int ModelEngine::checkModel(){
               break;
             }
           }else{
-            Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
+            Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
           }
         }
       }
@@ -240,43 +245,46 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   mb->d_addedLemmas = 0;
   mb->d_incomplete_check = false;
   if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
-    Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
+    Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
     d_triedLemmas += mb->d_triedLemmas;
     d_addedLemmas += mb->d_addedLemmas;
     d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
     d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
   }else{
-    Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
-    Debug("inst-fmf-ei") << "   Instantiation Constants: ";
+    Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+      Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
     }
-    Debug("inst-fmf-ei") << std::endl;
+    Trace("fmf-exh-inst-debug") << std::endl;
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
-      int triedLemmas = 0;
-      int addedLemmas = 0;
-      while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
-        //instantiation was not shown to be true, construct the match
-        InstMatch m( f );
-        for( int i=0; i<riter.getNumTerms(); i++ ){
-          m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
-        }
-        Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
-        triedLemmas++;
-        //add as instantiation
-        if( d_quantEngine->addInstantiation( f, m ) ){
-          addedLemmas++;
-        }else{
-          Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+      Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl;
+      if( !riter.d_incomplete || options::fmfFullSaturate() ){
+        int triedLemmas = 0;
+        int addedLemmas = 0;
+        while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+          //instantiation was not shown to be true, construct the match
+          InstMatch m( f );
+          for( int i=0; i<riter.getNumTerms(); i++ ){
+            m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
+          }
+          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+          triedLemmas++;
+          //add as instantiation
+          if( d_quantEngine->addInstantiation( f, m ) ){
+            addedLemmas++;
+          }else{
+            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+          }
+          riter.increment();
         }
-        riter.increment();
+        d_addedLemmas += addedLemmas;
+        d_triedLemmas += triedLemmas;
+        d_statistics.d_exh_inst_lemmas += addedLemmas;
       }
-      d_addedLemmas += addedLemmas;
-      d_triedLemmas += triedLemmas;
-      d_statistics.d_exh_inst_lemmas += addedLemmas;
+    }else{
+      Assert( 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;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index fe81df7f8..2af66e60a 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -137,8 +137,10 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
+option fmfFullSaturate --fmf-full-saturate bool :default false
+ instantiate with all known ground terms for infinite domain quantifiers when finite model finding
 option fmfInstGen --fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
+ 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.h b/src/theory/quantifiers/quant_util.h
index ca24de5f7..5e0f511e0 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -110,8 +110,6 @@ public:
   virtual eq::EqualityEngine* getEngine() = 0;
   /** get the equivalence class of a */
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-
-  virtual void setLiberal( bool l ) = 0;
 };/* class EqualityQuery */
 
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2671f616b..20d622122 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -409,7 +409,7 @@ bool TermDb::isInstClosure( Node r ) {
   return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
 }
 
-//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated
+//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
 bool TermDb::mayComplete( TypeNode tn ) {
   std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
   if( it==d_may_complete.end() ){
@@ -1756,13 +1756,13 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool d
   }
 }
 
-int TermDbSygus::getTermSize( Node n ){
+int TermDbSygus::getSygusTermSize( Node n ){
   if( isVar( n ) ){
     return 0;
   }else{
     int sum = 0;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      sum += getTermSize( n[i] );
+      sum += getSygusTermSize( n[i] );
     }
     return 1+sum;
   }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index b7fa4e999..1ede29c12 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -465,7 +465,7 @@ public:
   Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true );
-  int getTermSize( Node n );
+  int getSygusTermSize( Node n );
   /** given a term, construct an equivalent smaller one that respects syntax */
   Node minimizeBuiltinTerm( Node n );
   /** given a term, expand it into more basic components */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e654a689d..2d9ba5713 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -99,7 +99,7 @@ d_lemmas_produced_c(u){
   }else{
     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
-  if( !options::finiteModelFind() ){
+  if( options::fullSaturateQuant() ){
     d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
   }else{
     d_rel_dom = NULL;
@@ -783,12 +783,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
     //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
-      Node ti = d_eq_query->getInternalRepresentative( terms[i], f, i );
-      //check if it is a subtype (can be violated in mixed int/real) FIXME : do this check inside getInternalRepresentative
-      if( ti.getType().isSubtypeOf( f[0][i].getType() ) ){
-        terms[i] = ti;
-        Trace("inst-add-debug2") << " (" << terms[i] << ")";
-      }
+      terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
     }
   }
   Trace("inst-add-debug") << std::endl;
@@ -1070,16 +1065,12 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
     return true;
   }else{
     eq::EqualityEngine* ee = getEngine();
-    if( d_liberal ){
-      return true;//!areDisequal( a, b );
-    }else{
-      if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-        if( ee->areEqual( a, b ) ){
-          return true;
-        }
+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+      if( ee->areEqual( a, b ) ){
+        return true;
       }
-      return false;
     }
+    return false;
   }
 }
 
@@ -1094,6 +1085,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
 }
 
 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
+  Assert( f.isNull() || f.getKind()==FORALL );
   Node r = getRepresentative( a );
   if( !options::internalReps() ){
     return r;
@@ -1108,16 +1100,17 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
             r = getRepresentative( r );
           }else{
             if( r.getType().isSort() ){
-              //TODO : this can happen in rare cases
-              // say x:(Array Int U), select( x, 0 ), x assigned (const @u1).
               Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+              //should never happen : UF constants should never escape model
+              Assert( false );
             }
           }
         }
       }
     }
-    std::map< Node, Node >::iterator itir = d_int_rep.find( r );
-    if( itir==d_int_rep.end() ){
+    TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
+    std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
+    if( itir==d_int_rep[v_tn].end() ){
       //find best selection for representative
       Node r_best;
       //if( options::fmfRelevantDomain() && !f.isNull() ){
@@ -1134,8 +1127,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       }
       Trace("internal-rep-select")  << " } " << std::endl;
       int r_best_score = -1;
+      TypeNode v_tn = f[0][index].getType();
       for( size_t i=0; i<eqc.size(); i++ ){
-        int score = getRepScore( eqc[i], f, index );
+        int score = getRepScore( eqc[i], f, index, v_tn );
         if( score!=-2 ){
           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
             r_best = eqc[i];
@@ -1144,12 +1138,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         }
       }
       if( r_best.isNull() ){
-        if( !f.isNull() ){
-          Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
-          r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-        }else{
-          r_best = a;
-        }
+		Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
+        r_best = r;
       }
       //now, make sure that no other member of the class is an instance
       std::hash_map<TNode, Node, TNodeHashFunction> cache;
@@ -1159,7 +1149,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         d_rep_score[ r_best ] = d_reset_count;
       }
       Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
-      d_int_rep[r] = r_best;
+      d_int_rep[v_tn][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;
@@ -1181,8 +1171,10 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode,
     }
   }
   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;
+  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+    }
   }
   //store representatives for newly created terms
   std::map< Node, Node > temp_rep_map;
@@ -1190,51 +1182,55 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode,
   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];
+    for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+      for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.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( itt->second.find( r )==itt->second.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;
+                itt->second[it->first] = ni[j];
+                changed = false;
+                success = true;
+                break;
+              }else{
+                Node ir = itt->second[r];
+                cc.push_back( ir );
+                if( ni[j]!=ir ){
+                  changed = true;
+                }
+              }
+            }else{
               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;
+          if( changed ){
+            Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
+            Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
+            success = true;
+            itt->second[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;
+  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+    }
   }
 }
 
@@ -1277,6 +1273,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod
   }
 }
 
+/*
 int getDepth( Node n ){
   if( n.getNumChildren()==0 ){
     return 0;
@@ -1291,10 +1288,13 @@ int getDepth( Node n ){
     return maxDepth;
   }
 }
+*/
 
-//smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
-  if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){
+//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
+int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
+  if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){  //reject
+    return -2;
+  }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
     return -2;
   }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
     return -1;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d5887f907..c9f14b2c4 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -337,20 +337,18 @@ private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
   /** internal representatives */
-  std::map< Node, Node > d_int_rep;
+  std::map< TypeNode, std::map< Node, Node > > d_int_rep;
   /** rep score */
   std::map< Node, int > d_rep_score;
   /** reset count */
   int d_reset_count;
-
-  bool d_liberal;
 private:
   /** node contains */
   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
-  int getRepScore( Node n, Node f, int index );
+  int getRepScore( Node n, Node f, int index, TypeNode v_tn );
 public:
-  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
+  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
   ~EqualityQueryQuantifiersEngine(){}
   /** reset */
   void reset();
@@ -368,8 +366,6 @@ public:
   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 */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index eb05564e5..6a64f762e 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -16,6 +16,7 @@
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace std;
 using namespace CVC4;
@@ -187,8 +188,14 @@ bool RepSetIterator::initialize(){
     TypeNode tn = d_types[i];
     Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl;
     if( tn.isSort() ){
+      //must ensure uninterpreted type is non-empty.
       if( !d_rep_set->hasType( tn ) ){
-        Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
+        //FIXME:
+        // terms in rep_set are now constants which mapped to terms through TheoryModel
+        // thus, should introduce a constant and a term.  for now, just a term.
+        
+        //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
+        Node var = d_qe->getModel()->getSomeDomainElement( tn );
         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
         d_rep_set->add( tn, var );
       }
@@ -216,15 +223,18 @@ bool RepSetIterator::initialize(){
           d_incomplete = true;
         }
       }
-    //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now
+    //enumerate if the sort is reasonably small
     }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
       Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
       d_rep_set->complete( tn );
+      //must have succeeded
+      Assert( d_rep_set->hasType( tn ) );
     }else{
       Trace("rsi") << "  variable cannot be bounded." << std::endl;
       Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
       d_incomplete = true;
     }
+    //if we have yet to determine the type of enumeration
     if( d_enum_type.size()<=i ){
       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
       if( d_rep_set->hasType( tn ) ){
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 52b018234..05d0c896a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -478,6 +478,14 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac
   cache.insert(n);
 }
 
+void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) {
+  constantReps[eqc] = const_rep;
+  Trace("model-builder") << "    Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
+  if( !fullModel ){
+    tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
+  }
+}
+
 
 void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 {
@@ -551,7 +559,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     if (!const_rep.isNull()) {
       // Theories should not specify a rep if there is already a constant in the EC
       Assert(rep.isNull() || rep == const_rep);
-      constantReps[eqc] = const_rep;
+      assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
       typeConstSet.add(eqct.getBaseType(), const_rep);
     }
     else if (!rep.isNull()) {
@@ -615,7 +623,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                 Node normalized = normalize(tm, n, constantReps, true);
                 if (normalized.isConst()) {
                   typeConstSet.add(tb, normalized);
-                  constantReps[*i2] = normalized;
+                  assignConstantRep( tm, constantReps, *i2, normalized, fullModel );
                   Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                   changed = true;
                   evaluated = true;
@@ -648,7 +656,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             if (normalized.isConst()) {
               changed = true;
               typeConstSet.add(tb, normalized);
-              constantReps[*i] = normalized;
+              assignConstantRep( tm, constantReps, *i, normalized, fullModel );
               assertedReps.erase(*i);
               i2 = i;
               ++i;
@@ -727,11 +735,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             n = *te;
           }
           Assert(!n.isNull());
-          constantReps[*i2] = n;
-          Trace("model-builder") << "    Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
-          if( !fullModel ){
-            tm->d_rep_set.d_values_to_terms[n] = (*i2);
-          }
+          assignConstantRep( tm, constantReps, *i2, n, fullModel );
           changed = true;
           noRepSet.erase(i2);
           if (assignOne) {
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index be202fb69..a161f02f4 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -261,7 +261,7 @@ protected:
   Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
   bool isAssignable(TNode n);
   void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-
+  void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
 public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder(){}
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 9aef059bd..c88d9adff 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -296,7 +296,7 @@ void SortInference::setEqual( int t1, int t2 ){
           d_type_types[rt2] = it1->second;
           d_type_types.erase( rt1 );
         }else{
-          //may happen for mixed int/real
+          Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl;
           return;
         }
       }
@@ -361,14 +361,25 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
 
   int retType;
   if( n.getKind()==kind::EQUAL ){
-    //we only require that the left and right hand side must be equal
-    setEqual( child_types[0], child_types[1] );
+    Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl;
+    //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
+    if( n[0].getType()!=n[1].getType() ){
+      //for now, assume the original types
+      for( unsigned i=0; i<2; i++ ){
+        int ct = getIdForType( n[i].getType() );
+        setEqual( child_types[i], ct );
+      }
+    }else{
+      //we only require that the left and right hand side must be equal
+      setEqual( child_types[0], child_types[1] );
+    }
     //int eqType = getIdForType( n[0].getType() );
     //setEqual( child_types[0], eqType );
     //setEqual( child_types[1], eqType );
     retType = getIdForType( n.getType() );
   }else if( n.getKind()==kind::APPLY_UF ){
     Node op = n.getOperator();
+    TypeNode tn_op = op.getType();
     if( d_op_return_types.find( op )==d_op_return_types.end() ){
       if( n.getType().isBoolean() ){
         //use booleans
@@ -387,7 +398,17 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
     }
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       //the argument of the operator must match the return type of the subterm
-      setEqual( child_types[i], d_op_arg_types[op][i] );
+      if( n[i].getType()!=tn_op[i] ){
+        //if type mismatch, assume original types
+        Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType();
+        Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl;
+        int ct1 = getIdForType( n[i].getType() );
+        setEqual( child_types[i], ct1 );
+        int ct2 = getIdForType( tn_op[i] );
+        setEqual( d_op_arg_types[op][i], ct2 );
+      }else{
+        setEqual( child_types[i], d_op_arg_types[op][i] );
+      }
     }
     //return type is the return type
     retType = d_op_return_types[op];