projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 98cdd72) | patch
Add new arithmetic BoundInference class (#5148)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 28 Sep 2020 11:48:26 +0000 (13:48 +0200)
committerGitHub <noreply@github.com>
Mon, 28 Sep 2020 11:48:26 +0000 (06:48 -0500)
commit2117152db35fe1e8cee1632303789dceda311d1a
tree6418a342f55cd23c08c56d27d517b98b4089d3edtree
parent98cdd72fca04e76eb1057d694e1dad9717351f7fcommit | 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.
src/CMakeLists.txt diff | blob | history
src/theory/arith/bound_inference.cpp [new file with mode: 0644] blob
src/theory/arith/bound_inference.h [new file with mode: 0644] blob
src/theory/arith/nl/icp/icp_solver.cpp diff | blob | history
src/theory/arith/nl/icp/icp_solver.h diff | blob | history
src/theory/arith/nl/icp/variable_bounds.cpp [deleted file] blob | history
src/theory/arith/nl/icp/variable_bounds.h [deleted file] blob | history
src/theory/arith/nl/poly_conversion.cpp diff | blob | history
src/theory/arith/nl/poly_conversion.h diff | blob | history