Solver Wrapper Implementation for Solver

Solver wrappers derive a solver class from murxla::Solver, which manages construction and destruction of an instance of the solver under test. It further implements required and optional member function overrides.

Murxla uses naming convention <solver name (short)>Solver for solver wrapper solver implementations, e.g., the cvc5 implementation is called Cvc5Solver and the Bitwuzla implementation is called BitwuzlaSolver.

Note that the constructor of murxla::Solver is not to be overriden. A solver instance is created and deleted via the required member function overrides of functions murxla::Solver::new_solver() and murxla::Solver::delete_solver(). For example, in the solver wrapper for cvc5 (using its C++ API) these are implemented as follows:

void
Cvc5Solver::new_solver()
{
  assert(d_solver == nullptr);
  d_solver = new ::cvc5::Solver();
  d_tracer.init();
  // Incremental solving is enabled by default via cvc5's API. We disable it
  // when creating a new solver instance and explicitly enable it later on in
  // order to correctly trace the option.
  TRACE_SOLVER(setOption, "incremental", "false");
}

void
Cvc5Solver::delete_solver()
{
  assert(d_solver != nullptr);
  delete d_solver;
  d_solver = nullptr;
}

Another example for a required override is member function murxla::Solver::get_name(), which returns the name of the solver under test. It is implemented for cvc5 as follows:

const std::string
Cvc5Solver::get_name() const
{
  return "cvc5";
}

An example for an optional override is member function murxla::Solver::get_unsat_core(), which returns a vector of terms representing the unsat core of the currently asserted formula. It is implemented in the solver wrapper for Bitwuzla (using its C API) as follows:

std::vector<Term>
BitwuzlaSolver::get_unsat_core()
{
  assert(d_solver != nullptr);
  return BitwuzlaTerm::bitwuzla_terms_to_terms(d_tm.get(),
                                               d_solver->get_unsat_core());
}