diff options
| -rw-r--r-- | pkgs/applications/science/logic/monosat/default.nix | 73 | ||||
| -rw-r--r-- | pkgs/top-level/all-packages.nix | 2 | ||||
| -rw-r--r-- | pkgs/top-level/python-packages.nix | 2 |
3 files changed, 77 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/monosat/default.nix b/pkgs/applications/science/logic/monosat/default.nix new file mode 100644 index 000000000000..b0de08e489ad --- /dev/null +++ b/pkgs/applications/science/logic/monosat/default.nix @@ -0,0 +1,73 @@ +{ stdenv, fetchFromGitHub, cmake, zlib, gmp, jdk8, + # The JDK we use on Darwin currenly makes extensive use of rpaths which are + # annoying and break the python library, so let's not bother for now + includeJava ? !stdenv.hostPlatform.isDarwin, includeGplCode ? true }: + +with stdenv.lib; + +let + boolToCmake = x: if x then "ON" else "OFF"; + + rev = "cbaf79cfd01cba97b46cae5a9d7b832771ff442c"; + sha256 = "1nx3wh34y53lrwgh94cskdrdyrj26jn3py7z2cn4bvacz0wzhi6n"; + + pname = "monosat"; + version = substring 0 7 sha256; + + src = fetchFromGitHub { + owner = "sambayless"; + repo = pname; + inherit rev sha256; + }; + + core = stdenv.mkDerivation rec { + name = "${pname}-${version}"; + inherit src; + buildInputs = [ cmake zlib gmp jdk8 ]; + + cmakeFlags = [ "-DJAVA=${boolToCmake includeJava}" "-DGPL=${boolToCmake includeGplCode}" ]; + + # Minor logic bug: https://github.com/sambayless/monosat/issues/11#issuecomment-403297720 + postPatch = '' + substituteInPlace CMakeLists.txt \ + --replace '"&&" "true"' '"||" "true"' + ''; + + postInstall = optionalString includeJava '' + mkdir -p $out/share/java + cp monosat.jar $out/share/java + ''; + + passthru = { inherit python; }; + + meta = { + description = "SMT solver for Monotonic Theories"; + platforms = platforms.unix; + license = if includeGplCode then licenses.gpl2 else licenses.mit; + homepage = https://github.com/sambayless/monosat; + }; + }; + + python = { buildPythonPackage, cython }: buildPythonPackage { + inherit pname version src; + + # The top-level "source" is what fetchFromGitHub gives us. The rest is inside the repo + sourceRoot = "source/src/monosat/api/python/"; + + propagatedBuildInputs = [ core cython ]; + + # The relative paths here don't make sense for our Nix build + # Also, let's use cython since it should produce faster bindings + # TODO: do we want to just reference the core monosat library rather than copying the + # shared lib? The current setup.py copies the .dylib/.so... + postPatch = '' + substituteInPlace setup.py \ + --replace '../../../../libmonosat.dylib' '${core}/lib/libmonosat.dylib' \ + --replace '../../../../libmonosat.so' '${core}/lib/libmonosat.so' \ + --replace 'use_cython=False' 'use_cython=True' + + # This seems to be forgotten and unused. See https://github.com/sambayless/monosat/issues/10 + rm monosat/cnf.py + ''; + }; +in core \ No newline at end of file diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 5c49b6f47970..2e8285db1aab 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -20575,6 +20575,8 @@ with pkgs; minisat = callPackage ../applications/science/logic/minisat {}; minisatUnstable = callPackage ../applications/science/logic/minisat/unstable.nix {}; + monosat = callPackage ../applications/science/logic/monosat {}; + opensmt = callPackage ../applications/science/logic/opensmt { }; ott = callPackage ../applications/science/logic/ott { }; diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix index 381ad48b0e71..0cbd5f0b468b 100644 --- a/pkgs/top-level/python-packages.nix +++ b/pkgs/top-level/python-packages.nix @@ -8283,6 +8283,8 @@ in { }; }; + monosat = disabledIf (!isPy3k) (pkgs.monosat.python { inherit buildPythonPackage; inherit (self) cython; }); + monotonic = buildPythonPackage rec { pname = "monotonic"; version = "1.3"; |