Weaken assertion in relevance manager (#7943)

Fixes #7937.

diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 39e1eb2e5b0eb84f093fbf5d52e97dcddd3d72a7..ddff64ef100a01a4f0bdf2cd743b9ea3bf3de782 100644 (file)
--- 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 c8057606e4e49bfedbaf5e261da55be286c3e5c8..3092664cd359754602784265d38cba9462d20c0d 100644 (file)
--- 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 19db389b47ec40b77fd1602fe59c1b628490c3af..f9fc93e58e075d52367f3ee6422212b5b9d1f0a3 100644 (file)
--- 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 (file)
index 0000000..a18dc82
--- /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)