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.

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();
 }