blob: 2f2128d542f1bc5624e2766360eb539b2b8f018d (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
{ lib
, stdenv
, fetchFromGitHub
, fetchzip
, cmake
, gmp
, mpfr
}:
let
satlib-bmc = fetchzip {
url = "https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/BMC/bmc.tar.gz";
stripRoot = false;
sha256 = "sha256-F1Jfrj4iMMf/3LFCShIDMs4JfLkJ51Z4wkL1FDT9b/A=";
};
# needed for mpfr 4.2.0+ support
mpreal = fetchFromGitHub {
owner = "advanpix";
repo = "mpreal";
rev = "mpfrc++-3.6.9";
sha256 = "sha256-l61SKEx4pBocADrEGPVacQ6F2ep9IuvNZ8W08dKeZKg=";
};
in stdenv.mkDerivation rec {
pname = "sharpsat-td";
version = "unstable-2021-09-05";
src = fetchFromGitHub {
owner = "Laakeri";
repo = pname;
rev = "b9bb015305ea5d4e1ac7141691d0fe55ca983d31";
sha256 = "sha256-FE+DUd58eRr5w9RFw0fMHfjIiNDWIcG7XbyWJ/pI28U=";
};
postPatch = ''
# just say no to bundled binaries
rm bin/*
# ensure resultant build calls its own binaries
substituteInPlace src/decomposition.cpp \
--replace '"../../../flow-cutter-pace17/flow_cutter_pace17"' '"'"$out"'/bin/flow_cutter_pace17"'
substituteInPlace src/preprocessor/treewidth.cpp \
--replace '"./flow_cutter_pace17"' '"'"$out"'/bin/flow_cutter_pace17"'
# replace bundled version of mpreal/mpfrc++
rm -r src/mpfr
cp -r ${mpreal} src/mpfr
'';
nativeBuildInputs = [ cmake ];
buildInputs = [ gmp mpfr ];
installPhase = ''
runHook preInstall
mkdir -p $out/bin
install -Dm755 sharpSAT $out/bin/sharpSAT-td
install -Dm755 flow_cutter_pace17 $out/bin/flow_cutter_pace17
runHook postInstall
'';
doInstallCheck = true;
installCheckPhase = ''
runHook preInstallCheck
# "correct" answer from https://sites.google.com/site/marcthurley/sharpsat/benchmarks/collected-model-counts
$out/bin/sharpSAT-td -decot 1 -decow 100 -cs 3500 -tmpdir "$TMPDIR" \
${satlib-bmc}/bmc-ibm-1.cnf | grep -F 'c s exact arb int 7333984412904350856728851870196181665291102236046537207120878033973328441091390427157620940515935993557837912658856672133150412904529478729364681871717139154252602322050981277183916105207406949425074710972297902317183503443350157267211568852295978718386711142950559533715161449971311118966214098944000'
runHook postInstallCheck
'';
meta = {
description = "A fast solver for the #SAT model counting problem";
homepage = "https://github.com/Laakeri/sharpsat-td";
license = with lib.licenses; [ mit asl20 ];
maintainers = with lib.maintainers; [ ris ];
# uses clhash, which is non-portable
platforms = [ "x86_64-linux" "x86_64-darwin" ];
};
}
|
