From: Andrew Reynolds Date: Sun, 9 Aug 2020 22:36:22 +0000 (-0500) Subject: Make valuation class more robust to null underlying TheoryEngine. (#4864) X-Git-Tag: cvc5-1.0.0~3029 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33b96c656515f9634ec97b021da8da5dee2b9bcd;p=cvc5.git 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. --- diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 52321ffd4..bc6e18a83 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -62,17 +62,15 @@ void TheoryArith::preRegisterTerm(TNode n){ void TheoryArith::finishInit() { - TheoryModel* tm = d_valuation.getModel(); - Assert(tm != nullptr); if (getLogicInfo().isTheoryEnabled(THEORY_ARITH) && getLogicInfo().areTranscendentalsUsed()) { // witness is used to eliminate square root - tm->setUnevaluatedKind(kind::WITNESS); + d_valuation.setUnevaluatedKind(kind::WITNESS); // we only need to add the operators that are not syntax sugar - tm->setUnevaluatedKind(kind::EXPONENTIAL); - tm->setUnevaluatedKind(kind::SINE); - tm->setUnevaluatedKind(kind::PI); + d_valuation.setUnevaluatedKind(kind::EXPONENTIAL); + d_valuation.setUnevaluatedKind(kind::SINE); + d_valuation.setUnevaluatedKind(kind::PI); } } diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7365960e9..1475446fe 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -67,12 +67,10 @@ TheoryQuantifiers::~TheoryQuantifiers() { void TheoryQuantifiers::finishInit() { // quantifiers are not evaluated in getModelValue - TheoryModel* tm = d_valuation.getModel(); - Assert(tm != nullptr); - tm->setUnevaluatedKind(EXISTS); - tm->setUnevaluatedKind(FORALL); + d_valuation.setUnevaluatedKind(EXISTS); + d_valuation.setUnevaluatedKind(FORALL); // witness is used in several instantiation strategies - tm->setUnevaluatedKind(WITNESS); + d_valuation.setUnevaluatedKind(WITNESS); } void TheoryQuantifiers::preRegisterTerm(TNode n) { diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index c4e3e9add..9c680cc64 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -54,11 +54,9 @@ TheoryRewriter* TheorySets::getTheoryRewriter() void TheorySets::finishInit() { - TheoryModel* tm = d_valuation.getModel(); - Assert(tm != nullptr); - tm->setUnevaluatedKind(COMPREHENSION); + d_valuation.setUnevaluatedKind(COMPREHENSION); // choice is used to eliminate witness - tm->setUnevaluatedKind(WITNESS); + d_valuation.setUnevaluatedKind(WITNESS); } void TheorySets::addSharedTerm(TNode n) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2c7573949..54c4759a8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -114,9 +114,8 @@ eq::EqualityEngine* TheoryStrings::getEqualityEngine() } void TheoryStrings::finishInit() { - TheoryModel* tm = d_valuation.getModel(); // witness is used to eliminate str.from_code - tm->setUnevaluatedKind(WITNESS); + d_valuation.setUnevaluatedKind(WITNESS); } bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 5d47cef4a..02c9cb467 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -80,9 +80,7 @@ void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { void TheoryUF::finishInit() { // combined cardinality constraints are not evaluated in getModelValue - TheoryModel* tm = d_valuation.getModel(); - Assert(tm != nullptr); - tm->setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); + d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); // Initialize the cardinality constraints solver if the logic includes UF, // finite model finding is enabled, and it is not disabled by // options::ufssMode(). 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 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(); } diff --git a/src/theory/valuation.h b/src/theory/valuation.h index b1985971a..d8d57d2e5 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -110,7 +110,20 @@ public: * Returns pointer to model. */ TheoryModel* getModel(); - + + //-------------------------------------- static configuration of the model + /** + * Set that k is an unevaluated kind in the TheoryModel, if it exists. + * See TheoryModel::setUnevaluatedKind for details. + */ + void setUnevaluatedKind(Kind k); + /** + * Set that k is an unevaluated kind in the TheoryModel, if it exists. + * See TheoryModel::setSemiEvaluatedKind for details. + */ + void setSemiEvaluatedKind(Kind k); + //-------------------------------------- end static configuration of the model + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function