Solver Wrapper Interface: AbsSort

class AbsSort

The abstract base class for sorts.

A solver wrapper must implement a solver-specific sort wrapper class derived from this class.

Subclassed by murxla::ParamSort, murxla::UnresolvedSort, murxla::shadow::ShadowSort, murxla::smt2::Smt2Sort

Public Types

using DatatypeConstructorMap = std::unordered_map<std::string, std::vector<std::pair<std::string, Sort>>>

A map representation of the constructors of a datatype sort. Maps constructor names to vectors of selectors, represented as pairs of selector name and selector sort.

Public Functions

inline virtual ~AbsSort()

Destructor.

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.

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_ff() const

Determine if this sort is a finite-field sort.

Returns:

True if this sort is a finite-field 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 std::string get_ff_size() const

Get the size of this finite-field sort.

Returns:

The finite-field size of this finite-field sort, or 0 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.

virtual void set_kind(SortKind sort_kind)

Set the kind of this sort.

Parameters:

sort_kind – The kind of this sort.

virtual void set_sorts(const std::vector<Sort> &sorts)

Set the sort parameters of this sort.

The given vector sorts consists of the following sorts, depending on the kind of this sort.

• SORT_ARRAY: A vector of size 2, with index and element sort.

• SORT_BAG: A vector of size 1, with the element sort.

• SORT_DT (parametric):

  • non-instantiated: A vector of size n, with sorts of type ParamSort.

  • instantiated: A vector of size n, with the sorts this sort is instantiated with. May be of type ParamSort or UnresolvedSort.

• SORT_FUN: A vector of size n, with the function domain sorts.

• SORT_SEQ: A vector of size 1, with the element sort.

• SORT_SET: A vector of size 1, with the element sort.

• UnresolvedSort: A vector of size n, with the sorts this (parametric) unresolved sort is to be instantiated with. UnresolvedSorts only occur when constructing mutually recursive datatype sorts.

Parameters:

sorts – The sort parameters of this sort.

virtual void set_associated_sort(Sort sort)

Set the associated sort.

This is for sorts of type ParamSort and UnresolvedSort to add a back reference to the associated sort. For ParamSort, this is the sort this sort has been assigned as a parameter to. For UnresolvedSort, this is the resolved DT sort this unresolved sort stands in for.

Note

For solver wrappers, only the associated sort of ParamSort will be relevant. The associated sort for UnresolvedSort is mainly required for book keeping on the Murxla level.

Parameters:

sort – The associated sort.

virtual void set_dt_ctors(const DatatypeConstructorMap &ctors)

Set the constructor map of this datatype sort.

The constructor map maps constructor names to lists of selectors, which are represented as pairs of selector name and sort.

Note

This is for book keeping on the Murxla level.

Parameters:

ctors – The constructor map.

virtual void set_dt_is_instantiated(bool value)

Mark this parametric datatype sort as instantiated sort.

Note

This is for book keeping on the Murxla level.

Parameters:

value – True if this datatype sort is an instantiated sort.

virtual bool is_param_sort() const

Determine if this sort is of type ParamSort.

Returns:

True if this sort is of type ParamSort.

virtual bool is_unresolved_sort() const

Determine if this sort is of type UnresolvedSort.

Returns:

True if this sort is of type UnresolvedSort.

void set_id(uint64_t id)

Set the (unique) id of this sort.

Parameters:

id – The id of this sort.

uint64_t get_id() const

Get the id of this sort.

Returns:

The id of this sort.

SortKind get_kind() const

Get the kind of this sort.

Returns:

The kind of this sort.

const std::vector<Sort> &get_sorts() const

Get the sort parameters of this sort (see set_sorts()).

Returns:

The sort parameters of this sort.

Sort get_associated_sort() const

Get the associated sort of this sort (see set_associated_sort()).

Returns:

The associated sort of this sort.

DatatypeConstructorMap &get_dt_ctors()

Get the constructor map of this datatype sort (see set_dt_ctors()).

Returns:

The datatype constructor map of this sort.

std::vector<std::string> get_dt_ctor_names() const

Get the list of constructor names of this sort, as recorded in the datatype constructor map (this does not query the solver!).

Returns:

