From 6faad286091f8a6a2b0af8841816bf32b4f2b43c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Sep 2021 10:26:34 -0500 Subject: [PATCH] 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 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 */ -- 2.30.2