Solver Wrapper Implementation for Sorts

Solver wrappers derive a sort class from murxla::AbsSort, which manages construction and destruction of solver sort objects and implements required and optional member function overrides.

Murxla uses naming convention <solver name (short)>Sort for solver wrapper sort implementations, e.g., the cvc5 implementation is called Cvc5Sort and the Bitwuzla implementation is called BitwuzlaSort.

An example for a required override is member function murxla::AbsSort::equals(), which determines if two given sorts are equal. It is implemented in the solver wrapper for cvc5 (using its C++ API) as follows:

bool
Cvc5Sort::equals(const Sort& other) const
{
  Cvc5Sort* cvc5_sort = checked_cast<Cvc5Sort*>(other.get());
  if (cvc5_sort)
  {
    return d_sort == cvc5_sort->d_sort;
  }
  return false;
}

An example for an optional override is member function murxla::AbsSort::is_bv(), which determines if a given sort is a bit-vector sort. It is implemented in the solver wrapper for Bitwuzla (using its C API) as follows:

bool
BitwuzlaSort::is_bv() const
{
  return d_sort.is_bv();
}