Incorporate non-bv parts of ajr/bvExt branch

4 files changed, 348 insertions, 164 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 2f6f7e9e7..3ef6df3fc 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -331,6 +331,92 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var
   return true;
 }
 
+int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
+  //determine the effort level to process the extf at
+  // 0 - at assertion time, 1+ - after no other reduction is applicable
+  Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
+  if( d_extf_info_tmp[n].d_model_active ){
+    int r_effort = -1;
+    int pol = d_extf_info_tmp[n].d_pol;
+    if( n.getKind()==kind::STRING_STRCTN ){
+      if( pol==1 ){
+        r_effort = 1;
+      }else if( pol==-1 ){
+        if( effort==2 ){
+          Node x = n[0];
+          Node s = n[1];
+          std::vector< Node > lexp;
+          Node lenx = getLength( x, lexp );
+          Node lens = getLength( s, lexp );
+          if( areEqual( lenx, lens ) ){
+            Trace("strings-extf-debug") << "  resolve extf : " << n << " based on equal lengths disequality." << std::endl;
+            //we can reduce to disequality when lengths are equal
+            if( !areDisequal( x, s ) ){
+              lexp.push_back( lenx.eqNode(lens) );
+              lexp.push_back( n.negate() );
+              Node xneqs = x.eqNode(s).negate();
+              sendInference( lexp, xneqs, "NEG-CTN-EQL", true );
+            }
+            return 1;
+          }else if( !areDisequal( lenx, lens ) ){
+            //split on their lenths
+            sendSplit( lenx, lens, "NEG-CTN-SP" );
+          }else{
+            r_effort = 2;
+          }
+        }
+      }
+    }else{
+      if( options::stringLazyPreproc() ){
+        if( n.getKind()==kind::STRING_SUBSTR ){
+          r_effort = 1;
+        }else if( n.getKind()!=kind::STRING_IN_REGEXP ){
+          r_effort = 2;
+        }
+      }
+    }
+    if( effort==r_effort ){
+      Node c_n = pol==-1 ? n.negate() : n;
+      if( d_preproc_cache.find( c_n )==d_preproc_cache.end() ){
+        d_preproc_cache[ c_n ] = true;
+        Trace("strings-process-debug") << "Process reduction for " << n << ", pol = " << pol << std::endl;
+        if( n.getKind()==kind::STRING_STRCTN && pol==1 ){
+          Node x = n[0];
+          Node s = n[1];
+          //positive contains reduces to a equality
+          Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" );
+          Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" );
+          Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) );
+          std::vector< Node > exp_vec;
+          exp_vec.push_back( n );
+          sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true );
+          //we've reduced this n
+          Trace("strings-extf-debug") << "  resolve extf : " << n << " based on positive contain reduction." << std::endl;
+          return 1;
+        }else{
+          // for STRING_SUBSTR, STRING_STRCTN with pol=-1,
+          //     STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
+          std::vector< Node > new_nodes;
+          Node res = d_preproc.simplify( n, new_nodes );
+          Assert( res!=n );
+          new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, n ) );
+          Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+          nnlem = Rewriter::rewrite( nnlem );
+          Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
+          Trace("strings-red-lemma") << "...from " << n << std::endl;
+          sendInference( d_empty_vec, nnlem, "Reduction", true );
+          //we've reduced this n
+          Trace("strings-extf-debug") << "  resolve extf : " << n << " based on reduction." << std::endl;
+          return 1;
+        }
+      }else{
+        return 1;
+      }
+    }
+  }
+  return 0;
+}
+
 /////////////////////////////////////////////////////////////////////////////
 // NOTIFICATIONS
 /////////////////////////////////////////////////////////////////////////////
@@ -404,15 +490,13 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
     for( unsigned j=0; j<col[i].size(); j++ ) {
       Trace("strings-model") << col[i][j] << " ";
       //check if col[i][j] has only variables
-      EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false );
-      Node cst = ei ? ei->d_const_term : Node::null();
-      if( cst.isNull() ){
+      if( !col[i][j].isConst() ){
         Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
         if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
           pure_eq.push_back( col[i][j] );
         }
       }else{
-        processed[col[i][j]] = cst;
+        processed[col[i][j]] = col[i][j];
       }
     }
     Trace("strings-model") << "have length " << lts_values[i] << std::endl;
