From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Nov 2012 21:16:26 +0000 (+0000)
Subject: refactoring of quantifiers rewriter based on code review from yesterday, refactoring... 
X-Git-Tag: cvc5-1.0.0~7606
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=795e5ba8a1138a371409ac9c8e9da78ce652bb94;p=cvc5.git

refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine
---

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 9c2ca7d45..2591143cb 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -52,7 +52,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class InstantiatorTheoryArith;
+class InstStrategySimplex;
 
 /**
  * Implementation of QF_LRA.
@@ -60,7 +60,7 @@ class InstantiatorTheoryArith;
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
-  friend class InstantiatorTheoryArith;
+  friend class InstStrategySimplex;
 private:
   bool d_nlIncomplete;
   // TODO A better would be:
@@ -304,7 +304,7 @@ private:
   /** Internal model value for the node */
   DeltaRational getDeltaValue(TNode n);
 
-  /** TODO : get rid of this. */ 
+  /** TODO : get rid of this. */
   DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed);
 
   /** Uninterpretted function symbol for use when interpreting
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index b6c85b7eb..6a783fc41 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -32,7 +32,49 @@ InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, Quantifie
   d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
 }
 
+TheoryArith* InstStrategySimplex::getTheoryArith(){
+  return (TheoryArith*)d_th->getTheory();
+}
+
 void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
+  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
+  d_instRows.clear();
+  d_tableaux_term.clear();
+  d_tableaux.clear();
+  d_ceTableaux.clear();
+  //search for instantiation rows in simplex tableaux
+  ArithVarToNodeMap avtnm = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap();
+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+    ArithVar x = (*it).first;
+    if( getTheoryArith()->d_partialModel.hasEitherBound( x ) ){
+      Node n = (*it).second;
+      Node f;
+      NodeBuilder<> t(kind::PLUS);
+      if( n.getKind()==PLUS ){
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          addTermToRow( x, n[i], f, t );
+        }
+      }else{
+        addTermToRow( x, n, f, t );
+      }
+      if( f!=Node::null() ){
+        d_instRows[f].push_back( x );
+        //this theory has constraints from f
+        Debug("quant-arith") << "Has constraints from " << f << std::endl;
+        d_th->setQuantifierActive( f );
+        //set tableaux term
+        if( t.getNumChildren()==0 ){
+          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
+        }else if( t.getNumChildren()==1 ){
+          d_tableaux_term[x] = t.getChild( 0 );
+        }else{
+          d_tableaux_term[x] = t;
+        }
+      }
+    }
+  }
+  //print debug
+  debugPrint( "quant-arith-debug" );
   d_counter++;
 }
 
@@ -43,10 +85,10 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
     //Notice() << f << std::endl;
     //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
     //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
-    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_th->d_instRows[f].size() << std::endl;
-    for( int j=0; j<(int)d_th->d_instRows[f].size(); j++ ){
-      ArithVar x = d_th->d_instRows[f][j];
-      if( !d_th->d_ceTableaux[x].empty() ){
+    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
+    for( int j=0; j<(int)d_instRows[f].size(); j++ ){
+      ArithVar x = d_instRows[f][j];
+      if( !d_ceTableaux[x].empty() ){
         Debug("quant-arith-simplex") << "Check row " << x << std::endl;
         //instantiation row will be A*e + B*t = beta,
         // where e is a vector of terms , and t is vector of ground terms.
@@ -54,13 +96,13 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
         // We will construct the term ( beta - B*t)/coeff to use for e_i.
         InstMatch m;
         //By default, choose the first instantiation constant to be e_i.
-        Node var = d_th->d_ceTableaux[x].begin()->first;
+        Node var = d_ceTableaux[x].begin()->first;
         if( var.getType().isInteger() ){
-          std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin();
+          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
           //try to find coefficent that is +/- 1
-          while( !var.isNull() && !d_th->d_ceTableaux[x][var].isNull() && d_th->d_ceTableaux[x][var]!=d_negOne ){
+          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
             ++it;
-            if( it==d_th->d_ceTableaux[x].end() ){
+            if( it==d_ceTableaux[x].end() ){
               var = Node::null();
             }else{
               var = it->first;
@@ -70,7 +112,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
         }
         if( !var.isNull() ){
           Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-          d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, m, var );
+          doInstantiation( f, d_tableaux_term[x], x, m, var );
         }else{
           Debug("quant-arith-simplex") << "Could not find var." << std::endl;
         }
@@ -91,78 +133,8 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
   return STATUS_UNKNOWN;
 }
 
-InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-  if( options::cbqi() ){
-    addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
-  }
-}
-
-void InstantiatorTheoryArith::preRegisterTerm( Node t ){
-
-}
-
-void InstantiatorTheoryArith::assertNode( Node assertion ){
-  Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
-  d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
-  if( options::cbqi() ){
-    Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
-    d_instRows.clear();
-    d_tableaux_term.clear();
-    d_tableaux.clear();
-    d_ceTableaux.clear();
-    //search for instantiation rows in simplex tableaux
-    ArithVarToNodeMap avtnm = ((TheoryArith*)getTheory())->d_arithvarNodeMap.getArithVarToNodeMap();
-    for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
-      ArithVar x = (*it).first;
-      if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
-        Node n = (*it).second;
-        Node f;
-        NodeBuilder<> t(kind::PLUS);
-        if( n.getKind()==PLUS ){
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            addTermToRow( x, n[i], f, t );
-          }
-        }else{
-          addTermToRow( x, n, f, t );
-        }
-        if( f!=Node::null() ){
-          d_instRows[f].push_back( x );
-          //this theory has constraints from f
-          Debug("quant-arith") << "Has constraints from " << f << std::endl;
-          setQuantifierActive( f );
-          //set tableaux term
-          if( t.getNumChildren()==0 ){
-            d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
-          }else if( t.getNumChildren()==1 ){
-            d_tableaux_term[x] = t.getChild( 0 );
-          }else{
-            d_tableaux_term[x] = t;
-          }
-        }
-      }
-    }
-    //print debug
-    debugPrint( "quant-arith-debug" );
-  }
-}
 
-int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-void InstantiatorTheoryArith::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
+void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
   if( n.getKind()==MULT ){
     if( n[1].hasAttribute(InstConstantAttribute()) ){
       f = n[1].getAttribute(InstConstantAttribute());
@@ -190,23 +162,23 @@ void InstantiatorTheoryArith::addTermToRow( ArithVar x, Node n, Node& f, NodeBui
   }
 }
 
-void InstantiatorTheoryArith::debugPrint( const char* c ){
-  ArithVarToNodeMap avtnm = ((TheoryArith*)getTheory())->d_arithvarNodeMap.getArithVarToNodeMap();
+void InstStrategySimplex::debugPrint( const char* c ){
+  ArithVarToNodeMap avtnm = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap();
   for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
     ArithVar x = (*it).first;
     Node n = (*it).second;
     //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
       Debug(c) << x << " : " << n << ", bounds = ";
-      if( ((TheoryArith*)getTheory())->d_partialModel.hasLowerBound( x ) ){
-        Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getLowerBound( x );
+      if( getTheoryArith()->d_partialModel.hasLowerBound( x ) ){
+        Debug(c) << getTheoryArith()->d_partialModel.getLowerBound( x );
       }else{
         Debug(c) << "-infty";
       }
       Debug(c) << " <= ";
-      Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getAssignment( x );
+      Debug(c) << getTheoryArith()->d_partialModel.getAssignment( x );
       Debug(c) << " <= ";
-      if( ((TheoryArith*)getTheory())->d_partialModel.hasUpperBound( x ) ){
-        Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getUpperBound( x );
+      if( getTheoryArith()->d_partialModel.hasUpperBound( x ) ){
+        Debug(c) << getTheoryArith()->d_partialModel.getUpperBound( x );
       }else{
         Debug(c) << "+infty";
       }
@@ -254,7 +226,7 @@ void InstantiatorTheoryArith::debugPrint( const char* c ){
 // t[e] is a vector of terms containing instantiation constants from f,
 // and term is a ground term (c1*t1 + ... + cn*tn).
 // We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstantiatorTheoryArith::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
+bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
   //first try +delta
   if( doInstantiation2( f, term, x, m, var ) ){
     ++(d_statistics.d_instantiations);
@@ -275,7 +247,7 @@ bool InstantiatorTheoryArith::doInstantiation( Node f, Node term, ArithVar x, In
   }
 }
 
-bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
+bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
   // make term ( beta - term )/coeff
   Node beta = getTableauxValue( x, minus_delta );
   Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
@@ -295,31 +267,71 @@ bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, I
   return d_quantEngine->addInstantiation( f, m );
 }
 
-Node InstantiatorTheoryArith::getTableauxValue( Node n, bool minus_delta ){
-  if( ((TheoryArith*)getTheory())->d_arithvarNodeMap.hasArithVar(n) ){
-    ArithVar v = ((TheoryArith*)getTheory())->d_arithvarNodeMap.asArithVar( n );
+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
+  if( getTheoryArith()->d_arithvarNodeMap.hasArithVar(n) ){
+    ArithVar v = getTheoryArith()->d_arithvarNodeMap.asArithVar( n );
     return getTableauxValue( v, minus_delta );
   }else{
     return NodeManager::currentNM()->mkConst( Rational(0) );
   }
 }
 
-Node InstantiatorTheoryArith::getTableauxValue( ArithVar v, bool minus_delta ){
-  const Rational& delta = ((TheoryArith*)getTheory())->d_partialModel.getDelta();
-  DeltaRational drv = ((TheoryArith*)getTheory())->d_partialModel.getAssignment( v );
+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
+  const Rational& delta = getTheoryArith()->d_partialModel.getDelta();
+  DeltaRational drv = getTheoryArith()->d_partialModel.getAssignment( v );
   Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
   return mkRationalNode(qmodel);
 }
 
-InstantiatorTheoryArith::Statistics::Statistics():
-  d_instantiations("InstantiatorTheoryArith::Instantiations_Total", 0),
-  d_instantiations_minus("InstantiatorTheoryArith::Instantiations_minus_delta", 0)
+
+
+InstStrategySimplex::Statistics::Statistics():
+  d_instantiations("InstStrategySimplex::Instantiations_Total", 0),
+  d_instantiations_minus("InstStrategySimplex::Instantiations_minus_delta", 0)
 {
   StatisticsRegistry::registerStat(&d_instantiations);
   StatisticsRegistry::registerStat(&d_instantiations_minus);
 }
 
-InstantiatorTheoryArith::Statistics::~Statistics(){
+InstStrategySimplex::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations);
   StatisticsRegistry::unregisterStat(&d_instantiations_minus);
 }
+
+
+
+
+
+
+
+InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
+Instantiator( c, ie, th ){
+  if( options::cbqi() ){
+    addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
+  }
+}
+
+void InstantiatorTheoryArith::preRegisterTerm( Node t ){
+
+}
+
+void InstantiatorTheoryArith::assertNode( Node assertion ){
+  Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
+  d_quantEngine->addTermToDatabase( assertion );
+  if( options::cbqi() ){
+    if( assertion.hasAttribute(InstConstantAttribute()) ){
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
+    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
+    }
+  }
+}
+
+void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){
+  Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
+  return InstStrategy::STATUS_UNKNOWN;
+}
diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h
index 7ffe36b41..70bc97bd8 100644
--- a/src/theory/arith/theory_arith_instantiator.h
+++ b/src/theory/arith/theory_arith_instantiator.h
@@ -27,9 +27,33 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class TheoryArith;
 class InstantiatorTheoryArith;
 
 class InstStrategySimplex : public InstStrategy{
+private:
+  /** delta */
+  std::map< TypeNode, Node > d_deltas;
+  /** for each quantifier, simplex rows */
+  std::map< Node, std::vector< ArithVar > > d_instRows;
+  /** tableaux */
+  std::map< ArithVar, Node > d_tableaux_term;
+  std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
+  std::map< ArithVar, std::map< Node, Node > > d_tableaux;
+  /** ce tableaux */
+  std::map< ArithVar, std::map< Node, Node > > d_ceTableaux;
+  /** get value */
+  Node getTableauxValue( Node n, bool minus_delta = false );
+  Node getTableauxValue( ArithVar v, bool minus_delta = false );
+  /** do instantiation */
+  bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var );
+  bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
+  /** add term to row */
+  void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
+  /** get arith theory */
+  TheoryArith* getTheoryArith();
+  /** print debug */
+  void debugPrint( const char* c );
 private:
   /** InstantiatorTheoryUf class */
   InstantiatorTheoryArith* d_th;
