projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c2311f9) | patch
(proof-new) Add proof generator for CAD solver (#5964)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 23 Feb 2021 16:17:45 +0000 (17:17 +0100)
committerGitHub <noreply@github.com>
Tue, 23 Feb 2021 16:17:45 +0000 (17:17 +0100)
commit7a695fd7c29af97dbcc363eb277ffeae1617cffe
treeae3ae02313dadfb126b9c76ded8aadc3e743120ftree
parentc2311f97441befbf10e80ab597455b3ab8ccc10ccommit | diff
(proof-new) Add proof generator for CAD solver (#5964)

This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
src/CMakeLists.txt diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/arith/nl/cad/proof_checker.cpp [new file with mode: 0644] blob
src/theory/arith/nl/cad/proof_checker.h [new file with mode: 0644] blob
src/theory/arith/nl/cad/proof_generator.cpp [new file with mode: 0644] blob
src/theory/arith/nl/cad/proof_generator.h [new file with mode: 0644] blob