arjun-cnf: init at 2.5.2
This commit is contained in:
parent
7bb1056605
commit
02f58ae811
28
pkgs/by-name/ar/arjun-cnf/fix-red-clause.patch
Normal file
28
pkgs/by-name/ar/arjun-cnf/fix-red-clause.patch
Normal file
@ -0,0 +1,28 @@
|
||||
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,
|
48
pkgs/by-name/ar/arjun-cnf/package.nix
Normal file
48
pkgs/by-name/ar/arjun-cnf/package.nix
Normal file
@ -0,0 +1,48 @@
|
||||
{ stdenv
|
||||
, fetchFromGitHub
|
||||
, fetchpatch
|
||||
, cmake
|
||||
, cryptominisat
|
||||
, boost
|
||||
, louvain-community
|
||||
, lib
|
||||
}:
|
||||
|
||||
stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "arjun-cnf";
|
||||
version = "2.5.2";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "meelgroup";
|
||||
repo = "arjun";
|
||||
rev = finalAttrs.version;
|
||||
hash = "sha256-5duc05s654HLjbf+dPgyMn6QUVvB0vLji3M4S2o/QYU=";
|
||||
};
|
||||
|
||||
# Can be removed after next release
|
||||
patches = [
|
||||
(fetchpatch {
|
||||
url = "https://github.com/meelgroup/arjun/commit/34188760f1ab4b1b557c45ccaee8d2b9b6f0b901.patch";
|
||||
hash = "sha256-E/yk2ohHP2BAFg353r8EU01bZCqeEjvpJCrBsxPiOWM=";
|
||||
})
|
||||
# Based on https://github.com/meelgroup/arjun/commit/99c4ed4ad820674632c5d9bbcc98c001f8cac98f
|
||||
./fix-red-clause.patch
|
||||
];
|
||||
|
||||
nativeBuildInputs = [ cmake ];
|
||||
|
||||
buildInputs = [
|
||||
boost
|
||||
cryptominisat
|
||||
louvain-community
|
||||
];
|
||||
|
||||
meta = with lib; {
|
||||
description = "CNF minimizer and minimal independent set calculator";
|
||||
homepage = "https://github.com/meelgroup/arjun";
|
||||
license = licenses.mit;
|
||||
maintainers = with maintainers; [ t4ccer ];
|
||||
platforms = platforms.linux;
|
||||
mainProgram = "arjun";
|
||||
};
|
||||
})
|
Loading…
Reference in New Issue
Block a user