Merge pull request #178159 from risicle/ris-sharpsat-td
sharpsat-td: init at unstable-2021-09-05
This commit is contained in:
commit
cfbb8e82c6
64
pkgs/applications/science/logic/sharpsat-td/default.nix
Normal file
64
pkgs/applications/science/logic/sharpsat-td/default.nix
Normal file
|
@ -0,0 +1,64 @@
|
|||
{ 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=";
|
||||
};
|
||||
|
||||
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"'
|
||||
'';
|
||||
|
||||
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" ];
|
||||
};
|
||||
}
|
|
@ -34273,6 +34273,8 @@ with pkgs;
|
|||
inherit (darwin.apple_sdk_11_0.frameworks) CoreServices CoreMIDI;
|
||||
};
|
||||
|
||||
sharpsat-td = callPackage ../applications/science/logic/sharpsat-td { };
|
||||
|
||||
shntool = callPackage ../applications/audio/shntool { };
|
||||
|
||||
sipp = callPackage ../development/tools/misc/sipp { };
|
||||
|
|
Loading…
Reference in a new issue