From 709d61c8ffaf89e544ca2c8eead966348da2160c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Feb 2022 12:11:21 -0600 Subject: [PATCH] Add variant of get-difficulty for full effort lemmas (#8018) Add variant of get-difficulty for full effort lemmas --- src/options/smt_options.toml | 3 +++ src/theory/difficulty_manager.cpp | 14 ++++++++++++-- src/theory/difficulty_manager.h | 4 +++- src/theory/relevance_manager.cpp | 2 +- 4 files changed, 19 insertions(+), 4 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 1d82ac15b..2ae6fbd31 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -215,6 +215,9 @@ name = "SMT Layer" help_mode = "difficulty output modes." [[option.mode.LEMMA_LITERAL]] name = "lemma-literal" + help = "Difficulty of an assertion is how many lemmas (at full effort) use a literal that the assertion depends on to be satisfied." +[[option.mode.LEMMA_LITERAL_ALL]] + name = "lemma-literal-all" 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" diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp index b66b56e56..2b6640391 100644 --- a/src/theory/difficulty_manager.cpp +++ b/src/theory/difficulty_manager.cpp @@ -51,9 +51,19 @@ void DifficultyManager::getDifficultyMap(std::map& dmap) } } -void DifficultyManager::notifyLemma(Node n) +void DifficultyManager::notifyLemma(Node n, bool inFullEffortCheck) { - if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL) + // compute if we should consider the lemma + bool considerLemma = false; + if (options::difficultyMode() == options::DifficultyMode::LEMMA_LITERAL_ALL) + { + considerLemma = true; + } + else if (options::difficultyMode() == options::DifficultyMode::LEMMA_LITERAL) + { + considerLemma = inFullEffortCheck; + } + if (!considerLemma) { return; } diff --git a/src/theory/difficulty_manager.h b/src/theory/difficulty_manager.h index 5e6e038de..902e29dd6 100644 --- a/src/theory/difficulty_manager.h +++ b/src/theory/difficulty_manager.h @@ -57,9 +57,11 @@ class DifficultyManager * * @param rse Mapping from literals to the preprocessed assertion that was * the reason why that literal was relevant in the current context + * @param inFullEffortCheck Whether we are in a full effort check when the + * lemma was sent. * @param lem The lemma */ - void notifyLemma(Node lem); + void notifyLemma(Node lem, bool inFullEffortCheck); /** * Notify that `m` is a (candidate) model. This increments the difficulty * of assertions that are not satisfied by that model. diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index ddff64ef1..b501deffc 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -533,7 +533,7 @@ void RelevanceManager::notifyLemma(TNode n) { // notice that we don't compute relevance here, instead it is computed // on demand based on the literals in n. - d_dman->notifyLemma(n); + d_dman->notifyLemma(n, d_inFullEffortCheck); } } -- 2.30.2