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/theory_strings.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/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c78e8dc2a..6d81c742a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -81,6 +81,8 @@ TheoryStrings::TheoryStrings(context::Context* c, // add checkers d_sProofChecker.registerTo(pc); } + // use the state object as the official theory state + d_theoryState = &d_state; } TheoryStrings::~TheoryStrings() { @@ -126,8 +128,6 @@ void TheoryStrings::finishInit() d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval); - - d_state.finishInit(d_equalityEngine); } std::string TheoryStrings::identify() const @@ -196,7 +196,7 @@ bool TheoryStrings::propagate(TNode literal) { // Propagate out bool ok = d_out->propagate(literal); if (!ok) { - d_state.setConflict(); + d_state.notifyInConflict(); } return ok; } @@ -762,7 +762,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ if (!d_state.isInConflict()) { Debug("strings-conflict") << "Making conflict..." << std::endl; - d_state.setConflict(); + d_state.notifyInConflict(); TrustNode conflictNode = explain(a.eqNode(b)); Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode.getNode() |