Enable Yices2 backend (#350)

CMakeLists.txt

@@ -36,6 +36,10 @@ if (WITH_MSAT)
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_MSAT")
 endif()
 
+if (WITH_YICES2)
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_YICES2")
+endif()
+
 if (WITH_PROFILING)
   find_library(GOOGLE_PERF profiler REQUIRED)
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_PROFILING")
@@ -104,6 +108,12 @@ if (WITH_MSAT)
   endif()
 endif()
 
+if (WITH_YICES2)
+  if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-yices2.a")
+    message(FATAL_ERROR "Missing smt-switch Yices2 library -- try running ./contrib/setup-smt-switch.sh --with-yices2")
+  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")
@@ -246,6 +256,10 @@ if (WITH_MSAT)
   target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-msat.a")
 endif()
 
+if (WITH_YICES2)
+  target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-yices2.a")
+endif()
+
 if (WITH_MSAT_IC3IA)
   target_link_libraries(pono-lib PUBLIC "${PROJECT_SOURCE_DIR}/deps/ic3ia/build/libic3ia.a")
 endif()

configure.sh

@@ -16,6 +16,7 @@ Configures the CMAKE build environment.
 --with-btor             build with Boolector  (default: off)
 --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-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)
@@ -39,6 +40,7 @@ install_prefix=default
 build_type=default
 with_boolector=default
 with_msat=default
+with_yices2=default
 with_msat_ic3ia=default
 with_coreir=default
 with_coreir_extern=default
@@ -77,6 +79,7 @@ do
             ;;
         --with-btor) with_boolector=ON;;
         --with-msat) with_msat=ON;;
+        --with-yices2) with_yices2=ON;;
         --with-msat-ic3ia) with_msat_ic3ia=ON;;
         --with-coreir) with_coreir=ON;;
         --with-coreir-extern) with_coreir_extern=ON;;
@@ -115,6 +118,9 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$buildtype -DPONO_LIB_TYPE=${lib_type} -DPONO_STA
 [ $with_msat != default ] \
     && cmake_opts="$cmake_opts -DWITH_MSAT=$with_msat"
 
+[ $with_yices2 != default ] \
+    && cmake_opts="$cmake_opts -DWITH_YICES2=$with_yices2"
+
 [ $with_msat_ic3ia != default ] \
     && cmake_opts="$cmake_opts -DWITH_MSAT_IC3IA=$with_msat_ic3ia"
 

contrib/setup-smt-switch.sh

@@ -15,6 +15,7 @@ Sets up the smt-switch API for interfacing with SMT solvers through a C++ API.
 -h, --help              display this message and exit
 --with-btor             include Boolector (default: off)
 --with-msat             include MathSAT which is under a custom non-BSD compliant license (default: off)
+--with-yices2           include Yices2 which is under a custom non-BSD compliant license (default: off)
 --cvc5-home             use an already downloaded version of cvc5
 --python                build python bindings (default: off)
 EOF
@@ -28,6 +29,7 @@ die () {
 
 WITH_BOOLECOR=default
 WITH_MSAT=default
+WITH_YICES2=default
 CONF_OPTS=""
 WITH_PYTHON=default
 cvc5_home=default
@@ -42,6 +44,9 @@ do
         --with-btor)
             WITH_BOOLECTOR=ON
             CONF_OPTS="$CONF_OPTS --btor";;
+        --with-yices2)
+            WITH_YICES2=ON
+            CONF_OPTS="$CONF_OPTS --yices2";;
         --python)
             WITH_PYTHON=YES
             CONF_OPTS="$CONF_OPTS --python";;

options/options.cpp

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