From: Dejan Jovanović Date: Fri, 24 Feb 2012 20:29:12 +0000 (+0000) Subject: Theory interface changes: X-Git-Tag: cvc5-1.0.0~8305 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8da6a3644d1cdbe62d44a8eb80068da4d1d2855;p=cvc5.git Theory interface changes: solve -> ppAsert staticLearning -> ppStaticLearn preprocess -> ppRewrite SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*) via Eclipse refactoring magic. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 12288e40a..5a7209c40 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -622,7 +622,7 @@ void SmtEnginePrivate::staticLearning() { NodeBuilder<> learned(kind::AND); learned << d_assertionsToCheck[i]; - d_smt.d_theoryEngine->staticLearning(d_assertionsToCheck[i], learned); + d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned); if(learned.getNumChildren() == 1) { learned.clear(); } else { @@ -689,10 +689,10 @@ void SmtEnginePrivate::nonClausalSimplify() { // Solve it with the corresponding theory Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "solving " << learnedLiteral << endl; - Theory::SolveStatus solveStatus = + Theory::PPAssertStatus solveStatus = d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions); switch (solveStatus) { - case Theory::SOLVE_STATUS_CONFLICT: + case Theory::PP_ASSERT_STATUS_CONFLICT: // If in conflict, we return false Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict while solving " @@ -700,7 +700,7 @@ void SmtEnginePrivate::nonClausalSimplify() { d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); return; - case Theory::SOLVE_STATUS_SOLVED: + case Theory::PP_ASSERT_STATUS_SOLVED: // The literal should rewrite to true Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "solved " << learnedLiteral << endl; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index ec5752d3a..1c01c35ab 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -141,7 +141,7 @@ void TheoryArith::addSharedTerm(TNode n){ d_differenceManager.addSharedTerm(n); } -Node TheoryArith::preprocess(TNode atom) { +Node TheoryArith::ppRewrite(TNode atom) { Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; Node a = d_pbSubstitutions.apply(atom); @@ -167,7 +167,7 @@ Node TheoryArith::preprocess(TNode atom) { return a; } -Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheoryArith::ppAsert(TNode in, SubstitutionMap& outSubstitutions) { TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer); Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl; @@ -220,7 +220,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio // substitution is integral Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl; outSubstitutions.addSubstitution(minVar, elim); - return SOLVE_STATUS_SOLVED; + return PP_ASSERT_STATUS_SOLVED; } else { Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl; } @@ -243,10 +243,10 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio break; } - return SOLVE_STATUS_UNSOLVED; + return PP_ASSERT_STATUS_UNSOLVED; } -void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { +void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); d_learner.staticLearning(n, learned); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 256a197cd..9e6a725bf 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -268,9 +268,9 @@ public: void presolve(); void notifyRestart(); - SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); - Node preprocess(TNode atom); - void staticLearning(TNode in, NodeBuilder<>& learned); + PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); + void ppStaticLearn(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 601805343..9ef81cc96 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -187,18 +187,18 @@ Node TheoryArrays::getValue(TNode n) { } } -Theory::SolveStatus TheoryArrays::solve(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheoryArrays::ppAsert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: { d_staticFactManager.addEq(in); 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; } break; } @@ -214,7 +214,7 @@ Theory::SolveStatus TheoryArrays::solve(TNode in, SubstitutionMap& outSubstituti default: break; } - return SOLVE_STATUS_UNSOLVED; + return PP_ASSERT_STATUS_UNSOLVED; } Node TheoryArrays::preprocessTerm(TNode term) { @@ -382,7 +382,7 @@ Node TheoryArrays::recursivePreprocessTerm(TNode term) { return newTerm; } -Node TheoryArrays::preprocess(TNode atom) { +Node TheoryArrays::ppRewrite(TNode atom) { if (d_donePreregister) return atom; Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str()); return recursivePreprocessTerm(atom); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 366c2d3f7..3e12c3499 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -479,8 +479,8 @@ public: Node explain(TNode n); Node getValue(TNode n); - SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); - Node preprocess(TNode atom); + PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); void shutdown() { } std::string identify() const { return std::string("TheoryArrays"); } diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 229a40532..3b3cde33d 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -134,11 +134,11 @@ Node TheoryBool::getValue(TNode n) { } } -Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheoryBool::ppAsert(TNode in, SubstitutionMap& outSubstitutions) { if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst()) { // If we get a false literal, we're in conflict - return SOLVE_STATUS_CONFLICT; + return PP_ASSERT_STATUS_CONFLICT; } // Add the substitution from the variable to it's value @@ -146,17 +146,17 @@ Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitution if (in[0].getKind() == kind::VARIABLE) { outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst(false)); } else { - return SOLVE_STATUS_UNSOLVED; + return PP_ASSERT_STATUS_UNSOLVED; } } else { if (in.getKind() == kind::VARIABLE) { outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst(true)); } else { - return SOLVE_STATUS_UNSOLVED; + return PP_ASSERT_STATUS_UNSOLVED; } } - return SOLVE_STATUS_SOLVED; + return PP_ASSERT_STATUS_SOLVED; } diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index bd4c8d565..dd15436d8 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -36,7 +36,7 @@ public: Node getValue(TNode n); - SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); + PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions); std::string identify() const { return std::string("TheoryBool"); } };/* class TheoryBool */ 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(); 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::hasStaticLearning) { \ - reinterpret_cast::theory_class*>(theoryOf(THEORY))->staticLearning(in, learned); \ + reinterpret_cast::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; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2c1c9a436..ceefa88e8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -507,7 +507,7 @@ public: /** * Solve the given literal with a theory that owns it. */ - theory::Theory::SolveStatus solve(TNode literal, + theory::Theory::PPAssertStatus solve(TNode literal, theory::SubstitutionMap& substitutionOut); /** @@ -543,10 +543,10 @@ public: void combineTheories(); /** - * Calls staticLearning() on all theories, accumulating their + * Calls ppStaticLearn() on all theories, accumulating their * combined contributions in the "learned" builder. */ - void staticLearning(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder<>& learned); /** * Calls presolve() on all theories and returns true diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 2344adc70..7f5e11a64 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -282,7 +282,7 @@ void TheoryUF::presolve() { Debug("uf") << "uf: end presolve()" << endl; } -void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { +void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); vector workList; @@ -393,7 +393,7 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { if(Options::current()->ufSymmetryBreaker) { d_symb.assertFormula(n); } -}/* TheoryUF::staticLearning() */ +}/* TheoryUF::ppStaticLearn() */ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { if (d_equalityEngine.areEqual(a, b)) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 2a02208dc..ab391e242 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -109,7 +109,7 @@ public: void preRegisterTerm(TNode term); Node explain(TNode n); - void staticLearning(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); void addSharedTerm(TNode n);