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/uf/theory_uf.cpp | |
| 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/uf/theory_uf.cpp')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
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(). |