Merge pull request #1451 from madebr/z3

z3: add z3/4.8.7 recipe

recipes/z3/all/CMakeLists.txt

@@ -0,0 +1,7 @@
+cmake_minimum_required(VERSION 3.1)
+project(cmake_wrapper)
+
+include(conanbuildinfo.cmake)
+conan_basic_setup(TARGETS)
+
+add_subdirectory(source_subfolder)

recipes/z3/all/conandata.yml

@@ -0,0 +1,8 @@
+sources:
+  "4.8.8":
+    url: "https://github.com/Z3Prover/z3/archive/z3-4.8.8.tar.gz"
+    sha256: "6962facdcdea287c5eeb1583debe33ee23043144d0e5308344e6a8ee4503bcff"
+patches:
+  "4.8.8":
+    - patch_file: "patches/0001-cmake-use-conan-mpir.patch"
+      base_path: "source_subfolder"

recipes/z3/all/conanfile.py

@@ -0,0 +1,98 @@
+from conans import CMake, ConanFile, tools
+import os
+import textwrap
+
+
+class Z3Conan(ConanFile):
+    name = "z3"
+    description = "The Z3 Theorem Prover"
+    topics = ("conan", "z3", "theorem", "SMT", "satisfiability", "prover", "solver")
+    url = "https://github.com/conan-io/conan-center-index"
+    homepage = "https://github.com/Z3Prover/z3"
+    exports_sources = "CMakeLists.txt", "patches/**"
+    generators = "cmake"
+    license = "MIT"
+    settings = "os", "arch", "compiler", "build_type"
+    options = {
+        "shared": [True, False],
+        "fPIC": [True, False],
+        "multithreaded": [True, False],
+    }
+    default_options = {
+        "shared": False,
+        "fPIC": True,
+        "multithreaded": True,
+    }
+
+    _cmake = None
+
+    @property
+    def _source_subfolder(self):
+        return "source_subfolder"
+
+    @property
+    def _build_subfolder(self):
+        return "build_subfolder"
+
+    def config_options(self):
+        if self.settings.os == "Windows":
+            del self.options.fPIC
+
+    def configure(self):
+        if self.options.shared:
+            del self.options.fPIC
+
+    def requirements(self):
+        self.requires("mpir/3.0.0")
+
+    def source(self):
+        tools.get(**self.conan_data["sources"][self.version])
+        os.rename("{0}-{0}-{1}".format(self.name, self.version), self._source_subfolder)
+
+    def _configure_cmake(self):
+        if self._cmake:
+            return self._cmake
+        self._cmake = CMake(self)
+        self._cmake.definitions["Z3_USE_LIB_GMP"] = True
+        self._cmake.definitions["SINGLE_THREADED"] = not self.options.multithreaded
+        self._cmake.definitions["Z3_BUILD_LIBZ3_SHARED"] = self.options.shared
+        self._cmake.definitions["Z3_INCLUDE_GIT_HASH"] = False
+        self._cmake.definitions["Z3_INCLUDE_GIT_DESCRIBE"] = False
+        self._cmake.definitions["Z3_ENABLE_EXAMPLE_TARGETS"] = False
+        self._cmake.definitions["Z3_BUILD_DOCUMENTATION"] = False
+        self._cmake.configure(build_folder=self._build_subfolder)
+        return self._cmake
+
+    def build(self):
+        for patch in self.conan_data.get("patches", {}).get(self.version, []):
+            tools.patch(**patch)
+        tools.save(os.path.join(self._build_subfolder, "gmp.h"), textwrap.dedent("""\
+            #pragma once
+            #include <mpir.h>
+            """))
+        cmake = self._configure_cmake()
+        cmake.build()
+
+    def package(self):
+        self.copy("LICENSE.txt", src=self._source_subfolder, dst="licenses")
+        cmake = self._configure_cmake()
+        cmake.install()
+
+        tools.rmdir(os.path.join(self.package_folder, "lib", "cmake"))
+
+    def package_info(self):
+        # z3 generates a Z3Config.cmake file
+        self.cpp_info.names["cmake_find_package"] = "z3"
+        self.cpp_info.names["cmake_find_package_multi"] = "z3"
+        self.cpp_info.filenames["cmake_find_package"] = "Z3"
+        self.cpp_info.filenames["cmake_find_package_multi"] = "Z3"
+
+        self.cpp_info.components["libz3"].libs = ["libz3" if self.settings.os == "Windows" else "z3"]
+        self.cpp_info.components["libz3"].requires = ["mpir::mpir"]
+        # Z3COnfig.cmake generates a z3::libz3 target
+        self.cpp_info.components["libz3"].names["cmake_find_package"] = "libz3"
+        self.cpp_info.components["libz3"].names["cmake_find_package_multi"] = "libz3"
+        if not self.options.shared:
+            if self.settings.os  =="Linux":
+                self.cpp_info.components["libz3"].system_libs.append("pthread")
+        # FIXME: this generates a Z3::libz3 target instead of z3::libz3.

