minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver

14 files changed, 617 insertions, 128 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a66134e0d..bf222d189 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -295,8 +295,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
           iend = n.end();
         i != iend; ) {
       out << '(';
-      (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-                    types, language::output::LANG_SMTLIB_V2);
+      toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types);
       out << ' ';
       out << (*i).getType();
       // The following code do stange things
diff --git a/src/smt/options b/src/smt/options
index ab903c951..a3038cd4e 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -46,6 +46,9 @@ option unconstrainedSimp --unconstrained-simp bool :default false :read-write
 option repeatSimp --repeat-simp bool :read-write
  make multiple passes with nonclausal simplifier
 
+option sortInference --sort-inference bool :default false
+ apply sort inference to input problem
+
 common-option incrementalSolving incremental -i --incremental bool
  enable incremental solving
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ee0d9debc..e0d7c8e98 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -63,6 +63,7 @@
 #include "printer/printer.h"
 #include "prop/options.h"
 #include "theory/arrays/options.h"
+#include "util/sort_inference.h"
 
 using namespace std;
 using namespace CVC4;
@@ -898,7 +899,7 @@ void SmtEngine::setLogicInternal() throw() {
     if (options::checkModels()) {
       Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
       setOption("check-models", SExpr("false"));
-    }    
+    }
   }
 }
 
@@ -1298,6 +1299,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
         }else{
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
           Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
+          //DOTHIS: set attribute on op, marking that it should not be selected as trigger
           std::vector< Node > funcArgs;
           funcArgs.push_back( op );
           funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
@@ -1965,6 +1967,13 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
 
+  if( options::sortInference() ){
+    //sort inference technique
+    //TODO: use this as a rewrite technique here?
+    SortInference si;
+    si.simplify( d_assertionsToPreprocess );
+  }
+
   dumpAssertions("pre-simplify", d_assertionsToPreprocess);
   Chat() << "simplifying assertions..." << endl;
   bool noConflict = simplifyAssertions();
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index acd733e22..a70fd9d7e 100755
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -122,7 +122,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
     d_cg = new CandidateGeneratorQueue;

     if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){

       Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

-      Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

+      //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

       d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;

     }else{

       Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index defb58bf2..456914818 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -157,7 +157,7 @@ int ModelEngine::checkModel( int checkOption ){
   int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
   //for debugging
-  if( Trace.isOn("model-engine") ){
+  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();
          it != fm->d_rep_set.d_type_reps.end(); ++it ){
       if( it->first.isSort() ){
@@ -180,7 +180,7 @@ int ModelEngine::checkModel( int checkOption ){
   d_testLemmas = 0;
   d_relevantLemmas = 0;
   d_totalLemmas = 0;
-  Debug("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
+  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
@@ -235,88 +235,89 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
 
   //create a rep set iterator and iterate over the (relevant) domain of the quantifier
   RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
-  riter.setQuantifier( f );
-  //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;
-  //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] );
-  }
-  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;
-      }
+  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] );
     }
-    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 ) );
+    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;
+        }
       }
-      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->getTermDatabase()->getInstantiationConstant( 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;
+    Debug("inst-fmf-ei") << "Finished: " << std::endl;
+    //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
+    Debug("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;
-  Debug("inst-fmf-ei") << "Finished: " << std::endl;
-  //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-  Debug("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;
   return addedLemmas;
 }
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 5802a05cd..2c36520e4 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -91,4 +91,5 @@ option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :defau
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
 
+
 endmodule
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 553189d13..ae08fe863 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -459,13 +459,15 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
     return true;
   }else if( n.getKind()==MULT ){
     if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){
-      Assert( !n[1].hasAttribute(InstConstantAttribute()) );
-      coeffs[ n[0] ] = n[1];
-      return true;
+      if( !n[1].hasAttribute(InstConstantAttribute()) ){
+        coeffs[ n[0] ] = n[1];
+        return true;
+      }
     }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){
-      Assert( !n[0].hasAttribute(InstConstantAttribute()) );
-      coeffs[ n[1] ] = n[0];
-      return true;
+      if( !n[0].hasAttribute(InstConstantAttribute()) ){
+        coeffs[ n[1] ] = n[0];
+        return true;
+      }
     }
   }
   return false;
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 2770a4e77..b50878e70 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -99,25 +99,25 @@ RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){
 

 }

 

