diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-03 16:14:59 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-03 16:14:59 -0600 |
| commit | 01d8991ad7059fff4807c2c597c04959d39ab176 (patch) | |
| tree | c18ef1c577c8470927f3beddfb254f0c166edfe0 /src/prop/prop_engine.h | |
| parent | 5e79f55ac4a2e21834b094f44a344f333f74e8b0 (diff) | |
(proof-new) Updates to SMT proof manager and SmtEngine (#5446)
This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode.
This makes it so that it only remains to make PropEngine to be proof producing.
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1fb79231d..e4d536c29 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -219,6 +219,13 @@ class PropEngine */ bool properExplanation(TNode node, TNode expl) const; + /** + * Return the prop engine proof. This should be called only when proofs are + * enabled. Returns a proof of false whose free assumptions are the + * preprocessed assertions. + */ + std::shared_ptr<ProofNode> getProof(); + private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); |