From 4b0650bfe0c1df81ad3236def912543510932320 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 15:54:22 -0500 Subject: Improve pre-skolemization, move quantifiers preprocess to own file (#7153) This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache. It makes minor cleanup to the dependencies of this method. --- src/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ba88080b8..5c898b654 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -855,6 +855,8 @@ libcvc5_add_sources( theory/quantifiers/quantifiers_macros.h theory/quantifiers/quantifiers_modules.cpp theory/quantifiers/quantifiers_modules.h + theory/quantifiers/quantifiers_preprocess.cpp + theory/quantifiers/quantifiers_preprocess.h theory/quantifiers/quantifiers_registry.cpp theory/quantifiers/quantifiers_registry.h theory/quantifiers/quantifiers_rewriter.cpp -- cgit v1.2.3 From b9dcd4d141cef256b4371aa103af4ee1aa7c61bd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 16:42:30 -0500 Subject: Add Lfsc print channel utilities (#7123) These are utilities used for two-pass printing of LFSC proofs. --- src/CMakeLists.txt | 2 + src/proof/lfsc/lfsc_print_channel.cpp | 161 ++++++++++++++++++++++++++++++++++ src/proof/lfsc/lfsc_print_channel.h | 128 +++++++++++++++++++++++++++ 3 files changed, 291 insertions(+) create mode 100644 src/proof/lfsc/lfsc_print_channel.cpp create mode 100644 src/proof/lfsc/lfsc_print_channel.h (limited to 'src/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5c898b654..4484f9447 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -182,6 +182,8 @@ libcvc5_add_sources( proof/lfsc/lfsc_list_sc_node_converter.h proof/lfsc/lfsc_node_converter.cpp proof/lfsc/lfsc_node_converter.h + proof/lfsc/lfsc_print_channel.cpp + proof/lfsc/lfsc_print_channel.h proof/lfsc/lfsc_util.cpp proof/lfsc/lfsc_util.h proof/method_id.cpp diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp new file mode 100644 index 000000000..36fd8831b --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.cpp @@ -0,0 +1,161 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "proof/lfsc/lfsc_print_channel.h" + +#include + +#include "proof/lfsc/lfsc_util.h" + +namespace cvc5 { +namespace proof { + +LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {} +void LfscPrintChannelOut::printNode(TNode n) +{ + d_out << " "; + printNodeInternal(d_out, n); +} + +void LfscPrintChannelOut::printTypeNode(TypeNode tn) +{ + d_out << " "; + printTypeNodeInternal(d_out, tn); +} + +void LfscPrintChannelOut::printHole() { d_out << " _ "; } +void LfscPrintChannelOut::printTrust(TNode res, PfRule src) +{ + d_out << std::endl << "(trust "; + printNodeInternal(d_out, res); + d_out << ") ; from " << src << std::endl; +} + +void LfscPrintChannelOut::printOpenRule(const ProofNode* pn) +{ + d_out << std::endl << "("; + printRule(d_out, pn); +} + +void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr) +{ + d_out << std::endl << "(" << lr; +} + +void LfscPrintChannelOut::printCloseRule(size_t nparen) +{ + for (size_t i = 0; i < nparen; i++) + { + d_out << ")"; + } +} + +void LfscPrintChannelOut::printProofId(size_t id) +{ + d_out << " "; + printProofId(d_out, id); +} +void LfscPrintChannelOut::printAssumeId(size_t id) +{ + d_out << " "; + printAssumeId(d_out, id); +} + +void LfscPrintChannelOut::printEndLine() { d_out << std::endl; } + +void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + tn.toStream(ss, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn) +{ + if (pn->getRule() == PfRule::LFSC_RULE) + { + const std::vector& args = pn->getArguments(); + out << getLfscRule(args[0]); + return; + } + // Otherwise, convert to lower case + std::stringstream ss; + ss << pn->getRule(); + std::string rname = ss.str(); + std::transform( + rname.begin(), rname.end(), rname.begin(), [](unsigned char c) { + return std::tolower(c); + }); + out << rname; +} + +void LfscPrintChannelOut::printId(std::ostream& out, size_t id) +{ + out << "__t" << id; +} + +void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id) +{ + out << "__p" << id; +} + +void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id) +{ + out << "__a" << id; +} + +void LfscPrintChannelOut::cleanSymbols(std::string& s) +{ + size_t start_pos = 0; + while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos) + { + s.replace(start_pos, 3, "("); + start_pos += 1; + } + start_pos = 0; + while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos) + { + s.replace(start_pos, 10, ""); + } +} + +LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {} + +void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); } +void LfscPrintChannelPre::printTrust(TNode res, PfRule src) +{ + d_lbind.process(res); +} + +void LfscPrintChannelPre::printOpenRule(const ProofNode* pn) +{ + +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_print_channel.h b/src/proof/lfsc/lfsc_print_channel.h new file mode 100644 index 000000000..655fa192c --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.h @@ -0,0 +1,128 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H +#define CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H + +#include +#include + +#include "expr/node.h" +#include "printer/let_binding.h" +#include "proof/lfsc/lfsc_util.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * LFSC proofs are printed in two phases: the first phase computes the + * letification of terms in the proof as well as other information that is + * required for printing the preamble of the proof. The second phase prints the + * proof to an output stream. This is the base class for these two phases. + */ +class LfscPrintChannel +{ + public: + LfscPrintChannel() {} + virtual ~LfscPrintChannel() {} + /** Print node n */ + virtual void printNode(TNode n) {} + /** Print type node n */ + virtual void printTypeNode(TypeNode tn) {} + /** Print a hole */ + virtual void printHole() {} + /** + * Print an application of the trusting the result res, whose source is the + * given proof rule. + */ + virtual void printTrust(TNode res, PfRule src) {} + /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */ + virtual void printOpenRule(const ProofNode* pn) {} + /** Print the opening of LFSC rule lr, e.g. "(cong " */ + virtual void printOpenLfscRule(LfscRule lr) {} + /** Print the closing of # nparen proof rules */ + virtual void printCloseRule(size_t nparen = 1) {} + /** Print a letified proof with the given identifier */ + virtual void printProofId(size_t id) {} + /** Print a proof assumption with the given identifier */ + virtual void printAssumeId(size_t id) {} + /** Print an end line */ + virtual void printEndLine() {} +}; + +/** Prints the proof to output stream d_out */ +class LfscPrintChannelOut : public LfscPrintChannel +{ + public: + LfscPrintChannelOut(std::ostream& out); + void printNode(TNode n) override; + void printTypeNode(TypeNode tn) override; + void printHole() override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + void printOpenLfscRule(LfscRule lr) override; + void printCloseRule(size_t nparen = 1) override; + void printProofId(size_t id) override; + void printAssumeId(size_t id) override; + void printEndLine() override; + //------------------- helper methods + /** + * Print node to stream in the expected format of LFSC. + */ + static void printNodeInternal(std::ostream& out, Node n); + /** + * Print type node to stream in the expected format of LFSC. + */ + static void printTypeNodeInternal(std::ostream& out, TypeNode tn); + static void printRule(std::ostream& out, const ProofNode* pn); + static void printId(std::ostream& out, size_t id); + static void printProofId(std::ostream& out, size_t id); + static void printAssumeId(std::ostream& out, size_t id); + //------------------- end helper methods + private: + /** + * Replaces "(_ " with "(" to eliminate indexed symbols + * Replaces "__LFSC_TMP" with "" + */ + static void cleanSymbols(std::string& s); + /** The output stream */ + std::ostream& d_out; +}; + +/** + * Run on the proof before it is printed, and does two preparation steps: + * - Computes the letification of nodes that appear in the proof. + * - Computes the set of DSL rules that appear in the proof. + */ +class LfscPrintChannelPre : public LfscPrintChannel +{ + public: + LfscPrintChannelPre(LetBinding& lbind); + void printNode(TNode n) override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + + private: + /** The let binding */ + LetBinding& d_lbind; +}; + +} // namespace proof +} // namespace cvc5 + +#endif -- cgit v1.2.3 From d184659d9dafc1719076d2949beb1e9f92865ae9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 22:05:42 -0500 Subject: 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. --- src/CMakeLists.txt | 2 + src/smt/difficulty_post_processor.cpp | 77 ++++++++++++++++++++++++++++++ src/smt/difficulty_post_processor.h | 88 +++++++++++++++++++++++++++++++++++ 3 files changed, 167 insertions(+) create mode 100644 src/smt/difficulty_post_processor.cpp create mode 100644 src/smt/difficulty_post_processor.h (limited to 'src/CMakeLists.txt') 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 -- cgit v1.2.3 From 6faad286091f8a6a2b0af8841816bf32b4f2b43c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Sep 2021 10:26:34 -0500 Subject: Add difficulty manager (#7151) Towards supporting a (get-difficulty) command. This tracks an estimate of the difficulty of preprocessed assertions during solving. It will be connected to TheoryEngine (via RelevanceManager) in a followup PR. --- src/CMakeLists.txt | 2 + src/options/smt_options.toml | 15 ++++++ src/theory/difficulty_manager.cpp | 109 ++++++++++++++++++++++++++++++++++++++ src/theory/difficulty_manager.h | 83 +++++++++++++++++++++++++++++ 4 files changed, 209 insertions(+) create mode 100644 src/theory/difficulty_manager.cpp create mode 100644 src/theory/difficulty_manager.h (limited to 'src/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 401fc5976..ecfef1c22 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -690,6 +690,8 @@ libcvc5_add_sources( theory/decision_manager.h theory/decision_strategy.cpp theory/decision_strategy.h + theory/difficulty_manager.cpp + theory/difficulty_manager.h theory/ee_manager.cpp theory/ee_manager.h theory/ee_manager_central.cpp diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 40a37fa7b..7d0dab720 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -220,6 +220,21 @@ name = "SMT Layer" default = "false" help = "turn on unsat assumptions generation" +[[option]] + name = "difficultyMode" + category = "regular" + long = "difficulty-mode=MODE" + type = "DifficultyMode" + default = "LEMMA_LITERAL" + help = "choose output mode for get-difficulty, see --difficulty-mode=help" + help_mode = "difficulty output modes." +[[option.mode.LEMMA_LITERAL]] + name = "lemma-literal" + help = "Difficulty of an assertion is how many lemmas use a literal that the assertion depends on to be satisfied." +[[option.mode.MODEL_CHECK]] + name = "model-check" + help = "Difficulty of an assertion is how many times it was not satisfied in a candidate model." + [[option]] name = "checkSynthSol" category = "regular" diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp new file mode 100644 index 000000000..3df86383f --- /dev/null +++ b/src/theory/difficulty_manager.cpp @@ -0,0 +1,109 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Difficulty manager. + */ + +#include "theory/difficulty_manager.h" + +#include "options/smt_options.h" +#include "smt/env.h" +#include "theory/theory_model.h" +#include "util/rational.h" + +namespace cvc5 { +namespace theory { + +DifficultyManager::DifficultyManager(context::Context* c, Valuation val) + : d_val(val), d_dfmap(c) +{ +} + +void DifficultyManager::getDifficultyMap(std::map& dmap) +{ + NodeManager* nm = NodeManager::currentNM(); + for (const std::pair p : d_dfmap) + { + dmap[p.first] = nm->mkConst(Rational(p.second)); + } +} + +void DifficultyManager::notifyLemma(const std::map& rse, Node n) +{ + if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL) + { + return; + } + Trace("diff-man") << "notifyLemma: " << n << std::endl; + Kind nk = n.getKind(); + // for lemma (or a_1 ... a_n), if a_i is a literal that is not true in the + // valuation, then we increment the difficulty of that assertion + std::vector litsToCheck; + if (nk == kind::OR) + { + litsToCheck.insert(litsToCheck.end(), n.begin(), n.end()); + } + else if (nk == kind::IMPLIES) + { + litsToCheck.push_back(n[0].negate()); + litsToCheck.push_back(n[1]); + } + else + { + litsToCheck.push_back(n); + } + std::map::const_iterator it; + for (TNode nc : litsToCheck) + { + bool pol = nc.getKind() != kind::NOT; + TNode atom = pol ? nc : nc[0]; + it = rse.find(atom); + if (it != rse.end()) + { + incrementDifficulty(it->second); + } + } +} + +void DifficultyManager::notifyCandidateModel(const NodeList& input, + TheoryModel* m) +{ + if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK) + { + return; + } + Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input=" + << input.size() << std::endl; + for (const Node& a : input) + { + // should have miniscoped the assertions upstream + Assert(a.getKind() != kind::AND); + // check if each input is satisfied + Node av = m->getValue(a); + if (av.isConst() && av.getConst()) + { + continue; + } + Trace("diff-man") << " not true: " << a << std::endl; + // not satisfied, increment counter + incrementDifficulty(a); + } + Trace("diff-man") << std::endl; +} +void DifficultyManager::incrementDifficulty(TNode a, uint64_t amount) +{ + Assert(a.getType().isBoolean()); + d_dfmap[a] = d_dfmap[a] + amount; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/difficulty_manager.h b/src/theory/difficulty_manager.h new file mode 100644 index 000000000..3030bcc9b --- /dev/null +++ b/src/theory/difficulty_manager.h @@ -0,0 +1,83 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Relevance manager. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__DIFFICULTY_MANAGER__H +#define CVC5__THEORY__DIFFICULTY_MANAGER__H + +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/node.h" +#include "theory/valuation.h" + +namespace cvc5 { +namespace theory { + +class TheoryModel; + +/** + * Difficulty manager, which tracks an estimate of the difficulty of each + * preprocessed assertion during solving. + */ +class DifficultyManager +{ + typedef context::CDList NodeList; + typedef context::CDHashMap NodeUIntMap; + + public: + DifficultyManager(context::Context* c, Valuation val); + /** + * Get difficulty map, which populates dmap mapping preprocessed assertions + * to a difficulty measure (a constant integer). + */ + void getDifficultyMap(std::map& dmap); + /** + * Notify lemma, for difficulty measurements. This increments the difficulty + * of assertions that share literals with that lemma if the difficulty mode + * is LEMMA_LITERAL. In particular, for each literal lit in the lemma lem, we + * increment the difficulty of the assertion res[lit], which corresponds to + * the assertion that was the reason why the literal is relevant in the + * current context. + * + * @param rse Mapping from literals to the preprocessed assertion that was + * the reason why that literal was relevant in the current context + * @param lem The lemma + */ + void notifyLemma(const std::map& rse, Node lem); + /** + * Notify that `m` is a (candidate) model. This increments the difficulty + * of assertions that are not satisfied by that model. + * + * @param input The list of preprocessed assertions + * @param m The candidate model. + */ + void notifyCandidateModel(const NodeList& input, TheoryModel* m); + + private: + /** Increment difficulty on assertion a */ + void incrementDifficulty(TNode a, uint64_t amount = 1); + /** The valuation object, used to query current value of theory literals */ + Valuation d_val; + /** + * User-context dependent mapping from input assertions to difficulty measure + */ + NodeUIntMap d_dfmap; +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__DIFFICULTY_MANAGER__H */ -- cgit v1.2.3