Remove cvc5

CMakeLists.txt

@@ -92,10 +92,6 @@ if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a")
   message(FATAL_ERROR "Missing smt-switch Bitwuzla library -- try running ./contrib/setup-smt-switch.sh")
 endif()
 
-if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-cvc5.a")
-  message(FATAL_ERROR "Missing smt-switch cvc5 library -- try running ./contrib/setup-smt-switch.sh")
-endif()
-
 if (WITH_BOOLECTOR)
   if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a")
     message(FATAL_ERROR "Missing smt-switch Boolector library -- try running ./contrib/setup-smt-switch.sh --with-btor")
@@ -246,7 +242,6 @@ if (BUILD_PYTHON_BINDINGS)
 endif()
 
 target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a")
-target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-cvc5.a")
 
 if (WITH_BOOLECTOR)
   target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a")

contrib/setup-smt-switch.sh

@@ -16,7 +16,6 @@ Sets up the smt-switch API for interfacing with SMT solvers through a C++ API.
 --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
     exit 0
@@ -32,7 +31,6 @@ WITH_MSAT=default
 WITH_YICES2=default
 CONF_OPTS=""
 WITH_PYTHON=default
-cvc5_home=default
 
 while [ $# -gt 0 ]
 do
@@ -50,17 +48,6 @@ do
         --python)
             WITH_PYTHON=YES
             CONF_OPTS="$CONF_OPTS --python";;
-        --cvc5-home) die "missing argument to $1 (see -h)" ;;
-        --cvc5-home=*)
-            cvc5_home=${1##*=}
-            # Check if cvc5_home is an absolute path and if not, make it
-            # absolute.
-            case $cvc5_home in
-                /*) ;;                            # absolute path
-                *) cvc5_home=$(pwd)/$cvc5_home ;; # make absolute path
-            esac
-            CONF_OPTS="$CONF_OPTS --cvc5-home=$cvc5_home"
-            ;;
         *) die "unexpected argument: $1";;
     esac
     shift
@@ -74,14 +61,11 @@ if [ ! -d "$DEPS/smt-switch" ]; then
     cd smt-switch
     git checkout -f $SMT_SWITCH_VERSION
     ./contrib/setup-bitwuzla.sh
-    if [ $cvc5_home = default ]; then
-        ./contrib/setup-cvc5.sh
-    fi
     if [ $WITH_BOOLECTOR = ON ]; then
         ./contrib/setup-btor.sh
     fi
     # pass bison/flex directories from smt-switch perspective
-    ./configure.sh --bitwuzla --cvc5 $CONF_OPTS --prefix=local --static --smtlib-reader --bison-dir=../bison/bison-install --flex-dir=../flex/flex-install
+    ./configure.sh --bitwuzla $CONF_OPTS --prefix=local --static --smtlib-reader --bison-dir=../bison/bison-install --flex-dir=../flex/flex-install
     cd build
     make -j$(nproc)
     make test
@@ -92,7 +76,7 @@ else
 fi
 
 if [ 0 -lt $(ls $DEPS/smt-switch/local/lib/libsmt-switch* 2>/dev/null | wc -w) ]; then
-    echo "It appears smt-switch with boolector and cvc5 was successfully installed to $DEPS/smt-switch/local."
+    echo "It appears smt-switch with bitwuzla was successfully installed to $DEPS/smt-switch/local."
     echo "You may now build pono with: ./configure.sh && cd build && make"
 else
     echo "Building smt-switch failed."

core/ts.h

@@ -19,7 +19,7 @@
 #include <string>
 #include <unordered_map>
 
-#include "smt-switch/cvc5_factory.h"
+#include "smt-switch/bitwuzla_factory.h"
 #include "smt-switch/smt.h"
 #include "utils/exceptions.h"
 
@@ -28,11 +28,8 @@ namespace pono {
 class TransitionSystem
 {
  public:
-  /** use cvc5 by default (doesn't require logging so pass false)
-   *  it supports the most theories and doesn't rewrite-on-the-fly or alias
-   * sorts
-   *  this makes it a great candidate for representing the TransitionSystem */
-  TransitionSystem() : TransitionSystem(smt::Cvc5SolverFactory::create(false))
+  /** use bitwuzla by default */
+  TransitionSystem() : TransitionSystem(smt::BitwuzlaSolverFactory::create(false))
   {
   }
 

options/options.cpp

@@ -180,7 +180,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, msat, or yices2." },
   { LOGGING_SMT_SOLVER,
     0,
     "",
@@ -693,8 +693,6 @@ ProverResult PonoOptions::parse_and_set_options(int argc,
             smt_solver_ = smt::BTOR;
           } else if (opt.arg == std::string("bzla")) {
             smt_solver_ = smt::BZLA;
-          } else if (opt.arg == std::string("cvc5")) {
-            smt_solver_ = smt::CVC5;
           } else if (opt.arg == std::string("msat")) {
             smt_solver_ = smt::MSAT;
           } else if (opt.arg == std::string("yices2")) {

smt/available_solvers.cpp

@@ -25,9 +25,7 @@
 #include "smt-switch/logging_solver.h"
 #include "smt-switch/printing_solver.h"
 
-// these two always included
 #include "smt-switch/bitwuzla_factory.h"
-#include "smt-switch/cvc5_factory.h"
 
 #if WITH_BOOLECTOR
 #include "smt-switch/boolector_factory.h"
@@ -52,7 +50,7 @@ namespace pono {
 
 // list of regular (non-interpolator) solver enums
 const std::vector<SolverEnum> solver_enums({
-  BZLA, CVC5,
+  BZLA,
 
 #if WITH_BOOLECTOR
       BTOR,
@@ -78,11 +76,6 @@ SmtSolver create_solver_base(SolverEnum se, bool logging, bool printing = false)
       s = BitwuzlaSolverFactory::create(logging);
       break;
     }
-    case CVC5: {
-      s = Cvc5SolverFactory::create(logging);
-      printing_style = smt::PrintingStyleEnum::CVC5_STYLE;
-      break;
-    }
 #if WITH_BOOLECTOR
     case BTOR: {
       s = BoolectorSolverFactory::create(logging);