Sort

Murxla defines type Sort for sort representations as an alias of shared pointer (std::shared_ptr) to AbsSort. We only deal with Sort objects in Murxla core components and at the interface between Murxla and the solver wrapper.

using murxla::Sort = std::shared_ptr<AbsSort>

The Murxla-internal representation of a sort.

bool murxla::operator==(const Sort &a, const Sort &b)

Operator overload for equality over Sorts.

Parameters

• a – The sort to be compared with the other sort.

• b – The other sort.

Returns

True if AbsSort::equals() (which queries the solver) is true and the kinds (murxla::SortKind) of a and b are equal.

bool murxla::operator!=(const Sort &a, const Sort &b)

Operator overload for disequality over Sorts.

Parameters

• a – The sort to be compared with the other sort.

• b – The other sort.

Returns

True if AbsSort::not_equals() (which queries the solver) is true and the kinds (murxla::SortKind) of a and b are not equal.

std::ostream &murxla::operator<<(std::ostream &out, const Sort s)

Serialize a Sort to given stream.

This represents a sort as ‘s’ + its id and is mainly intended for tracing purposes. For a representation of a term as provided by the corresponding solver, user AbsSort::to_string() insted.

Parameters

• out – The output stream.

• s – The sort to be serialized.

Returns

The output stream.

std::ostream &murxla::operator<<(std::ostream &out, const std::vector<Sort> &vector)

Serialize a vector of Sorts to given stream.

As above, a sort is represented as s + its id, so this will yield a list of space separated s<id>s.

Parameters

• out – The output stream.

• vector – The vector of sorts to be serialized.

Returns

The output stream.