-void RepSetIterator::setQuantifier( Node f ){

+bool RepSetIterator::setQuantifier( Node f ){

   Assert( d_types.empty() );

   //store indicies

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

     d_types.push_back( f[0][i].getType() );

   }

-  initialize();

+  return initialize();

 }

 

-void RepSetIterator::setFunctionDomain( Node op ){

+bool RepSetIterator::setFunctionDomain( Node op ){

   Assert( d_types.empty() );

   TypeNode tn = op.getType();

   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){

     d_types.push_back( tn[i] );

   }

-  initialize();

+  return initialize();

 }

 

-void RepSetIterator::initialize(){

+bool RepSetIterator::initialize(){

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

     d_index.push_back( 0 );

     //store default index order

@@ -146,7 +146,7 @@ void RepSetIterator::initialize(){
         d_incomplete = true;

       }

     }else{

-      Trace("fmf-incomplete") << "Incomplete because of type " << tn << std::endl;

+      Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;

       d_incomplete = true;

     }

     if( d_rep_set->hasType( tn ) ){

@@ -154,11 +154,10 @@ void RepSetIterator::initialize(){
         d_domain[i].push_back( j );

       }

     }else{

-      Trace("fmf-incomplete") << "Incomplete, unknown type " << tn << std::endl;

-      d_incomplete = true;

-      Unimplemented("Cannot create representative set iterator for unknown type quantifier");

+      return false;

     }

   }

