projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 383d061) | patch
(proof-new) Add SMT proof manager (#5054)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 12 Sep 2020 03:38:04 +0000 (22:38 -0500)
committerGitHub <noreply@github.com>
Sat, 12 Sep 2020 03:38:04 +0000 (22:38 -0500)
commit3a8a27994584ca2168ef71d5eb0ce46ef558ba34
treeefa67475c597a8fdb6664a67dd80e7b022919bd2tree
parent383d061be2bc8162d3379c98ad106555d21e5f86commit | diff
(proof-new) Add SMT proof manager (#5054)

This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.

This PR includes setting up some connections into the various modules for proof production.
src/CMakeLists.txt diff | blob | history
src/options/smt_options.toml diff | blob | history
src/preprocessing/assertion_pipeline.cpp diff | blob | history
src/smt/assertions.cpp diff | blob | history
src/smt/assertions.h diff | blob | history
src/smt/proof_manager.cpp [new file with mode: 0644] blob
src/smt/proof_manager.h [new file with mode: 0644] blob
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/smt_solver.cpp diff | blob | history
src/smt/smt_solver.h diff | blob | history