Add variant of get-difficulty for full effort lemmas (#8018)

Add variant of get-difficulty for full effort lemmas

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 1d82ac15bc15febe43bc31a62d771695bb4a7045..2ae6fbd31503fecec96d7eaf14ec65a147f13276 100644 (file)
--- 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 b66b56e560ce0d99e37a66c1edcc617c2f5b7e34..2b66403916df5a1e210a900a9d8cbbd5c12218a2 100644 (file)
--- a/src/theory/difficulty_manager.cpp
+++ b/src/theory/difficulty_manager.cpp
@@ -51,9 +51,19 @@ void DifficultyManager::getDifficultyMap(std::map<Node, Node>& 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 5e6e038de2949d213e9f62f97f55041d04f7f6c4..902e29dd64fcf09ee8cb83e4e265b5b933d2a0c5 100644 (file)
--- 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 ddff64ef100a01a4f0bdf2cd743b9ea3bf3de782..b501deffc39e95e0a8dce4700b1d03ce565b837c 100644 (file)
--- 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);
   }
 }