diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-18 18:42:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-18 18:42:46 -0500 |
| commit | 912ada0fb5368f3420b455b8bc76e88db164c37c (patch) | |
| tree | 0452820fe6d4df223681bcc28817b7d928261e81 /src/smt/witness_form.h | |
| parent | 738676c39badd9a03db0feaa00bb4bd467f0600a (diff) | |
(proof-new) Witness axiom reconstruction for purification skolems (#5289)
This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.
This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
Diffstat (limited to 'src/smt/witness_form.h')
| -rw-r--r-- | src/smt/witness_form.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 50c913ae9..eb0cf3005 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -81,6 +81,10 @@ class WitnessFormGenerator : public ProofGenerator * of this class (d_tcpg). */ Node convertToWitnessForm(Node t); + /** + * Return a proof generator that can prove the given axiom exists. + */ + ProofGenerator* convertExistsInternal(Node exists); /** The term conversion proof generator */ TConvProofGenerator d_tcpg; /** The nodes we have already added rewrite steps for in d_tcpg */ @@ -89,6 +93,8 @@ class WitnessFormGenerator : public ProofGenerator std::unordered_set<Node, NodeHashFunction> d_eqs; /** Lazy proof storing witness intro steps */ LazyCDProof d_wintroPf; + /** CDProof for justifying purification existentials */ + CDProof d_pskPf; }; } // namespace smt |