From a9f70d542d1e492aaa4e012b264c2a19ae4af8bc Mon Sep 17 00:00:00 2001
From: Michael Raskin <7c6f434c@mail.ru>
Date: Sun, 5 Dec 2010 17:28:41 +0000
Subject: [PATCH] Adding CVC3 satisfiability modulo theory (SMT) solver

svn path=/nixpkgs/trunk/; revision=24975
---
 .../science/logic/cvc3/default.nix            | 54 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 +
 2 files changed, 56 insertions(+)
 create mode 100644 pkgs/applications/science/logic/cvc3/default.nix

diff --git a/pkgs/applications/science/logic/cvc3/default.nix b/pkgs/applications/science/logic/cvc3/default.nix
new file mode 100644
index 000000000000..9bb8f8cde4ca
--- /dev/null
+++ b/pkgs/applications/science/logic/cvc3/default.nix
@@ -0,0 +1,54 @@
+x@{builderDefsPackage
+  , flex, bison, gmp, perl
+  , ...}:
+builderDefsPackage
+(a :  
+let 
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+    ["gmp"];
+
+  buildInputs = (map (n: builtins.getAttr n x)
+    (builtins.attrNames (builtins.removeAttrs x helperArgNames)))
+    ++ [(a.lib.overrideDerivation x.gmp (y: {dontDisableStatic=true;}))];
+  sourceInfo = rec {
+    baseName="cvc3";
+    version="2.2";
+    name="${baseName}-${version}";
+    url="http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${name}.tar.gz";
+    hash="1dw12d5vrixfr6l9j6j7026vrr22zb433xyl6n5yxx4hgfywi0ji";
+  };
+in
+rec {
+  src = a.fetchurl {
+    url = sourceInfo.url;
+    sha256 = sourceInfo.hash;
+  };
+
+  inherit (sourceInfo) name version;
+  inherit buildInputs;
+
+  /* doConfigure should be removed if not needed */
+  phaseNames = ["fixPaths" "doConfigure" "doMakeInstall"];
+  fixPaths = a.fullDepEntry (''
+    sed -e "s@ /bin/bash@bash@g" -i Makefile.std
+    find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';'
+  '') ["minInit" "doUnpack"];
+      
+  meta = {
+    description = "A prover for satisfiability modulo theory (SMT)";
+    maintainers = with a.lib.maintainers;
+    [
+      raskin
+    ];
+    platforms = with a.lib.platforms;
+      linux;
+    license = "free-noncopyleft";
+    homepage = "http://www.cs.nyu.edu/acsys/cvc3/index.html";
+  };
+  passthru = {
+    updateInfo = {
+      downloadPage = "http://www.cs.nyu.edu/acsys/cvc3/download.html";
+    };
+  };
+}) x
+
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 7aec966045e8..7fbe22c97e04 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6955,6 +6955,8 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  cvc3 = callPackage ../applications/science/logic/cvc3 {};
+
   eprover = callPackage ../applications/science/logic/eProver {
     texLive = texLiveAggregationFun {
       paths = [