Term

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

using murxla::Term = std::shared_ptr<AbsTerm>

The Murxla-internal representation of a term.

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

Operator overload for equality over Terms.

Parameters

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

• b – The other term.

Returns

True if AbsTerm::equals() (which queries the solver) is true and the sorts of a and b are equal.

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

Parameters

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

• b – The other term. Operator overload for disequality over Terms.

Returns

True if AbsTerm::not_equals() (which queries the solver) is true and the sorts of a and b are not equal.

std::ostream &murxla::operator<<(std::ostream &out, const Term t)

Serialize a Term to given stream.

This represents a term as ‘t’ + its id and is mainly intended for tracing purposes. For a representation of a term as provided by the corresponding solver, use AbsTerm::to_string() instead.

Parameters

• out – The output stream.

• t – The term to be serialized.

Returns

The output stream.

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

Serialize a vector of Terms to given stream.

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

Parameters

• out – The output stream.

• vector – The vector of terms to be serialized.

Returns

The output stream.