diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-09-09 19:48:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-09 19:48:18 -0700 |
commit | 25597467c8df64c36e8353bfcf9d99d02fdd798b (patch) | |
tree | 9be8240f0ce11022100072bb6fb46c61ff448420 /src/smt/difficulty_post_processor.h | |
parent | 5fbc99c94d65b7e3fc0212e9f1e49ae8907643fe (diff) | |
parent | 5369982ff5c493f72e6f8309d8be632866314805 (diff) |
Merge branch 'master' into stdAttrsstdAttrs
Diffstat (limited to 'src/smt/difficulty_post_processor.h')
-rw-r--r-- | src/smt/difficulty_post_processor.h | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/src/smt/difficulty_post_processor.h b/src/smt/difficulty_post_processor.h new file mode 100644 index 000000000..ef1c9a9ea --- /dev/null +++ b/src/smt/difficulty_post_processor.h @@ -0,0 +1,88 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of module for processing the difficulty of input assumptions + * based on proof nodes. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H +#define CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H + +#include <map> + +#include "proof/proof_node_updater.h" + +namespace cvc5 { +namespace smt { + +/** + * A postprocess callback that computes difficulty based on the structure + * of the proof. In particular, this class assesses what the source of an + * assertion was by considering the shape of the proof. For instance, if + * assertion A entails x=t, and this was used to derive a substitution + * { x -> t } to assertion B, then B is the source of B*{ x -> t }. The + * difficulty of this assertion is carried to B and not A. The reason is that + * A can be understood as a definition, and is eliminated, whereas B was + * persistent if B*{ x -> t } was a prepreprocessed assertion. + * + * Note that this postprocess callback is intended to be run on the proof + * of a single preprocessed assertion C. If C was derived by proof with + * free assumptions A_1, ..., A_n, then for each A_i that is a "source" as + * described above, we increment the difficulty of A_i by the difficulty value + * assigned to C. + * + * This means that the user of this method should: + * (1) assign the current difficulty we are incrementing (setCurrentDifficulty), + * (2) process the proof using a proof node updater with this callback. + * The final difficulty map is accumulated in d_accMap, which can be accessed + * at any time via getDifficultyMap. + */ +class DifficultyPostprocessCallback : public ProofNodeUpdaterCallback +{ + public: + DifficultyPostprocessCallback(); + ~DifficultyPostprocessCallback() {} + /** + * Set current difficulty of the next proof to process to the (integer) + * value stored in Node d. This value will be assigned to all the free + * assumptions of the proof we traverse next. This value is stored in + * d_currDifficulty. + * + * @return true if the difficulty value was successfully extracted + */ + bool setCurrentDifficulty(Node d); + /** + * Should proof pn be updated? This is used to selectively traverse to e.g. + * the source of an assertion. + */ + bool shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, + bool& continueUpdate) override; + /** Get the (acculumated) difficulty map for the last processed proof node */ + void getDifficultyMap(std::map<Node, Node>& dmap) const; + + private: + /** + * The current difficulty of the assertion whose proof of preprocessing + * we are considering. + */ + uint64_t d_currDifficulty; + /** The current accumulated difficulty map */ + std::map<Node, uint64_t> d_accMap; +}; + +} // namespace smt +} // namespace cvc5 + +#endif |