Solver Wrapper Interface: AbsSort

class murxla::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_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.

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 std::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 murxla::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_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 murxla::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_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.