+  return true;

 }

 

 void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 8e7da4ce5..61b2ebf9f 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -54,14 +54,14 @@ typedef std::vector< int > RepDomain;
 class RepSetIterator {

 private:

   //initialize function

-  void initialize();

+  bool initialize();

 public:

   RepSetIterator( RepSet* rs );

   ~RepSetIterator(){}

   //set that this iterator will be iterating over instantiations for a quantifier

-  void setQuantifier( Node f );

+  bool setQuantifier( Node f );

   //set that this iterator will be iterating over the domain of a function

-  void setFunctionDomain( Node op );

+  bool setFunctionDomain( Node op );

 public:

   //pointer to model

   RepSet* d_rep_set;

diff --git a/src/theory/uf/options b/src/theory/uf/options
index 0799ba4d5..2569ccbff 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -15,15 +15,15 @@ option ufssEagerSplits --uf-ss-eager-split bool :default false
 option ufssColoringSat --uf-ss-coloring-sat bool :default false
  use coloring-based SAT heuristic for uf strong solver
 option ufssTotality --uf-ss-totality bool :default false
- use totality axioms for enforcing cardinality constraints
+ always use totality axioms for enforcing cardinality constraints
+option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
+ apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
 option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
  apply totality axioms lazily
 option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
  tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
 option ufssSmartSplits --uf-ss-smart-split bool :default false
  use smart splitting heuristic for uf strong solver
-option ufssModelInference --uf-ss-model-infer bool :default false
- use model inference method for uf strong solver
 option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
  add explained clique lemmas for uf strong solver
 
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 548d6f2f0..edeb6b6ec 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -561,19 +561,8 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan
       }
       return;
     }else{
-      if( applyTotality( d_cardinality ) ){
-        //if we are applying totality to this cardinality
-        if( options::ufssTotalityLazy() ){
-          //add totality axioms for all nodes that have not yet been equated to cardinality terms
-          if( level==Theory::EFFORT_FULL ){
-            for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
-              if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
-                addTotalityAxiom( (*it).first, d_cardinality, &d_th->getOutputChannel() );
-              }
-            }
-          }
-        }
-      }else{
+      //first check if we can generate a clique conflict
+      if( !options::ufssTotality() ){
         //do a check within each region
         for( int i=0; i<(int)d_regions_index; i++ ){
           if( d_regions[i]->d_valid ){
@@ -587,8 +576,21 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan
             }
           }
         }
-        bool addedLemma = false;
+      }
+      if( applyTotality( d_cardinality ) ){
+        //add totality axioms for all nodes that have not yet been equated to cardinality terms
+        if( options::ufssTotalityLazy() ){    //this should always be true
+          if( level==Theory::EFFORT_FULL ){
+            for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
+              if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
+                addTotalityAxiom( (*it).first, d_cardinality, &d_th->getOutputChannel() );
+              }
+            }
+          }
+        }
+      }else{
         //do splitting on demand
+        bool addedLemma = false;
         if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
           Trace("uf-ss-debug") << "Add splits?" << std::endl;
           //see if we have any recommended splits from large regions
@@ -768,6 +770,7 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out,
         }
       }
     }else{
+      /*
       if( options::ufssModelInference() ){
         //check if we are at decision level 0
         if( d_th->d_valuation.getAssertionLevel()==0 ){
@@ -781,6 +784,7 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out,
           }
         }
       }
+      */
       //see if we need to request a new cardinality
       if( !d_hasCard ){
         bool needsCard = true;
@@ -915,15 +919,15 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out
     Message() << "Maximum cardinality reached." << std::endl;
     exit( 0 );
   }else{
-    if( options::ufssTotality() ){
+    if( applyTotality( d_aloc_cardinality ) ){
       //must generate new cardinality lemma term
-      std::stringstream ss;
-      ss << "_c_" << d_aloc_cardinality;
       Node var;
-      if( d_totality_terms[0].empty() ){
+      if( d_aloc_cardinality==1 ){
         //get arbitrary ground term
         var = d_cardinality_term;
       }else{
+        std::stringstream ss;
+        ss << "_c_" << d_aloc_cardinality;
         var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
       }
       d_totality_terms[0].push_back( var );
@@ -1026,7 +1030,8 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
     out->lemma( lem );
     return;
   }
-  if( options::ufssModelInference() || Trace.isOn("uf-ss-cliques") ){
+  //if( options::ufssModelInference() ||
+  if( Trace.isOn("uf-ss-cliques") ){
     std::vector< Node > clique_vec;
     clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
     d_cliques[ d_cardinality ].push_back( clique_vec );
@@ -1141,16 +1146,16 @@ void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinali
 
 /** apply totality */
 bool StrongSolverTheoryUf::SortRepModel::applyTotality( int cardinality ){
-  return options::ufssTotality() || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
+  return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
+  // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
 }
 
 /** get totality lemma terms */
 Node StrongSolverTheoryUf::SortRepModel::getTotalityLemmaTerm( int cardinality, int i ){
-  if( options::ufssTotality() ){
-    return d_totality_terms[0][i];
-  }else{
-    return d_totality_terms[cardinality][i];
-  }
+  return d_totality_terms[0][i];
+  //}else{
+  //  return d_totality_terms[cardinality][i];
+  //}
 }
 
 void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){
@@ -1467,12 +1472,13 @@ Node StrongSolverTheoryUf::getNextDecisionRequest(){
 }
 
 void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
+  Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
   //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
   TypeNode tn = n.getType();
   if( d_rep_model.find( tn )==d_rep_model.end() ){
     RepModel* rm = NULL;
     if( tn.isSort() ){
-      Debug("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
+      Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
       rm  = new SortRepModel( n, d_th->getSatContext(), d_th );
     }else if( tn.isInteger() ){
       //rm = new InfRepModel( tn, d_th->getSatContext(), d_th );
@@ -1497,6 +1503,8 @@ void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
       d_rep_model[tn] = rm;
       d_rep_model_init[tn] = true;
     }
+  }else{
+    Trace("uf-ss-register") << "Already preregistered sort " << tn << "." << std::endl;
   }
 }
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 098024912..aa122905b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -84,7 +84,9 @@ libutil_la_SOURCES = \
 	array_store_all.h \
 	array_store_all.cpp \
 	util_model.h \
-	util_model.cpp
+	util_model.cpp \
+	sort_inference.h \
+	sort_inference.cpp
 
 libutil_la_LIBADD = \
 	@builddir@/libutilcudd.la
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
new file mode 100755
index 000000000..5dc60dbb0
--- /dev/null
+++ b/src/util/sort_inference.cpp
@@ -0,0 +1,393 @@
+/*********************                                                        */

+/*! \file sort_inference.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Sort inference module

+ **

+ ** This class implements sort inference, based on a simple algorithm:

+ ** First, we assume all functions and predicates have distinct uninterpreted types.

+ ** One pass is made through the input assertions, while a union-find data structure

+ ** maintains necessary information regarding constraints on these types.

+ **/

+

+#include <vector>

+

+#include "util/sort_inference.h"

+

+using namespace CVC4;

+using namespace std;

+

+namespace CVC4 {

+

+

+void SortInference::printSort( const char* c, int t ){

+  int rt = getRepresentative( t );

+  if( d_type_types.find( rt )!=d_type_types.end() ){

+    Trace(c) << d_type_types[rt];

+  }else{

+    Trace(c) << "s_" << rt;

+  }

+}

+

+void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){

+  //process all assertions

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

+    Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;

+    std::map< Node, Node > var_bound;

+    process( assertions[i], var_bound );

+  }

+  //print debug

+  if( Trace.isOn("sort-inference") ){

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

+      Trace("sort-inference") << it->first << " : ";

+      if( !d_op_arg_types[ it->first ].empty() ){

+        Trace("sort-inference") << "( ";

+        for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){

+          printSort( "sort-inference", d_op_arg_types[ it->first ][i] );

+          Trace("sort-inference") << " ";

+        }

+        Trace("sort-inference") << ") -> ";

+      }

+      printSort( "sort-inference", it->second );

+      Trace("sort-inference") << std::endl;

+    }

+  }

+  if( doRewrite ){

+    //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)

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

+      std::map< Node, Node > var_bound;

+      assertions[i] = simplify( assertions[i], var_bound );

+      Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;

+    }

+    //now, ensure constants are distinct

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

+      std::vector< Node > consts;

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

+        consts.push_back( it2->second );

+      }

+      //add lemma enforcing introduced constants to be distinct?

+    }

+  }

+}

