add compile

src/solvers/CMakeLists.txt

@@ -23,6 +23,7 @@ target_link_libraries(solvers INTERFACE solve smttuple smtfp smt prop)
 
 # Logic for each of these are duplicated -- cmake doesn't have indirect function
 # calling, so it's hard to structure it how I want
+add_subdirectory(z3-slhv)
 add_subdirectory(z3)
 add_subdirectory(boolector)
 add_subdirectory(cvc4)

src/solvers/solve.cpp

@@ -161,6 +161,7 @@ smt_convt *create_solver(
   else
     ctx->set_fp_conv(fp_api);
 
+  // TODO: SLHV
   ctx->smt_post_init();
   return ctx;
 }

src/solvers/z3-slhv/CMakeLists.txt

@@ -0,0 +1,60 @@
+set(Z3_MIN_VERSION "4.8.9")
+
+if(DEFINED Z3_DIR)
+    set(ENABLE_Z3 ON)
+elseif(EXISTS $ENV{HOME}/z3)
+    set(ENABLE_Z3 ON)
+else()
+    if(ENABLE_Z3 AND DOWNLOAD_DEPENDENCIES)
+        message("Downloading Z3")
+        download_zip_and_extract(Z3 ${ESBMC_Z3_URL})
+        set(Z3_DIR ${CMAKE_BINARY_DIR}/Z3/${ESBMC_Z3_NAME})
+    endif()
+endif()
+
+if(ENABLE_Z3)
+    find_library(Z3_LIB z3 libz3 HINTS ${Z3_DIR} $ENV{HOME}/z3 PATH_SUFFIXES lib bin)
+    find_path(Z3_INCLUDE_DIRS z3.h HINTS ${Z3_DIR} $ENV{HOME}/z3 PATH_SUFFIXES include)
+
+    if(Z3_INCLUDE_DIRS STREQUAL "Z3_INCLUDE_DIRS-NOTFOUND")
+        message(FATAL_ERROR "Could not find z3 include headers, please check Z3_DIR")
+    endif()
+
+    if(Z3_LIB STREQUAL "Z3_LIB-NOTFOUND")
+        message(FATAL_ERROR "Could not find libz3, please check Z3_DIR")
+    endif()
+
+    try_run(Z3_RUNS Z3_COMPILES ${CMAKE_CURRENT_BINARY_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/try_z3.c
+            CMAKE_FLAGS -DINCLUDE_DIRECTORIES=${Z3_INCLUDE_DIRS}
+            LINK_LIBRARIES ${Z3_LIB} ${OS_Z3_LIBS}
+            COMPILE_OUTPUT_VARIABLE Z3COMPILESTR
+            RUN_OUTPUT_VARIABLE Z3_VERSION)
+
+    if(NOT Z3_COMPILES)
+        message(FATAL_ERROR "Could not use Z3: \n${Z3COMPILESTR}")
+    endif()
+
+    message(STATUS "Using Z3 at: ${Z3_LIB}")
+    string(REGEX MATCH "(Z3 )?([0-9]+.[0-9]+.[0-9]+.[0-9]+)"  REGEX_OUTPUT ${Z3_VERSION})
+    set(Z3_VERSION "${CMAKE_MATCH_2}")
+    message(STATUS "Z3 version: ${Z3_VERSION}")
+    if(Z3_VERSION VERSION_LESS Z3_MIN_VERSION)
+        message(FATAL_ERROR "Expected version ${Z3_MIN_VERSION} or greater")
+    endif()
+
+
+    add_library(solverz3slhv z3_slhv_conv.cpp)
+    target_include_directories(solverz3slhv
+            PRIVATE ${Z3_INCLUDE_DIRS}
+            PRIVATE ${Boost_INCLUDE_DIRS}
+            PRIVATE ${CMAKE_CURRENT_SOURCE_DIR})
+
+    if (BUILD_STATIC)
+        target_link_libraries(solverz3slhv fmt::fmt "${Z3_LIB}" -pthread "${LIBGOMP_LIB}" -ldl)
+    else ()
+        target_link_libraries(solverz3slhv fmt::fmt "${Z3_LIB}")
+    endif ()
+    # Add to solver link
+    target_link_libraries(solvers INTERFACE solverz3slhv)
+
+endif()

src/solvers/z3-slhv/try_z3.c

@@ -0,0 +1,8 @@
+#include <z3_version.h>
+#include <stdio.h>
+
+int main()
+{
+  printf(Z3_FULL_VERSION);
+  return 0;
+}

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -0,0 +1,16 @@
+#include <cassert>
+#include <iostream>
+#include <z3_slhv_conv.h>
+
+
+smt_convt *create_new_z3_slhv_solver(
+    const optionst &options,
+    const namespacet &ns
+) {
+    z3_slhv_convt* conv = new z3_slhv_convt(ns, options);
+    return conv;
+}
+
+z3_slhv_convt::z3_slhv_convt(const namespacet &_ns, const optionst& _options) : smt_convt(_ns, _options) {
+    // initialize the z3 based slhv converter here
+}

src/solvers/z3-slhv/z3_slhv_conv.h

@@ -0,0 +1,58 @@
+#ifndef _ESBMC_SOLVERS_Z3_SLHV_CONV_H
+#define _ESBMC_SOLVERS_Z3_SLHV_CONV_H
+
+// this file does not follow the translation procedure in the 
+
+#include <solvers/smt/smt_conv.h>
+#include <z3++.h>
+
+
+class z3_slhv_smt_ast : public solver_smt_ast<z3::expr>
+{
+public:
+  using solver_smt_ast<z3::expr>::solver_smt_ast;
+  ~z3_smt_ast() override = default;
+
+  smt_astt
+  update(smt_convt *ctx, smt_astt value, unsigned int idx, expr2tc idx_expr)
+    const override;
+
+  smt_astt project(smt_convt *ctx, unsigned int elem) const override;
+
+  void dump() const override;
+};
+
+/* Be sure to not make smt_convt a *virtual* base class: our dtor ~z3_convt()
+ * erases all smt_asts early. */
+
+class z3_slhv_convt : public smt_convt {
+public:
+    z3_slhv_convt(const namespacet &ns, const optionst &options);
+    ~z3_slhv_convt() override;
+public:
+    void push_ctx() override;
+    void pop_ctx() override;
+
+    void assert_ast(smt_astt a) override;
+    resultt dec_solver() override;
+    std::string solver_text() override;
+
+    smt_astt mk_smt_int(const BigInt &theint) override;
+    smt_astt mk_smt_real(const std::string &str) override;
+    smt_astt mk_smt_bv(const BigInt &theint, smt_sortt s) override;
+    smt_astt mk_smt_bool(bool val) override;
+    smt_astt mk_smt_symbol(const std::string &name, smt_sortt s) override;
+    smt_astt mk_extract(smt_astt a, unsigned int high, unsigned int low) override;
+    smt_astt mk_sign_ext(smt_astt a, unsigned int topwidth) override;
+    smt_astt mk_zero_ext(smt_astt a, unsigned int topwidth) override;
+    smt_astt mk_concat(smt_astt a, smt_astt b) override;
+    smt_astt mk_ite(smt_astt cond, smt_astt t, smt_astt f) override;
+    bool get_bool(smt_astt a) override;
+    BigInt get_bv(smt_astt a, bool is_signed) override;
+    smt_astt overflow_arith(const expr2tc *&expr) override;
+
+    void dump_smt() override;
+
+}
+
+#endif