projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6d45b6f) | patch
(proof-new) Add proofs for CAD solver (#5981)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 24 Feb 2021 15:04:59 +0000 (16:04 +0100)
committerGitHub <noreply@github.com>
Wed, 24 Feb 2021 15:04:59 +0000 (16:04 +0100)
commit6478f414ad7d6dcbf597db037e81d97175757605
tree976de5c11f2cf0b32005fe85b90f6b2d586c2213tree
parent6d45b6fb6f797eb9dc51ea70b20ec875d1dfe49dcommit | diff
(proof-new) Add proofs for CAD solver (#5981)

This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.
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_solver.cpp diff | blob | history
src/theory/arith/nl/cad_solver.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history