tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 stdenv,
3 fetchFromGitHub,
4 lib,
5 python3,
6 meson,
7 ninja,
8 git,
9 btor2tools,
10 symfpu,
11 gtest,
12 gmp,
13 cadical,
14 cryptominisat,
15 kissat,
16 zlib,
17 pkg-config,
18 cmake,
19 aiger,
20}:
21
22stdenv.mkDerivation (finalAttrs: {
23 pname = "bitwuzla";
24 version = "0.8.1";
25
26 src = fetchFromGitHub {
27 owner = "bitwuzla";
28 repo = "bitwuzla";
29 rev = finalAttrs.version;
30 hash = "sha256-4Gf06aZ3iBEu0bNZAGgWCXVgKA0ew37Zf6XArnlVAXw=";
31 };
32
33 strictDeps = true;
34
35 nativeBuildInputs = [
36 meson
37 pkg-config
38 git
39 ninja
40 cmake
41 ];
42
43 buildInputs = [
44 cadical
45 cryptominisat
46 btor2tools
47 symfpu
48 gmp
49 zlib
50 kissat
51 aiger
52 ];
53
54 mesonFlags = [
55 # note: the default value for default_library fails to link dynamic dependencies
56 # but setting it to shared works even in pkgsStatic
57 "-Ddefault_library=shared"
58 "-Dcryptominisat=true"
59 "-Dkissat=true"
60 "-Daiger=true"
61
62 (lib.strings.mesonEnable "testing" finalAttrs.finalPackage.doCheck)
63 ];
64
65 nativeCheckInputs = [ python3 ];
66 checkInputs = [ gtest ];
67 # two tests fail on darwin
68 doCheck = stdenv.hostPlatform.isLinux;
69 doInstallCheck = true;
70 installCheckPhase = ''
71 runHook preInstallCheck
72
73 export needle=11011110101011011011111011101111
74
75 cat > file.smt2 <<EOF
76 (declare-fun a () (_ BitVec 32))
77 (assert (= a #b$needle))
78 (check-sat)
79 (get-model)
80 EOF
81
82 # check each backend
83 (
84 set -euxo pipefail;
85 $out/bin/bitwuzla -S cms -j 3 -m file.smt2 | tee /dev/stderr | grep $needle;
86 $out/bin/bitwuzla -S cadical -m file.smt2 | tee /dev/stderr | grep $needle;
87 $out/bin/bitwuzla -S kissat -m file.smt2 | tee /dev/stderr | grep $needle;
88 )
89
90 runHook postInstallCheck
91 '';
92
93 meta = {
94 description = "SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";
95 mainProgram = "bitwuzla";
96 homepage = "https://bitwuzla.github.io";
97 license = lib.licenses.mit;
98 platforms = lib.platforms.unix;
99 maintainers = with lib.maintainers; [ symphorien ];
100 };
101})