(cad-solver) Fix square-free-basis computation (#5085)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 17 Sep 2020 20:44:53 +0000 (22:44 +0200)
committerGitHub <noreply@github.com>
Thu, 17 Sep 2020 20:44:53 +0000 (15:44 -0500)
commit6cc837f99a37287bf583491649797486650f77e7
tree22974bc24c4e5b93643ad5ed5acea3e2e4fcab36
parentbd6f48ec9ecdd0547b77e9e8a49d3028f4281fe0
(cad-solver) Fix square-free-basis computation (#5085)

This PR fixes a subtle issue when making the polynomials of two subsequent (overlapping) intervals relative square-free. We now make sure that the resulting polynomials are ignored (if constant) or pushed to the lower dimension (if lower main variable). Also, we now appropriately update the main polynomials of the corresponding intervals.
src/theory/arith/nl/cad/cdcac.cpp
src/theory/arith/nl/cad/cdcac_utils.cpp
src/theory/arith/nl/cad/cdcac_utils.h
src/theory/arith/nl/cad/projections.cpp
src/theory/arith/nl/cad/projections.h