The list of constructor names of this datatype sort as recorded on the Murxla level.

std::vector<std::string> get_dt_sel_names(const std::string &ctor) const

Get the list of selector names of the given constructor, as recorded in the datatype constructor map (this does not query the solver!).

Parameters:

ctor – The constructor to retrieve the selector name list for.

Returns:

The selector names for the given constructor of this datatype sort.

Sort get_dt_sel_sort(Sort dt_sort, const std::string &ctor, const std::string &sel) const

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

Note

Sort dt_sort must be the sort that this function is called on. We need to pass this for handling the self selector case (where the selector codomain sort is a nullptr).

Parameters:

• dt_sort – The datatype sort this function is called on.

• ctor – The name of the constructor.

• sel – The name of the selector of the given constructor.

Returns:

The sort of the given selector, or dt_sort in case of a self selector.

DatatypeConstructorMap instantiate_dt_param_sort(const std::vector<Sort> &sorts) const

Instantiate datatype constructor map of this parametric datatype sort with the given vector of sorts.

Note

This is only for book keeping on the Murxla level.

Parameters:

sorts – The sorts to instantiate this parametric datatype with.

Returns:

The datatype constructor map of this sort instantiated with the given sorts.

bool is_dt_instantiated() const

Determine if this sort is an instantiated parametric datatype sort.

Returns:

True if this is an instantiated parametric datatype sort.

Protected Attributes

uint64_t d_id = 0u

The (unique) id of this sort.

SortKind d_kind = SORT_ANY

The kind of this sort.

std::vector<Sort> d_sorts

The sort parameters for sorts parameterized over sorts (see set_sorts()).

Note

If this is an UnresolvedSort that refers to a parametric datatype, this contains the set of sort parameters to instantiate the sort with.

Sort d_associated_sort = nullptr

The sort this sort is associated with. This is only non-null for ParamSorts and UnresolvedSorts and refers to their associated DT sort.

DatatypeConstructorMap d_dt_ctors

The datatype constructors of this sort.

This is only used for datatype sorts and required for book keeping on the murxla level. Maps constructor names to vectors of selectors, which are represented as pairs of selector name and codomain sort.

bool d_dt_is_instantiated = false

True if this is an instantiated parametric datatype sort.

template<>
struct hash<murxla::Sort>

Specialization of std::hash for Sort.

Public Functions

size_t operator()(const murxla::Sort &s) const

Operator overload to get the hash value of a sort.

Parameters:

s – The sort to compute the hash value for.

Returns:

The hash value of a sort.

class ParamSort : public murxla::AbsSort

Parameter sort.

A parameter sort is a sort place holder representing a sort parameter for parametric datatype sorts. Parameter sorts are only to be used for parametric datatypes.

ParamSort is explicitly not a wrapper around a solver sort type, but a dedicated type that requires special handling in the solver wrapper.

A back reference to the associated datatype sort is stored in d_associated_sort and can be accessed via get_associated_sort().

Note

Instances of ParamSort may never be added to the solver manager’s sort database. No terms of ParamSort may ever be created.

Public Functions

inline ParamSort(const std::string &symbol)

Constructor.

virtual size_t hash() const override

Get the hash value of this sort.

Returns:

The hash value of this sort.

virtual std::string to_string() const override

Get the string representation of this sort.

Returns:

A string representation of this sort.

bool equals(const Sort &other) const override

inline virtual bool is_array() const override

Determine if this sort is an Array sort.

Returns:

True if this sort is an Array sort.

inline virtual bool is_bag() const override

Determine if this sort is a Bag sort.

Returns:

True if this sort is a Bag sort.

inline virtual bool is_bool() const override

Determine if this sort is a Boolean sort.

Returns:

True if this sort is a Boolean sort.

inline virtual bool is_bv() const override

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 override

Determine if this sort is a datatype sort.

Returns:

True if this sort is a datatype sort.

inline virtual bool is_dt_parametric() const override

Determine if this sort is a parametric datatype sort.

Returns:

True if this sort is a parametric datatype sort.

inline virtual bool is_ff() const override

Determine if this sort is a finite-field sort.

Returns:

True if this sort is a finite-field sort.

