From d66d778a2261e80a505910edb45965ec14e9a04c Mon Sep 17 00:00:00 2001
From: Robert Scott <code@humanleg.org.uk>
Date: Sat, 18 Jun 2022 14:59:23 +0100
Subject: [PATCH] sharpsat-td: init at unstable-2021-09-05

---
 .../science/logic/sharpsat-td/default.nix     | 64 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 +
 2 files changed, 66 insertions(+)
 create mode 100644 pkgs/applications/science/logic/sharpsat-td/default.nix

diff --git a/pkgs/applications/science/logic/sharpsat-td/default.nix b/pkgs/applications/science/logic/sharpsat-td/default.nix
new file mode 100644
index 000000000000..de9e212d8cc8
--- /dev/null
+++ b/pkgs/applications/science/logic/sharpsat-td/default.nix
@@ -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" ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index d525f2e5da02..9be479d86117 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -29813,6 +29813,8 @@ with pkgs;
     inherit (darwin.apple_sdk.frameworks) CoreServices CoreMIDI;
   };
 
+  sharpsat-td = callPackage ../applications/science/logic/sharpsat-td { };
+
   shntool = callPackage ../applications/audio/shntool { };
 
   sipp = callPackage ../development/tools/misc/sipp { };