@@ -45,29 +69,21 @@ public:
   ~InstStrategySimplex(){}
   /** identify */
   std::string identify() const { return std::string("Simplex"); }
+
+  class Statistics {
+  public:
+    IntStat d_instantiations;
+    IntStat d_instantiations_minus;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
 };
 
 class InstantiatorTheoryArith : public Instantiator{
   friend class QuantifiersEngine;
   friend class InstStrategySimplex;
   friend class InstStrategySimplexUfMatch;
-private:
-  /** delta */
-  std::map< TypeNode, Node > d_deltas;
-  /** for each quantifier, simplex rows */
-  std::map< Node, std::vector< ArithVar > > d_instRows;
-  /** tableaux */
-  std::map< ArithVar, Node > d_tableaux_term;
-  std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
-  std::map< ArithVar, std::map< Node, Node > > d_tableaux;
-  /** ce tableaux */
-  std::map< ArithVar, std::map< Node, Node > > d_ceTableaux;
-  /** get value */
-  Node getTableauxValue( Node n, bool minus_delta = false );
-  Node getTableauxValue( ArithVar v, bool minus_delta = false );
-  /** do instantiation */
-  bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var );
-  bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
 public:
   InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th);
   ~InstantiatorTheoryArith() {}
@@ -78,24 +94,13 @@ public:
   void preRegisterTerm( Node t );
   /** identify */
   std::string identify() const { return std::string("InstantiatorTheoryArith"); }
