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, 14 insertions, 1 deletions

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