+

+int SortInference::getRepresentative( int t ){

+  std::map< int, int >::iterator it = d_type_union_find.find( t );

+  if( it!=d_type_union_find.end() ){

+    if( it->second==t ){

+      return t;

+    }else{

+      int rt = getRepresentative( it->second );

+      d_type_union_find[t] = rt;

+      return rt;

+    }

+  }else{

+    return t;

+  }

+}

+

+void SortInference::setEqual( int t1, int t2 ){

+  if( t1!=t2 ){

+    int rt1 = getRepresentative( t1 );

+    int rt2 = getRepresentative( t2 );

+    if( rt1!=rt2 ){

+      Trace("sort-inference-debug") << "Set equal : ";

+      printSort( "sort-inference-debug", rt1 );

+      Trace("sort-inference-debug") << " ";

+      printSort( "sort-inference-debug", rt2 );

+      Trace("sort-inference-debug") << std::endl;

+      //check if they must be a type

+      std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );

+      std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 );

+      if( it2!=d_type_types.end() ){

+        if( it1==d_type_types.end() ){

+          //swap sides

+          int swap = rt1;

+          rt1 = rt2;

+          rt2 = swap;

+        }else{

+          Assert( rt1==rt2 );

+        }

+      }

+      /*

+      d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );

+      d_type_eq_class[rt2].clear();

+      Trace("sort-inference-debug") << "EqClass : { ";

+      for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){

+        Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";

+      }

+      Trace("sort-inference-debug") << "}" << std::endl;

+      */

+      d_type_union_find[rt2] = rt1;

+    }

+  }

+}

+

+int SortInference::getIdForType( TypeNode tn ){

+  //register the return type

+  std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn );

+  if( it==d_id_for_types.end() ){

+    int sc = sortCount;

+    d_type_types[ sortCount ] = tn;

+    d_id_for_types[ tn ] = sortCount;

+    sortCount++;

+    return sc;

+  }else{

+    return it->second;

+  }

+}

+

+int SortInference::process( Node n, std::map< Node, Node >& var_bound ){

+  Trace("sort-inference-debug") << "Process " << n << std::endl;

+  //add to variable bindings

+  if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){

+    for( size_t i=0; i<n[0].getNumChildren(); i++ ){

+      //TODO: try applying sort inference to quantified variables

+      //d_var_types[n][ n[0][i] ] = sortCount;

+      //sortCount++;

+

+      //type of the quantified variable must be the same

+      d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );

+      var_bound[ n[0][i] ] = n;

+    }

+  }

+

+  //process children

+  std::vector< Node > children;

+  std::vector< int > child_types;

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

+    bool processChild = true;

+    if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){

+      processChild = i==1;

+    }

+    if( processChild ){

+      children.push_back( n[i] );

+      child_types.push_back( process( n[i], var_bound ) );

+    }

+  }

+

+  //remove from variable bindings

+  if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){

+    //erase from variable bound

+    for( size_t i=0; i<n[0].getNumChildren(); i++ ){

+      var_bound.erase( n[0][i] );

+    }

+  }

