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/smt_engine.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/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 091f69642..558bd2b40 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -684,6 +684,12 @@ class CVC4_PUBLIC SmtEngine UnsatCore getUnsatCore(); /** + * Get a refutation proof (only if immediately preceded by an UNSAT or + * ENTAILED query). Only permitted if CVC4 was built with proof support and + * the proof option is on. */ + std::string getProof(); + + /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. */ |