Unverified Commit 45571284 authored by Guillaume Girol's avatar Guillaume Girol Committed by GitHub
Browse files

Merge pull request #130663 from symphorien/bitwuzla 

bitwuzla: init at unstable-2021-07-01
parents b27f145c 1894e8d9

pkgs/applications/science/logic/bitwuzla/default.nix

0 → 100644
+67 −0
Original line number Diff line number Diff line 
{ stdenv

, fetchFromGitHub

, lib

, python3

, cmake

, lingeling

, btor2tools

, 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-2021-07-01";



  src = fetchFromGitHub {

    owner = "bitwuzla";

    repo = "bitwuzla";

    rev = "58d720598e359b1fdfec4a469c76f1d1f24db51a";

    sha256 = "06ymqsdppyixb918161rmbgqvbnarj4nm4az88lkn3ri4gyimw04";

  };



  nativeBuildInputs = [ cmake pkg-config ];

  buildInputs = [

    cadical

    cryptominisat

    picosat

    minisat

    btor2tools

    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";



  checkInputs = [ python3 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";

    homepage = "https://bitwuzla.github.io";

    license = licenses.mit;

    platforms = platforms.unix;

    maintainers = with maintainers; [ symphorien ];

  };

}

pkgs/applications/science/logic/cadical/default.nix

+19 −3
Original line number Diff line number Diff line
@@ -11,14 +11,30 @@ stdenv.mkDerivation rec { 
    sha256 = "05lvnvapjawgkky38xknb9lgaliiwan4kggmb9yggl4ifpjrh8qf";

  };



  outputs = [ "out" "dev" "lib" ];

  doCheck = true;

  dontAddPrefix = true;



  # the configure script is not generated by autotools and does not accept the

  # arguments that the default configurePhase passes like --prefix and --libdir

  configurePhase = ''

    runHook preConfigure



    ./configure



    runHook postConfigure

  '';



  installPhase = ''

    runHook preInstall



    install -Dm0755 build/cadical "$out/bin/cadical"

    install -Dm0755 build/mobical "$out/bin/mobical"

    mkdir -p "$out/share/doc/${pname}-${version}/"

    install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}-${version}/"

    install -Dm0644 src/ccadical.h "$dev/include/ccadical.h"

    install -Dm0644 build/libcadical.a "$lib/lib/libcadical.a"

    mkdir -p "$out/share/doc/${pname}/"

    install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}/"



    runHook postInstall

  '';



  meta = with lib; {

pkgs/top-level/all-packages.nix

+2 −0
Original line number Diff line number Diff line
@@ -30535,6 +30535,8 @@ in 














  boolector = callPackage ../applications/science/logic/boolector {};



























  bitwuzla = callPackage ../applications/science/logic/bitwuzla {};



























  symbiyosys = callPackage ../applications/science/logic/symbiyosys {};





























  mcy = callPackage ../applications/science/logic/mcy {};