depot/third_party/nixpkgs/pkgs/by-name/ar/arjun-cnf/fix-red-clause.patch
Default email 23b612e36f Project import generated by Copybara.
GitOrigin-RevId: ae5c332cbb5827f6b1f02572496b141021de335f
2024-01-25 23:12:00 +09:00

28 lines
1.2 KiB
Diff

diff --git a/src/arjun.cpp b/src/arjun.cpp
index d6ad786..119a267 100644
--- a/src/arjun.cpp
+++ b/src/arjun.cpp
@@ -98,6 +98,11 @@ DLL_PUBLIC bool Arjun::add_clause(const vector<CMSat::Lit>& lits)
return arjdata->common.solver->add_clause(lits);
}
+DLL_PUBLIC bool Arjun::add_red_clause(const vector<CMSat::Lit>& lits)
+{
+ return arjdata->common.solver->add_red_clause(lits);
+}
+
DLL_PUBLIC bool Arjun::add_xor_clause(const vector<uint32_t>& vars, bool rhs)
{
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.");
diff --git a/src/arjun.h b/src/arjun.h
index a39070c..907472a 100644
--- a/src/arjun.h
+++ b/src/arjun.h
@@ -61,6 +61,7 @@ namespace ArjunNS {
void new_var();
bool add_xor_clause(const std::vector<uint32_t>& vars, bool rhs);
bool add_clause(const std::vector<CMSat::Lit>& lits);
+ bool add_red_clause(const std::vector<CMSat::Lit>& lits);
bool add_bnn_clause(
const std::vector<CMSat::Lit>& lits,
signed cutoff,