Fixing this up to not use this add_clause with red

meelgroup · Nov 21, 2023 · 807f707 · 807f707
1 parent 1425a30
commit 807f707
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/src/approxmc.cpp b/src/approxmc.cpp
@@ -273,10 +273,9 @@ DLL_PUBLIC bool AppMC::add_red_clause(const vector<CMSat::Lit>& lits)
     return data->counter.solver->add_red_clause(lits);
 }
 
-DLL_PUBLIC bool AppMC::add_clause(const vector<CMSat::Lit>& lits, bool red)
+DLL_PUBLIC bool AppMC::add_clause(const vector<CMSat::Lit>& lits)
 {
-    if (red == false) return data->counter.solver_add_clause(lits);
-    else return data->counter.solver->okay();
+    return data->counter.solver_add_clause(lits);
 }
 
 DLL_PUBLIC bool AppMC::add_xor_clause(const vector<uint32_t>& vars, bool rhs)

diff --git a/src/approxmc.h b/src/approxmc.h
@@ -75,7 +75,7 @@ class AppMC
     void new_var();
     void new_vars(uint32_t num);
     uint32_t nVars();
-    bool add_clause(const std::vector<CMSat::Lit>& lits, bool red = false);
+    bool add_clause(const std::vector<CMSat::Lit>& lits);
     bool add_red_clause(const std::vector<CMSat::Lit>& lits);
     bool add_xor_clause(const std::vector<uint32_t>& vars, bool rhs);
     bool add_bnn_clause(

diff --git a/src/main.cpp b/src/main.cpp
@@ -414,7 +414,7 @@ void get_cnf_from_arjun() {
         for(auto l: clause) {
             if (l.var() >= orig_num_vars) { ok = false; break; }
         }
-        if (ok) appmc->add_clause(clause, false);
+        if (ok) appmc->add_clause(clause);
     }
     arjun->end_getting_small_clauses();
 
@@ -515,7 +515,7 @@ void transfer_unit_clauses_from_arjun()
     for(const auto& unit: units) {
         if (unit.var() < appmc->nVars()) {
             cl[0] = unit;
-            appmc->add_clause(cl, false);
+            appmc->add_clause(cl);
         }
     }
 }
@@ -573,6 +573,7 @@ int main(int argc, char** argv)
                     sampling_vars, false, false, false, 2, 2, true, false);
             appmc->new_vars(ret.nvars);
             for(const auto& cl: ret.cnf) appmc->add_clause(cl);
+            for(const auto& cl: ret.red_cnf) appmc->add_red_clause(cl);
             sampling_vars = ret.sampling_vars;
             offset_count_by_2_pow = ret.empty_occs;
         } else {