projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e5358e4) | patch
Add identifiers for extended function reductions (#6314)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 9 Apr 2021 19:21:11 +0000 (14:21 -0500)
committerGitHub <noreply@github.com>
Fri, 9 Apr 2021 19:21:11 +0000 (19:21 +0000)
commit6923f0cb9930332a61e187d3b4d1a7ec7e65b15c
treedc6712e1b30352c60c9ca2f091b38136e2e92108tree
parente5358e498db6d934d0b8704cfd023b0f67b6fbc0commit | 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.
src/theory/arith/nl/ext_theory_callback.cpp diff | blob | history
src/theory/arith/nl/ext_theory_callback.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/ext_theory.cpp diff | blob | history
src/theory/ext_theory.h diff | blob | history
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/inference_manager.h diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history