-  /** print debug */
-  void debugPrint( const char* c );
 private:
   /**  reset instantiation */
   void processResetInstantiationRound( Theory::Effort effort );
   /** process at effort */
   int process( Node f, Theory::Effort effort, int e );
-  /** add term to row */
-  void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
 
-  class Statistics {
-  public:
-    IntStat d_instantiations;
-    IntStat d_instantiations_minus;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
+
 };/* class InstantiatiorTheoryArith  */
 
 }
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp
index e9f255c65..cfc45f4cc 100644
--- a/src/theory/datatypes/theory_datatypes_instantiator.cpp
+++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp
@@ -26,50 +26,34 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
+InstStrategyDatatypesValue::InstStrategyDatatypesValue( QuantifiersEngine* qe ) : InstStrategy( qe ){
 
-InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) :
-Instantiator( c, ie, th ){
-}
-
-void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
-  Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
-  d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
 }
 
-void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort effort ){
+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
 
 }
 
-
-int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){
+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
   Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( options::cbqi() ){
-    if( e<2 ){
-      return InstStrategy::STATUS_UNFINISHED;
-    }else if( e==2 ){
-      InstMatch m;
-      for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-        Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-        if( i.getType().isDatatype() ){
-          Node n = getValueFor( i );
-          Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
-          m.set(i,n);
-        }
+  if( e<2 ){
+    return InstStrategy::STATUS_UNFINISHED;
+  }else if( e==2 ){
+    InstMatch m;
+    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
+      if( i.getType().isDatatype() ){
+        Node n = getValueFor( i );
+        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
+        m.set(i,n);
       }
-      //d_quantEngine->addInstantiation( f, m );
     }
+    //d_quantEngine->addInstantiation( f, m );
   }
   return InstStrategy::STATUS_UNKNOWN;
 }
 
-Node InstantiatorTheoryDatatypes::getValueFor( Node n ){
+Node InstStrategyDatatypesValue::getValueFor( Node n ){
   //simply get the ground value for n in the current model, if it exists,
   //  or return an arbitrary ground term otherwise
   if( !n.hasAttribute(InstConstantAttribute()) ){
@@ -151,16 +135,45 @@ Node InstantiatorTheoryDatatypes::getValueFor( Node n ){
   */
 }
 
-InstantiatorTheoryDatatypes::Statistics::Statistics():
-  d_instantiations("InstantiatorTheoryDatatypes::Instantiations_Total", 0)
+InstStrategyDatatypesValue::Statistics::Statistics():
+  d_instantiations("InstStrategyDatatypesValue::Instantiations_Total", 0)
 {
   StatisticsRegistry::registerStat(&d_instantiations);
 }
 
-InstantiatorTheoryDatatypes::Statistics::~Statistics(){
+InstStrategyDatatypesValue::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations);
 }
 
+
+
+InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) :
+Instantiator( c, ie, th ){
+  if( options::cbqi() ){
+    addInstStrategy( new InstStrategyDatatypesValue( ie ) );
+  }
+}
+
+void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
+  Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
+  d_quantEngine->addTermToDatabase( assertion );
+  if( options::cbqi() ){
+    if( assertion.hasAttribute(InstConstantAttribute()) ){
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
+    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
+    }
+  }
+}
+
+void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){
+  return InstStrategy::STATUS_UNKNOWN;
+}
+
 bool InstantiatorTheoryDatatypes::hasTerm( Node a ){
   return ((TheoryDatatypes*)d_th)->getEqualityEngine()->hasTerm( a );
 }
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h
index a9bb739c8..d7806a21d 100644
--- a/src/theory/datatypes/theory_datatypes_instantiator.h
+++ b/src/theory/datatypes/theory_datatypes_instantiator.h
@@ -28,6 +28,31 @@ namespace datatypes {
 
 class TheoryDatatypes;
 
+class InstStrategyDatatypesValue : public InstStrategy
+{
+private:
+  Node getValueFor( Node n );
+public:
+  //constructor
+  InstStrategyDatatypesValue( QuantifiersEngine* qe );
+  ~InstStrategyDatatypesValue(){}
+  /** reset instantiation */
+  void processResetInstantiationRound( Theory::Effort effort );
+  /** process method, returns a status */
+  int process( Node f, Theory::Effort effort, int e );
+  /** identify */
+  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
+
+  class Statistics {
+  public:
+    IntStat d_instantiations;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+};/* class InstStrategy */
+
+
 class InstantiatorTheoryDatatypes : public Instantiator{
   friend class QuantifiersEngine;
 public:
@@ -43,16 +68,6 @@ private:
   void processResetInstantiationRound( Theory::Effort effort );
   /** process at effort */
   int process( Node f, Theory::Effort effort, int e );
-  /** get value for */
-  Node getValueFor( Node n );
-
-  class Statistics {
-  public:
-    IntStat d_instantiations;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
 public:
   /** general queries about equality */
   bool hasTerm( Node a );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d25e516fe..dabaa2188 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -185,51 +185,55 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+    RewriteStatus status = REWRITE_DONE;
+    Node ret = in;
     //get the arguments
     std::vector< Node > args;
     for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
       args.push_back( in[0][i] );
     }
-    //get the body
-    Node body = in[1];
-    if( in.getKind()==EXISTS ){
-      body = body.getKind()==NOT ? body[0] : body.notNode();
-    }
     //get the instantiation pattern list
     Node ipl;
     if( in.getNumChildren()==3 ){
       ipl = in[2];
     }
-    bool isNested = in.hasAttribute(NestedQuantAttribute());
-    //compute miniscoping first
-    Node n = body;//computeNNF( body ); TODO: compute NNF here (current bad idea since arithmetic rewrites equalities)
-    if( body!=n ){
-      Notice() << "NNF " << body << " -> " << n << std::endl;
-    }
-    n = computeMiniscoping( args, n, ipl, isNested );
-    if( in.getKind()==kind::EXISTS ){
-      n = n.getKind()==NOT ? n[0] : n.notNode();
+    //get the body
+    if( in.getKind()==EXISTS ){
+      std::vector< Node > children;
+      children.push_back( in[0] );
+      children.push_back( in[1].negate() );
+      if( in.getNumChildren()==3 ){
+        children.push_back( in[2] );
+      }
+      ret = NodeManager::currentNM()->mkNode( FORALL, children );
+      ret = ret.negate();
+      status = REWRITE_AGAIN_FULL;
+    }else{
+      bool isNested = in.hasAttribute(NestedQuantAttribute());
+      for( int op=0; op<COMPUTE_LAST; op++ ){
+        if( doOperation( in, isNested, op ) ){
+          ret = computeOperation( in, op );
+          if( ret!=in ){
+            status = REWRITE_AGAIN_FULL;
+            break;
+          }
+        }
+      }
     }
-    //compute other rewrite options for each produced quantifier
-    n = rewriteQuants( n, isNested, true );
     //print if changed
-    if( in!=n ){
+    if( in!=ret ){
       if( in.hasAttribute(NestedQuantAttribute()) ){
-        setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+        setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) );
       }
-      Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
-      Trace("quantifiers-rewrite") << " to " << std::endl;
-      Trace("quantifiers-rewrite") << n << std::endl;
       if( in.hasAttribute(InstConstantAttribute()) ){
         InstConstantAttribute ica;
-        n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
+        ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
       }
-
-      // This is required if substitute in computePrenex() is used.
-      return RewriteResponse(REWRITE_AGAIN_FULL, n );
-    }else{
-      return RewriteResponse(REWRITE_DONE, n );
+      Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+      Trace("quantifiers-rewrite") << " to " << std::endl;
+      Trace("quantifiers-rewrite") << ret << std::endl;
     }
+    return RewriteResponse( status, ret );
   }
   return RewriteResponse(REWRITE_DONE, in);
 }
@@ -542,7 +546,10 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
     if( f.getNumChildren()==3 ){
       ipl = f[2];
     }
-    if( computeOption==COMPUTE_NNF ){
+    if( computeOption==COMPUTE_MINISCOPING ){
+      //return directly
+      return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
+    }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
       n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
@@ -663,25 +670,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
   }
   return mkForAll( args, body, ipl );
 }
