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

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
BzlaSort::is_bv() const
{
  return bitwuzla_sort_is_bv(d_sort);
}

The following list provides all the member functions of class murxla::AbsSort 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.

AbsSort: Functions Required to be Overriden

virtual size_t hash() const = 0

Get the hash value of this sort.

Returns: The hash value of this sort.

virtual std::string to_string() const = 0

Get the string representation of this sort.

Returns: A string representation of this sort.

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

Determine if this sort is equal to the given sort.

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

AbsSort: Functions to be Overriden Optionally

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

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

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

inline virtual bool is_array() const

Determine if this sort is an Array sort.

Returns: True if this sort is an Array sort.

inline virtual bool is_bag() const

Determine if this sort is a Bag sort.

Returns: True if this sort is a Bag sort.

inline virtual bool is_bool() const

Determine if this sort is a Boolean sort.

Returns: True if this sort is a Boolean sort.

inline virtual bool is_bv() const

Determine if this sort is a bit-vector sort.

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

inline virtual bool is_dt() const

Determine if this sort is a datatype sort.

Returns: True if this sort is a datatype sort.

inline virtual bool is_dt_parametric() const

Determine if this sort is a parametric datatype sort.

Returns: True if this sort is a parametric datatype sort.

inline virtual bool is_fp() const

Determine if this sort is a floating-point sort.

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

inline virtual bool is_fun() const

Determine if this sort is a function sort.

Returns: True if this sort is a function sort.

inline virtual bool is_int() const

Determine if this sort is an integer sort.

Returns: True if this sort is an Int sort.

inline virtual bool is_real() const

Determine if this sort is a real sort.

Returns: True if this sort is a Real sort.

inline virtual bool is_rm() const

Determine if this sort is a rounding mode sort.

Returns: True if this sort is a RoundingMode sort.

inline virtual bool is_reglan() const

Determine if this sort is a regular language sort.

Returns: True if this sort is a RegLan sort.

inline virtual bool is_seq() const

Determine if this sort is a sequence sort.

Returns: True if this sort is a Sequence sort.

inline virtual bool is_set() const

Determine if this sort is a set sort.

Returns: True if this sort is a Set sort.

inline virtual bool is_string() const

Determine if this sort is a string sort.

Returns: True if this sort is a String sort.

inline virtual bool is_uninterpreted() const

Determine if this sort is an uninterpreted sort.

Returns: True if this sort is an uninterpreted sort.

virtual bool is_dt_well_founded() const

Determine if this datatype sort is well founded.

We use this to filter out datatype sorts that are not well founded. Default returns always true, must be overriden by solver to actually check if the datatype sort is well founded. If not, this may trigger (properly handled) errors in the solver due to non-well-foundedness.

Returns: True if this datatype sort is well founded.

virtual Sort get_array_index_sort() const

Get the array index sort of this sort.

Returns: The index sort of this array sort, or a nullptr by default.

virtual Sort get_array_element_sort() const

Get the array element sort of this sort.

Returns: The element sort of this array sort, or a nullptr by default.

virtual Sort get_bag_element_sort() const

Get the bag element sort of this sort.

Returns: The element sort of this bag sort, or a nullptr by default.

virtual uint32_t get_bv_size() const

Get the bit-vector size of this sort.

Returns: The size of this bit-vector sort, or 0 by default.

virtual std::string get_dt_name() const

Get the datatype name of this sort.

Returns: The name of this datatype sort, or an empty string by default.

virtual uint32_t get_dt_num_cons() const

Get the number of datatype constructors of this sort.

Returns: The number of constructors of this datatype sort, or 0 by default.

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

Get the datatype constructor names of this sort.

Returns: A vector with the constructor names of this datatype sort, or an empty vector by default.

virtual uint32_t get_dt_cons_num_sels(const std::string &name) const

Get the number of selectors of the given datatype constructor of this sort.

Returns: The number of selectors of this datatype sort, or 0 by default.

virtual std::vector<std::string> get_dt_cons_sel_names(const std::string &name) const

Get the selector names of the given datatype constructor of this sort.

Parameters: name – The name of the constructor for which to get the selector names.
Returns: A vector with the selector names of the given constructor of this datatype sort, or an empty vector by default.

virtual uint32_t get_fp_exp_size() const

Get the floating-point exponent size of this sort.

Returns: The exponent size of this floating-point sort, or 0 by default.

virtual uint32_t get_fp_sig_size() const

Get the floating-point significand size of this sort.

Returns: The significand size of this floating-point sort, or 0 by default.

virtual uint32_t get_fun_arity() const

Get the function arity of this sort.

Returns: The arity of this function sort, or 0 by default.

virtual Sort get_fun_codomain_sort() const

Get the function codomain sort of this sort.

Returns: The codomain sort of this function sort, or a nullptr by default.

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

Get the function domain sorts of this sort.

Returns: A vector with the domain sorts of this function sort, or an empty vector by default.

virtual Sort get_seq_element_sort() const

Get the sequence element sort of this sort.

Returns: The element sort of this sequence sort, or a nullptr by default.

virtual Sort get_set_element_sort() const

Get the set element sort of this sort.

Returns: The element sort of this set sort, or a nullptr by default.