projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4ac6c51) | patch
Integrate Lazard into CAD module (#6812)
authorGereon Kremer <nafur42@gmail.com>
Tue, 6 Jul 2021 23:01:13 +0000 (01:01 +0200)
committerGitHub <noreply@github.com>
Tue, 6 Jul 2021 23:01:13 +0000 (23:01 +0000)
commit468ba87a10e3f3fadf7c48a0b3923ecc489616ad
tree22d5645b349f7b6620c6f86c33e606c85f95954ftree
parent4ac6c5179265ef9895bc9e939be0e47b3754137ecommit | diff
Integrate Lazard into CAD module (#6812)

This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.
src/CMakeLists.txt diff | blob | history
src/options/arith_options.toml diff | blob | history
src/theory/arith/nl/cad/cdcac.cpp diff | blob | history
src/theory/arith/nl/cad/projections.cpp diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/theory_arith_cad_white.cpp [new file with mode: 0644] blob