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.h | |
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.h')
-rw-r--r-- | src/theory/valuation.h | 15 |
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 |