diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-09 17:36:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-09 17:36:22 -0500 |
commit | 33b96c656515f9634ec97b021da8da5dee2b9bcd (patch) | |
tree | dcfb186b6bfadf2824e2b22b2f6ebb7f1fcc5cb6 /src/theory/valuation.cpp | |
parent | 28f5438df1e5ba87aab60552658aa09b79c35ba2 (diff) |
Make valuation class more robust to null underlying TheoryEngine. (#4864)
In some use cases (unit tests, old proofs infrastructure), we use a Theory with no associated TheoryEngine. This PR makes the Valuation class more robust to this case.
This includes making the "unevaluated kinds" a no-op in this case (this is necessary for Theory::finishInit with no TheoryEngine) and adding some assertions to cases that the Theory should never call without TheoryEngine.
This is required for a new policy for dynamically configuring equality engine infrastructure in Theory.
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r-- | src/theory/valuation.cpp | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index d8233bff7..1a2b9220a 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -20,6 +20,7 @@ #include "options/theory_options.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" +#include "theory/theory_model.h" namespace CVC4 { namespace theory { @@ -76,10 +77,12 @@ bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) { } bool Valuation::isSatLiteral(TNode n) const { + Assert(d_engine != nullptr); return d_engine->getPropEngine()->isSatLiteral(n); } Node Valuation::getSatValue(TNode n) const { + Assert(d_engine != nullptr); if(n.getKind() == kind::NOT) { Node atomRes = d_engine->getPropEngine()->getValue(n[0]); if(atomRes.getKind() == kind::CONST_BOOLEAN) { @@ -94,6 +97,7 @@ Node Valuation::getSatValue(TNode n) const { } bool Valuation::hasSatValue(TNode n, bool& value) const { + Assert(d_engine != nullptr); if (d_engine->getPropEngine()->isSatLiteral(n)) { return d_engine->getPropEngine()->hasValue(n, value); } else { @@ -102,36 +106,69 @@ bool Valuation::hasSatValue(TNode n, bool& value) const { } EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) { + Assert(d_engine != nullptr); return d_engine->getEqualityStatus(a, b); } Node Valuation::getModelValue(TNode var) { + Assert(d_engine != nullptr); return d_engine->getModelValue(var); } TheoryModel* Valuation::getModel() { + if (d_engine == nullptr) + { + // no theory engine, thus we don't have a model object + return nullptr; + } return d_engine->getModel(); } +void Valuation::setUnevaluatedKind(Kind k) +{ + TheoryModel* m = getModel(); + if (m != nullptr) + { + m->setUnevaluatedKind(k); + } + // If no model is available, this command has no effect. This is the case + // when e.g. calling Theory::finishInit for theories that are using a + // Valuation with no model. +} + +void Valuation::setSemiEvaluatedKind(Kind k) +{ + TheoryModel* m = getModel(); + if (m != nullptr) + { + m->setSemiEvaluatedKind(k); + } +} + Node Valuation::ensureLiteral(TNode n) { + Assert(d_engine != nullptr); return d_engine->ensureLiteral(n); } bool Valuation::isDecision(Node lit) const { + Assert(d_engine != nullptr); return d_engine->getPropEngine()->isDecision(lit); } unsigned Valuation::getAssertionLevel() const{ + Assert(d_engine != nullptr); return d_engine->getPropEngine()->getAssertionLevel(); } std::pair<bool, Node> Valuation::entailmentCheck(options::TheoryOfMode mode, TNode lit) { + Assert(d_engine != nullptr); return d_engine->entailmentCheck(mode, lit); } bool Valuation::needCheck() const{ + Assert(d_engine != nullptr); return d_engine->needCheck(); } |