projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63d27f0) | patch
[proof-new] Implementing getProof in the API and SMT engine (#5751)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 8 Jan 2021 16:38:24 +0000 (13:38 -0300)
committerGitHub <noreply@github.com>
Fri, 8 Jan 2021 16:38:24 +0000 (13:38 -0300)
commit2958e98eff88ce14aefcdeee3c6ec579fcc2bb1d
treeaf304364b3fdd8f98663b4dcfb2d2632719f0ee2tree
parent63d27f031f8942607d869080d0e2cfb6078d40b1commit | diff
[proof-new]  Implementing getProof in the API and SMT engine (#5751)

A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).
src/api/cvc4cpp.cpp diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/command.h diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
src/smt/proof_manager.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history