diff options
| -rw-r--r-- | src/smt/proof_manager.cpp | 53 | ||||
| -rw-r--r-- | src/smt/proof_manager.h | 17 |
2 files changed, 70 insertions, 0 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 2c3a22a78..4d6e2b495 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -24,6 +24,7 @@ #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "smt/assertions.h" +#include "smt/difficulty_post_processor.h" #include "smt/env.h" #include "smt/preprocess_proof_generator.h" #include "smt/proof_post_processor.h" @@ -195,6 +196,58 @@ void PfManager::checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as) << std::endl; } +void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap, + Assertions& as) +{ + Trace("difficulty") << "PfManager::translateDifficultyMap" << std::endl; + if (dmap.empty()) + { + return; + } + std::map<Node, Node> dmapp = dmap; + dmap.clear(); + std::vector<Node> ppAsserts; + for (const std::pair<const Node, Node>& ppa : dmapp) + { + Trace("difficulty") << " preprocess difficulty: " << ppa.second << " for " + << ppa.first << std::endl; + ppAsserts.push_back(ppa.first); + } + // assume a SAT refutation from all input assertions that were marked + // as having a difficulty + CDProof cdp(d_pnm.get()); + Node fnode = NodeManager::currentNM()->mkConst(false); + cdp.addStep(fnode, PfRule::SAT_REFUTATION, ppAsserts, {}); + std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode); + std::shared_ptr<ProofNode> fpf = getFinalProof(pf, as); + Trace("difficulty-debug") << "Final proof is " << *fpf.get() << std::endl; + Assert(fpf->getRule() == PfRule::SCOPE); + fpf = fpf->getChildren()[0]; + // analyze proof + Assert(fpf->getRule() == PfRule::SAT_REFUTATION); + const std::vector<std::shared_ptr<ProofNode>>& children = fpf->getChildren(); + DifficultyPostprocessCallback dpc; + ProofNodeUpdater dpnu(d_pnm.get(), dpc); + // For each child of SAT_REFUTATION, we increment the difficulty on all + // "source" free assumptions (see DifficultyPostprocessCallback) by the + // difficulty of the preprocessed assertion. + for (const std::shared_ptr<ProofNode>& c : children) + { + Node res = c->getResult(); + Assert(dmapp.find(res) != dmapp.end()); + Trace("difficulty-debug") << " process: " << res << std::endl; + Trace("difficulty-debug") << " .dvalue: " << dmapp[res] << std::endl; + Trace("difficulty-debug") << " ..proof: " << *c.get() << std::endl; + if (!dpc.setCurrentDifficulty(dmapp[res])) + { + continue; + } + dpnu.process(c); + } + // get the accumulated difficulty map from the callback + dpc.getDifficultyMap(dmap); +} + ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); } ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); } diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 034a4554f..45be71771 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -96,6 +96,23 @@ class PfManager : protected EnvObj void checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as); /** + * Translate difficulty map. This takes a mapping dmap from preprocessed + * assertions to values estimating their difficulty. It translates this + * map so that dmap contains a mapping from *input* assertions to values + * estimating their difficulty. + * + * It does this translation by constructing a proof of preprocessing for all + * preprocessed assertions marked as having a difficulty, traversing those + * proofs, and conditionally incrementing the difficulty of the input + * assertion on which they depend. This is based on whether the free + * assumption is the "source" of an assertion. + * + * @param dmap Map estimating the difficulty of preprocessed assertions + * @param as The input assertions + */ + void translateDifficultyMap(std::map<Node, Node>& dmap, Assertions& as); + + /** * Get final proof. * * The argument pfn is the proof for false in the current context. |