diff options
Diffstat (limited to 'src/theory/ext_theory.cpp')
-rw-r--r-- | src/theory/ext_theory.cpp | 62 |
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); } |