From 18758ae6ba02fb30744e560bf660c75a3af78008 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Dec 2021 11:16:42 -0600 Subject: [PATCH] Improvements for get-difficulty (#7720) This makes 2 improvements for get-difficulty: (1) Ensures that we recompute relevance info for lemmas sent at STANDARD effort. (2) An open proof error was reported by Certora using --produce-difficulty. This makes get-difficulty more robust by ensuring that lemmas are not marked as having a difficulty. It also minimizes the cases where we mark lemmas as having a difficulty internally. --- src/smt/proof_manager.cpp | 11 ++++++++++- src/theory/difficulty_manager.cpp | 3 +++ src/theory/relevance_manager.cpp | 33 +++++++++++++++++++------------ src/theory/relevance_manager.h | 5 +---- src/theory/theory_engine.cpp | 18 +++++++---------- 5 files changed, 41 insertions(+), 29 deletions(-) diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 4b4291075..4cb9d5bf9 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -227,11 +227,20 @@ 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; - ppAsserts.push_back(ppa.first); + // 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); + } } // assume a SAT refutation from all input assertions that were marked // as having a difficulty diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp index c09120771..0a9eba60d 100644 --- a/src/theory/difficulty_manager.cpp +++ b/src/theory/difficulty_manager.cpp @@ -69,6 +69,9 @@ void DifficultyManager::notifyLemma(const std::map& rse, Node n) bool pol = nc.getKind() != kind::NOT; TNode atom = pol ? nc : nc[0]; it = rse.find(atom); + Trace("diff-man-debug") + << "Check literal: " << atom << ", has reason = " << (it != rse.end()) + << std::endl; if (it != rse.end()) { incrementDifficulty(it->second); diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index 6b19f2146..972a2918c 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -29,7 +29,6 @@ RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val) : d_val(val), d_input(lemContext), d_computed(false), - d_inFullEffortCheck(false), d_success(false), d_trackRSetExp(false), d_miniscopeTopLevel(true) @@ -104,11 +103,8 @@ void RelevanceManager::addAssertionsInternal(std::vector& toProcess) void RelevanceManager::beginRound() { d_computed = false; - d_inFullEffortCheck = true; } -void RelevanceManager::endRound() { d_inFullEffortCheck = false; } - void RelevanceManager::computeRelevance() { d_computed = true; @@ -116,24 +112,35 @@ void RelevanceManager::computeRelevance() d_rsetExp.clear(); Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl; std::unordered_map cache; + d_success = true; for (const Node& node: d_input) { TNode n = node; int val = justify(n, cache); if (val != 1) { - std::stringstream serr; - serr << "RelevanceManager::computeRelevance: WARNING: failed to justify " - << n; - Trace("rel-manager") << serr.str() << std::endl; - Assert(false) << serr.str(); + if (Trace.isOn("rel-manager")) + { + std::stringstream serr; + serr + << "RelevanceManager::computeRelevance: WARNING: failed to justify " + << n; + Trace("rel-manager") << serr.str() << std::endl; + } d_success = false; - d_rset.clear(); - return; + // 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) + { + d_rset.clear(); + return; + } Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl; - d_success = true; } bool RelevanceManager::isBooleanConnective(TNode cur) @@ -357,7 +364,7 @@ void RelevanceManager::notifyLemma(Node n) { // only consider lemmas that were sent at full effort, when we have a // complete SAT assignment. - if (d_dman != nullptr && d_inFullEffortCheck) + if (d_dman != nullptr) { // ensure we know which literals are relevant, and why computeRelevance(); diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index 7d6434c6b..fbc50801c 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -90,12 +90,9 @@ class RelevanceManager /** Singleton version of above */ void notifyPreprocessedAssertion(Node n); /** - * Begin round, called at the beginning of a full effort check in - * TheoryEngine. + * Begin round, called at the beginning of a 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 diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ea1209b47..1b2ad3358 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -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,10 +488,6 @@ 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 @@ -1319,7 +1315,7 @@ void TheoryEngine::lemma(TrustNode tlemma, std::vector sks; Node retLemma = d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks); - if (isLemmaPropertyNeedsJustify(p)) + if (options().theory.relevanceFilter && isLemmaPropertyNeedsJustify(p)) { d_relManager->notifyPreprocessedAssertion(retLemma); d_relManager->notifyPreprocessedAssertions(skAsserts); -- 2.30.2