inline virtual bool is_fp() const override

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 override

Determine if this sort is a function sort.

Returns:

True if this sort is a function sort.

inline virtual bool is_int() const override

Determine if this sort is an integer sort.

Returns:

True if this sort is an Int sort.

inline virtual bool is_real() const override

Determine if this sort is a real sort.

Returns:

True if this sort is a Real sort.

inline virtual bool is_rm() const override

Determine if this sort is a rounding mode sort.

Returns:

True if this sort is a RoundingMode sort.

inline virtual bool is_reglan() const override

Determine if this sort is a regular language sort.

Returns:

True if this sort is a RegLan sort.

inline virtual bool is_seq() const override

Determine if this sort is a sequence sort.

Returns:

True if this sort is a Sequence sort.

inline virtual bool is_set() const override

Determine if this sort is a set sort.

Returns:

True if this sort is a Set sort.

inline virtual bool is_string() const override

Determine if this sort is a string sort.

Returns:

True if this sort is a String sort.

inline virtual bool is_param_sort() const override

Determine if this sort is of type ParamSort.

Returns:

True if this sort is of type ParamSort.

inline const std::string &get_symbol() const

Get the symbol of this parameter sort.

Returns:

The symbol.

class UnresolvedSort : public murxla::AbsSort

Unresolved sort.

An unresolved sort is a sort place holder for yet unresolved datatype sorts when constructing mutually recursive datatype sorts. Unresolved sorts are only to be used for mutually recursive datatypes.

UnresolvedSort is explicitly not a wrapper around a solver sort type, but a dedicated type that requires special handling in the solver wrapper.

A back reference to the associated datatype sort is stored in d_associated_sort and can be accessed via get_associated_sort().

Note

Instances of UnresolvedSort may never be added to the solver manager’s sort database. No terms of UnresolvedSort may ever be created.

Public Functions

inline UnresolvedSort(const std::string &symbol)

Constructor.

virtual size_t hash() const override

Get the hash value of this sort.

Returns:

The hash value of this sort.

virtual std::string to_string() const override

Get the string representation of this sort.

Returns:

A string representation of this sort.

bool equals(const Sort &other) const override

inline virtual bool is_array() const override

Determine if this sort is an Array sort.

Returns:

True if this sort is an Array sort.

inline virtual bool is_bag() const override

Determine if this sort is a Bag sort.

Returns:

True if this sort is a Bag sort.

inline virtual bool is_bool() const override

Determine if this sort is a Boolean sort.

Returns:

True if this sort is a Boolean sort.

inline virtual bool is_bv() const override

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 override

Determine if this sort is a datatype sort.

Returns:

True if this sort is a datatype sort.

inline virtual bool is_dt_parametric() const override

Determine if this sort is a parametric datatype sort.

Returns:

True if this sort is a parametric datatype sort.

inline virtual bool is_ff() const override

Determine if this sort is a finite-field sort.

Returns:

True if this sort is a finite-field sort.

inline virtual bool is_fp() const override

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 override

Determine if this sort is a function sort.

Returns:

True if this sort is a function sort.

inline virtual bool is_int() const override

Determine if this sort is an integer sort.

Returns:

True if this sort is an Int sort.

inline virtual bool is_real() const override

Determine if this sort is a real sort.

Returns:

True if this sort is a Real sort.

inline virtual bool is_rm() const override

Determine if this sort is a rounding mode sort.

Returns:

True if this sort is a RoundingMode sort.

inline virtual bool is_reglan() const override

Determine if this sort is a regular language sort.

Returns:

True if this sort is a RegLan sort.

inline virtual bool is_seq() const override

Determine if this sort is a sequence sort.

Returns:

True if this sort is a Sequence sort.

inline virtual bool is_set() const override

Determine if this sort is a set sort.

Returns:

True if this sort is a Set sort.

inline virtual bool is_string() const override

Determine if this sort is a string sort.

Returns:

True if this sort is a String sort.

inline virtual bool is_unresolved_sort() const override

Determine if this sort is of type UnresolvedSort.

Returns:

True if this sort is of type UnresolvedSort.

inline const std::string &get_symbol() const

Get the symbol of this unresolved sort.

Returns:

The symbol.