recipes/z3/all/patches/0001-cmake-use-conan-mpir.patch

@@ -0,0 +1,16 @@
+--- CMakeLists.txt
++++ CMakeLists.txt
+@@ -246,10 +246,10 @@
+ if (Z3_USE_LIB_GMP)
+   # Because this is off by default we will make the configure fail if libgmp
+   # can't be found
+-  find_package(GMP REQUIRED)
++  #find_package(GMP REQUIRED)
+   message(STATUS "Using libgmp")
+-  list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES})
+-  list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS})
++  list(APPEND Z3_DEPENDENT_LIBS CONAN_PKG::mpir)
++  list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS "${CMAKE_BINARY_DIR}" ${CONAN_INCLUDE_DIRS})
+   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP")
+ else()
+   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL")

recipes/z3/all/test_package/CMakeLists.txt

@@ -0,0 +1,10 @@
+cmake_minimum_required(VERSION 3.1)
+project(test_package)
+
+include(${CMAKE_BINARY_DIR}/conanbuildinfo.cmake)
+conan_basic_setup(TARGETS)
+
+find_package(Z3 REQUIRED)
+
+add_executable(${PROJECT_NAME} test_package.cpp)
+target_link_libraries(${PROJECT_NAME} PRIVATE z3::libz3)

recipes/z3/all/test_package/conanfile.py

@@ -0,0 +1,17 @@
+from conans import ConanFile, CMake, tools
+import os
+
+
+class TestPackageConan(ConanFile):
+    settings = "os", "compiler", "build_type", "arch"
+    generators = "cmake", "cmake_find_package"
+
+    def build(self):
+        cmake = CMake(self)
+        cmake.configure()
+        cmake.build()
+
+    def test(self):
+        if not tools.cross_building(self.settings):
+            bin_path = os.path.join("bin", "test_package")
+            self.run(bin_path, run_environment=True)

recipes/z3/all/test_package/test_package.cpp