@@ -692,104 +776,29 @@ bool TheoryStrings::needsCheckLastEffort() {
 }
 
 void TheoryStrings::checkExtfReductions( int effort ) {
+  //standardize this?
+  //std::vector< Node > nred;
+  //d_extt->doReductions( effort, nred, false );
+
   std::vector< Node > extf;
   d_extt->getActive( extf );
+  Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl;
   for( unsigned i=0; i<extf.size(); i++ ){
     Node n = extf[i];
-    if( d_extf_info_tmp[n].d_model_active ){
-      Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
-      if( checkExtfReduction( n, d_extf_info_tmp[n].d_pol, effort ) ){
-        d_extt->markReduced( n );
-      }
-      if( hasProcessed() ){
+    Trace("strings-process") << "Check " << n << ", active in model=" << d_extf_info_tmp[n].d_model_active << std::endl;
+    Node nr;
+    int ret = getReduction( effort, n, nr );
+    Assert( nr.isNull() );
+    if( ret!=0 ){
+      d_extt->markReduced( extf[i] );
+      if( options::stringOpt1() && hasProcessed() ){
         return;
       }
     }
   }
 }
 
-bool TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
-  //determine the effort level to process the extf at
-  // 0 - at assertion time, 1+ - after no other reduction is applicable
-  int r_effort = -1;
-  if( atom.getKind()==kind::STRING_STRCTN ){
-    if( pol==1 ){
-      r_effort = 1;
-    }else{
-      Assert( pol==-1 );
-      if( effort==2 ){
-        Node x = atom[0];
-        Node s = atom[1];
-        std::vector< Node > lexp;
-        Node lenx = getLength( x, lexp );
-        Node lens = getLength( s, lexp );
-        if( areEqual( lenx, lens ) ){
-          Trace("strings-extf-debug") << "  resolve extf : " << atom << " based on equal lengths disequality." << std::endl;
-          //we can reduce to disequality when lengths are equal
-          if( !areDisequal( x, s ) ){
-            lexp.push_back( lenx.eqNode(lens) );
-            lexp.push_back( atom.negate() );
-            Node xneqs = x.eqNode(s).negate();
-            sendInference( lexp, xneqs, "NEG-CTN-EQL", true );
-          }
-          return true;
-        }else if( !areDisequal( lenx, lens ) ){
-          //split on their lenths
-          sendSplit( lenx, lens, "NEG-CTN-SP" );
-        }else{
-          r_effort = 2;
-        }
-      }
-    }
-  }else{
-    if( options::stringLazyPreproc() ){
-      if( atom.getKind()==kind::STRING_SUBSTR ){
-        r_effort = 1;
-      }else if( atom.getKind()!=kind::STRING_IN_REGEXP ){
-        r_effort = 2;
-      }
-    }
-  }
-  if( effort==r_effort ){
-    Node c_atom = pol==-1 ? atom.negate() : atom;
-    if( d_preproc_cache.find( c_atom )==d_preproc_cache.end() ){
-      d_preproc_cache[ c_atom ] = true;
-      Trace("strings-process-debug") << "Process reduction for " << atom << ", pol = " << pol << std::endl;
-      if( atom.getKind()==kind::STRING_STRCTN && pol==1 ){
-        Node x = atom[0];
-        Node s = atom[1];
-        //positive contains reduces to a equality
-        Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" );
-        Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" );
-        Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) );
-        std::vector< Node > exp_vec;
-        exp_vec.push_back( atom );
-        sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true );
-        //we've reduced this atom
-        Trace("strings-extf-debug") << "  resolve extf : " << atom << " based on positive contain reduction." << std::endl;
-        return true;
-      }else{
-        // for STRING_SUBSTR, STRING_STRCTN with pol=-1,
-        //     STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
-        std::vector< Node > new_nodes;
-        Node res = d_preproc.simplify( atom, new_nodes );
-        Assert( res!=atom );
-        new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, atom ) );
-        Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
-        nnlem = Rewriter::rewrite( nnlem );
-        Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
-        Trace("strings-red-lemma") << "...from " << atom << std::endl;
-        sendInference( d_empty_vec, nnlem, "Reduction", true );
-        //we've reduced this atom
-        Trace("strings-extf-debug") << "  resolve extf : " << atom << " based on reduction." << std::endl;
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
+TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
 
 }
 
