tjh.dev
1{
2 lib,
3 stdenv,
4 fetchgit,
5 cmake,
6 zlib,
7 boost,
8}:
9
10stdenv.mkDerivation {
11 pname = "avy";
12 version = "2019.05.01"; # date of cav19 tag
13
14 src = fetchgit {
15 url = "https://bitbucket.org/arieg/extavy";
16 rev = "cav19";
17 sha256 = "0qdzy9srxp5f38x4dbb3prnr9il6cy0kz80avrvd7fxqzy7wdlwy";
18 fetchSubmodules = true;
19 };
20
21 nativeBuildInputs = [ cmake ];
22 buildInputs = [
23 zlib
24 boost.out
25 boost.dev
26 ];
27 env.NIX_CFLAGS_COMPILE = toString (
28 [ "-Wno-narrowing" ]
29 # Squelch endless stream of warnings on same few things
30 ++ lib.optionals stdenv.cc.isClang [
31 "-Wno-empty-body"
32 "-Wno-tautological-compare"
33 "-Wc++11-compat-deprecated-writable-strings"
34 "-Wno-deprecated"
35 ]
36 );
37
38 prePatch = ''
39 sed -i -e '1i#include <stdint.h>' abc/src/bdd/dsd/dsd.h
40 substituteInPlace abc/src/bdd/dsd/dsd.h --replace \
41 '((Child = Dsd_NodeReadDec(Node,Index))>=0);' \
42 '((intptr_t)(Child = Dsd_NodeReadDec(Node,Index))>=0);'
43
44 patch -p1 -d minisat -i ${./minisat-fenv.patch}
45 patch -p1 -d glucose -i ${./glucose-fenv.patch}
46 '';
47
48 installPhase = ''
49 mkdir -p $out/bin
50 cp avy/src/{avy,avybmc} $out/bin/
51 '';
52
53 meta = {
54 description = "AIGER model checking for Property Directed Reachability";
55 homepage = "https://arieg.bitbucket.io/avy/";
56 license = lib.licenses.mit;
57 maintainers = with lib.maintainers; [ thoughtpolice ];
58 platforms = lib.platforms.linux;
59 };
60}