+

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

+    retType = getIdForType( n.getType() );

+  }else if( n.getKind()==kind::APPLY_UF ){

+    Node op = n.getOperator();

+    if( d_op_return_types.find( op )==d_op_return_types.end() ){

+      //assign arbitrary sort for return type

+      d_op_return_types[op] = sortCount;

+      sortCount++;

+      //d_type_eq_class[sortCount].push_back( op );

+      //assign arbitrary sort for argument types

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

+        d_op_arg_types[op].push_back( sortCount );

+        sortCount++;

+      }

+    }

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

+    }

+    //return type is the return type

+    retType = d_op_return_types[op];

+  }else{

+    std::map< Node, Node >::iterator it = var_bound.find( n );

+    if( it!=var_bound.end() ){

+      Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;

+      //the return type was specified while binding

+      retType = d_var_types[it->second][n];

+    }else if( n.getKind() == kind::VARIABLE ){

+      Trace("sort-inference-debug") << n << " is a variable." << std::endl;

+      if( d_op_return_types.find( n )==d_op_return_types.end() ){

+        //assign arbitrary sort

+        d_op_return_types[n] = sortCount;

+        sortCount++;

+        //d_type_eq_class[sortCount].push_back( n );

+      }

+      retType = d_op_return_types[n];

+    }else if( n.isConst() ){

+      Trace("sort-inference-debug") << n << " is a constant." << std::endl;

+      //can be any type we want

+      retType = sortCount;

+      sortCount++;

+    }else{

+      Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;

+      //it is an interpretted term

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

+        Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl;

+        //must enforce the actual type of the operator on the children

+        int ct = getIdForType( children[i].getType() );

+        setEqual( child_types[i], ct );

+      }

+      //return type must be the actual return type

+      retType = getIdForType( n.getType() );

+    }

+  }

+  Trace("sort-inference-debug") << "Type( " << n << " ) = ";

+  printSort("sort-inference-debug", retType );

+  Trace("sort-inference-debug") << std::endl;

+  return retType;

+}

+

+

+TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){

+  int rt = getRepresentative( t );

+  if( d_type_types.find( rt )!=d_type_types.end() ){

+    return d_type_types[rt];

+  }else{

+    TypeNode retType;

+    //see if we can assign pref

+    if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){

+      retType = pref;

+    }else{

+      if( d_subtype_count.find( pref )==d_subtype_count.end() ){

+        d_subtype_count[pref] = 0;

+      }

+      //must create new type

+      std::stringstream ss;

+      ss << "it_" << d_subtype_count[pref] << "_" << pref;

+      d_subtype_count[pref]++;

+      retType = NodeManager::currentNM()->mkSort( ss.str() );

+    }

+    d_id_for_types[ retType ] = rt;

+    d_type_types[ rt ] = retType;

+    return retType;

+  }

+}

+

+TypeNode SortInference::getTypeForId( int t ){

+  int rt = getRepresentative( t );

+  if( d_type_types.find( rt )!=d_type_types.end() ){

+    return d_type_types[rt];

+  }else{

+    return TypeNode::null();

+  }

+}

+

+Node SortInference::getNewSymbol( Node old, TypeNode tn ){

+  if( tn==old.getType() ){

+    return old;

+  }else{

+    std::stringstream ss;

+    ss << "i_$$_" << old;

+    return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );

+  }

+}

+

+Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){

+  std::vector< Node > children;

+  if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){

+    //recreate based on types of variables

+    std::vector< Node > new_children;

+    for( size_t i=0; i<n[0].getNumChildren(); i++ ){

+      TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );

+      Node v = getNewSymbol( n[0][i], tn );

+      new_children.push_back( v );

+      var_bound[ n[0][i] ] = v;

+    }

+    children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );

+  }

+

+  //process children

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

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

+  }

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

+    bool processChild = true;

+    if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){

+      processChild = i>=1;

+    }

+    if( processChild ){

+      children.push_back( simplify( n[i], var_bound ) );

+    }

+  }

+

+  //remove from variable bindings