@@ -827,10 +836,6 @@ void TheoryStrings::conflict(TNode a, TNode b){
 
 /** called when a new equivalance class is created */
 void TheoryStrings::eqNotifyNewClass(TNode t){
-  if( t.getKind() == kind::CONST_STRING ){
-    EqcInfo * ei =getOrMakeEqcInfo( t, true );
-    ei->d_const_term = t;
-  }
   if( t.getKind() == kind::STRING_LENGTH ){
     Trace("strings-debug") << "New length eqc : " << t << std::endl;
     Node r = d_equalityEngine.getRepresentative(t[0]);
@@ -838,6 +843,8 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
     ei->d_length_term = t[0];
     //we care about the length of this string
     registerTerm( t[0], 1 );
+  }else{
+    //d_extt->registerTerm( t );
   }
 }
 
@@ -847,9 +854,6 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
   if( e2 ){
     EqcInfo * e1 = getOrMakeEqcInfo( t1 );
     //add information from e2 to e1
-    if( !e2->d_const_term.get().isNull() ){
-      e1->d_const_term.set( e2->d_const_term );
-    }
     if( !e2->d_length_term.get().isNull() ){
       e1->d_length_term.set( e2->d_length_term );
     }
@@ -987,7 +991,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
     d_equalityEngine.assertPredicate( atom, polarity, exp );
     //process extf
     if( atom.getKind()==kind::STRING_IN_REGEXP ){
-      d_extt->registerTerm( atom );
       if( polarity && atom[1].getKind()==kind::REGEXP_RANGE ){
         if( d_extf_infer_cache_u.find( atom )==d_extf_infer_cache_u.end() ){
           d_extf_infer_cache_u.insert( atom );
@@ -999,6 +1002,8 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
         }
       }
     }
+    //register the atom here, since it may not create a new equivalence class
+    //d_extt->registerTerm( atom );
   }
   Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
   //collect extended function terms in the atom
@@ -1292,7 +1297,8 @@ void TheoryStrings::checkExtfEval( int effort ) {
   std::vector< Node > terms; 
   std::vector< Node > sterms; 
   std::vector< std::vector< Node > > exp;
-  d_extt->getInferences( effort, terms, sterms, exp );
+  d_extt->getActive( terms );
+  d_extt->getSubstitutedTerms( effort, terms, sterms, exp );
   for( unsigned i=0; i<terms.size(); i++ ){
     Node n = terms[i];
     Node sn = sterms[i];
@@ -3875,16 +3881,6 @@ Node TheoryStrings::ppRewrite(TNode atom) {
   return atom;
 }
 
-void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    d_extt->registerTerm( n );
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectExtendedFuncTerms( n[i], visited );
-    }
-  }
-}
-
 // Stats
 TheoryStrings::Statistics::Statistics():
   d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
@@ -3974,17 +3970,11 @@ Node TheoryStrings::normalizeRegexp(Node r) {
           if(r[0].isConst()) {
             break;
           } else {
-            if (d_normal_forms.find(r[0]) != d_normal_forms.end()) {
-              const std::vector<Node>& nf_r0 = d_normal_forms[r[0]];
-              nf_r = mkConcat(nf_r0);
-              Debug("regexp-nf") << "Term: " << r[0] << " has a normal form "
-                                 << nf_r << std::endl;
-              std::vector<Node>::iterator nf_end_exp = nf_exp.end();
-              std::vector<Node>::const_iterator nf_r0_begin = nf_r0.begin();
-              std::vector<Node>::const_iterator nf_r0_end = nf_r0.end();
-              nf_exp.insert(nf_end_exp, nf_r0_begin, nf_r0_end);
-              nf_r = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
-                  kind::STRING_TO_REGEXP, nf_r));
+            if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) {
+              nf_r = mkConcat( d_normal_forms[r[0]] );
+              Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl;
+              nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end());
+              nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) );
             }
           }
         }
@@ -4873,6 +4863,16 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
   return ret;
 }
 
+void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    d_extt->registerTerm( n );
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectExtendedFuncTerms( n[i], visited );
+    }
+  }
+}
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index fe72bd8e7..fd984bd58 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -72,6 +72,7 @@ public:
   Node explain( TNode literal );
   eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
   bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+  int getReduction( int effort, Node n, Node& nr );
  
   // NotifyClass for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
@@ -237,7 +238,6 @@ private:
     EqcInfo( context::Context* c );
     ~EqcInfo(){}
     //constant in this eqc
-    context::CDO< Node > d_const_term;
     context::CDO< Node > d_length_term;
     context::CDO< unsigned > d_cardinality_lem_k;
     // 1 = added length lemma
