Making it all work with red as a parameter, which is the old way

meelgroup · Nov 12, 2023 · 1425a30 · 1425a30
1 parent 0039f23
commit 1425a30
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/src/approxmc.cpp b/src/approxmc.cpp
@@ -273,9 +273,10 @@ 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)
+DLL_PUBLIC bool AppMC::add_clause(const vector<CMSat::Lit>& lits, bool red)
 {
-    return data->counter.solver_add_clause(lits);
+    if (red == false) return data->counter.solver_add_clause(lits);
+    else return data->counter.solver->okay();
 }
 
 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 add_clause(const std::vector<CMSat::Lit>& lits, bool red = false);
     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);
+        if (ok) appmc->add_clause(clause, false);
     }
     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);
+            appmc->add_clause(cl, false);
         }
     }
 }