Fixing up a bug in gate-based lit removal

msoos · Jan 23, 2024 · f3e96a8 · f3e96a8
1 parent 56afaa1
commit f3e96a8
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 3 deletions.
diff --git a/src/occsimplifier.cpp b/src/occsimplifier.cpp
@@ -661,6 +661,17 @@ bool OccSimplifier::check_varelim_when_adding_back_cl(const Clause* cl) const
     return notLinkedNeedFree;
 }
 
+void OccSimplifier::check_cls_sanity() {
+    if (!solver->okay()) return;
+    for (const ClOffset offs: clauses) {
+        Clause* cl = solver->cl_alloc.ptr(offs);
+        if (cl->getRemoved() || cl->freed()) continue;
+        assert(!cl->stats.marked_clause);
+        if (cl->size() <= 2) cout << "ERROR: too short cl: " << *cl << endl;
+        assert(cl->size() > 2);
+    }
+}
+
 void OccSimplifier::add_back_to_solver()
 {
     solver->clean_occur_from_removed_clauses_only_smudged();
@@ -2057,6 +2068,7 @@ bool OccSimplifier::lit_rem_with_or_gates()
     uint64_t shortened = 0;
     uint64_t removed = 0;
     for(const auto& gate: gates) {
+        if (!solver->okay()) goto end;
         if (solver->value(gate.rhs) != l_Undef) continue;
         for(auto const& l: gate.lits) seen[l.toInt()] = 1;
 
@@ -2074,6 +2086,7 @@ bool OccSimplifier::lit_rem_with_or_gates()
 
         VERBOSE_PRINT("Checking to shorten with gate: " << gate);
         for(const auto& w: poss) {
+            if (!solver->okay()) break;
             if (w.isBin() || w. isBNN()) continue;
             assert(w.isClause());
             const auto off = w.get_offset();
@@ -2142,7 +2155,12 @@ bool OccSimplifier::lit_rem_with_or_gates()
                 solver->attach_bin_clause((*cl)[0], (*cl)[1], false, cl->stats.ID, false);
                 unlink_clause(off, false, false, true);
 //                 cout << "Became bin." << endl;
-            }
+            } else if (cl->size() == 1) {
+                tmp_tern_res.clear(); tmp_tern_res.push_back((*cl)[0]);
+                Clause* newCl = full_add_clause(tmp_tern_res, finalLits_ternary, NULL, false);
+                assert(newCl == NULL);
+                unlink_clause(off, true, false, true);
+            } else assert(cl->size() > 2);
         }
         for(auto const& l: gate.lits) seen[l.toInt()] = 0;
     }
@@ -2171,8 +2189,6 @@ bool OccSimplifier::lit_rem_with_or_gates()
         );
     }
 
-    assert(solver->okay());
-    assert(solver->prop_at_head());
     return solver->okay();
 }
 
@@ -2309,6 +2325,7 @@ bool OccSimplifier::execute_simplifier_strategy(const string& strategy)
         #ifdef CHECK_N_OCCUR
         check_n_occur();
         #endif //CHECK_N_OCCUR
+        SLOW_DEBUG_DO(check_cls_sanity());
     }
 
     if (solver->okay()) {

diff --git a/src/occsimplifier.h b/src/occsimplifier.h
@@ -314,6 +314,7 @@ class OccSimplifier
     SubsumeStrengthen* sub_str;
     friend class BVA;
     BVA* bva;
+    void check_cls_sanity();
 
     bool startup = false;
     bool backward_sub_str();