Merge branch 'master' into staging-next

Hydra: ?compare=1473892

4 files changed, 126 insertions, 33 deletions

diff --git a/pkgs/applications/science/logic/aiger/default.nix b/pkgs/applications/science/logic/aiger/default.nix
index 1a60c5e148cc..03524fc6b222 100644
--- a/pkgs/applications/science/logic/aiger/default.nix
+++ b/pkgs/applications/science/logic/aiger/default.nix
@@ -13,18 +13,15 @@ stdenv.mkDerivation rec {
 
   configurePhase = ''
     # Set up picosat, so we can build 'aigbmc'
-    echo $(pwd)
-    ls ..
     mkdir ../picosat
     ln -s ${picosat}/include/picosat/picosat.h ../picosat/picosat.h
     ln -s ${picosat}/lib/picosat.o             ../picosat/picosat.o
     ln -s ${picosat}/share/picosat.version     ../picosat/VERSION
-    ls ..
     ./configure.sh
   '';
 
   installPhase = ''
-    mkdir -p $out/bin
+    mkdir -p $out/bin $dev/include $lib/lib
 
     # Do the installation manually, as the Makefile has odd
     # cyrillic characters, and this is easier than adding
@@ -41,8 +38,13 @@ stdenv.mkDerivation rec {
     for x in ''${BINS[*]}; do
       install -m 755 -s $x $out/bin/$x
     done
+
+    cp -v aiger.o $lib/lib
+    cp -v aiger.h $dev/include
   '';
 
+  outputs = [ "out" "dev" "lib" ];
+
   meta = {
     description = "And-Inverter Graph (AIG) utilities";
     homepage    = http://fmv.jku.at/aiger/;
diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix
index aa815e48db41..8e0ad22bba18 100644
--- a/pkgs/applications/science/logic/boolector/default.nix
+++ b/pkgs/applications/science/logic/boolector/default.nix
@@ -1,41 +1,50 @@
-{ stdenv, fetchurl, writeShellScriptBin }:
+{ stdenv, fetchFromGitHub
+, cmake, lingeling, btor2tools
+}:
 
 stdenv.mkDerivation rec {
   name    = "boolector-${version}";
-  version = "2.4.1";
-  src = fetchurl {
-    url    = "http://fmv.jku.at/boolector/boolector-${version}-with-lingeling-bbc.tar.bz2";
-    sha256 = "0mdf7hwix237pvknvrpazcx6s3ininj5k7vhysqjqgxa7lxgq045";
+  version = "3.0.0";
+
+  src = fetchFromGitHub {
+    owner  = "boolector";
+    repo   = "boolector";
+    rev    = "refs/tags/${version}";
+    sha256 = "15i3ni5klss423m57wcy1gx0m5wfrjmglapwg85pm7fb3jj1y7sz";
   };
 
-  prePatch =
-    let
-      lingelingPatch = writeShellScriptBin "lingeling-patch" ''
-        sed -i -e "1i#include <stdint.h>" lingeling/lglib.h
-
-        ${crossFix}/bin/crossFix lingeling
-      '';
-      crossFix = writeShellScriptBin "crossFix" ''
-        # substituteInPlace not available here
-        sed -i $1/makefile.in \
-          -e 's@ar rc@$(AR) rc@' \
-          -e 's@ranlib@$(RANLIB)@'
-      '';
-    in ''
-    sed -i -e 's@mv lingeling\* lingeling@\0 \&\& ${lingelingPatch}/bin/lingeling-patch@' makefile
-    sed -i -e 's@mv boolector\* boolector@\0 \&\& ${crossFix}/bin/crossFix boolector@' makefile
-  '';
+  nativeBuildInputs = [ cmake ];
+  buildInputs = [ lingeling btor2tools ];
+
+  cmakeFlags =
+    [ "-DSHARED=ON"
+      "-DUSE_LINGELING=YES"
+      "-DBTOR2_INCLUDE_DIR=${btor2tools.dev}/include"
+      "-DBTOR2_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so"
+      "-DLINGELING_INCLUDE_DIR=${lingeling.dev}/include"
+      "-DLINGELING_LIBRARIES=${lingeling.lib}/lib/liblgl.a"
+    ];
 
   installPhase = ''
-    mkdir $out
-    mv boolector/bin $out
+    mkdir -p $out/bin $lib/lib $dev/include
+
+    cp -vr bin/* $out/bin
+    cp -vr lib/* $lib/lib
+
+    rm -rf $out/bin/{examples,test}
+
+    cd ../src
+    find . -iname '*.h' -exec cp --parents '{}' $dev/include \;
+    rm -rf $dev/include/tests
   '';
 
-  meta = {
-    license = stdenv.lib.licenses.unfreeRedistributable;
+  outputs = [ "out" "dev" "lib" ];
+
+  meta = with stdenv.lib; {
     description = "An extremely fast SMT solver for bit-vectors and arrays";
-    homepage    = "http://fmv.jku.at/boolector";
-    platforms   = stdenv.lib.platforms.linux;
-    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+    homepage    = https://boolector.github.io;
+    license     = licenses.mit;
+    platforms   = platforms.linux;
+    maintainers = with maintainers; [ thoughtpolice ];
   };
 }
diff --git a/pkgs/applications/science/logic/btor2tools/default.nix b/pkgs/applications/science/logic/btor2tools/default.nix
new file mode 100644
index 000000000000..ed3d9e638121
--- /dev/null
+++ b/pkgs/applications/science/logic/btor2tools/default.nix
@@ -0,0 +1,33 @@
+{ stdenv, fetchFromGitHub }:
+
+stdenv.mkDerivation rec {
+  name = "btor2tools-${version}";
+  version = "pre55_8c150b39";
+
+  src = fetchFromGitHub {
+    owner  = "boolector";
+    repo   = "btor2tools";
+    rev    = "8c150b39cdbcdef4247344acf465d75ef642365d";
+    sha256 = "1r5pid4x567nms02ajjrz3v0zj18k0fi5pansrmc2907rnx2acxx";
+  };
+
+  configurePhase = "./configure.sh -shared";
+
+  installPhase = ''
+    mkdir -p $out $dev/include/btor2parser/ $lib/lib
+
+    cp -vr bin $out
+    cp -v  src/btor2parser/btor2parser.h $dev/include/btor2parser
+    cp -v  build/libbtor2parser.* $lib/lib
+  '';
+
+  outputs = [ "out" "dev" "lib" ];
+
+  meta = with stdenv.lib; {
+    description = "Fast SAT solver";
+    homepage    = http://fmv.jku.at/lingeling/;
+    license     = licenses.mit;
+    platforms   = platforms.linux;
+    maintainers = with maintainers; [ thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/lingeling/default.nix b/pkgs/applications/science/logic/lingeling/default.nix
new file mode 100644
index 000000000000..000587a22e67
--- /dev/null
+++ b/pkgs/applications/science/logic/lingeling/default.nix
@@ -0,0 +1,49 @@
+{ stdenv, fetchFromGitHub
+, aiger
+}:
+
+stdenv.mkDerivation rec {
+  name = "lingeling-${version}";
+  # This is the version used in satcomp2018, which was
+  # relicensed, and also known as version 'bcj'
+  version = "pre1_03b4860d";
+
+  src = fetchFromGitHub {
+    owner  = "arminbiere";
+    repo   = "lingeling";
+    rev    = "03b4860d14016f42213ea271014f2f13d181f504";
+    sha256 = "1lw1yfy219p7rrk88sbq4zl24b70040zapbjdrpv5a6i0jsblksx";
+  };
+
+  configurePhase = ''
+    ./configure.sh
+
+    # Rather than patch ./configure, just sneak in use of aiger here, since it
+    # doesn't handle real build products very well (it works on a build-time
+    # dir, not installed copy)... This is so we can build 'blimc'
+    substituteInPlace ./makefile \
+      --replace 'targets: liblgl.a' 'targets: liblgl.a blimc'      \
+      --replace '$(AIGER)/aiger.o'  '${aiger.lib}/lib/aiger.o'     \
+      --replace '$(AIGER)/aiger.h'  '${aiger.dev}/include/aiger.h' \
+      --replace '-I$(AIGER)'        '-I${aiger.dev}/include'
+  '';
+
+  installPhase = ''
+    mkdir -p $out/bin $lib/lib $dev/include
+
+    cp lglib.h  $dev/include
+    cp liblgl.a $lib/lib
+
+    cp lingeling plingeling treengeling ilingeling blimc $out/bin
+  '';
+
+  outputs = [ "out" "dev" "lib" ];
+
+  meta = with stdenv.lib; {
+    description = "Fast SAT solver";
+    homepage    = http://fmv.jku.at/lingeling/;
+    license     = licenses.mit;
+    platforms   = platforms.linux;
+    maintainers = with maintainers; [ thoughtpolice ];
+  };
+}