pkgs/by-name/sh/sharpsat-td/package.nix

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