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.

7 files changed, 62 insertions, 21 deletions

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