about summary refs log tree commit diff
path: root/pkgs/applications/science/logic/bitwuzla
diff options
context:
space:
mode:
authorGuillaume Girol <symphorien+git@xlumurb.eu>2024-04-03 12:00:00 +0000
committerGuillaume Girol <symphorien+git@xlumurb.eu>2024-04-03 12:00:00 +0000
commit457090959e06536fa01a2b91f005eb61e40d83dc (patch)
tree85bd83e4ae7971b6ceacdaf85a4f50482aeb9584 /pkgs/applications/science/logic/bitwuzla
parent5ff10ee902e80132c5e92321a03452cd7b0d403b (diff)
bitwuzla: unstable-2022-10-03 -> 0.4.0
lingeling, picosat and minisat are no longer dependencies
Diffstat (limited to 'pkgs/applications/science/logic/bitwuzla')
-rw-r--r--pkgs/applications/science/logic/bitwuzla/default.nix40
1 files changed, 13 insertions, 27 deletions
diff --git a/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix
index bacf8620e5fdc..0d85540c280ba 100644
--- a/pkgs/applications/science/logic/bitwuzla/default.nix
+++ b/pkgs/applications/science/logic/bitwuzla/default.nix
@@ -2,62 +2,48 @@
 , fetchFromGitHub
 , lib
 , python3
-, cmake
-, lingeling
+, meson
+, ninja
+, git
 , btor2tools
 , symfpu
 , gtest
 , gmp
 , cadical
-, minisat
-, picosat
 , cryptominisat
 , zlib
 , pkg-config
-  # "*** internal error in 'lglib.c': watcher stack overflow" on aarch64-linux
-, withLingeling ? !stdenv.hostPlatform.isAarch64
 }:
 
 stdenv.mkDerivation rec {
   pname = "bitwuzla";
-  version = "unstable-2022-10-03";
+  version = "0.4.0";
 
   src = fetchFromGitHub {
     owner = "bitwuzla";
     repo = "bitwuzla";
-    rev = "3bc0f9f1aca04afabe1aff53dd0937924618b2ad";
-    hash = "sha256-UXZERl7Nedwex/oUrcf6/GkDSgOQ537WDYm117RfvWo=";
+    rev = version;
+    hash = "sha256-ZEdV4ml1LwrYwscgOcL2gLx/ijPYqRktXMQH/Njh8OI=";
   };
 
-  nativeBuildInputs = [ cmake pkg-config ];
+  strictDeps = true;
+
+  nativeBuildInputs = [ meson pkg-config git ninja ];
   buildInputs = [
     cadical
     cryptominisat
-    picosat
-    minisat
     btor2tools
     symfpu
     gmp
     zlib
-  ] ++ lib.optional withLingeling lingeling;
+  ];
 
-  cmakeFlags = [
-    "-DBUILD_SHARED_LIBS=ON"
-    "-DPicoSAT_INCLUDE_DIR=${lib.getDev picosat}/include/picosat"
-    "-DBtor2Tools_INCLUDE_DIR=${lib.getDev btor2tools}/include/btor2parser"
-    "-DBtor2Tools_LIBRARIES=${lib.getLib btor2tools}/lib/libbtor2parser${stdenv.hostPlatform.extensions.sharedLibrary}"
-  ] ++ lib.optional doCheck "-DTESTING=YES";
+  mesonFlags = [ "-Ddefault_library=shared" ];
 
-  nativeCheckInputs = [ python3 gtest ];
+  nativeCheckInputs = [ python3 ];
+  checkInputs = [ gtest ];
   # two tests fail on darwin and 3 on aarch64-linux
   doCheck = stdenv.hostPlatform.isLinux && (!stdenv.hostPlatform.isAarch64);
-  preCheck = let
-    var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH";
-  in
-    ''
-      export ${var}=$(readlink -f lib)
-      patchShebangs ..
-    '';
 
   meta = with lib; {
     description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";