@@ -274,8 +274,6 @@ private:
     int d_pol;
     //explanation
     std::vector< Node > d_exp;
-    //reps -> list of variables
-    //std::map< Node, std::vector< Node > > d_rep_vars;
     //false if it is reduced in the model
     bool d_model_active;
   };
@@ -321,7 +319,6 @@ private:
   Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
   //check extf reduction
   void checkExtfReductions( int effort );
-  bool checkExtfReduction( Node atom, int pol, int effort );
   //flat forms check
   void checkFlatForms();
   Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
@@ -523,6 +520,7 @@ public:
     ~Statistics();
   };/* class TheoryStrings::Statistics */
   Statistics d_statistics;
+  
 };/* class TheoryStrings */
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 7fa74df6a..9e71a1ddf 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -314,15 +314,18 @@ EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
 
 
 ExtTheory::ExtTheory( Theory * p ) : d_parent( p ), 
-d_ext_func_terms( p->getSatContext() ), d_has_extf( p->getSatContext() ){
-
+d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), 
+d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_has_extf( p->getSatContext() ){
+  d_true = NodeManager::currentNM()->mkConst( true );
 }
 
+//gets all leaf terms in n
 void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
   if( !n.isConst() ){
     if( visited.find( n )==visited.end() ){
       visited[n] = true;
-      if( n.getNumChildren()>0 ){
+      //treat terms not belonging to this theory as leaf
+      if( n.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           collectVars( n[i], vars, visited );
         }
@@ -334,17 +337,17 @@ void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node,
 }
 
 //do inferences 
-void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) {
-  //all variables we need to find a substitution for
-  std::vector< Node > vars;
-  std::vector< Node > sub;
-  std::map< Node, std::vector< Node > > expc;
-  Trace("extt-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
-  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
-    //if not already reduced
-    if( (*it).second ){
-      Node n = (*it).first;
-      terms.push_back( n );
+void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) {
+  Trace("extt-debug") << "Currently " << d_ext_func_terms.size() << " extended functions." << std::endl;
+  Trace("extt-debug") << "..." << terms.size() << " to reduce." << std::endl;
+  if( !terms.empty() ){
+    //all variables we need to find a substitution for
+    std::vector< Node > vars;
+    std::vector< Node > sub;
+    std::map< Node, std::vector< Node > > expc;
+    for( unsigned i=0; i<terms.size(); i++ ){
+      //do substitution, rewrite
+      Node n = terms[i];
       std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
       Assert( iti!=d_extf_info.end() );
       for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
@@ -353,13 +356,11 @@ void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vect
         } 
       }
     }
-  }
-  Trace("extt-debug") << "..." << terms.size() << " unreduced." << std::endl;
-  if( !terms.empty() ){
-    //get the current substitution
+    //get the current substitution for all variables
     if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){
+      Assert( vars.size()==sub.size() );
       for( unsigned i=0; i<terms.size(); i++ ){
-        //do substitution, rewrite
+        //do substitution
         Node n = terms[i];
         Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
         std::vector< Node > expn;
@@ -392,13 +393,134 @@ void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vect
   }
 }
 
+bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ) {
+  if( batch ){
+    bool addedLemma = false;
+    if( isRed ){
+      for( unsigned i=0; i<terms.size(); i++ ){
+        Node n = terms[i];
+        Node nr;
+        //TODO: reduction with substitution?
+        int ret = d_parent->getReduction( effort, n, nr );
+        if( ret==0 ){
+          nred.push_back( n );
+        }else{
+          if( !nr.isNull() && n!=nr ){
+            Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr );
+            if( sendLemma( lem, true ) ){
+              Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl;
+              addedLemma = true;
+            }
+          }
+          markReduced( terms[i], ret<0 );
+        }
+      }
+    }else{
+      std::vector< Node > sterms; 
+      std::vector< std::vector< Node > > exp;
+      getSubstitutedTerms( effort, terms, sterms, exp );
+      for( unsigned i=0; i<terms.size(); i++ ){
+        bool processed = false;
+        if( sterms[i]!=terms[i] ){
+          Node sr = Rewriter::rewrite( sterms[i] );
+          if( sr.isConst() ){
+            processed = true;
+            markReduced( terms[i] );
+            Node eq = terms[i].eqNode( sr );
+            Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true );
+            Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl;
+            Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq );
+            Trace("extt-debug") << "...send lemma " << lem << std::endl;
+            if( sendLemma( lem ) ){
+              Trace("extt-lemma") << "ExtTheory : Constant rewrite lemma : " << lem << std::endl;
+              addedLemma = true;
+            }
+          }
+        }
+        if( !processed ){
+          nred.push_back( terms[i] );
+        }
+      }
+    }
+    return addedLemma;
+  }else{
+    std::vector< Node > nnred;
+    if( terms.empty() ){
+      for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+        if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
+          std::vector< Node > nterms;
+          nterms.push_back( (*it).first );
+          if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
+            return true;
+          }       
+        }
+      }
+    }else{
+      for( unsigned i=0; i<terms.size(); i++ ){
+        std::vector< Node > nterms;
+        nterms.push_back( terms[i] );
+        if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
+          return true;
+        }   
+      }
+    }
+    return false;
+  }
+}
+
+bool ExtTheory::sendLemma( Node lem, bool preprocess ) {
+  if( preprocess ){
+    if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){
+      d_pp_lemmas.insert( lem );
+      d_parent->getOutputChannel().lemma( lem, false, true );
+      return true;
+    }
+  }else{
+    if( d_lemmas.find( lem )==d_lemmas.end() ){
+      d_lemmas.insert( lem );
+      d_parent->getOutputChannel().lemma( lem );
+      return true;
+    }
+  }
+  return false;
+}
+
+bool ExtTheory::doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) {
+  if( !terms.empty() ){
+    return doInferencesInternal( effort, terms, nred, batch, false );
+  }else{
+    return false;
+  }
+}
+
+bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) {
+  std::vector< Node > terms;
+  getActive( terms );
+  return doInferencesInternal( effort, terms, nred, batch, false );
+}
+
+bool ExtTheory::doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) {
+  if( !terms.empty() ){
+    return doInferencesInternal( effort, terms, nred, batch, true );
+  }else{
+    return false;
+  }
+}
+
+bool ExtTheory::doReductions( int effort, std::vector< Node >& nred, bool batch ) {
+  std::vector< Node > terms;
+  getActive( terms );
+  return doInferencesInternal( effort, terms, nred, batch, true );
+}
+
+
 //register term
 void ExtTheory::registerTerm( Node n ) {
   if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){
     if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){
       Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl;
       d_ext_func_terms[n] = true;
-      d_has_extf = true;
+      d_has_extf = n;
       std::map< Node, bool > visited;
       collectVars( n, d_extf_info[n].d_vars, visited );
     }