@@ -0,0 +1,145 @@
+#include "z3.h"
+
+#include <cstdio>
+#include <cstdlib>
+
+/* Adapted from z3/examples/c/test_capi.c */
+
+/**
+   \brief Simpler error handler.
+ */
+static void error_handler(Z3_context c, Z3_error_code e)
+{
+    fprintf(stderr, "Error code: %d\n", e);
+    fprintf(stderr, "incorrect use of Z3\n");
+    exit(1);
+}
+
+/**
+   \brief Create a logical context.
+
+   Enable model construction. Other configuration parameters can be passed in the cfg variable.
+
+   Also enable tracing to stderr and register custom error handler.
+*/
+static Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
+{
+    Z3_context ctx;
+
+    Z3_set_param_value(cfg, "model", "true");
+    ctx = Z3_mk_context(cfg);
+    Z3_set_error_handler(ctx, err);
+
+    return ctx;
+}
+
+/**
+   \brief Create a logical context.
+
+   Enable model construction only.
+
+   Also enable tracing to stderr and register standard error handler.
+*/
+static Z3_context mk_context()
+{
+    Z3_config  cfg;
+    Z3_context ctx;
+    cfg = Z3_mk_config();
+    ctx = mk_context_custom(cfg, error_handler);
+    Z3_del_config(cfg);
+    return ctx;
+}
+
+Z3_solver mk_solver(Z3_context ctx)
+{
+  Z3_solver s = Z3_mk_solver(ctx);
+  Z3_solver_inc_ref(ctx, s);
+  return s;
+}
+
+static void del_solver(Z3_context ctx, Z3_solver s)
+{
+  Z3_solver_dec_ref(ctx, s);
+}
+
+/**
+   @name Examples
+*/
+/*@{*/
+/**
+   \brief "Hello world" example: create a Z3 logical context, and delete it.
+*/
+void simple_example()
+{
+    Z3_context ctx;
+    printf("\nsimple_example\n");
+
+    ctx = mk_context();
+
+    /* delete logical context */
+    Z3_del_context(ctx);
+}
+
+/**
+  Demonstration of how Z3 can be used to prove validity of
+  De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
+*/
+void demorgan()
+{
+    Z3_config cfg;
+    Z3_context ctx;
+    Z3_solver s;
+    Z3_sort bool_sort;
+    Z3_symbol symbol_x, symbol_y;
+    Z3_ast x, y, not_x, not_y, x_and_y, ls, rs, conjecture, negated_conjecture;
+    Z3_ast args[2];
+
+    printf("\nDeMorgan\n");
+
+    cfg                = Z3_mk_config();
+    ctx                = Z3_mk_context(cfg);
+    Z3_del_config(cfg);
+    bool_sort          = Z3_mk_bool_sort(ctx);
+    symbol_x           = Z3_mk_int_symbol(ctx, 0);
+    symbol_y           = Z3_mk_int_symbol(ctx, 1);
+    x                  = Z3_mk_const(ctx, symbol_x, bool_sort);
+    y                  = Z3_mk_const(ctx, symbol_y, bool_sort);
+
+    /* De Morgan - with a negation around */
+    /* !(!(x && y) <-> (!x || !y)) */
+    not_x              = Z3_mk_not(ctx, x);
+    not_y              = Z3_mk_not(ctx, y);
+    args[0]            = x;
+    args[1]            = y;
+    x_and_y            = Z3_mk_and(ctx, 2, args);
+    ls                 = Z3_mk_not(ctx, x_and_y);
+    args[0]            = not_x;
+    args[1]            = not_y;
+    rs                 = Z3_mk_or(ctx, 2, args);
+    conjecture         = Z3_mk_iff(ctx, ls, rs);
+    negated_conjecture = Z3_mk_not(ctx, conjecture);
+
+    s = mk_solver(ctx);
+    Z3_solver_assert(ctx, s, negated_conjecture);
+    switch (Z3_solver_check(ctx, s)) {
+    case Z3_L_FALSE:
+        /* The negated conjecture was unsatisfiable, hence the conjecture is valid */
+        printf("DeMorgan is valid\n");
+        break;
+    case Z3_L_UNDEF:
+        /* Check returned undef */
+        printf("Undef\n");
+        break;
+    case Z3_L_TRUE:
+        /* The negated conjecture was satisfiable, hence the conjecture is not valid */
+        printf("DeMorgan is not valid\n");
+        break;
+    }
+    del_solver(ctx, s);
+    Z3_del_context(ctx);
+}
+
+int main() {
+    simple_example();
+    demorgan();
+}

recipes/z3/config.yml

@@ -0,0 +1,3 @@
+versions:
+  "4.8.8":
+    folder: "all"