-
-Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested, bool duringRewrite ){
+/*
+Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){
   if( n.getKind()==FORALL ){
-    return rewriteQuant( n, isNested, duringRewrite );
+    return rewriteQuant( n, isNested );
   }else if( isLiteral( n ) ){
     return n;
   }else{
     NodeBuilder<> tt(n.getKind());
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      tt << rewriteQuants( n[i], isNested, duringRewrite );
+      tt << rewriteQuants( n[i], isNested );
     }
     return tt.constructNode();
   }
 }
 
-Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrite ){
+Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){
   Node prev = n;
   for( int op=0; op<COMPUTE_LAST; op++ ){
-    if( doOperation( n, isNested, op, duringRewrite ) ){
+    if( doOperation( n, isNested, op ) ){
       Node prev2 = n;
       n = computeOperation( n, op );
       if( prev2!=n ){
@@ -695,9 +702,10 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit
     return n;
   }else{
     //rewrite again until fix point is reached
-    return rewriteQuant( n, isNested, duringRewrite );
+    return rewriteQuant( n, isNested );
   }
 }
+*/
 
 bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
   return options::miniscopeQuantFreeVar();
@@ -715,17 +723,19 @@ bool QuantifiersRewriter::doMiniscopingAnd(){
   }
 }
 
-bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, bool duringRewrite ){
-  if( computeOption==COMPUTE_NNF ){
+bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
+  if( computeOption==COMPUTE_MINISCOPING ){
+    return true;
+  }else if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
   }else if( computeOption==COMPUTE_PRE_SKOLEM ){
-    return false;//options::preSkolemQuant() && !duringRewrite;
+    return false;//options::preSkolemQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return options::varElimQuant();
   }else if( computeOption==COMPUTE_CNF ){
-    return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind();
+    return false;//return options::cnfQuant() ;
   }else{
     return false;
   }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 636e00774..00301c610 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -51,7 +51,8 @@ private:
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq );
 private:
   enum{
-    COMPUTE_NNF = 0,
+    COMPUTE_MINISCOPING = 0,
+    COMPUTE_NNF,
     COMPUTE_PRE_SKOLEM,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
@@ -69,10 +70,10 @@ private:
   /** options */
   static bool doMiniscopingNoFreeVar();
   static bool doMiniscopingAnd();
-  static bool doOperation( Node f, bool isNested, int computeOption, bool duringRewrite = true );
+  static bool doOperation( Node f, bool isNested, int computeOption );
 public:
-  static Node rewriteQuants( Node n, bool isNested = false, bool duringRewrite = true );
-  static Node rewriteQuant( Node n, bool isNested = false, bool duringRewrite = true );
+  //static Node rewriteQuants( Node n, bool isNested = false );
+  //static Node rewriteQuant( Node n, bool isNested = false );
 };/* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 591270ab0..b55e8abdf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/options.h"
@@ -80,7 +80,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         d_op_map[op].push_back( n );
         added.insert( n );
 
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+        for( size_t i=0; i<n.getNumChildren(); i++ ){
           addTerm( n[i], added, withinQuant );
           if( options::efficientEMatching() ){
             EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher();
@@ -100,10 +100,9 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
           }
           if( options::eagerInstQuant() ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
-              uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
               int addedLemmas = 0;
-              for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){
-                addedLemmas += ith->d_op_triggers[op][i]->addTerm( n );
+              for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
+                addedLemmas += d_op_triggers[op][i]->addTerm( n );
               }
               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
               d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
@@ -468,3 +467,9 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain
     }
   }
 }
+
+void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
+  if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
+    d_op_triggers[op].push_back( tr );
+  }
+}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5060ac1a7..2bae5a043 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -205,6 +205,8 @@ private:
   void computeVarContains2( Node n, Node parent );
   /** var contains */
   std::map< TNode, std::vector< TNode > > d_var_contains;
