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/smt/proof_manager.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/smt/proof_manager.h')
-rw-r--r-- | src/smt/proof_manager.h | 42 |
1 files changed, 31 insertions, 11 deletions
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 1916f0162..be05fc2f7 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -17,6 +17,7 @@ #ifndef CVC4__SMT__PROOF_MANAGER_H #define CVC4__SMT__PROOF_MANAGER_H +#include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/node.h" #include "expr/proof_checker.h" @@ -32,6 +33,7 @@ class SmtEngine; namespace smt { class Assertions; +class DefinedFunction; /** * This class is responsible for managing the proof output of SmtEngine, as @@ -39,31 +41,41 @@ class Assertions; */ class PfManager { + /** The type of our internal map of defined functions */ + using DefinedFunctionMap = + context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>; + public: PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** * Print the proof on the output channel of the current options in scope. * - * The argument pg is the module that can provide a proof for false in the - * current context. + * The argument pfn is the proof for false in the current context. * * Throws an assertion failure if pg cannot provide a closed proof with - * respect to assertions in as. + * respect to assertions in as and df. For the latter, entries in the defined + * function map correspond to equalities of the form (= f (lambda (...) t)), + * which are considered assertions in the final proof. */ - void printProof(ProofGenerator* pg, Assertions& as); + void printProof(std::shared_ptr<ProofNode> pfn, + Assertions& as, + DefinedFunctionMap& df); /** * Check proof, same as above, without printing. */ - void checkProof(ProofGenerator* pg, Assertions& as); + void checkProof(std::shared_ptr<ProofNode> pfn, + Assertions& as, + DefinedFunctionMap& df); /** * Get final proof. * - * The argument pg is the module that can provide a proof for false in the - * current context. + * The argument pfn is the proof for false in the current context. */ - std::shared_ptr<ProofNode> getFinalProof(ProofGenerator* pg, Assertions& as); + std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn, + Assertions& as, + DefinedFunctionMap& df); //--------------------------- access to utilities /** Get a pointer to the ProofChecker owned by this. */ ProofChecker* getProofChecker() const; @@ -74,10 +86,18 @@ class PfManager //--------------------------- end access to utilities private: /** - * Set final proof, which initializes d_finalProof to the proof of false - * from pg, postprocesses it, and stores it in d_finalProof. + * Set final proof, which initializes d_finalProof to the given proof node of + * false, postprocesses it, and stores it in d_finalProof. + */ + void setFinalProof(std::shared_ptr<ProofNode> pfn, + Assertions& as, + DefinedFunctionMap& df); + /** + * Get assertions from the assertions */ - void setFinalProof(ProofGenerator* pg, context::CDList<Node>* al); + void getAssertions(Assertions& as, + DefinedFunctionMap& df, + std::vector<Node>& assertions); /** The false node */ Node d_false; /** For the new proofs module */ |