1 files changed, 44 insertions, 18 deletions

diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index bdcd5dcff..e8ed60ae4 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -28,13 +28,41 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
-ExtTheory::ExtTheory(Theory* p, bool cacheEnabled)
+bool ExtTheoryCallback::getCurrentSubstitution(
+    int effort,
+    const std::vector<Node>& vars,
+    std::vector<Node>& subs,
+    std::map<Node, std::vector<Node> >& exp)
+{
+  return false;
+}
+bool ExtTheoryCallback::isExtfReduced(int effort,
+                                      Node n,
+                                      Node on,
+                                      std::vector<Node>& exp)
+{
+  return n.isConst();
+}
+bool ExtTheoryCallback::getReduction(int effort,
+                                    Node n,
+                                    Node& nr,
+                                    bool& isSatDep)
+{
+  return false;
+}
+
+ExtTheory::ExtTheory(ExtTheoryCallback& p,
+                     context::Context* c,
+                     context::UserContext* u,
+                     OutputChannel& out,
+                     bool cacheEnabled)
     : d_parent(p),
-      d_ext_func_terms(p->getSatContext()),
-      d_ci_inactive(p->getUserContext()),
-      d_has_extf(p->getSatContext()),
-      d_lemmas(p->getUserContext()),
-      d_pp_lemmas(p->getUserContext()),
+      d_out(out),
+      d_ext_func_terms(c),
+      d_ci_inactive(u),
+      d_has_extf(c),
+      d_lemmas(u),
+      d_pp_lemmas(u),
       d_cacheEnabled(cacheEnabled)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -61,7 +89,6 @@ std::vector<Node> ExtTheory::collectVars(Node n)
     // (commented below)
     if (current.getNumChildren() > 0)
     {
-      //&& Theory::theoryOf(n)==d_parent->getId() ){
       worklist.insert(worklist.end(), current.begin(), current.end());
     }
     else
@@ -140,7 +167,7 @@ void ExtTheory::getSubstitutedTerms(int effort,
           }
         }
       }
-      bool useSubs = d_parent->getCurrentSubstitution(effort, vars, sub, expc);
+      bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
       // get the current substitution for all variables
       Assert(!useSubs || vars.size() == sub.size());
       for (const Node& n : terms)
@@ -206,8 +233,8 @@ bool ExtTheory::doInferencesInternal(int effort,
       {
         Node nr;
         // note: could do reduction with substitution here
-        int ret = d_parent->getReduction(effort, n, nr);
-        if (ret == 0)
+        bool satDep = false;
+        if (!d_parent.getReduction(effort, n, nr, satDep))
         {
           nred.push_back(n);
         }
@@ -223,7 +250,7 @@ bool ExtTheory::doInferencesInternal(int effort,
               addedLemma = true;
             }
           }
-          markReduced(n, ret < 0);
+          markReduced(n, satDep);
         }
       }
     }
@@ -242,7 +269,7 @@ bool ExtTheory::doInferencesInternal(int effort,
           Node sr = Rewriter::rewrite(sterms[i]);
           // ask the theory if this term is reduced, e.g. is it constant or it
           // is a non-extf term.
-          if (d_parent->isExtfReduced(effort, sr, terms[i], exp[i]))
+          if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i]))
           {
             processed = true;
             markReduced(terms[i]);
@@ -344,7 +371,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess)
     if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
     {
       d_pp_lemmas.insert(lem);
-      d_parent->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
+      d_out.lemma(lem, LemmaProperty::PREPROCESS);
       return true;
     }
   }
@@ -353,7 +380,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess)
     if (d_lemmas.find(lem) == d_lemmas.end())
     {
       d_lemmas.insert(lem);
-      d_parent->getOutputChannel().lemma(lem);
+      d_out.lemma(lem);
       return true;
     }
   }
@@ -403,8 +430,7 @@ void ExtTheory::registerTerm(Node n)
   {
     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;
+      Trace("extt-debug") << "Found extended function : " << n << std::endl;
       d_ext_func_terms[n] = true;
       d_has_extf = n;
       d_extf_info[n].d_vars = collectVars(n);
@@ -435,13 +461,13 @@ void ExtTheory::registerTermRec(Node n)
 }
 
 // mark reduced
-void ExtTheory::markReduced(Node n, bool contextDepend)
+void ExtTheory::markReduced(Node n, bool satDep)
 {
   Trace("extt-debug") << "Mark reduced " << n << std::endl;
   registerTerm(n);
   Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
   d_ext_func_terms[n] = false;
-  if (!contextDepend)
+  if (!satDep)
   {
     d_ci_inactive.insert(n);
   }