diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-11 20:00:18 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-11 20:00:18 +0100 |
| commit | f5486884229348516ac26300273e4f5458a74208 (patch) | |
| tree | 8e48bd833c3e55b247adca891ec2081fc9077528 /src/theory/strings/solver_state.cpp | |
| parent | 8fcb59d072b09bfaf8f56334182d425274842461 (diff) | |
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
Diffstat (limited to 'src/theory/strings/solver_state.cpp')
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index b6e9c68f4..e42952175 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -28,7 +28,7 @@ namespace strings { SolverState::SolverState(context::Context* c, context::UserContext* u, Valuation& v) - : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false) + : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_false = NodeManager::currentNM()->mkConst(false); @@ -137,8 +137,7 @@ void SolverState::setPendingPrefixConflictWhen(Node conf) { return; } - InferInfo iiPrefixConf; - iiPrefixConf.d_id = InferenceId::STRINGS_PREFIX_CONFLICT; + InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT); iiPrefixConf.d_conc = d_false; utils::flattenOp(AND, conf, iiPrefixConf.d_premises); setPendingConflict(iiPrefixConf); |