diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/proof_manager.cpp | 24 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 36 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.h | 18 |
3 files changed, 67 insertions, 11 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index b651e390c..846df7e41 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -34,7 +34,27 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pnm(new ProofNodeManager(d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), u, "smt::PreprocessProofGenerator")), - d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())), + d_pfpp(new ProofPostproccess( + d_pnm.get(), + smte, + d_pppg.get(), + // by default the post-processor will update all assumptions, which + // can lead to SCOPE subproofs of the form + // A + // ... + // B1 B2 + // ... ... + // ------------ + // C + // ------------- SCOPE [B1, B2] + // B1 ^ B2 => C + // + // where A is an available assumption from outside the scope (note + // that B1 was an assumption of this SCOPE subproof but since it could + // be inferred from A, it was updated). This shape is problematic for + // the veriT reconstruction, so we disable the update of scoped + // assumptions (which would disable the update of B1 in this case). + options::proofFormatMode() != options::ProofFormatMode::VERIT)), d_finalProof(nullptr) { // add rules to eliminate here @@ -131,7 +151,7 @@ void PfManager::printProof(std::ostream& out, } // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node - + if (options::proofFormatMode() == options::ProofFormatMode::DOT) { proof::DotPrinter::print(out, fp.get()); diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index dedb686c3..a27a5697e 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -33,12 +33,15 @@ namespace smt { ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg) - : d_pnm(pnm), d_smte(smte), d_pppg(pppg), d_wfpm(pnm) + ProofGenerator* pppg, + bool updateScopedAssumptions) + : d_pnm(pnm), + d_smte(smte), + d_pppg(pppg), + d_wfpm(pnm), + d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); - // always check whether to update ASSUME - d_elimRules.insert(PfRule::ASSUME); } void ProofPostprocessCallback::initializeUpdate() @@ -53,9 +56,26 @@ void ProofPostprocessCallback::setEliminateRule(PfRule rule) } bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, bool& continueUpdate) { - return d_elimRules.find(pn->getRule()) != d_elimRules.end(); + PfRule id = pn->getRule(); + if (d_elimRules.find(id) != d_elimRules.end()) + { + return true; + } + // other than elimination rules, we always update assumptions as long as + // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in + // fa + if (id != PfRule::ASSUME + || (!d_updateScopedAssumptions + && std::find(fa.begin(), fa.end(), pn->getResult()) != fa.end())) + { + Trace("smt-proof-pp-debug") + << "... not updating in-scope assumption " << pn->getResult() << "\n"; + return false; + } + return true; } bool ProofPostprocessCallback::update(Node res, @@ -1108,6 +1128,7 @@ void ProofPostprocessFinalCallback::initializeUpdate() } bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, bool& continueUpdate) { PfRule r = pn->getRule(); @@ -1146,9 +1167,10 @@ bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg) + ProofGenerator* pppg, + bool updateScopedAssumptions) : d_pnm(pnm), - d_cb(pnm, smte, pppg), + d_cb(pnm, smte, pppg, updateScopedAssumptions), // the update merges subproofs d_updater(d_pnm, d_cb, true), d_finalCb(pnm), diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 9f3e7e55b..4111e83de 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -40,7 +40,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback public: ProofPostprocessCallback(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg); + ProofGenerator* pppg, + bool updateScopedAssumptions); ~ProofPostprocessCallback() {} /** * Initialize, called once for each new ProofNode to process. This initializes @@ -56,6 +57,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback void setEliminateRule(PfRule rule); /** Should proof pn be updated? */ bool shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, bool& continueUpdate) override; /** Update the proof rule application. */ bool update(Node res, @@ -80,6 +82,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback std::vector<Node> d_wfAssumptions; /** Kinds of proof rules we are eliminating */ std::unordered_set<PfRule, PfRuleHashFunction> d_elimRules; + /** Whether we post-process assumptions in scope. */ + bool d_updateScopedAssumptions; //---------------------------------reset at the begining of each update /** Mapping assumptions to their proof from preprocessing */ std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof; @@ -244,6 +248,7 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback void initializeUpdate(); /** Should proof pn be updated? Returns false, adds to stats. */ bool shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, bool& continueUpdate) override; /** was pedantic failure */ bool wasPedanticFailure(std::ostream& out) const; @@ -274,9 +279,18 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback class ProofPostproccess { public: + /** + * @param pnm The proof node manager we are using + * @param smte The SMT engine whose proofs are being post-processed + * @param pppg The proof generator for pre-processing proofs + * @param updateScopedAssumptions Whether we post-process assumptions in + * scope. Since doing so is sound and only problematic depending on who is + * consuming the proof, it's true by default. + */ ProofPostproccess(ProofNodeManager* pnm, SmtEngine* smte, - ProofGenerator* pppg); + ProofGenerator* pppg, + bool updateScopedAssumptions = true); ~ProofPostproccess(); /** post-process */ void process(std::shared_ptr<ProofNode> pf); |