mirror of
https://github.com/ilyakooo0/nixpkgs.git
synced 2024-10-06 04:27:27 +03:00
29 lines
1.2 KiB
Diff
29 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,
|