@@ -406,9 +528,22 @@ void ExtTheory::registerTerm( Node n ) {
 }
 
 //mark reduced
-void ExtTheory::markReduced( Node n ) {
+void ExtTheory::markReduced( Node n, bool contextDepend ) {
   d_ext_func_terms[n] = false;
-  //TODO update has_extf
+  if( !contextDepend ){
+    d_ci_inactive.insert( n );
+  }
+  
+  //update has_extf
+  if( d_has_extf.get()==n ){
+    for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+      //if not already reduced
+      if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
+         d_has_extf = (*it).first;
+      }
+    }
+  
+  }
 }
 
 //mark congruent
@@ -424,11 +559,19 @@ void ExtTheory::markCongruent( Node a, Node b ) {
   }
 }
 
+bool ExtTheory::isContextIndependentInactive( Node n ) {
+  return d_ci_inactive.find( n )!=d_ci_inactive.end();
+}
+
+bool ExtTheory::hasActiveTerm() {
+  return !d_has_extf.get().isNull();
+}
+  
 //is active
 bool ExtTheory::isActive( Node n ) {
   NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
   if( it!=d_ext_func_terms.end() ){
-    return (*it).second;
+    return (*it).second && !isContextIndependentInactive( n );
   }else{
     return false;
   }
@@ -437,7 +580,7 @@ bool ExtTheory::isActive( Node n ) {
 void ExtTheory::getActive( std::vector< Node >& active ) {
   for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
     //if not already reduced
-    if( (*it).second ){
+    if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
       active.push_back( (*it).first );
     }
   }
@@ -446,7 +589,7 @@ void ExtTheory::getActive( std::vector< Node >& active ) {
 void ExtTheory::getActive( std::vector< Node >& active, Kind k ) {
   for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
     //if not already reduced
-    if( (*it).second && (*it).first.getKind()==k ){
+    if( (*it).first.getKind()==k && (*it).second && !isContextIndependentInactive( (*it).first ) ){
       active.push_back( (*it).first );
     }
   }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 08505be66..5d64c6446 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -24,6 +24,7 @@
 #include <string>
 
 #include "context/cdlist.h"
+#include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
@@ -891,8 +892,11 @@ public:
    */
   virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
 
-  /* equality engine */
+  /* equality engine TODO: use? */
   virtual eq::EqualityEngine * getEqualityEngine() { return NULL; }
+  
+  /* get extended theory */
+  virtual ExtTheory * getExtTheory() { return d_extt; }
 
   /* get current substitution at an effort
    *   input : vars
@@ -900,6 +904,13 @@ public:
    *   where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
   */
   virtual bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { return false; }
+  
+  /* get reduction for node
+       if return value is not 0, then n is reduced. 
+       if return value <0 then n is reduced SAT-context-independently (e.g. by a lemma that persists at this user-context level).
+       if nr is non-null, then ( n = nr ) should be added as a lemma by caller, and return value should be <0.
+   */
+  virtual int getReduction( int effort, Node n, Node& nr ) { return 0; }
 
   /**
    * Turn on proof-production mode.
@@ -974,15 +985,23 @@ public:
 class ExtTheory {
   friend class Theory;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 protected:
   Theory * d_parent;
+  Node d_true;
   //extended string terms, map to whether they are active
   NodeBoolMap d_ext_func_terms;
-  //any non-reduced extended functions exist
-  context::CDO< bool > d_has_extf;
+  //set of terms from d_ext_func_terms that are SAT-context-independently inactive 
+  //  (e.g. term t when a reduction lemma of the form t = t' was added)
+  NodeSet d_ci_inactive;
+  //cache of all lemmas sent
+  NodeSet d_lemmas;
+  NodeSet d_pp_lemmas;
+  //watched term for checking if any non-reduced extended functions exist 
+  context::CDO< Node > d_has_extf;
   //extf kind
   std::map< Kind, bool > d_extf_kind;
-  //information for extf
+  //information for each term in d_ext_func_terms
   class ExtfInfo {
   public:
     //all variables in this term
@@ -991,25 +1010,49 @@ protected:
   std::map< Node, ExtfInfo > d_extf_info;
   //collect variables
   void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
+  // is context dependent inactive
+  bool isContextIndependentInactive( Node n );
+  //do inferences internal
+  bool doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ); 
+  //send lemma
+  bool sendLemma( Node lem, bool preprocess = false );
 public:
   ExtTheory( Theory * p );
   virtual ~ExtTheory(){}
   //add extf kind
   void addFunctionKind( Kind k ) { d_extf_kind[k] = true; }
-  //do inferences 
-  //  input : effort
-  //  output : terms, sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i 
-  void getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp );
   //register term
+  //  adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called
   void registerTerm( Node n );
-  //mark reduced
-  void markReduced( Node n );
-  //mark congruent
+  // set n as reduced/inactive
+  //   if contextDepend = false, then n remains inactive in the duration of this user-context level
+  void markReduced( Node n, bool contextDepend = true );
+  // mark that a and b are congruent terms: set b inactive, set a to inactive if b was inactive
   void markCongruent( Node a, Node b );
-  //is active
+  
+  //getSubstitutedTerms
+  //  input : effort, terms
+  //  output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i
+  void getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp );
+  //doInferences
+  //  * input : effort, terms, batch (whether to send one lemma or lemmas for all terms)
+  //  *   sends rewriting lemmas of the form ( exp => t = c ) where t is in terms and c is a constant, c = rewrite( t*sigma ) where exp |= sigma
+  //  * output : nred (the terms that are still active)
+  //  * return : true iff lemma is sent
+  bool doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); 
+  bool doInferences( int effort, std::vector< Node >& nred, bool batch=true  );
+  //doReductions 
+  //  same as doInferences, but will send reduction lemmas of the form ( t = t' ) where t is in terms, t' is equivalent, reduced term
+  bool doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true  ); 
+  bool doReductions( int effort, std::vector< Node >& nred, bool batch=true  ); 
+
+  //has active term 
+  bool hasActiveTerm();
+  //is n active
   bool isActive( Node n );
-  //get active 
+  //get the set of active terms from d_ext_func_terms
   void getActive( std::vector< Node >& active );
+  //get the set of active terms from d_ext_func_terms of kind k
   void getActive( std::vector< Node >& active, Kind k );
 };