From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 14 Jan 2022 17:05:20 +0000 (-0600)
Subject: Weaken assertion in relevance manager (#7943)
X-Git-Tag: cvc5-1.0.0~545
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b1ee9680aa68b93ab908ca190d65dc7c78026873;p=cvc5.git

Weaken assertion in relevance manager (#7943)

Fixes #7937.
---

diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 39e1eb2e5..ddff64ef1 100644
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -190,11 +190,13 @@ void RelevanceManager::computeRelevance()
 bool RelevanceManager::computeRelevanceFor(TNode input)
 {
   int32_t val = justify(input);
-  if (val != 1)
+  if (val == -1)
   {
     // 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.
+    // isRelevant cannot be trusted. It might also be the case that the
+    // assertion has no value (val == 0), since it may correspond to an
+    // irrelevant Skolem definition, in this case we don't throw a warning.
     if (d_inFullEffortCheck)
     {
       std::stringstream serr;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c8057606e..3092664cd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1790,6 +1790,15 @@ bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   bool hasFailure = false;
   std::stringstream serror;
+  // If possible, get the list of relevant assertions. Those that are not
+  // relevant will be skipped.
+  std::unordered_set<TNode> relevantAssertions;
+  bool hasRelevantAssertions = false;
+  if (d_relManager != nullptr)
+  {
+    relevantAssertions =
+        d_relManager->getRelevantAssertions(hasRelevantAssertions);
+  }
   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
     Theory* theory = d_theoryTable[theoryId];
     if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
@@ -1798,7 +1807,8 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
           it != it_end;
           ++it) {
         Node assertion = (*it).d_assertion;
-        if (!isRelevant(assertion))
+        if (hasRelevantAssertions
+            && relevantAssertions.find(assertion) == relevantAssertions.end())
         {
           // not relevant, skip
           continue;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19db389b4..f9fc93e58 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1805,6 +1805,7 @@ set(regress_1_tests
   regress1/issue5101-alira-subtypes.smt2
   regress1/issue5739-rtf-processed.smt2
   regress1/issue7902-abd-subsolver-uc.smt2
+  regress1/issue7937-difficulty-irr.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/minimal_unsat_core.smt2
diff --git a/test/regress/regress1/issue7937-difficulty-irr.smt2 b/test/regress/regress1/issue7937-difficulty-irr.smt2
new file mode 100644
index 000000000..a18dc82f9
--- /dev/null
+++ b/test/regress/regress1/issue7937-difficulty-irr.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-difficulty -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x Bool)
+(declare-fun a () Real)
+(declare-fun r () Real)
+(assert (xor (= 0 (/ 0 a)) (and x (= 0.0 (/ r a r)))))
+(check-sat)