diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index ddac9210..56a2fead 100644 --- a/src/solvers/CMakeLists.txt +++ b/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) diff --git a/src/solvers/solve.cpp b/src/solvers/solve.cpp index e3071875..2c420275 100644 --- a/src/solvers/solve.cpp +++ b/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; } diff --git a/src/solvers/z3-slhv/CMakeLists.txt b/src/solvers/z3-slhv/CMakeLists.txt new file mode 100644 index 00000000..abc3d755 --- /dev/null +++ b/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() diff --git a/src/solvers/z3-slhv/try_z3.c b/src/solvers/z3-slhv/try_z3.c new file mode 100644 index 00000000..70536c88 --- /dev/null +++ b/src/solvers/z3-slhv/try_z3.c @@ -0,0 +1,8 @@ +#include +#include + +int main() +{ + printf(Z3_FULL_VERSION); + return 0; +} \ No newline at end of file diff --git a/src/solvers/z3-slhv/z3_slhv_conv.cpp b/src/solvers/z3-slhv/z3_slhv_conv.cpp new file mode 100644 index 00000000..cac47ced --- /dev/null +++ b/src/solvers/z3-slhv/z3_slhv_conv.cpp @@ -0,0 +1,16 @@ +#include +#include +#include + + +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 +} \ No newline at end of file diff --git a/src/solvers/z3-slhv/z3_slhv_conv.h b/src/solvers/z3-slhv/z3_slhv_conv.h new file mode 100644 index 00000000..2e4b171a --- /dev/null +++ b/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 +#include + + +class z3_slhv_smt_ast : public solver_smt_ast +{ +public: + using solver_smt_ast::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 \ No newline at end of file