Merge pull request #128 from vprover/fix-bsd-check

Fix pre-check in BSD
vprover · Jul 13, 2020 · 033d34d · 033d34d
2 parents e2be959 + 9c5dabf
commit 033d34d
Showing 1 changed file with 17 additions and 22 deletions.
diff --git a/Inferences/BackwardSubsumptionDemodulation.cpp b/Inferences/BackwardSubsumptionDemodulation.cpp
@@ -180,13 +180,8 @@ void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRe
 
 void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, vvector<BwSimplificationRecord>& simplifications)
 {
-
-  //                      candidate
-  //                 vvvvvvvvvvvvvvvv
-  //     cl        matched      /-- only look for a term to demodulate in this part!
-  // vvvvvvvvvv      vv    vvvvvvvvvv
-  // eqLit                  dlit
-  // vvvvv                 vvvvv
+  //   sideCl
+  // vvvvvvvvvv
   //
   // l = r \/ C      CΘ \/ L[lΘ] \/ D
   // --------------------------------
@@ -201,7 +196,7 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera
 #endif
 
   bool mustPredInit = false;
-  // bool mustPredActive = false;
+  bool mustPredActive = false;
   unsigned mustPred;
 
   SLQueryResultIterator rit = _index->getInstances(candidateQueryLit, false, false);
@@ -268,30 +263,30 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera
           mustPred = pred;
         }
       }
-      /*
       if (mustPred == 0) {
         // for positive equality we need to have skipped at least in the remaining literals
         mustPredActive = (numPosEqs >= 2);
       } else {
         mustPredActive = true;
       }
-      */
     }
-    bool haveMustPred = false;
-    for (unsigned ii = 0; ii < candidate->length(); ++ii) {
-      Literal* lit = (*candidate)[ii];
-      if (lit == qr.literal) {
-        continue;
+    if (mustPredActive) {
+      bool haveMustPred = false;
+      for (unsigned ii = 0; ii < candidate->length(); ++ii) {
+        Literal* lit = (*candidate)[ii];
+        if (lit == qr.literal) {
+          continue;
+        }
+        unsigned pred = lit->header();
+        if (pred == mustPred) {
+          haveMustPred = true;
+          break;
+        }
       }
-      unsigned pred = lit->header();
-      if (pred == mustPred) {
-        haveMustPred = true;
-        break;
+      if (!haveMustPred) {
+        continue;
       }
     }
-    if (!haveMustPred) {
-      continue;
-    }
     RSTAT_CTR_INC("bsd 1 mustPred survivors");
 
     simplifyCandidate(sideCl, candidate, simplifications);