diff options
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. |