diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3486d9075..578f68d54 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -442,7 +442,7 @@ void TheoryEngine::notifyRestart() { CVC4_FOR_EACH_THEORY; } -void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { +void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) { // NOTE that we don't look at d_theoryIsActive[] here. First of // all, we haven't done any pre-registration yet, so we don't know // which theories are active. Second, let's give each theory a shot @@ -455,7 +455,7 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->staticLearning(in, learned); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->ppStaticLearn(in, learned); \ } // static learning for each theory using the statement above @@ -478,10 +478,10 @@ void TheoryEngine::shutdown() { theory::Rewriter::shutdown(); } -theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { +theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; - Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitutionOut); + Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAsert(literal, substitutionOut); Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl; return solveStatus; } @@ -519,7 +519,7 @@ Node TheoryEngine::preprocess(TNode assertion) { // If this is an atom, we preprocess it with the theory if (Theory::theoryOf(current) != THEORY_BOOL) { - d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current); + d_atomPreprocessingCache[current] = theoryOf(current)->ppRewrite(current); continue; } |