Solver Wrapper Implementation for Terms

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

Murxla uses naming convention <solver name (short)>Term for solver wrapper term implementations, e.g., the cvc5 implementation is called Cvc5Term and the Bitwuzla implementation is called BitwuzlaTerm.

An example for a required override is member function murxla::AbsTerm::hash(), which returns a hash value for a given term. It is implemented in the solver wrapper for cvc5 (using its C++ API) as follows:

size_t
Cvc5Term::hash() const
{
  return std::hash<::cvc5::Term>{}(d_term);
}

An example for an optional override is member function murxla::AbsTerm::get_children(), which returns the children of a given term. It is implemented in the solver wrapper for Bitwuzla (using its C API) as follows:

std::vector<Term>
BitwuzlaTerm::get_children() const
{
  return bitwuzla_terms_to_terms(d_tm, d_term.children());
}

We use a helper function std::vector<Term> BitwuzlaTerm::bitwuzla_terms_to_terms(const BitwuzlaTerm**, size_t) to convert Bitwuzla term objects to Bitwuzla solver wrapper term objects, which is defined as follows:

std::vector<Term>
BitwuzlaTerm::bitwuzla_terms_to_terms(
    ::bitwuzla::TermManager* tm, const std::vector<::bitwuzla::Term>& terms)
{
  std::vector<Term> res;
  for (const auto& t : terms)
  {
    res.push_back(std::shared_ptr<BitwuzlaTerm>(new BitwuzlaTerm(tm, t)));
  }
  return res;
}