BUILD.bazel

load("@rules_pkg//:pkg.bzl", "pkg_deb", "pkg_tar")
load("@bazel_skylib//rules:common_settings.bzl", "bool_flag")
load("//tools:dreal.bzl", "DREAL_PREFIX", "DREAL_VERSION", "dreal_cc_library")
load("//tools:make-variables.bzl", "var_providing_rule")
load("//third_party/com_github_grailbio_bazel-compilation-database:aspects.bzl", "compilation_database")

package(
    default_visibility = ["//visibility:private"],
)

exports_files([
    "CPPLINT.cfg",
    ".clang-format",
])

compilation_database(
    name = "compdb",
    exec_root = "bazel-dreal4",
    targets = [
        ":dreal",
        ":dreal_shared_library",
    ],
)

bool_flag(
    name = "enable-soplex",
    build_setting_default = False,
)

config_setting(
    name = "soplex-enabled",
    flag_values = {":enable-soplex": "True"}
)

var_providing_rule(
    name = "soplex-enabled-var",
    var_name = "SOPLEX_ENABLED",
    var_value = select({
        "//:soplex-enabled": "True",
        "//conditions:default": "False",
    }),
    visibility = [
        "//dreal:__subpackages__",
    ],
)

cc_library(
    name = "qsopt-ex",
    srcs = ["install/qsopt-ex/lib/libqsopt_ex.so"],
    hdrs = glob(["install/qsopt-ex/include/qsopt_ex/*.h"]),
    includes = ["install/qsopt-ex/include"],
    copts = ["-Iinstall/qsopt-ex/include"],
    visibility = [
        "//dreal:__subpackages__",
    ],
    deps = [
        "@linux_libs//:gmpxx",
    ],
)

cc_library(
    name = "soplex",
    srcs = ["soplex/lib/libsoplex-pic.a"],
    hdrs = glob(["soplex/include/**/*.h*"]),
    includes = ["soplex/include"],
    copts = ["-Isoplex/include"],
    visibility = [
        "//dreal:__subpackages__",
    ],
    deps = [
        "@linux_libs//:gmp",
        "@linux_libs//:z",
    ],
)

filegroup(
    name = "qsopt-ex-lib",
    srcs = ["install/qsopt-ex/lib"],
    visibility = ["//visibility:public"],
)

cc_binary(
    name = "libdreal.so",
    linkshared = 1,
    visibility = [
        "//dreal:__subpackages__",
    ],
    deps = [
        "//dreal/api",
        "//dreal/solver",
        "//dreal/symbolic",
        "//dreal/symbolic:prefix_printer",
        "//dreal/util:box",
        "//dreal/util:interrupt",
        "//dreal/util:logging",
    ],
)

cc_library(
    name = "dreal_shared_library",
    srcs = [":libdreal.so"],
    hdrs = [
        "//dreal:headers",
        "//dreal/api:headers",
        "//dreal/smt2:headers",
        "//dreal/solver:headers",
        "//dreal/symbolic:headers",
        "//dreal/util:headers",
        "//dreal/util:private_headers",
    ],
    includes = [
        "third_party/com_github_pinam45_dynamic_bitset",
        "third_party/com_github_robotlocomotion_drake",
        "third_party/com_github_tartanllama_optional",
    ],
    visibility = [
        "//dreal:__subpackages__",
    ],
    deps = [
        "//dreal/util:signal_handler_guard",
        "@fmt",
        #"@ibex",
        "@spdlog",
    ],
)

genrule(
    name = "generate_pkg_file",
    outs = [
        "dreal.pc",
    ],
    cmd =
        select({
            "@//tools:linux": "$(location //tools:generate_pkg_file_ubuntu) %s %s> $@" % (DREAL_VERSION, DREAL_PREFIX),
            "@//conditions:default": "$(location //tools:generate_pkg_file_osx) %s > $@" % DREAL_VERSION,
        }),
    tools = [
        "//tools:generate_pkg_file_osx",
        "//tools:generate_pkg_file_ubuntu",
    ],
)

pkg_tar(
    name = "package_pkg_file",
    srcs = ["dreal.pc"],
    extension = "tar.gz",
    package_dir = "lib/pkgconfig",
    tags = ["manual"],
)

pkg_tar(
    name = "package_license_file",
    srcs = ["LICENSE"],
    extension = "tar.gz",
    package_dir = "share/doc/dreal",
    tags = ["manual"],
)

pkg_tar(
    name = "package_qsoptex_sharedlib",
    srcs = ["install/qsopt-ex/lib/libqsopt_ex.so",
            "install/qsopt-ex/lib/libqsopt_ex.so.2",
            "install/qsopt-ex/lib/libqsopt_ex.so.2.1.0"],
    extension = "tar.gz",
    package_dir = "lib",
    tags = ["manual"],
)

pkg_tar(
    name = "archive",
    extension = "tar.gz",
    package_dir = DREAL_PREFIX,
    tags = ["manual"],
    deps = [
        ":package_license_file",
        ":package_pkg_file",
        ":package_qsoptex_sharedlib",
        "//dreal:package_bin",
        "//dreal:package_headers",
        "//dreal:package_sharedlib",
        "//dreal/api:package_headers",
        "//dreal/smt2:package_headers",
        "//dreal/solver:package_headers",
        "//dreal/symbolic:package_headers",
        "//dreal/util:package_headers",
    ],
)

pkg_deb(
    name = "package_debian",
    architecture = "amd64",
    built_using = "bazel (1.0.0)",
    data = ":archive",
    depends = [
        "coinor-libclp-dev",
        "libbz2-dev",
        "libibex-dev",
        #"libnlopt-dev",
        # The followings are Build-Depends:
        # "bison",
        # "flex",
        # "pkg-config",
    ],
    description = "SMT solver for nonlinear theories",
    homepage = "http://dreal.github.io",
    maintainer = "",
    package = "dreal",
    tags = ["manual"],
    version = DREAL_VERSION,
)

# External users need to include only this target and `dreal/dreal.h` header.
dreal_cc_library(
    name = "dreal",
    srcs = [],
    hdrs = [
        "//dreal:headers",
    ],
    visibility = [
        "//visibility:public",
    ],
    deps = [
        "//dreal/api",
        "//dreal/solver",
        "//dreal/util:box",
    ],
)

licenses(["notice"])  # Apache 2.0

exports_files(["LICENSE"])