diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 17:42:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-13 17:42:57 -0500 |
| commit | 1cb249c9dd06a049953f001cd6d82c0e6f1246f2 (patch) | |
| tree | 000398841f1869d9911e1e496623520ffb6de21a /src/theory/trust_node.h | |
| parent | a34f29798b3f4d1f83e1ced57fe53db53b9956f0 (diff) | |
(proof-new) SMT Preprocess proof generator (#4708)
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.
It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
Diffstat (limited to 'src/theory/trust_node.h')
| -rw-r--r-- | src/theory/trust_node.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index a3c0fbec5..ff174b63e 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -18,6 +18,7 @@ #define CVC4__THEORY__TRUST_NODE_H #include "expr/node.h" +#include "expr/proof_node.h" namespace CVC4 { @@ -127,6 +128,11 @@ class TrustNode ProofGenerator* getGenerator() const; /** is null? */ bool isNull() const; + /** + * Gets the proof node for this trust node, which is obtained by + * calling the generator's getProofFor method on the proven node. + */ + std::shared_ptr<ProofNode> toProofNode(); /** Get the proven formula corresponding to a conflict call */ static Node getConflictProven(Node conf); |