+  /** triggers for each operator */
+  std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
 public:
   /** compute var contains */
   void computeVarContains( Node n );
@@ -214,6 +216,8 @@ public:
   void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
   /** get var contains for node n */
   void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+  /** register trigger (for eager quantifier instantiation) */
+  void registerTrigger( inst::Trigger* tr, Node op );
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index ae08fe863..67b2e6bd8 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -67,10 +67,8 @@ d_quantEngine( qe ), d_f( f ){
   }
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
   if( options::eagerInstQuant() ){
-    Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF );
-    uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
     for( int i=0; i<(int)d_nodes.size(); i++ ){
-      ith->registerTrigger( this, d_nodes[i].getOperator() );
+      qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() );
     }
   }
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a4b918984..9d93c6cc0 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -321,13 +321,14 @@ void TheoryEngine::check(Theory::Effort effort) {
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
       if(d_logicInfo.isQuantified()) {
+        bool prevIncomplete = d_incomplete;
         // quantifiers engine must pass effort last call check
         d_quantEngine->check(Theory::EFFORT_LAST_CALL);
         // if we have given up, then possibly flip decision
         if(options::flipDecision()) {
           if(d_incomplete && !d_inConflict && !needCheck()) {
             if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) {
-              d_incomplete = false;
+              d_incomplete = prevIncomplete;
             }
           }
         }
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 099eb5b5e..e45842481 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -132,35 +132,7 @@ Node InstantiatorTheoryUf::getRepresentative( Node a ){
     return a;
   }
 }
