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/strings/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/strings/inference_manager.cpp')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 88cf6d958..a8ebd921a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -171,7 +171,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) // only keep stats if we process it here d_statistics.d_inferences << ii.d_id; d_out.conflict(conf); - d_state.setConflict(); + d_state.notifyInConflict(); return; } Trace("strings-infer-debug") << "...as lemma" << std::endl; @@ -435,7 +435,7 @@ void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp) Trace("strings-pending") << "Process pending conflict " << pc << std::endl; Node conflictNode = mkExplain(a); - d_state.setConflict(); + d_state.notifyInConflict(); Trace("strings-conflict") << "CONFLICT: Eager prefix : " << conflictNode << std::endl; ++(d_statistics.d_conflictsEagerPrefix); |