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/extf_solver.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/extf_solver.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index fd50e78ee..6051bc4ca 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -132,7 +132,7 @@ bool ExtfSolver::doReduction(int effort, Node n) } // this depends on the current assertions, so this // inference is context-dependent - d_extt.markReduced(n, true); + d_extt.markReduced(n, ExtReducedId::STRINGS_NEG_CTN_DEQ, true); return true; } else @@ -183,7 +183,7 @@ bool ExtfSolver::doReduction(int effort, Node n) Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n << " => " << eq << std::endl; // context-dependent because it depends on the polarity of n itself - d_extt.markReduced(n, true); + d_extt.markReduced(n, ExtReducedId::STRINGS_POS_CTN, true); } else if (k != kind::STRING_TO_CODE) { @@ -297,7 +297,7 @@ void ExtfSolver::checkExtfEval(int effort) { if (effort < 3) { - d_extt.markReduced(n); + d_extt.markReduced(n, ExtReducedId::STRINGS_SR_CONST); Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; std::vector<Node> exps; @@ -549,7 +549,7 @@ void ExtfSolver::checkExtfInference(Node n, else if (d_extt.hasFunctionKind(conc.getKind())) { // can mark as reduced, since model for n implies model for conc - d_extt.markReduced(conc); + d_extt.markReduced(conc, ExtReducedId::STRINGS_CTN_DECOMPOSE); } } } @@ -730,9 +730,10 @@ std::string ExtfSolver::debugPrintModel() for (const Node& n : extf) { ss << "- " << n; - if (!d_extt.isActive(n)) + ExtReducedId id; + if (!d_extt.isActive(n, id)) { - ss << " :extt-inactive"; + ss << " :extt-inactive " << id; } if (!d_extfInfoTmp[n].d_modelActive) { |