tjh.dev
1diff --git a/src/arjun.cpp b/src/arjun.cpp
2index d6ad786..119a267 100644
3--- a/src/arjun.cpp
4+++ b/src/arjun.cpp
5@@ -98,6 +98,11 @@ DLL_PUBLIC bool Arjun::add_clause(const vector<CMSat::Lit>& lits)
6 return arjdata->common.solver->add_clause(lits);
7 }
8
9+DLL_PUBLIC bool Arjun::add_red_clause(const vector<CMSat::Lit>& lits)
10+{
11+ return arjdata->common.solver->add_red_clause(lits);
12+}
13+
14 DLL_PUBLIC bool Arjun::add_xor_clause(const vector<uint32_t>& vars, bool rhs)
15 {
16 assert(false && "Funnily enough this does NOT work. The XORs would generate a BVA variable, and that would then not be returned as part of the simplified CNF. We could calculate a smaller independent set, but that's all.");
17diff --git a/src/arjun.h b/src/arjun.h
18index a39070c..907472a 100644
19--- a/src/arjun.h
20+++ b/src/arjun.h
21@@ -61,6 +61,7 @@ namespace ArjunNS {
22 void new_var();
23 bool add_xor_clause(const std::vector<uint32_t>& vars, bool rhs);
24 bool add_clause(const std::vector<CMSat::Lit>& lits);
25+ bool add_red_clause(const std::vector<CMSat::Lit>& lits);
26 bool add_bnn_clause(
27 const std::vector<CMSat::Lit>& lits,
28 signed cutoff,