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.h | |
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.h')
-rw-r--r-- | src/theory/theory.h | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index fade1e3c7..a67d3b7af 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -463,39 +463,39 @@ public: * *never* clear it. It is a conjunction to add to the formula at * the top-level and may contain other theories' contributions. */ - virtual void staticLearning(TNode in, NodeBuilder<>& learned) { } + virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { } - enum SolveStatus { + enum PPAssertStatus { /** Atom has been solved */ - SOLVE_STATUS_SOLVED, + PP_ASSERT_STATUS_SOLVED, /** Atom has not been solved */ - SOLVE_STATUS_UNSOLVED, + PP_ASSERT_STATUS_UNSOLVED, /** Atom is inconsistent */ - SOLVE_STATUS_CONFLICT + PP_ASSERT_STATUS_CONFLICT }; /** * Given a literal, add the solved substitutions to the map, if any. * The method should return true if the literal can be safely removed. */ - virtual SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions) { + virtual PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions) { if (in.getKind() == kind::EQUAL) { if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { outSubstitutions.addSubstitution(in[0], in[1]); - return SOLVE_STATUS_SOLVED; + return PP_ASSERT_STATUS_SOLVED; } if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { outSubstitutions.addSubstitution(in[1], in[0]); - return SOLVE_STATUS_SOLVED; + return PP_ASSERT_STATUS_SOLVED; } if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) { if (in[0] != in[1]) { - return SOLVE_STATUS_CONFLICT; + return PP_ASSERT_STATUS_CONFLICT; } } } - return SOLVE_STATUS_UNSOLVED; + return PP_ASSERT_STATUS_UNSOLVED; } /** @@ -504,7 +504,7 @@ public: * the atom into an equivalent form. This is only called just * before an input atom to the engine. */ - virtual Node preprocess(TNode atom) { return atom; } + virtual Node ppRewrite(TNode atom) { return atom; } /** * A Theory is called with presolve exactly one time per user @@ -639,13 +639,13 @@ inline std::ostream& operator<<(std::ostream& out, return out << theory.identify(); } -inline std::ostream& operator << (std::ostream& out, theory::Theory::SolveStatus status) { +inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertStatus status) { switch (status) { - case theory::Theory::SOLVE_STATUS_SOLVED: + case theory::Theory::PP_ASSERT_STATUS_SOLVED: out << "SOLVE_STATUS_SOLVED"; break; - case theory::Theory::SOLVE_STATUS_UNSOLVED: + case theory::Theory::PP_ASSERT_STATUS_UNSOLVED: out << "SOLVE_STATUS_UNSOLVED"; break; - case theory::Theory::SOLVE_STATUS_CONFLICT: + case theory::Theory::PP_ASSERT_STATUS_CONFLICT: out << "SOLVE_STATUS_CONFLICT"; break; default: Unhandled(); |