tjh.dev
1{
2 stdenv,
3 lib,
4 fetchFromGitHub,
5 cmake,
6 libedit,
7 gmpxx,
8 bison,
9 flex,
10 enableReadline ? false,
11 readline,
12 gtest,
13}:
14
15stdenv.mkDerivation rec {
16 pname = "opensmt";
17 version = "2.7.0";
18
19 src = fetchFromGitHub {
20 owner = "usi-verification-and-security";
21 repo = "opensmt";
22 rev = "v${version}";
23 sha256 = "sha256-zhNNnwc41B4sNq50kPub29EYhqV+FoDKRD/CLHnVyZw=";
24 };
25
26 nativeBuildInputs = [
27 cmake
28 bison
29 flex
30 ];
31 buildInputs = [
32 libedit
33 gmpxx
34 ]
35 ++ lib.optional enableReadline readline;
36
37 preConfigure = ''
38 substituteInPlace test/CMakeLists.txt \
39 --replace 'FetchContent_Populate' '#FetchContent_Populate'
40 '';
41 cmakeFlags = [
42 "-Dgoogletest_SOURCE_DIR=${gtest.src}"
43 "-Dgoogletest_BINARY_DIR=./gtest-build"
44 ];
45
46 meta = with lib; {
47 broken = (stdenv.hostPlatform.isLinux && stdenv.hostPlatform.isAarch64);
48 description = "Satisfiability modulo theory (SMT) solver";
49 mainProgram = "opensmt";
50 maintainers = [ maintainers.raskin ];
51 platforms = platforms.linux;
52 license = if enableReadline then licenses.gpl2Plus else licenses.mit;
53 homepage = "https://github.com/usi-verification-and-security/opensmt";
54 };
55}