From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Nov 2012 16:46:51 +0000 (+0000)
Subject: minor bug fixes for quantifiers, added sort inference module (not ready to be used... 
X-Git-Tag: cvc5-1.0.0~7618
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ba075e240b2083163ab35a3580547cae6927b6c;p=cvc5.git

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

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