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 BzlaTerm.

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>
BzlaTerm::get_children() const
{
  std::vector<Term> res;
  size_t size                   = 0;
  const BitwuzlaTerm** bzla_res = bitwuzla_term_get_children(d_term, &size);
  return bzla_terms_to_terms(bzla_res, size);
}

We use a helper function std::vector<Term> BzlaTerm::bzla_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>
BzlaTerm::bzla_terms_to_terms(const BitwuzlaTerm** terms, size_t size)
{
  std::vector<Term> res;
  for (size_t i = 0; i < size; ++i)
  {
    res.push_back(std::shared_ptr<BzlaTerm>(new BzlaTerm(terms[i])));
  }
  return res;
}

The following list provides all the member functions of class murxla::AbsTerm that are required or optional to be overriden by a solver wrapper.

Note

Optional overrides have default implementations, but should be overriden if supported by the solver.

AbsTerm: Functions Required to be Overriden

virtual size_t hash() const = 0

Get the hash value of this term.

Returns: The hash value of this term.

virtual std::string to_string() const = 0

Get a string representation of this term.

Returns: A string representation of this term.

virtual bool equals(const std::shared_ptr<AbsTerm> &other) const = 0

Determine if this term is equal to the given term.

Parameters: other – The term to compare this term to.
Returns: True if this term is equal to the other term.

AbsTerm: Functions to be Overriden Optionally

virtual bool not_equals(const std::shared_ptr<AbsTerm> &other) const

Determine if this term is not equal to the given term.

Parameters: other – The term to compare this term to.
Returns: True if this term is not equal to the other term.

virtual bool is_array() const

Determine if this term is an Array term.

Returns: True if this term is an Array term.

virtual bool is_bag() const

Determine if this term is a Bag term.

Returns: True if this term is a Bag term.

virtual bool is_bool() const

Determine if this term is a Boolean term.

Returns: True if this term is a Boolean term.

virtual bool is_bv() const

Determine if this term is a bit-vector term.

Returns: True if this term is a bit-vector term.

virtual bool is_dt() const

Determine if this term is a datatype term.

Returns: True if this term is a datatype term.

virtual bool is_fp() const

Determine if this term is a floating-point term.

Returns: True if this term is a floating-point term.

virtual bool is_fun() const

Determine if this term is a function term.

Returns: True if this term is a function term.

virtual bool is_int() const

Determine if this term is an Int term.

Returns: True if this term is an Int term.

virtual bool is_real() const

Determine if this term is a Real term.

Returns: True if this term is a Real term.

virtual bool is_rm() const

Determine if this term is a RoundingMode term.

Returns: True if this term is a RoundingMode term.

virtual bool is_reglan() const

Determine if this term is a RegLan term.

Returns: True if this term is a RegLan term.

virtual bool is_seq() const

Determine if this term is a Sequence term.

Returns: True if this term is a Sequence term.

virtual bool is_set() const

Determine if this term is a Set term.

Returns: True if this term is a Set term.

virtual bool is_string() const

Determine if this term is a String term.

Returns: True if this term is a String term.

virtual bool is_uninterpreted() const

Determine if this term is an uninterpreted term.

Returns: True if this term is an uninterpreted term.

virtual bool is_bag_value() const

Determine if this term is a Bag value.

Returns: True if this term is a Bag value.

virtual bool is_bool_value() const

Determine if this term is a Boolean value.

Returns: True if this term is a Boolean value.

virtual bool is_bv_value() const

Determine if this term is a bit-vector value.

Returns: True if this term is a bit-vector value.

virtual bool is_dt_value() const

Determine if this term is a datatype value.

Returns: True if this term is a datatype value.

virtual bool is_fp_value() const

Determine if this term is a floating-point value.

Returns: True if this term is a floating-point value.

virtual bool is_int_value() const

Determine if this term is an integer value.

Returns: True if this term is an integer value.

virtual bool is_real_value() const

Determine if this term is a real value.

Returns: True if this term is a real value.

virtual bool is_reglan_value() const

Determine if this term is a RegLan value.

Returns: True if this term is a RegLan value.

virtual bool is_rm_value() const

Determine if this term is a rounding mode value.

Returns: True if this term is a rounding mode value.

virtual bool is_seq_value() const

Determine if this term is a Sequence value.

Returns: True if this term is a Sequence value.

virtual bool is_set_value() const

Determine if this term is a Sequence value.

Returns: True if this term is a Sequence value.

virtual bool is_string_value() const

Determine if this term is a string value.

Returns: True if this term is a string value.

virtual bool is_special_value(const SpecialValueKind &kind) const

Determine if this term is a special value of given kind.

Returns: True if this term is a special value of given kind.

virtual bool is_const() const

Determine if this term is a first-order constant.

Returns: True if this term is a first-order constant.

virtual bool is_value() const

Determine if this term is a value.

Returns: True if this term is a value.

virtual bool is_var() const

Determine if this term is a variable.

Returns: True if this term is a variable.

virtual const Op::Kind &get_kind() const

Get the kind of this term.

This kind is not a kind we cache on creation, but the kind that the solver reports. May be Op::UNDEFINED.

Must be overriden and may not return Op::UNDEFINED if the solver supports the theory of bags, sets and sequences (required for properly initializing sorts that are implicitly created, e.g., sequence sorts for Op::SEQ_UNIT).

Returns: The kind of this term.

virtual std::vector<std::shared_ptr<AbsTerm>> get_children() const

Get the children of this term.

Note

As with Solver::mk_term, the returned terms are “raw” Terms, in the sense that they are only wrapped into a Term, with no additional book keeping information (all data members have default values).

Returns: The children of this term.

virtual bool is_indexed() const

Determine if this term is of an indexed operator kind.

Returns: True if this term is of an indexed operator kind.

virtual size_t get_num_indices() const

Get the number of indices of a term with an indexed operator kind.

Returns: The number of indices.

virtual std::vector<std::string> get_indices() const

Get the indices of a term with an indexed operator kind.

Returns: The indinces of a term with an indexed operator kind.

virtual uint32_t get_bv_size() const

Get the bit width of this term. Asserts that it is a bit-vector term.

Returns: The size of this bit-vector term.

virtual uint32_t get_fp_exp_size() const

Get the exponent bit width of this term. Asserts that it is a floating-point term.

Returns: The size of the exponent of this floating-point term.

virtual uint32_t get_fp_sig_size() const

Get the significand bit width of this term. Asserts that it is a floating-point term.

Returns: The size of the signifcand of this floating-point term.

virtual Sort get_array_index_sort() const

Get the array index sort of this term. Asserts that it is an array term.

Returns: The index sort of this array term.

virtual Sort get_array_element_sort() const

Get the array element sort of this term. Asserts that it is an array term.

Returns: The element sort of this array term.

virtual uint32_t get_fun_arity() const

Get the function arity of this term. Asserts that it is an function term.

Returns: The arity of this function term.

virtual Sort get_fun_codomain_sort() const

Get the function codomain sort of this term. Asserts that it is an function term.

Returns: The codomain sort of this function term.

virtual std::vector<Sort> get_fun_domain_sorts() const

Get the function domain sorts of this term. Asserts that it is an function term.

Returns: The domain sorts of this function term.