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/nl/nonlinear_extension.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/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
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()) { |