Add naive support for integer variables. (#4835)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 12 Aug 2020 15:01:58 +0000 (17:01 +0200)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 15:01:58 +0000 (10:01 -0500)
commit3f77b4ac0d4ff8ab69e2f2932e9ced088bd339ed
tree2d1448d22d06afef93e3a0afb763d6ed20f14a43
parenta852ea2c368a81c37eadccc02b3d36aec1a55c12
Add naive support for integer variables. (#4835)

This PR adds naive support for integer reasoning to the CAD-based solver.
Essentially, it checks whether the sampled value is integral. If this is not the case, we "invent" a new interval covering the area between the two neighbouring integers with appropriate border polynomials.
src/theory/arith/nl/cad/cdcac.cpp
src/theory/arith/nl/cad/cdcac.h