+  if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){

+    //erase from variable bound

+    for( size_t i=0; i<n[0].getNumChildren(); i++ ){

+      var_bound.erase( n[0][i] );

+    }

+    return NodeManager::currentNM()->mkNode( n.getKind(), children );

+  }else if( n.getKind()==kind::APPLY_UF ){

+    Node op = n.getOperator();

+    if( d_symbol_map.find( op )==d_symbol_map.end() ){

+      //make the new operator if necessary

+      bool opChanged = false;

+      std::vector< TypeNode > argTypes;

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

+        TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );

+        argTypes.push_back( tn );

+        if( tn!=n[i].getType() ){

+          opChanged = true;

+        }

+      }

+      TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() );

+      if( retType!=n.getType() ){

+        opChanged = true;

+      }

+      if( opChanged ){

+        std::stringstream ss;

+        ss << "io_$$_" << op;

+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );

+        d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );

+      }else{

+        d_symbol_map[op] = op;

+      }

+    }

+    children[0] = d_symbol_map[op];

+    //make sure all children have been taken care of

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

+      TypeNode tn = children[i+1].getType();

+      TypeNode tna = getTypeForId( d_op_arg_types[op][i] );

+      if( tn!=tna ){

+        if( n[i].isConst() ){

+          //must make constant of type tna

+          if( d_const_map[tna].find( n[i] )==d_const_map[tna].end() ){

+            std::stringstream ss;

+            ss << "ic_" << tna << "_" << n[i];

+            d_const_map[tna][ n[i] ] = NodeManager::currentNM()->mkSkolem( ss.str(), tna, "constant created during sort inference" );  //use mkConst???

+          }

+          children[i+1] = d_const_map[tna][ n[i] ];

+        }else{

+          Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;

+          Assert( false );

+        }

+      }

+    }

+    return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );

+  }else{

+    std::map< Node, Node >::iterator it = var_bound.find( n );

+    if( it!=var_bound.end() ){

+      return it->second;

+    }else if( n.getKind() == kind::VARIABLE ){

+      if( d_symbol_map.find( n )==d_symbol_map.end() ){

+        TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );

+        d_symbol_map[n] = getNewSymbol( n, tn );

+      }

+      return d_symbol_map[n];

+    }else if( n.isConst() ){

+      //just return n, we will fix at higher scope

+      return n;

+    }else{

+      return NodeManager::currentNM()->mkNode( n.getKind(), children );

+    }

+  }

+

+}

+

+}

diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
new file mode 100755
index 000000000..363dbd84d
--- /dev/null
+++ b/src/util/sort_inference.h
@@ -0,0 +1,72 @@
+/*********************                                                        */

+/*! \file sort_inference.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Pre-process step for performing sort inference

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__SORT_INFERENCE_H

+#define __CVC4__SORT_INFERENCE_H

+

+#include <iostream>

+#include <string>

+#include <vector>

+#include <map>

+#include "expr/node.h"

+#include "expr/type_node.h"

+

+namespace CVC4 {

+

+class SortInference{

+private:

+  //for debugging

+  //std::map< int, std::vector< Node > > d_type_eq_class;

+private:

+  int sortCount;

+  std::map< int, int > d_type_union_find;

+  std::map< int, TypeNode > d_type_types;

+  std::map< TypeNode, int > d_id_for_types;

+  //for apply uf operators

+  std::map< Node, int > d_op_return_types;

+  std::map< Node, std::vector< int > > d_op_arg_types;

+  //for bound variables

+  std::map< Node, std::map< Node, int > > d_var_types;

+  //get representative

+  int getRepresentative( int t );

+  void setEqual( int t1, int t2 );

+  int getIdForType( TypeNode tn );

+  void printSort( const char* c, int t );

+  //process

+  int process( Node n, std::map< Node, Node >& var_bound );

+private:

+  //mapping from old symbols to new symbols

+  std::map< Node, Node > d_symbol_map;

+  //mapping from constants to new symbols

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

+  //number of subtypes generated

+  std::map< TypeNode, int > d_subtype_count;

+  //helper functions for simplify

+  TypeNode getOrCreateTypeForId( int t, TypeNode pref );

+  TypeNode getTypeForId( int t );

+  Node getNewSymbol( Node old, TypeNode tn );

+  //simplify

+  Node simplify( Node n, std::map< Node, Node >& var_bound );

+public:

+  SortInference() : sortCount( 0 ){}

+  ~SortInference(){}

+

+  void simplify( std::vector< Node >& assertions, bool doRewrite = false );

+};

+

+}

+

+#endif