projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d1c5cb) | patch
Add branch and bound (#6865)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 12 Jul 2021 20:59:25 +0000 (15:59 -0500)
committerGitHub <noreply@github.com>
Mon, 12 Jul 2021 20:59:25 +0000 (20:59 +0000)
commitea0b6105f1bd2ce86ce2f5a07a6255801d6d7e64
treed0a8c648fba02126b6b62f20bf9190e063b55137tree
parent7d1c5cbef46f316d044a73ad11fac8a64c864f2ccommit | diff
Add branch and bound (#6865)

This PR moves https://github.com/cvc5/cvc5/blob/master/src/theory/arith/theory_arith_private.cpp#L3451 to its own module.

The next PR will connect this module to theory_arith / theory_arith_private.

Towards ensuring type constraints are met for linear arithmetic models.
src/CMakeLists.txt diff | blob | history
src/theory/arith/branch_and_bound.cpp [new file with mode: 0644] blob
src/theory/arith/branch_and_bound.h [new file with mode: 0644] blob