From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Feb 2022 18:11:21 +0000 (-0600)
Subject: Add variant of get-difficulty for full effort lemmas (#8018)
X-Git-Tag: cvc5-1.0.0~486
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=709d61c8ffaf89e544ca2c8eead966348da2160c;p=cvc5.git

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 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<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 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);
   }
 }