-/*
-Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
-  if( d_ground_reps.find( a )==d_ground_reps.end() ){
-    if( !hasTerm( a ) ){
-      return a;
-    }else{
-      Node rep = getRepresentative( a );
-      if( !rep.hasAttribute(InstConstantAttribute()) ){
-        //return the representative of a
-        d_ground_reps[a] = rep;
-        return rep;
-      }else{
-        //otherwise, must search eq class
-        eq::EqClassIterator eqc_iter( rep, getEqualityEngine() );
-        rep = Node::null();
-        while( !eqc_iter.isFinished() ){
-          if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){
-            d_ground_reps[ a ] = *eqc_iter;
-            return *eqc_iter;
-          }
-          eqc_iter++;
-        }
-        d_ground_reps[ a ] = a;
-      }
-    }
-  }
-  return d_ground_reps[a];
-}
-*/
+
 eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
   return &((TheoryUF*)d_th)->d_equalityEngine;
 }
@@ -224,12 +196,6 @@ void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){
 
 }
 
-void InstantiatorTheoryUf::registerTrigger( theory::inst::Trigger* tr, Node op ){
-  if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
-    d_op_triggers[op].push_back( tr );
-  }
-}
-
 void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
   if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){
     eq::EqClassIterator eqc_iter( getRepresentative( n ),
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 3cb4f97cc..b5a3aa765 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -107,12 +107,6 @@ public:
   void merge( TNode a, TNode b );
   /** assert terms are disequal */
   void assertDisequal( TNode a, TNode b, TNode reason );
-private:
-  /** triggers */
-  std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
-public:
-  /** register trigger (for eager quantifier instantiation) */
-  void registerTrigger( inst::Trigger* tr, Node op );
 public:
   /** output eq class */
   void outputEqClass( const char* c, Node n );
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 5dc60dbb0..7e0af3e9f 100755
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -281,6 +281,14 @@ TypeNode SortInference::getTypeForId( int t ){
 Node SortInference::getNewSymbol( Node old, TypeNode tn ){
   if( tn==old.getType() ){
     return old;
+  }else if( old.isConst() ){
+    //must make constant of type tn
+    if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
+      std::stringstream ss;
+      ss << "ic_" << tn << "_" << old;
+      d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" );  //use mkConst???
+    }
+    return d_const_map[tn][ old ];
   }else{
     std::stringstream ss;
     ss << "i_$$_" << old;
@@ -323,6 +331,19 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
       var_bound.erase( n[0][i] );
     }
     return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }else if( n.getKind()==kind::EQUAL ){
+    if( children[0].getType()!=children[1].getType() ){
+      if( children[0].isConst() ){
+        children[0] = getNewSymbol( children[0], children[1].getType() );
+      }else if( children[1].isConst() ){
+        children[1] = getNewSymbol( children[1], children[0].getType() );
+      }else{
+        Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;
+        Trace("sort-inference-warn") << "  Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
+        Assert( false );
+      }
+    }
+    return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
   }else if( n.getKind()==kind::APPLY_UF ){
     Node op = n.getOperator();
     if( d_symbol_map.find( op )==d_symbol_map.end() ){
@@ -356,13 +377,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
       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] ];
+          children[i+1] = getNewSymbol( n[i], tna );
         }else{
           Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;
           Assert( false );