diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2020-09-28 13:48:26 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-28 06:48:26 -0500 |
| commit | 2117152db35fe1e8cee1632303789dceda311d1a (patch) | |
| tree | 6418a342f55cd23c08c56d27d517b98b4089d3ed /src/CMakeLists.txt | |
| parent | 98cdd72fca04e76eb1057d694e1dad9717351f7f (diff) | |
Add new arithmetic BoundInference class (#5148)
This PR adds a new utility class that extracts bounds on single variables from theory atoms like x > 0 or y <= 17. It does not perform further reasoning (like recognizing x > y with y > 3 as a bound).
Note that the functionality was introduced in arith/nl/icp/variable_bounds.h, but is now available using Node only.
This PR also replaces the VariableBounds by BoundInference in the icp solver which allowed for checking the code.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index db274ebfb..717378b27 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -290,6 +290,8 @@ libcvc4_add_sources( theory/arith/attempt_solution_simplex.cpp theory/arith/attempt_solution_simplex.h theory/arith/bound_counts.h + theory/arith/bound_inference.cpp + theory/arith/bound_inference.h theory/arith/callbacks.cpp theory/arith/callbacks.h theory/arith/congruence_manager.cpp @@ -343,8 +345,6 @@ libcvc4_add_sources( theory/arith/nl/icp/icp_solver.h theory/arith/nl/icp/intersection.cpp theory/arith/nl/icp/intersection.h - theory/arith/nl/icp/variable_bounds.cpp - theory/arith/nl/icp/variable_bounds.h theory/arith/nl/nl_constraint.cpp theory/arith/nl/nl_constraint.h theory/arith/nl/nl_lemma_utils.cpp |