diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-09 14:21:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 19:21:11 +0000 |
commit | 6923f0cb9930332a61e187d3b4d1a7ec7e65b15c (patch) | |
tree | dc6712e1b30352c60c9ca2f091b38136e2e92108 /src/theory/strings/inference_manager.cpp | |
parent | e5358e498db6d934d0b8704cfd023b0f67b6fbc0 (diff) |
Add identifiers for extended function reductions (#6314)
This adds identifiers for extended function reductions, which are reasons for why an extended term no longer needs to be processed. The motivation is help understand check-model failures.
This PR adds identifiers to the ExtTheory utility. It also cleans up some unused parts of this utility. Some blocks of code changed indentation in this class.
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 8a0429fae..6f218e5be 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -268,18 +268,9 @@ bool InferenceManager::hasProcessed() const return d_state.isInConflict() || hasPending(); } -void InferenceManager::markCongruent(Node a, Node b) +void InferenceManager::markReduced(Node n, ExtReducedId id, bool contextDepend) { - Assert(a.getKind() == b.getKind()); - if (d_extt.hasFunctionKind(a.getKind())) - { - d_extt.markCongruent(a, b); - } -} - -void InferenceManager::markReduced(Node n, bool contextDepend) -{ - d_extt.markReduced(n, contextDepend); + d_extt.markReduced(n, id, contextDepend); } void InferenceManager::processConflict(const InferInfo& ii) |