diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-09 15:21:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-09 15:21:08 -0500 |
| commit | 68df2d8d6c9218fe6a9bf01d22c7dfe2abdf684d (patch) | |
| tree | 672f3d0953e7de0f50ccbaa173afc360e4b19bfe /src/CMakeLists.txt | |
| parent | c64575b7c65a9822955efbf7711736068394899a (diff) | |
Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)
This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.
The number of inferences can then be seen with --stats:
nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.
This also adds a few high level stats to the new statistics class for non-linear.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1b7236d3a..9331b1dc7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -302,6 +302,8 @@ libcvc4_add_sources( theory/arith/matrix.h theory/arith/nl/iand_solver.cpp theory/arith/nl/iand_solver.h + theory/arith/nl/inference.cpp + theory/arith/nl/inference.h theory/arith/nl/nl_constraint.cpp theory/arith/nl/nl_constraint.h theory/arith/nl/nl_lemma_utils.cpp @@ -314,6 +316,8 @@ libcvc4_add_sources( theory/arith/nl/nl_solver.h theory/arith/nl/nonlinear_extension.cpp theory/arith/nl/nonlinear_extension.h + theory/arith/nl/stats.cpp + theory/arith/nl/stats.h theory/arith/nl/transcendental_solver.cpp theory/arith/nl/transcendental_solver.h theory/arith/normal_form.cpp |