projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2043e2a) | patch
Make sure polynomials are properly factorized in nl-cad (#5733)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 7 Jan 2021 21:55:31 +0000 (22:55 +0100)
committerGitHub <noreply@github.com>
Thu, 7 Jan 2021 21:55:31 +0000 (15:55 -0600)
commit497a685f14ff12eb05e4aa6ad7b05682609bf7a9
tree198953b8dee2cd38ab1da59afb4d9f882a93022atree
parent2043e2a4f57942b6b81ae437de8a2aa00ffcd32fcommit | diff
Make sure polynomials are properly factorized in nl-cad (#5733)

CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.
src/theory/arith/nl/cad/cdcac.cpp diff | blob | history
src/theory/arith/nl/cad/cdcac.h diff | blob | history
src/theory/arith/nl/cad/cdcac_utils.cpp diff | blob | history
src/theory/arith/nl/cad/cdcac_utils.h diff | blob | history
src/theory/arith/nl/cad/projections.cpp diff | blob | history
src/theory/arith/nl/cad/projections.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/issue5726-downpolys.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/issue5726-sqfactor.smt2 [new file with mode: 0644] blob