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/arith | |
| 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/arith')
| -rw-r--r-- | src/theory/arith/nl/ext_theory_callback.cpp | 14 | ||||
| -rw-r--r-- | src/theory/arith/nl/ext_theory_callback.h | 3 | ||||
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 1 |
3 files changed, 11 insertions, 7 deletions
diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 72848ac89..8fa1a56c9 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -69,17 +69,21 @@ bool NlExtTheoryCallback::getCurrentSubstitution( return retVal; } -bool NlExtTheoryCallback::isExtfReduced(int effort, - Node n, - Node on, - std::vector<Node>& exp) +bool NlExtTheoryCallback::isExtfReduced( + int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id) { if (n != d_zero) { Kind k = n.getKind(); - return k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND; + if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND) + { + id = ExtReducedId::ARITH_SR_LINEAR; + return true; + } + return false; } Assert(n == d_zero); + id = ExtReducedId::ARITH_SR_ZERO; if (on.getKind() == NONLINEAR_MULT) { Trace("nl-ext-zero-exp") diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index 0e0e1411b..78ea3b2b6 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -72,7 +72,8 @@ class NlExtTheoryCallback : public ExtTheoryCallback bool isExtfReduced(int effort, Node n, Node on, - std::vector<Node>& exp) override; + std::vector<Node>& exp, + ExtReducedId& id) override; private: /** The underlying equality engine. */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 16142886f..20d64b0d5 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -248,7 +248,6 @@ void NonlinearExtension::check(Theory::Effort e) Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl; if (e == Theory::EFFORT_FULL) { - d_extTheory.clearCache(); d_needsLastCall = true; if (options::nlExtRewrites()) { |