diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-24 20:29:12 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-24 20:29:12 +0000 |
commit | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (patch) | |
tree | 773ccef817d1e5cbad85b4c0a1fb44666b1e0600 /src/theory/theory_engine.cpp | |
parent | 5a20a19a30929ad58a9e64a9d8d1f877f3a07ae6 (diff) |
Theory interface changes:
solve -> ppAsert
staticLearning -> ppStaticLearn
preprocess -> ppRewrite
SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*)
via Eclipse refactoring magic.
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; } |