From 2d1621012c52e4e6af53903d06a3017a77b3eff3 Mon Sep 17 00:00:00 2001
From: Shadaj Laddad <shadaj@users.noreply.github.com>
Date: Mon, 4 Apr 2022 20:30:28 +0000
Subject: [PATCH 1/2] symfpu: init at unstable-2019-05-17

---
 maintainers/maintainer-list.nix               |  6 +++++
 .../science/logic/symfpu/default.nix          | 26 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 ++
 3 files changed, 34 insertions(+)
 create mode 100644 pkgs/applications/science/logic/symfpu/default.nix

diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix
index af379f48cb2b..505eccda603d 100644
--- a/maintainers/maintainer-list.nix
+++ b/maintainers/maintainer-list.nix
@@ -11271,6 +11271,12 @@
     githubId = 1151264;
     name = "Sebastian Graf";
   };
+  shadaj = {
+    email = "shadaj@users.noreply.github.com";
+    github = "shadaj";
+    githubId = 543055;
+    name = "Shadaj Laddad";
+  };
   shahrukh330 = {
     email = "shahrukh330@gmail.com";
     github = "shahrukh330";
diff --git a/pkgs/applications/science/logic/symfpu/default.nix b/pkgs/applications/science/logic/symfpu/default.nix
new file mode 100644
index 000000000000..af61b7c617c7
--- /dev/null
+++ b/pkgs/applications/science/logic/symfpu/default.nix
@@ -0,0 +1,26 @@
+{ lib, stdenv, fetchFromGitHub }:
+
+stdenv.mkDerivation rec {
+  pname = "symfpu";
+  version = "unstable-2019-05-17";
+
+  src = fetchFromGitHub {
+    owner  = "martin-cs";
+    repo   = "symfpu";
+    rev    = "8fbe139bf0071cbe0758d2f6690a546c69ff0053";
+    sha256 = "1jf5lkn67q136ppfacw3lsry369v7mdr1rhidzjpbz18jfy9zl9q";
+  };
+
+  installPhase = ''
+    mkdir -p $out/symfpu
+    cp -r * $out/symfpu/
+  '';
+
+  meta = with lib; {
+    description = "A (concrete or symbolic) implementation of IEEE-754 / SMT-LIB floating-point";
+    homepage    = "https://github.com/martin-cs/symfpu";
+    license     = licenses.gpl3Only;
+    platforms   = platforms.unix;
+    maintainers = with maintainers; [ shadaj ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 3a88b23b73b5..eadd2c5fd94b 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -32934,6 +32934,8 @@ with pkgs;
 
   symbiyosys = callPackage ../applications/science/logic/symbiyosys {};
 
+  symfpu = callPackage ../applications/science/logic/symfpu {};
+
   mcy = callPackage ../applications/science/logic/mcy {};
 
   lingeling = callPackage ../applications/science/logic/lingeling {};

From 74b7319023a3428d2d2acb761c6e4a3489211684 Mon Sep 17 00:00:00 2001
From: Shadaj Laddad <shadaj@users.noreply.github.com>
Date: Mon, 4 Apr 2022 20:30:47 +0000
Subject: [PATCH 2/2] cvc5: init at 1.0.0

---
 .../science/logic/cvc5/default.nix            | 34 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 ++
 2 files changed, 36 insertions(+)
 create mode 100644 pkgs/applications/science/logic/cvc5/default.nix

diff --git a/pkgs/applications/science/logic/cvc5/default.nix b/pkgs/applications/science/logic/cvc5/default.nix
new file mode 100644
index 000000000000..c1bf56b45d5b
--- /dev/null
+++ b/pkgs/applications/science/logic/cvc5/default.nix
@@ -0,0 +1,34 @@
+{ lib, stdenv, fetchFromGitHub, pkg-config, cmake, cadical, symfpu, gmp, git, python3, gtest, libantlr3c, antlr3_4, boost, jdk }:
+
+stdenv.mkDerivation rec {
+  pname = "cvc5";
+  version = "1.0.0";
+
+  src = fetchFromGitHub {
+    owner  = "cvc5";
+    repo   = "cvc5";
+    rev    = "cvc5-${version}";
+    sha256 = "03sxqwmlajffmv7lncqs1bx8gyihkpnikk87q9wjrd4776n13ign";
+  };
+
+  nativeBuildInputs = [ pkg-config cmake ];
+  buildInputs = [ cadical.dev symfpu gmp git python3 python3.pkgs.toml gtest libantlr3c antlr3_4 boost jdk ];
+
+  preConfigure = ''
+    patchShebangs ./src/
+  '';
+
+  cmakeFlags = [
+    "-DCMAKE_BUILD_TYPE=Production"
+    "-DBUILD_SHARED_LIBS=1"
+    "-DANTLR3_JAR=${antlr3_4}/lib/antlr/antlr-3.4-complete.jar"
+  ];
+
+  meta = with lib; {
+    description = "A high-performance theorem prover and SMT solver";
+    homepage    = "https://cvc5.github.io";
+    license     = licenses.gpl3Only;
+    platforms   = platforms.unix;
+    maintainers = with maintainers; [ shadaj ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index eadd2c5fd94b..34bb636eac4b 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -32770,6 +32770,8 @@ with pkgs;
     jdk = jdk8; # TODO: remove override https://github.com/NixOS/nixpkgs/pull/89731
   };
 
+  cvc5 = callPackage ../applications/science/logic/cvc5 { };
+
   drat-trim = callPackage ../applications/science/logic/drat-trim {};
 
   ekrhyper = callPackage ../applications/science/logic/ekrhyper {