projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c84db77) | patch
Add CAD-based solver (#4834)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 4 Aug 2020 10:57:34 +0000 (12:57 +0200)
committerGitHub <noreply@github.com>
Tue, 4 Aug 2020 10:57:34 +0000 (05:57 -0500)
commit4844afa3d254bdabac397556e166a2534bb6c2ac
tree1da4a957cf073c25c6cfc9a7393afe29a1b14b3btree
parentc84db77ecdaa7107a33824484bf9c649f8fcbbffcommit | diff
Add CAD-based solver (#4834)

Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail:

add --nl-cad option
add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation
add new Inference types for the NlLemma class
use CadSolver in NonlinearExtension (if --nl-cad is given)
src/CMakeLists.txt diff | blob | history
src/options/arith_options.toml diff | blob | history
src/theory/arith/nl/cad_solver.cpp [new file with mode: 0644] blob
src/theory/arith/nl/cad_solver.h [new file with mode: 0644] blob
src/theory/arith/nl/inference.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history