diff --git a/resources/3rdparty/nix-scripts/carl/default.nix b/resources/3rdparty/nix-scripts/carl/default.nix
new file mode 100644
index 000000000..69241252f
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/carl/default.nix
@@ -0,0 +1,51 @@
+{ stdenv, fetchFromGitHub, autoconf, pkgconfig, cmake
+, cln, ginac, gmp, boost, eigen3_3, python2, googletest }:
+
+let
+ gtest-cmake = ./gtest.cmake;
+
+in stdenv.mkDerivation rec {
+ name = "carl-${version}";
+ version = "17.12";
+
+ buildInputs = [ cln ginac gmp boost python2 googletest ];
+
+ nativeBuildInputs = [ autoconf pkgconfig cmake ];
+
+ propagatedBuildInputs = [ eigen3_3 ];
+
+ src = fetchFromGitHub {
+ owner = "smtrat";
+ repo = "carl";
+ rev = version;
+ sha256 = "1299i0b6w4v6s2a2kci3jrpdq1lpaw4j3p34gx6gmp9g3n1yp6xq";
+ };
+
+ enableParallelBuilding = true;
+
+ cmakeFlags = [
+ "-DEXPORT_TO_CMAKE=off"
+ "-DUSE_CLN_NUMBERS=on"
+ "-DTHREAD_SAFE=on"
+ "-DUSE_GINAC=on"
+ "-DGINAC_FOUND=on"
+ "-DGINAC_INCLUDE_DIR=${ginac}/include/ginac"
+ "-DGINAC_LIBRARY=${ginac}/lib/libginac.so"
+ "-DGTEST_FOUND=on"
+ "-DGTEST_MAIN_LIBRARY=${googletest}/lib/libgtest_main.a"
+ "-DGTEST_LIBRARY=${googletest}/lib/libgtest.a"
+ ];
+
+ postPatch = ''
+ cp ${gtest-cmake} resources/gtest.cmake
+ substituteInPlace resources/gtest.cmake --subst-var-by googletest ${googletest}
+ sed -e '/set(GTEST/i include(resources/gtest.cmake)' -i resources/resources.cmake
+ '';
+
+ meta = with stdenv.lib; {
+ description = "Computer ARithmetic and Logic library";
+ homepage = http://smtrat.github.io/carl;
+ mainainers = [ maintainers.spacefrogg ];
+ platforms = platforms.all;
+ };
+}
diff --git a/resources/3rdparty/nix-scripts/carl/gtest.cmake b/resources/3rdparty/nix-scripts/carl/gtest.cmake
new file mode 100644
index 000000000..4f098157f
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/carl/gtest.cmake
@@ -0,0 +1,3 @@
+add_imported_library(GTESTCORE STATIC "@googletest@/lib/${CMAKE_FIND_LIBRARY_PREFIXES}gtest${STATIC_EXT}" "@googletest@/include")
+add_imported_library(GTESTMAIN STATIC "@googletest@/lib/${CMAKE_FIND_LIBRARY_PREFIXES}gtest_main${STATIC_EXT}" "@googletest@/include")
+set(GTEST_LIBRARIES GTESTCORE_STATIC GTESTMAIN_STATIC pthread dl)
\ No newline at end of file
diff --git a/resources/3rdparty/nix-scripts/default.nix b/resources/3rdparty/nix-scripts/default.nix
new file mode 100644
index 000000000..9d4aae3cb
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/default.nix
@@ -0,0 +1,14 @@
+self: super:
+with self;
+with self.lib;
+let
+ callPackage = super.lib.callPackageWith self;
+ _self = {
+ z3 = callPackage ./z3 { };
+ stormChecker = callPackage ./storm-checker { ltoSupport = false; tbbSupport = false; mathsatSupport = false; z3Support = false; };
+ carl = callPackage ./carl { };
+ googletest = callPackage ./googletest { };
+ l3pp = callPackage ./l3pp { };
+ mathsat = callPackage ./mathsat { };
+ };
+in _self
diff --git a/resources/3rdparty/nix-scripts/googletest/default.nix b/resources/3rdparty/nix-scripts/googletest/default.nix
new file mode 100644
index 000000000..b46d51765
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/googletest/default.nix
@@ -0,0 +1,22 @@
+{ stdenv, fetchFromGitHub, cmake }:
+
+stdenv.mkDerivation rec {
+ name = "googletest-${version}";
+ version = "1.8.0";
+
+ buildInputs = [ cmake ];
+
+ src = fetchFromGitHub {
+ owner = "google";
+ repo = "googletest";
+ rev = "release-${version}";
+ sha256 = "0bjlljmbf8glnd9qjabx73w6pd7ibv43yiyngqvmvgxsabzr8399";
+ };
+
+ meta = with stdenv.lib; {
+ description = "Google's C++ test framework";
+ homepage = "https://github.com/google/googletest";
+ maintainers = [ maintainers.spacefrogg ];
+ platforms = platforms.all;
+ };
+}
diff --git a/resources/3rdparty/nix-scripts/l3pp/default.nix b/resources/3rdparty/nix-scripts/l3pp/default.nix
new file mode 100644
index 000000000..ac21c5f05
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/l3pp/default.nix
@@ -0,0 +1,26 @@
+{ stdenv, fetchFromGitHub }:
+stdenv.mkDerivation rec {
+ name = "l3pp-${version}";
+ version = "git";
+
+ src = fetchFromGitHub {
+ owner = "hbruintjes";
+ repo = "l3pp";
+ rev = "e4f8d7fe6c328849aff34d2dfd6fd592c14070d5";
+ sha256 = "0bd0m4hj7iy5y9546sr7d156hmq6q7d5jys495jd26ngvibkv9hp";
+ };
+ phases = "unpackPhase installPhase fixupPhase";
+
+ installPhase = ''
+ mkdir -p $out/include $out/share/doc/l3pp
+ cp LICENSE Readme.md $out/share/doc/l3pp
+ cp -r *.h impl $out/include
+ '';
+
+ meta = with stdenv.lib; {
+ description = "Lightweight Logging Library for C++";
+ homepage = https://github.com/hbruintjes/l3pp;
+ maintainers = [ maintainers.spacefrogg ];
+ platforms = platforms.all;
+ };
+}
diff --git a/resources/3rdparty/nix-scripts/mathsat/default.nix b/resources/3rdparty/nix-scripts/mathsat/default.nix
new file mode 100644
index 000000000..180e50a21
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/mathsat/default.nix
@@ -0,0 +1,46 @@
+{ stdenv, fetchurl, file
+, gmp
+, reentrantBuild ? true
+}:
+
+let
+ version = "5.5.1";
+ name = "mathsat-${version}";
+ genUrl = reentrant: "http://mathsat.fbk.eu/download.php?file=${name}-linux-x86_64${reentrant}.tar.gz";
+ srcAttrs = if reentrantBuild then {
+ url = genUrl "-reentrant";
+ sha256 = "10ng53nvxyyvml3gbzl87vj3c75fgb14zdlakwasz7zczn7hm978";
+ } else {
+ url = genUrl "";
+ sha256 = "0jnbiaq27hzdzavkr3sdh2ym0bc3ykamacj8k08pvyf7vil2hkdz";
+ };
+
+in stdenv.mkDerivation rec {
+ inherit name version;
+
+ src = fetchurl srcAttrs;
+
+ nativeBuildInputs = [ gmp ];
+
+ libPath = stdenv.lib.makeLibraryPath [ stdenv.cc.cc stdenv.cc.libc stdenv.glibc gmp ];
+ phases = "unpackPhase installPhase fixupPhase";
+
+ installPhase = ''
+ mkdir -p $out/{bin,lib,include}
+ patchelf --set-rpath "$libPath" lib/libmathsat.so
+ cp bin/* $out/bin
+ cp lib/* $out/lib
+ cp -r include/* $out/include
+ '';
+
+ meta = with stdenv.lib; {
+ description = "Satisfiability modulo theories (SMT) solver";
+ homepage = http://mathsat.fbk.eu;
+ license = {
+ fullName = "Unfree, redistributable for non-commercial applications";
+ free = false;
+ };
+ maintainer = [ maintainers.spacefrogg ];
+ platforms = platforms.linux;
+ };
+}
diff --git a/resources/3rdparty/nix-scripts/storm-checker/default.nix b/resources/3rdparty/nix-scripts/storm-checker/default.nix
new file mode 100644
index 000000000..6c322500b
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/storm-checker/default.nix
@@ -0,0 +1,52 @@
+{ stdenv, fetchFromGitHub, writeText, autoconf, automake, cmake
+, boost, carl, cln, doxygen, gmp, ginac, glpk, hwloc, l3pp, xercesc
+, ltoSupport ? true
+, mathsatSupport ? false, mathsat
+, tbbSupport ? false, tbb
+, z3Support ? true, z3
+}:
+
+let
+ l3ppCmakeSed = writeText "l3pp-sed" ''
+8,27d
+28i\
+set(l3pp_INCLUDE "${l3pp}/include/")
+30d
+ '';
+ inherit (stdenv.lib) optional singleton;
+ genCmakeOption = bool: name:
+ singleton "-D${name}=${if bool then "on" else "off"}";
+
+in stdenv.mkDerivation {
+ name = "storm-git";
+
+ src = fetchFromGitHub {
+ owner = "moves-rwth";
+ repo = "storm";
+ rev = "4378279c6419541e7100270937c849e5c5d53fea";
+ sha256 = "1yhz9642s09izy9qid0a03i4c29cdvrmrrx9wa35dw5vkv6gxp0f";
+ };
+
+ buildInputs = [ boost carl cln doxygen gmp ginac glpk hwloc l3pp xercesc ]
+ ++ optional tbbSupport tbb
+ ++ optional z3Support z3;
+
+ nativeBuildInputs = [ autoconf automake cmake ];
+
+ cmakeFlags = genCmakeOption tbbSupport "STORM_USE_INTELTBB"
+ ++ genCmakeOption ltoSupport "STORM_USE_LTO"
+ ++ optional mathsatSupport "-DMSAT_ROOT=${mathsat}" ;
+
+ postPatch = ''
+ sed -f ${l3ppCmakeSed} -i resources/3rdparty/CMakeLists.txt
+ substituteInPlace CMakeLists.txt --replace "include(export)" ""
+ '';
+
+ meta = with stdenv.lib; {
+ description = "Probabilistic Model Checker";
+ homepage = http://www.stormchecker.org;
+ license = licenses.gpl3;
+ maintainer = [ maintainers.spacefrogg ];
+ platforms = platforms.all;
+ };
+}
diff --git a/resources/3rdparty/nix-scripts/z3/default.nix b/resources/3rdparty/nix-scripts/z3/default.nix
new file mode 100644
index 000000000..3bb9d1aec
--- /dev/null
+++ b/resources/3rdparty/nix-scripts/z3/default.nix
@@ -0,0 +1,20 @@
+{ stdenv, fetchFromGitHub, python3 }:
+
+stdenv.mkDerivation rec {
+ name = "z3-${version}";
+ version = "4.6.0";
+
+ src = fetchFromGitHub {
+ owner = "Z3Prover";
+ repo = "z3";
+ rev = "z3-${version}";
+ sha256 = "1cgwlmjdbf4rsv2rriqi2sdpz9qxihxrcpm6a4s37ijy437xg78l";
+ };
+
+ buildInputs = [ python3 ];
+ phases = "unpackPhase buildPhase installPhase fixupPhase";
+ preBuild = ''
+ python3 scripts/mk_make.py --prefix=$out
+ cd build
+ '';
+}