diff options
Diffstat (limited to 'pkgs/applications/science/logic/drat-trim/default.nix')
-rw-r--r-- | pkgs/applications/science/logic/drat-trim/default.nix | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/drat-trim/default.nix b/pkgs/applications/science/logic/drat-trim/default.nix new file mode 100644 index 000000000000..50454847baf1 --- /dev/null +++ b/pkgs/applications/science/logic/drat-trim/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation rec { + name = "drat-trim-2017-08-31"; + + src = fetchFromGitHub { + owner = "marijnheule"; + repo = "drat-trim"; + rev = "37ac8f874826ffa3500a00698910e137498defac"; + sha256 = "1m9q47dfnvdli1z3kb1jvvbm0dgaw725k1aw6h9w00bggqb91bqh"; + }; + + postPatch = '' + substituteInPlace Makefile --replace gcc cc + ''; + + installPhase = '' + install -Dt $out/bin drat-trim + ''; + + meta = with stdenv.lib; { + description = "A proof checker for unSAT proofs"; + longDescription = '' + DRAT-trim is a satisfiability proof checking and trimming + utility designed to validate proofs for all known satisfiability + solving and preprocessing techniques. DRAT-trim can also emit + trimmed formulas, optimized proofs, and TraceCheck+ dependency + graphs. + + DRAT-trim has been used as part of the judging process in the + annual SAT Competition in recent years, in order to check + competing SAT solvers' work when they claim that a SAT instance + is unsatisfiable. + ''; + homepage = https://www.cs.utexas.edu/~marijn/drat-trim/; + license = licenses.mit; + maintainers = with maintainers; [ kini ]; + platforms = platforms.all; + }; +} |