diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-14 14:01:57 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-14 07:01:57 -0500 |
| commit | 7b7246935910173c67917ee947639ac8ab450edc (patch) | |
| tree | 08f83ed8c366e1c24e8d5a1ba451e8d3a4aceb22 /src/theory/uf | |
| parent | 02fa1dea5a8335a6bd5a1f3e8718796a9489ac8e (diff) | |
Inspect roots to avoid certain resultants (Algorithm 4, lines 8,9). (#4892)
This PR adds a small improvement to the CAD solver.
In Algorithm 4 of https://arxiv.org/pdf/2003.05633.pdf in lines 8 and 9, we only consider polynomials for resultant computations that have roots outside of the current interval.
This PR implements this check.
Fixes CVC4/cvc4-projects#210.
Diffstat (limited to 'src/theory/uf')
0 files changed, 0 insertions, 0 deletions