From ffbf4a88580c72d7db41a807d3b39008a82b51f4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Dec 2021 11:28:39 -0600 Subject: [PATCH] Make data structures in relevance manager SAT-context dependent (#7733) This PR significantly improves the quality of values in get-difficulty. It fixes several bugs related to get-difficulty, including over-pruning values in ProofManager, and not tracking explanations for certain literals. It also improves performance by tracking justifications in relevance manager in a SAT-context dependent manner. This is to support difficulty measurements based on lemmas sent at STANDARD effort. It also adds 2 simple regressions. A further PR will further improve the quality by being more careful about the relationships between literals and the assertions that entail that they are relevant. --- src/smt/proof_manager.cpp | 14 +- src/smt/set_defaults.cpp | 5 +- src/theory/difficulty_manager.cpp | 26 ++- src/theory/difficulty_manager.h | 16 +- src/theory/relevance_manager.cpp | 170 +++++++++++------- src/theory/relevance_manager.h | 62 +++++-- src/theory/theory_engine.cpp | 30 ++-- src/theory/theory_engine.h | 7 +- test/regress/CMakeLists.txt | 2 + .../regress/regress0/difficulty-model-ex.smt2 | 22 +++ test/regress/regress0/difficulty-simple.smt2 | 16 ++ 11 files changed, 237 insertions(+), 133 deletions(-) create mode 100644 test/regress/regress0/difficulty-model-ex.smt2 create mode 100644 test/regress/regress0/difficulty-simple.smt2 diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 4cb9d5bf9..e12d6fbe0 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -227,20 +227,14 @@ void PfManager::translateDifficultyMap(std::map& dmap, std::map dmapp = dmap; dmap.clear(); std::vector ppAsserts; - std::vector asserts; - getAssertions(as, asserts); for (const std::pair& ppa : dmapp) { Trace("difficulty") << " preprocess difficulty: " << ppa.second << " for " << ppa.first << std::endl; - // Ensure that only input assertions are marked as having a difficulty. - // In some cases, a lemma may be marked as having a difficulty - // internally, e.g. for lemmas that require justification, which we should - // skip or otherwise we end up with an open proof below. - if (std::find(asserts.begin(), asserts.end(), ppa.first) != asserts.end()) - { - ppAsserts.push_back(ppa.first); - } + // The difficulty manager should only report difficulty for preprocessed + // assertions, or we will get an open proof below. This is ensured + // internally by the difficuly manager. + ppAsserts.push_back(ppa.first); } // assume a SAT refutation from all input assertions that were marked // as having a difficulty diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index aeb732dd5..9c5a5a6b3 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1161,9 +1161,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, bool SetDefaults::safeUnsatCores(const Options& opts) const { // whether we want to force safe unsat cores, i.e., if we are in the default - // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental - return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS - || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY; + // ASSUMPTIONS mode, since other ones are experimental + return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS; } bool SetDefaults::incompatibleWithQuantifiers(Options& opts, diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp index 0a9eba60d..d50d10d9f 100644 --- a/src/theory/difficulty_manager.cpp +++ b/src/theory/difficulty_manager.cpp @@ -26,10 +26,19 @@ namespace cvc5 { namespace theory { DifficultyManager::DifficultyManager(context::Context* c, Valuation val) - : d_val(val), d_dfmap(c) + : d_input(c), d_val(val), d_dfmap(c) { } +void DifficultyManager::notifyInputAssertions( + const std::vector& assertions) +{ + for (const Node& a : assertions) + { + d_input.insert(a); + } +} + void DifficultyManager::getDifficultyMap(std::map& dmap) { NodeManager* nm = NodeManager::currentNM(); @@ -39,7 +48,8 @@ void DifficultyManager::getDifficultyMap(std::map& dmap) } } -void DifficultyManager::notifyLemma(const std::map& rse, Node n) +void DifficultyManager::notifyLemma(const context::CDHashMap& rse, + Node n) { if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL) { @@ -63,7 +73,7 @@ void DifficultyManager::notifyLemma(const std::map& rse, Node n) { litsToCheck.push_back(n); } - std::map::const_iterator it; + context::CDHashMap::const_iterator it; for (TNode nc : litsToCheck) { bool pol = nc.getKind() != kind::NOT; @@ -72,23 +82,23 @@ void DifficultyManager::notifyLemma(const std::map& rse, Node n) Trace("diff-man-debug") << "Check literal: " << atom << ", has reason = " << (it != rse.end()) << std::endl; - if (it != rse.end()) + // must be an input assertion + if (it != rse.end() && d_input.find(it->second) != d_input.end()) { incrementDifficulty(it->second); } } } -void DifficultyManager::notifyCandidateModel(const NodeList& input, - TheoryModel* m) +void DifficultyManager::notifyCandidateModel(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) + << d_input.size() << std::endl; + for (const Node& a : d_input) { // should have miniscoped the assertions upstream Assert(a.getKind() != kind::AND); diff --git a/src/theory/difficulty_manager.h b/src/theory/difficulty_manager.h index 3030bcc9b..1437965fe 100644 --- a/src/theory/difficulty_manager.h +++ b/src/theory/difficulty_manager.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__DIFFICULTY_MANAGER__H #include "context/cdhashmap.h" -#include "context/cdlist.h" +#include "context/cdhashset.h" #include "expr/node.h" #include "theory/valuation.h" @@ -34,11 +34,13 @@ class TheoryModel; */ class DifficultyManager { - typedef context::CDList NodeList; + typedef context::CDHashSet NodeSet; typedef context::CDHashMap NodeUIntMap; public: DifficultyManager(context::Context* c, Valuation val); + /** Notify input assertions */ + void notifyInputAssertions(const std::vector& assertions); /** * Get difficulty map, which populates dmap mapping preprocessed assertions * to a difficulty measure (a constant integer). @@ -56,19 +58,23 @@ class DifficultyManager * the reason why that literal was relevant in the current context * @param lem The lemma */ - void notifyLemma(const std::map& rse, Node lem); + void notifyLemma(const context::CDHashMap& 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); + void notifyCandidateModel(TheoryModel* m); private: /** Increment difficulty on assertion a */ void incrementDifficulty(TNode a, uint64_t amount = 1); + /** + * The input assertions, tracked to ensure we do not increment difficulty + * on lemmas. + */ + NodeSet d_input; /** The valuation object, used to query current value of theory literals */ Valuation d_val; /** diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index 972a2918c..0ce021e08 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -25,17 +25,21 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { -RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val) - : d_val(val), - d_input(lemContext), - d_computed(false), +RelevanceManager::RelevanceManager(Env& env, Valuation val) + : EnvObj(env), + d_val(val), + d_input(userContext()), + d_rset(context()), + d_inFullEffortCheck(false), d_success(false), d_trackRSetExp(false), - d_miniscopeTopLevel(true) + d_miniscopeTopLevel(true), + d_rsetExp(context()), + d_jcache(context()) { - if (options::produceDifficulty()) + if (options().smt.produceDifficulty) { - d_dman.reset(new DifficultyManager(lemContext, val)); + d_dman.reset(new DifficultyManager(userContext(), val)); d_trackRSetExp = true; // we cannot miniscope AND at the top level, since we need to // preserve the exact form of preprocessed assertions so the dependencies @@ -45,7 +49,7 @@ RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val) } void RelevanceManager::notifyPreprocessedAssertions( - const std::vector& assertions) + const std::vector& assertions, bool isInput) { // add to input list, which is user-context dependent std::vector toProcess; @@ -65,13 +69,18 @@ void RelevanceManager::notifyPreprocessedAssertions( } } addAssertionsInternal(toProcess); + // notify the difficulty manager if these are input assertions + if (isInput && d_dman != nullptr) + { + d_dman->notifyInputAssertions(assertions); + } } -void RelevanceManager::notifyPreprocessedAssertion(Node n) +void RelevanceManager::notifyPreprocessedAssertion(Node n, bool isInput) { std::vector toProcess; toProcess.push_back(n); - addAssertionsInternal(toProcess); + notifyPreprocessedAssertions(toProcess, isInput); } void RelevanceManager::addAssertionsInternal(std::vector& toProcess) @@ -100,47 +109,53 @@ void RelevanceManager::addAssertionsInternal(std::vector& toProcess) } } -void RelevanceManager::beginRound() -{ - d_computed = false; -} +void RelevanceManager::beginRound() { d_inFullEffortCheck = true; } + +void RelevanceManager::endRound() { d_inFullEffortCheck = false; } void RelevanceManager::computeRelevance() { - d_computed = true; - d_rset.clear(); - d_rsetExp.clear(); - Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl; - std::unordered_map cache; - d_success = true; + // if not at full effort, should be tracking something else, e.g. explanation + // for why literals are relevant. + Assert(d_inFullEffortCheck || d_trackRSetExp); + Trace("rel-manager") << "RelevanceManager::computeRelevance, full effort = " + << d_inFullEffortCheck << "..." << std::endl; for (const Node& node: d_input) { TNode n = node; - int val = justify(n, cache); + int val = justify(n); if (val != 1) { - if (Trace.isOn("rel-manager")) + // if we are in full effort check and fail to justify, then we should + // give a failure and set success to false, or otherwise calls to + // isRelevant cannot be trusted. + if (d_inFullEffortCheck) { std::stringstream serr; serr << "RelevanceManager::computeRelevance: WARNING: failed to justify " << n; Trace("rel-manager") << serr.str() << std::endl; + Assert(false) << serr.str(); + d_success = false; + return; } - d_success = false; - // If we fail to justify an assertion, we set success to false and - // continue to try to justify the remaining assertions. This is important - // for cases where the difficulty manager is measuring based on lemmas - // that are being sent at STANDARD effort, before all assertions are - // satisfied. } } - if (!d_success) + if (Trace.isOn("rel-manager")) { - d_rset.clear(); - return; + if (d_inFullEffortCheck) + { + Trace("rel-manager") << "...success (full), size = " << d_rset.size() + << std::endl; + } + else + { + Trace("rel-manager") << "...success, exp size = " << d_rsetExp.size() + << std::endl; + } } - Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl; + d_success = true; } bool RelevanceManager::isBooleanConnective(TNode cur) @@ -150,10 +165,8 @@ bool RelevanceManager::isBooleanConnective(TNode cur) || (k == EQUAL && cur[0].getType().isBoolean()); } -bool RelevanceManager::updateJustifyLastChild( - TNode cur, - std::vector& childrenJustify, - std::unordered_map& cache) +bool RelevanceManager::updateJustifyLastChild(TNode cur, + std::vector& childrenJustify) { // This method is run when we are informed that child index of cur // has justify status lastChildJustify. We return true if we would like to @@ -163,14 +176,14 @@ bool RelevanceManager::updateJustifyLastChild( Assert(isBooleanConnective(cur)); size_t index = childrenJustify.size(); Assert(index < nchildren); - Assert(cache.find(cur[index]) != cache.end()); + Assert(d_jcache.find(cur[index]) != d_jcache.end()); Kind k = cur.getKind(); // Lookup the last child's value in the overall cache, we may choose to // add this to childrenJustify if we return true. - int lastChildJustify = cache[cur[index]]; + int lastChildJustify = d_jcache[cur[index]]; if (k == NOT) { - cache[cur] = -lastChildJustify; + d_jcache[cur] = -lastChildJustify; } else if (k == IMPLIES || k == AND || k == OR) { @@ -181,7 +194,7 @@ bool RelevanceManager::updateJustifyLastChild( if (lastChildJustify == ((k == AND || (k == IMPLIES && index == 0)) ? -1 : 1)) { - cache[cur] = k == AND ? -1 : 1; + d_jcache[cur] = k == AND ? -1 : 1; return false; } } @@ -197,7 +210,7 @@ bool RelevanceManager::updateJustifyLastChild( break; } } - cache[cur] = ret; + d_jcache[cur] = ret; } else { @@ -209,7 +222,7 @@ bool RelevanceManager::updateJustifyLastChild( else if (lastChildJustify == 0) { // all other cases, an unknown child implies we are unknown - cache[cur] = 0; + d_jcache[cur] = 0; } else if (k == ITE) { @@ -230,7 +243,7 @@ bool RelevanceManager::updateJustifyLastChild( // should be in proper branch Assert(childrenJustify[0] == (index == 1 ? 1 : -1)); // we are the value of the branch - cache[cur] = lastChildJustify; + d_jcache[cur] = lastChildJustify; } } else @@ -248,7 +261,7 @@ bool RelevanceManager::updateJustifyLastChild( { // both children known, compute value Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0); - cache[cur] = + d_jcache[cur] = ((k == XOR ? -1 : 1) * lastChildJustify == childrenJustify[0]) ? 1 : -1; } @@ -256,11 +269,15 @@ bool RelevanceManager::updateJustifyLastChild( return false; } -int RelevanceManager::justify(TNode n, std::unordered_map& cache) +int RelevanceManager::justify(TNode n) { + // The set of nodes that we have computed currently have no value. Those + // that are marked as having no value in d_jcache must be recomputed, since + // the values for SAT literals may have changed. + std::unordered_set noJustify; // the vector of values of children std::unordered_map> childJustify; - std::unordered_map::iterator it; + NodeUIntMap::iterator it; std::unordered_map>::iterator itc; std::vector visit; TNode cur; @@ -270,12 +287,15 @@ int RelevanceManager::justify(TNode n, std::unordered_map& cache) cur = visit.back(); // should always have Boolean type Assert(cur.getType().isBoolean()); - it = cache.find(cur); - if (it != cache.end()) + it = d_jcache.find(cur); + if (it != d_jcache.end()) { - visit.pop_back(); - // already computed value - continue; + if (it->second != 0 || noJustify.find(cur) != noJustify.end()) + { + visit.pop_back(); + // already computed value + continue; + } } itc = childJustify.find(cur); // have we traversed to children yet? @@ -304,16 +324,22 @@ int RelevanceManager::justify(TNode n, std::unordered_map& cache) if (d_trackRSetExp) { d_rsetExp[cur] = n; + Trace("rel-manager-exp") + << "Reason for " << cur << " is " << n << std::endl; } } - cache[cur] = ret; + d_jcache[cur] = ret; + if (ret == 0) + { + noJustify.insert(cur); + } } } else { // this processes the impact of the current child on the value of cur, // and possibly requests that a new child is computed. - if (updateJustifyLastChild(cur, itc->second, cache)) + if (updateJustifyLastChild(cur, itc->second)) { Assert(itc->second.size() < cur.getNumChildren()); TNode nextChild = cur[itc->second.size()]; @@ -322,19 +348,22 @@ int RelevanceManager::justify(TNode n, std::unordered_map& cache) else { visit.pop_back(); + Assert(d_jcache.find(cur) != d_jcache.end()); + if (d_jcache[cur] == 0) + { + noJustify.insert(cur); + } } } } while (!visit.empty()); - Assert(cache.find(n) != cache.end()); - return cache[n]; + Assert(d_jcache.find(n) != d_jcache.end()); + return d_jcache[n]; } bool RelevanceManager::isRelevant(Node lit) { - if (!d_computed) - { - computeRelevance(); - } + Assert(d_inFullEffortCheck); + computeRelevance(); if (!d_success) { // always relevant if we failed to compute @@ -348,22 +377,25 @@ bool RelevanceManager::isRelevant(Node lit) return d_rset.find(lit) != d_rset.end(); } -const std::unordered_set& RelevanceManager::getRelevantAssertions( - bool& success) +std::unordered_set RelevanceManager::getRelevantAssertions(bool& success) { - if (!d_computed) - { - computeRelevance(); - } + computeRelevance(); // update success flag success = d_success; - return d_rset; + std::unordered_set rset; + if (success) + { + for (const Node& a : d_rset) + { + rset.insert(a); + } + } + return rset; } void RelevanceManager::notifyLemma(Node n) { - // only consider lemmas that were sent at full effort, when we have a - // complete SAT assignment. + // notice that we may be in FULL or STANDARD effort here. if (d_dman != nullptr) { // ensure we know which literals are relevant, and why @@ -376,7 +408,7 @@ void RelevanceManager::notifyCandidateModel(TheoryModel* m) { if (d_dman != nullptr) { - d_dman->notifyCandidateModel(d_input, m); + d_dman->notifyCandidateModel(m); } } diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index fbc50801c..9bcf4af42 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -21,8 +21,11 @@ #include #include +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/difficulty_manager.h" #include "theory/valuation.h" @@ -71,28 +74,39 @@ class TheoryModel; * selection is computed lazily, i.e. only when someone asks if a literal is * relevant, and only at most once per FULL effort check. */ -class RelevanceManager +class RelevanceManager : protected EnvObj { - typedef context::CDList NodeList; + using NodeList = context::CDList; + using NodeMap = context::CDHashMap; + using NodeSet = context::CDHashSet; + using NodeUIntMap = context::CDHashMap; public: /** - * @param lemContext The context which lemmas live at + * @param env The environment * @param val The valuation class, for computing what is relevant. */ - RelevanceManager(context::Context* lemContext, Valuation val); + RelevanceManager(Env& env, Valuation val); /** * Notify (preprocessed) assertions. This is called for input formulas or * lemmas that need justification that have been fully processed, just before * adding them to the PropEngine. + * + * @param assertions The assertions + * @param isInput Whether the assertions are preprocessed input assertions; + * this flag is false for lemmas. */ - void notifyPreprocessedAssertions(const std::vector& assertions); + void notifyPreprocessedAssertions(const std::vector& assertions, + bool isInput); /** Singleton version of above */ - void notifyPreprocessedAssertion(Node n); + void notifyPreprocessedAssertion(Node n, bool isInput); /** - * Begin round, called at the beginning of a check in TheoryEngine. + * Begin round, called at the beginning of a full effort check in + * TheoryEngine. */ void beginRound(); + /** End round, called at the end of a full effort check in TheoryEngine. */ + void endRound(); /** * Is lit part of the current relevant selection? This computes the set of * relevant assertions if not already done so. This call is valid during a @@ -110,8 +124,11 @@ class RelevanceManager * the assertions we are notified of. This should never happen. * * The value of this return is only valid if success was not updated to false. + * + * Note that this returns a context-independent set to the user, which + * copies the assertions. */ - const std::unordered_set& getRelevantAssertions(bool& success); + std::unordered_set getRelevantAssertions(bool& success); /** Notify lemma, for difficulty measurements */ void notifyLemma(Node n); /** Notify that m is a (candidate) model, for difficulty measurements */ @@ -138,32 +155,31 @@ class RelevanceManager * This method returns 1 if we justified n to be true, -1 means * justified n to be false, 0 means n could not be justified. */ - int justify(TNode n, std::unordered_map& cache); + int justify(TNode n); /** Is the top symbol of cur a Boolean connective? */ bool isBooleanConnective(TNode cur); /** * Update justify last child. This method is a helper function for justify, * which is called at the moment that Boolean connective formula cur - * has a new child that has been computed in the justify cache. + * has a new child that has been computed in the justify cache maintained + * by this class. * * @param cur The Boolean connective formula * @param childrenJustify The values of the previous children (not including * the current one) - * @param cache The justify cache * @return True if we wish to visit the next child. If this is the case, then * the justify value of the current child is added to childrenJustify. */ - bool updateJustifyLastChild(TNode cur, - std::vector& childrenJustify, - std::unordered_map& cache); + bool updateJustifyLastChild(TNode cur, std::vector& childrenJustify); /** The valuation object, used to query current value of theory literals */ Valuation d_val; /** The input assertions */ NodeList d_input; - /** The current relevant selection. */ - std::unordered_set d_rset; - /** Have we computed the relevant selection this round? */ - bool d_computed; + /** + * The current relevant selection, SAT-context dependent, includes + * literals that are definitely relevant in this context. + */ + NodeSet d_rset; /** Are we in a full effort check? */ bool d_inFullEffortCheck; /** @@ -172,6 +188,8 @@ class RelevanceManager * assignment since this class found that the input formula was not satisfied * by the assignment. This should never happen, but if it does, this class * aborts and indicates that all literals are relevant. + * + * This flag is only valid at FULL effort. */ bool d_success; /** Are we tracking the sources of why a literal is relevant */ @@ -187,7 +205,13 @@ class RelevanceManager * Map from the domain of d_rset to the assertion in d_input that is the * reason why that literal is currently relevant. */ - std::map d_rsetExp; + NodeMap d_rsetExp; + /** + * Set of nodes that we have justified (SAT context dependent). This is SAT + * context dependent to avoid repeated calls to justify for uses of + * the relevance manager at standard effort. + */ + NodeUIntMap d_jcache; /** Difficulty module */ std::unique_ptr d_dman; }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1b2ad3358..8421107a4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -155,7 +155,7 @@ void TheoryEngine::finishInit() // create the relevance filter if any option requires it if (options().theory.relevanceFilter || options().smt.produceDifficulty) { - d_relManager.reset(new RelevanceManager(userContext(), Valuation(this))); + d_relManager.reset(new RelevanceManager(d_env, Valuation(this))); } // initialize the quantifiers engine @@ -384,15 +384,15 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl; - // Reset round for the relevance manager, which notice only sets a flag - // to indicate that its information must be recomputed. - if (d_relManager != nullptr) - { - d_relManager->beginRound(); - } // If in full effort, we have a fake new assertion just to jumpstart the checking if (Theory::fullEffort(effort)) { d_factsAsserted = true; + // Reset round for the relevance manager, which notice only sets a flag + // to indicate that its information must be recomputed. + if (d_relManager != nullptr) + { + d_relManager->beginRound(); + } d_tc->resetRound(); } @@ -488,6 +488,10 @@ void TheoryEngine::check(Theory::Effort effort) { if (Theory::fullEffort(effort)) { + if (d_relManager != nullptr) + { + d_relManager->endRound(); + } if (!d_inConflict && !needCheck()) { // Do post-processing of model from the theories (e.g. used for @@ -775,7 +779,7 @@ void TheoryEngine::notifyPreprocessedAssertions( } if (d_relManager != nullptr) { - d_relManager->notifyPreprocessedAssertions(assertions); + d_relManager->notifyPreprocessedAssertions(assertions, true); } } @@ -1075,14 +1079,14 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return d_sharedSolver->getEqualityStatus(a, b); } -const std::unordered_set& TheoryEngine::getRelevantAssertions( - bool& success) +std::unordered_set TheoryEngine::getRelevantAssertions(bool& success) { // if we are not in SAT mode, or there is no relevance manager, we fail if (!d_inSatMode || d_relManager == nullptr) { success = false; - return d_emptyRelevantSet; + // return empty set + return std::unordered_set(); } return d_relManager->getRelevantAssertions(success); } @@ -1317,8 +1321,8 @@ void TheoryEngine::lemma(TrustNode tlemma, d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks); if (options().theory.relevanceFilter && isLemmaPropertyNeedsJustify(p)) { - d_relManager->notifyPreprocessedAssertion(retLemma); - d_relManager->notifyPreprocessedAssertions(skAsserts); + d_relManager->notifyPreprocessedAssertion(retLemma, false); + d_relManager->notifyPreprocessedAssertions(skAsserts, false); } d_relManager->notifyLemma(retLemma); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index efde513a9..03f7555b7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -374,7 +374,7 @@ class TheoryEngine : protected EnvObj * relevance manager failed to compute relevant assertions due to an internal * error. */ - const std::unordered_set& getRelevantAssertions(bool& success); + std::unordered_set getRelevantAssertions(bool& success); /** * Get difficulty map, which populates dmap, mapping preprocessed assertions @@ -544,11 +544,6 @@ class TheoryEngine : protected EnvObj std::unique_ptr d_decManager; /** The relevance manager */ std::unique_ptr d_relManager; - /** - * An empty set of relevant assertions, which is returned as a dummy value for - * getRelevantAssertions when relevance is disabled. - */ - std::unordered_set d_emptyRelevantSet; /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5afff3246..8c79b292a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -558,6 +558,8 @@ set(regress_0_tests regress0/declare-fun-is-match.smt2 regress0/declare-funs.smt2 regress0/define-fun-model.smt2 + regress0/difficulty-simple.smt2 + regress0/difficulty-model-ex.smt2 regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/echo.smt2 diff --git a/test/regress/regress0/difficulty-model-ex.smt2 b/test/regress/regress0/difficulty-model-ex.smt2 new file mode 100644 index 000000000..0546b5118 --- /dev/null +++ b/test/regress/regress0/difficulty-model-ex.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --produce-difficulty --difficulty-mode=model-check +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :produce-difficulty true) +(declare-fun P (Int) Bool) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) + +(assert (= z 78)) + +(assert (! (= (* x x) z) :named a1)) + +(assert (= y 0)) + +(assert (P y)) + +(check-sat) + +(get-difficulty) diff --git a/test/regress/regress0/difficulty-simple.smt2 b/test/regress/regress0/difficulty-simple.smt2 new file mode 100644 index 000000000..a82a96550 --- /dev/null +++ b/test/regress/regress0/difficulty-simple.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --produce-difficulty +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :produce-difficulty true) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) + +(assert (or (> a 0) (> b 0) (> c 0))) + +(assert (< (ite (> a b) a b) 0)) + +(check-sat) +(get-difficulty) -- 2.30.2