tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 flex,
6 bison,
7 gmp,
8 perl,
9}:
10
11stdenv.mkDerivation rec {
12 pname = "cvc3";
13 version = "2.4.1";
14
15 src = fetchurl {
16 url = "https://cs.nyu.edu/acsys/cvc3/releases/${version}/${pname}-${version}.tar.gz";
17 sha256 = "1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym";
18 };
19
20 buildInputs = [
21 gmp
22 flex
23 bison
24 perl
25 ];
26
27 patches = [ ./cvc3-2.4.1-gccv6-fix.patch ];
28
29 # fails to configure on darwin due to gmp not found
30 configureFlags = [
31 "LIBS=-L${gmp}/lib"
32 "CXXFLAGS=-I${gmp.dev}/include"
33 ];
34
35 postPatch = ''
36 sed -e "s@ /bin/bash@bash@g" -i Makefile.std
37 find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';'
38
39 # bison 3.7 workaround
40 for f in parsePL parseLisp parsesmtlib parsesmtlib2 ; do
41 ln -s ../parser/''${f}_defs.h src/include/''${f}.hpp
42 done
43 '';
44
45 meta = with lib; {
46 description = "Prover for satisfiability modulo theory (SMT)";
47 mainProgram = "cvc3";
48 maintainers = with maintainers; [ raskin ];
49 platforms = platforms.unix;
50 license = licenses.free;
51 homepage = "https://cs.nyu.edu/acsys/cvc3/index.html";
52 };
53 passthru = {
54 updateInfo = {
55 downloadPage = "https://cs.nyu.edu/acsys/cvc3/download.html";
56 };
57 };
58}