projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d03fa56) | patch
(cad-solver) Fixed excluding lemma generation. (#4958)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 28 Aug 2020 15:26:02 +0000 (17:26 +0200)
committerGitHub <noreply@github.com>
Fri, 28 Aug 2020 15:26:02 +0000 (10:26 -0500)
commit64eae4836286d95a04126d7bcffb18c5eb383bc1
tree799679356ba6e17a9684b7d94d6773c3e58e0bb3tree
parentd03fa5697e278bef5cbc385978634421cb5a050bcommit | diff
(cad-solver) Fixed excluding lemma generation. (#4958)

The lemma generation for partial cad checks had a number of issues that have been fixed in this PR.
The previous version had both soundness issues and a very naive approach to handling algebraic numbers.
This new version is sound (fingers crossed) and allows to construct more precise, but also more complex lemmas.
To avoid constructing very large lemmas, a (somewhat arbitrary) limit based on the size of coefficients was added.
src/theory/arith/nl/cad_solver.cpp diff | blob | history
src/theory/arith/nl/poly_conversion.cpp diff | blob | history
src/theory/arith/nl/poly_conversion.h diff | blob | history