diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-14 14:58:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-14 19:58:01 +0000 |
commit | 1014428633ca233aa0c51818d995acaca6ebfda6 (patch) | |
tree | 91264d548a5b678a07eeba0c197f3a1e5eb3d7f6 /src/smt/proof_manager.h | |
parent | 8ad6a175415d74d4a5bcf5d3e04816277a237ccc (diff) |
Add proof manager method to translate difficulty map (#7159)
This method will be called from SmtEngine in the implementation for (get-difficulty).
Diffstat (limited to 'src/smt/proof_manager.h')
-rw-r--r-- | src/smt/proof_manager.h | 17 |
1 files changed, 17 insertions, 0 deletions
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. |