diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-08 13:38:24 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-08 13:38:24 -0300 |
| commit | 2958e98eff88ce14aefcdeee3c6ec579fcc2bb1d (patch) | |
| tree | af304364b3fdd8f98663b4dcfb2d2632719f0ee2 /src/smt/proof_manager.h | |
| parent | 63d27f031f8942607d869080d0e2cfb6078d40b1 (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).
Diffstat (limited to 'src/smt/proof_manager.h')
| -rw-r--r-- | src/smt/proof_manager.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index be05fc2f7..a6f284cad 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -49,7 +49,7 @@ class PfManager PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** - * Print the proof on the output channel of the current options in scope. + * Print the proof on the given output stream. * * The argument pfn is the proof for false in the current context. * @@ -58,7 +58,8 @@ class PfManager * function map correspond to equalities of the form (= f (lambda (...) t)), * which are considered assertions in the final proof. */ - void printProof(std::shared_ptr<ProofNode> pfn, + void printProof(std::ostream& out, + std::shared_ptr<ProofNode> pfn, Assertions& as, DefinedFunctionMap& df); /** |