diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-19 13:36:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-19 13:36:59 -0500 |
| commit | 31717bf7c014bf1971cabcc9b871de5818278126 (patch) | |
| tree | d7331da2db605b16b67920990ae6def5db03dfd9 /src/theory/sets/inference_manager.cpp | |
| parent | 466520464a8ed862c3a323bb2fbcc92332d9384b (diff) | |
Make sets and strings solver states inherit from TheoryState (#4918)
This is towards the new standard for theory solvers.
This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager.
Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).
Diffstat (limited to 'src/theory/sets/inference_manager.cpp')
| -rw-r--r-- | src/theory/sets/inference_manager.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index f99dad91e..8f25f6511 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -72,7 +72,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) if (fact == d_false) { Trace("sets-lemma") << "Conflict : " << exp << std::endl; - d_state.setConflict(exp); + conflict(exp); return true; } return false; @@ -233,6 +233,12 @@ bool InferenceManager::hasProcessed() const bool InferenceManager::hasSentLemma() const { return d_sentLemma; } bool InferenceManager::hasAddedFact() const { return d_addedFact; } +void InferenceManager::conflict(Node conf) +{ + d_parent.getOutputChannel()->conflict(conf); + d_state.notifyInConflict(); +} + } // namespace sets } // namespace theory } // namespace CVC4 |