From: Andrew Reynolds Date: Thu, 9 Sep 2021 03:05:42 +0000 (-0500) Subject: Add difficulty post-processor (#7150) X-Git-Tag: cvc5-1.0.0~1248 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d184659d9dafc1719076d2949beb1e9f92865ae9;p=cvc5.git Add difficulty post-processor (#7150) This is work towards supporting a (get-difficulty) command. This is a helper class for transforming the difficulty of preprocessed assertions to difficulty of the input assertions. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4484f9447..401fc5976 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -294,6 +294,8 @@ libcvc5_add_sources( smt/check_models.h smt/command.cpp smt/command.h + smt/difficulty_post_processor.cpp + smt/difficulty_post_processor.h smt/dump.cpp smt/dump.h smt/dump_manager.cpp diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp new file mode 100644 index 000000000..748092238 --- /dev/null +++ b/src/smt/difficulty_post_processor.cpp @@ -0,0 +1,77 @@ +/****************************************************************************** + * 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 "smt/difficulty_post_processor.h" + +#include "smt/env.h" +#include "util/rational.h" + +using namespace cvc5::kind; +using namespace cvc5::theory; + +namespace cvc5 { +namespace smt { + +DifficultyPostprocessCallback::DifficultyPostprocessCallback() + : d_currDifficulty(0) +{ +} + +bool DifficultyPostprocessCallback::setCurrentDifficulty(Node d) +{ + if (d.isConst() && d.getType().isInteger() + && d.getConst().sgn() >= 0 + && d.getConst().getNumerator().fitsUnsignedInt()) + { + d_currDifficulty = d.getConst().getNumerator().toUnsignedInt(); + return true; + } + return false; +} + +bool DifficultyPostprocessCallback::shouldUpdate(std::shared_ptr pn, + const std::vector& fa, + bool& continueUpdate) +{ + PfRule r = pn->getRule(); + if (r == PfRule::ASSUME) + { + Trace("difficulty-debug") + << " found assume: " << pn->getResult() << std::endl; + d_accMap[pn->getResult()] += d_currDifficulty; + } + else if (r == PfRule::MACRO_SR_EQ_INTRO || r == PfRule::MACRO_SR_PRED_INTRO) + { + // premise is just a substitution, ignore + continueUpdate = false; + return false; + } + return true; +} + +void DifficultyPostprocessCallback::getDifficultyMap( + std::map& dmap) const +{ + Assert(dmap.empty()); + NodeManager* nm = NodeManager::currentNM(); + for (const std::pair& d : d_accMap) + { + dmap[d.first] = nm->mkConst(Rational(d.second)); + } +} + +} // namespace smt +} // namespace cvc5 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 + +#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 pn, + const std::vector& fa, + bool& continueUpdate) override; + /** Get the (acculumated) difficulty map for the last processed proof node */ + void getDifficultyMap(std::map& 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 d_accMap; +}; + +} // namespace smt +} // namespace cvc5 + +#endif