Enable support for Z3

CMakeLists.txt

@@ -40,6 +40,10 @@ if (WITH_YICES2)
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_YICES2")
 endif()
 
+if (WITH_Z3)
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_Z3")
+endif()
+
 if (WITH_PROFILING)
   find_library(GOOGLE_PERF profiler REQUIRED)
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_PROFILING")
@@ -114,6 +118,12 @@ if (WITH_YICES2)
   endif()
 endif()
 
+if (WITH_Z3)
+  if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-z3.a")
+    message(FATAL_ERROR "Missing smt-switch Z3 library -- try running ./contrib/setup-smt-switch.sh --with-z3")
+  endif()
+endif()
+
 if (WITH_MSAT_IC3IA)
   if (NOT EXISTS "${PROJECT_SOURCE_DIR}/deps/ic3ia/build/libic3ia.a")
     message(FATAL_ERROR "Missing ic3ia library -- try running ./contrib/setup-ic3ia.sh")
@@ -260,6 +270,10 @@ if (WITH_YICES2)
   target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-yices2.a")
 endif()
 
+if (WITH_Z3)
+  target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-z3.a")
+endif()
+
 if (WITH_MSAT_IC3IA)
   target_link_libraries(pono-lib PUBLIC "${PROJECT_SOURCE_DIR}/deps/ic3ia/build/libic3ia.a")
 endif()

configure.sh

@@ -17,6 +17,7 @@ Configures the CMAKE build environment.
 --with-msat             build with MathSAT which has a custom non-BSD compliant license.  (default : off)
                         Required for interpolant based model checking
 --with-yices2           build with Yices2 which has a custom non-BSD compliant license (default : off)
+--with-z3               build with Z3 (default: off)
 --with-msat-ic3ia       build with the open-source IC3IA implementation as a backend. (default: off)
 --with-coreir           build the CoreIR frontend (default: off)
 --with-coreir-extern    build the CoreIR frontend using an installation of coreir in /usr/local/lib (default: off)
@@ -41,6 +42,7 @@ build_type=default
 with_boolector=default
 with_msat=default
 with_yices2=default
+with_z3=default
 with_msat_ic3ia=default
 with_coreir=default
 with_coreir_extern=default
@@ -80,6 +82,7 @@ do
         --with-btor) with_boolector=ON;;
         --with-msat) with_msat=ON;;
         --with-yices2) with_yices2=ON;;
+        --with-z3) with_z3=ON;;
         --with-msat-ic3ia) with_msat_ic3ia=ON;;
         --with-coreir) with_coreir=ON;;
         --with-coreir-extern) with_coreir_extern=ON;;
@@ -121,6 +124,9 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$buildtype -DPONO_LIB_TYPE=${lib_type} -DPONO_STA
 [ $with_yices2 != default ] \
     && cmake_opts="$cmake_opts -DWITH_YICES2=$with_yices2"
 
+[ $with_z3 != default ] \
+    && cmake_opts="$cmake_opts -DWITH_Z3=$with_z3"
+
 [ $with_msat_ic3ia != default ] \
     && cmake_opts="$cmake_opts -DWITH_MSAT_IC3IA=$with_msat_ic3ia"
 

options/options.cpp

@@ -177,7 +177,7 @@ const option::Descriptor usage[] = {
     "",
     "smt-solver",
     Arg::NonEmpty,
-    "  --smt-solver \tSMT Solver to use: btor, bzla, msat, yices2, or cvc5." },
+    "  --smt-solver \tSMT Solver to use: btor, bzla, cvc5, msat, yices2, or z3." },
   { LOGGING_SMT_SOLVER,
     0,
     "",
@@ -689,6 +689,8 @@ ProverResult PonoOptions::parse_and_set_options(int argc,
             smt_solver_ = smt::MSAT;
           } else if (opt.arg == std::string("yices2")) {
             smt_solver_ = smt::YICES2;
+          } else if (opt.arg == std::string("z3")) {
+            smt_solver_ = smt::Z3;
           } else {
             throw PonoException("Unknown solver: " + std::string(opt.arg));
             break;

smt/available_solvers.cpp

@@ -45,6 +45,10 @@
 #include "smt-switch/yices2_factory.h"
 #endif
 
+#if WITH_Z3
+#include "smt-switch/z3_factory.h"
+#endif
+
 using namespace smt;
 using namespace std;
 
@@ -65,6 +69,10 @@ const std::vector<SolverEnum> solver_enums({
 #if WITH_YICES2
       YICES2,
 #endif
+
+#if WITH_Z3
+      Z3,
+#endif
 });
 
 // internal method for creating a particular solver
@@ -101,6 +109,12 @@ SmtSolver create_solver_base(SolverEnum se, bool logging, bool printing = false)
       s = Yices2SolverFactory::create(logging);
       break;
     }
+#endif
+#if WITH_Z3
+    case Z3: {
+      s = Z3SolverFactory::create(logging);
+      break;
+    }
 #endif
     default: {
       throw SmtException("Unhandled solver enum");