Solver Wrapper Interface: AbsTerm

class murxla::AbsTerm

The abstract base class for terms.

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

Subclassed by murxla::shadow::ShadowTerm, murxla::smt2::Smt2Term

Public Types

enum LeafKind

The leaf kind of a term.

Values:

enumerator NONE

enumerator CONSTANT

enumerator VALUE

enumerator VARIABLE

using SpecialValueKind = std::string

The kind of a special value (see Solver::mk_special_value()).

Note

This is an std::string rather than an enum to allow for solvers to extend the set of special value kinds.

Public Functions

inline AbsTerm()

Constructor.

inline virtual ~AbsTerm()

Destructor.

virtual size_t hash() const = 0

Get the hash value of this term.

Returns

The hash value of this term.

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

Get a string representation of this term.

Returns

A string representation of this term.

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

Determine if this term is equal to the given term.

Parameters

other – The term to compare this term to.

Returns

True if this term is equal to the other term.

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

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

Parameters

other – The term to compare this term to.

Returns

True if this term is not equal to the other term.

virtual bool is_array() const

Determine if this term is an Array term.

Returns

True if this term is an Array term.

virtual bool is_bag() const

Determine if this term is a Bag term.

Returns

True if this term is a Bag term.

virtual bool is_bool() const

Determine if this term is a Boolean term.

Returns

True if this term is a Boolean term.

virtual bool is_bv() const

Determine if this term is a bit-vector term.

Returns

True if this term is a bit-vector term.

virtual bool is_dt() const

Determine if this term is a datatype term.

Returns

True if this term is a datatype term.

virtual bool is_fp() const

Determine if this term is a floating-point term.

Returns

True if this term is a floating-point term.

virtual bool is_fun() const

Determine if this term is a function term.

Returns

True if this term is a function term.

virtual bool is_int() const

Determine if this term is an Int term.

Returns

True if this term is an Int term.

virtual bool is_real() const

Determine if this term is a Real term.

Returns

True if this term is a Real term.

virtual bool is_rm() const

Determine if this term is a RoundingMode term.

Returns

True if this term is a RoundingMode term.

virtual bool is_reglan() const

Determine if this term is a RegLan term.

Returns

True if this term is a RegLan term.

virtual bool is_seq() const

Determine if this term is a Sequence term.

Returns

True if this term is a Sequence term.

virtual bool is_set() const

Determine if this term is a Set term.

Returns

True if this term is a Set term.

virtual bool is_string() const

Determine if this term is a String term.

Returns

True if this term is a String term.

virtual bool is_uninterpreted() const

Determine if this term is an uninterpreted term.

Returns

True if this term is an uninterpreted term.

virtual bool is_bag_value() const

Determine if this term is a Bag value.

Returns

True if this term is a Bag value.

virtual bool is_bool_value() const

Determine if this term is a Boolean value.

Returns

True if this term is a Boolean value.

virtual bool is_bv_value() const

Determine if this term is a bit-vector value.

Returns

True if this term is a bit-vector value.

virtual bool is_dt_value() const

Determine if this term is a datatype value.

Returns

True if this term is a datatype value.

virtual bool is_fp_value() const

Determine if this term is a floating-point value.

Returns

True if this term is a floating-point value.

virtual bool is_int_value() const

Determine if this term is an integer value.

Returns

True if this term is an integer value.

virtual bool is_real_value() const

Determine if this term is a real value.

Returns

True if this term is a real value.

virtual bool is_reglan_value() const

Determine if this term is a RegLan value.

Returns

True if this term is a RegLan value.

virtual bool is_rm_value() const

Determine if this term is a rounding mode value.

Returns

True if this term is a rounding mode value.

virtual bool is_seq_value() const

Determine if this term is a Sequence value.

Returns

True if this term is a Sequence value.

virtual bool is_set_value() const

Determine if this term is a Sequence value.

Returns

True if this term is a Sequence value.

virtual bool is_string_value() const

Determine if this term is a string value.

Returns

True if this term is a string value.

virtual bool is_special_value(const SpecialValueKind &kind) const

Determine if this term is a special value of given kind.

Returns

True if this term is a special value of given kind.

virtual bool is_const() const

Determine if this term is a first-order constant.

Returns

True if this term is a first-order constant.

virtual bool is_value() const

Determine if this term is a value.

Returns

True if this term is a value.

virtual bool is_var() const

Determine if this term is a variable.

Returns

True if this term is a variable.

virtual const Op::Kind &get_kind() const

Get the kind of this term.

This kind is not a kind we cache on creation, but the kind that the solver reports. May be Op::UNDEFINED.

Must be overriden and may not return Op::UNDEFINED if the solver supports the theory of bags, sets and sequences (required for properly initializing sorts that are implicitly created, e.g., sequence sorts for Op::SEQ_UNIT).

Returns

The kind of this term.

virtual std::vector<std::shared_ptr<AbsTerm>> get_children() const

Get the children of this term.

Note

As with Solver::mk_term, the returned terms are “raw” Terms, in the sense that they are only wrapped into a Term, with no additional book keeping information (all data members have default values).

Returns

The children of this term.

virtual bool is_indexed() const

Determine if this term is of an indexed operator kind.

Returns

True if this term is of an indexed operator kind.

virtual size_t get_num_indices() const

Get the number of indices of a term with an indexed operator kind.

Returns

The number of indices.

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

Get the indices of a term with an indexed operator kind.

Returns

The indinces of a term with an indexed operator kind.

virtual uint32_t get_bv_size() const

Get the bit width of this term. Asserts that it is a bit-vector term.

Returns

The size of this bit-vector term.

virtual uint32_t get_fp_exp_size() const

Get the exponent bit width of this term. Asserts that it is a floating-point term.

Returns

The size of the exponent of this floating-point term.

virtual uint32_t get_fp_sig_size() const

Get the significand bit width of this term. Asserts that it is a floating-point term.

Returns

The size of the signifcand of this floating-point term.

virtual Sort get_array_index_sort() const

Get the array index sort of this term. Asserts that it is an array term.

Returns

The index sort of this array term.

virtual Sort get_array_element_sort() const

Get the array element sort of this term. Asserts that it is an array term.

Returns

The element sort of this array term.

virtual uint32_t get_fun_arity() const

Get the function arity of this term. Asserts that it is an function term.

Returns

The arity of this function term.

virtual Sort get_fun_codomain_sort() const

Get the function codomain sort of this term. Asserts that it is an function term.

Returns

The codomain sort of this function term.

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

Get the function domain sorts of this term. Asserts that it is an function term.

Returns

The domain sorts of this function term.

virtual void set_sort(Sort sort)

Set the sort of this term.

This is not to be overriden by any solver implementations except the shadow solver.

Parameters

sort – The sort to be set.

virtual void set_leaf_kind(LeafKind kind)

Set leaf kind.

Set to LeafKind::NONE if this term is not a leaf.

Note

This is not to be overriden by any solver implementations except the shadow solver.

Parameters

kind – The leaf kind.

virtual void set_special_value_kind(const SpecialValueKind &value_kind)

Set special value kind.

Set to SPECIAL_VALUE_NONE if not a value or no special value.

Note

This is not to be overriden by any solver implementations except the shadow solver.

Parameters

value_kind – The kind of the special value.

void set_id(uint64_t id)

Set the id of this term.

Parameters

id – The id to be set.

uint64_t get_id() const

Get the id of this term.

Returns

The id of this term.

Sort get_sort() const

Get the sort of this term.

Returns

The sort of this term.

LeafKind get_leaf_kind() const

Get the leaf kind of this term.

Kind is LeafKind::NONE if this term is not a leaf.

Note

This is for Murxla level maintenance and not to be overriden with solver-specific implementations.

Returns

The leaf kind of this term.

Public Static Attributes

static const SpecialValueKind SPECIAL_VALUE_NONE = "not-a-special-value"

The kind of a term that is not a special value.

static const SpecialValueKind SPECIAL_VALUE_BAG_EMPTY = "bag.empty"

The kind of a term representing the empty bag.

static const SpecialValueKind SPECIAL_VALUE_BV_ZERO = "bv.zero"

The kind of a term representing a bit-vector zero value.

static const SpecialValueKind SPECIAL_VALUE_BV_ONE = "bv.one"

The kind of a term representing a bit-vector one value.

static const SpecialValueKind SPECIAL_VALUE_BV_ONES = "bv.ones"

The kind of a term representing a bit-vector ones value (all bits 1).

static const SpecialValueKind SPECIAL_VALUE_BV_MIN_SIGNED = "bv-min-signed"

The kind of a term representing a bit-vector minimum signed value.

static const SpecialValueKind SPECIAL_VALUE_BV_MAX_SIGNED = "bv-max-signed"

The kind of a term representing a bit-vector maximum signed value.

static const SpecialValueKind SPECIAL_VALUE_FP_NAN = "nan"

The kind of a term representing a floating-point not a number value.

static const SpecialValueKind SPECIAL_VALUE_FP_POS_INF = "+oo"

The kind of a term representing a floating-point positive infinity value.

static const SpecialValueKind SPECIAL_VALUE_FP_NEG_INF = "-oo"

The kind of a term representing a floating-point negative infinity value.

static const SpecialValueKind SPECIAL_VALUE_FP_POS_ZERO = "+zero"

The kind of a term representing a floating-point positive zero value.

static const SpecialValueKind SPECIAL_VALUE_FP_NEG_ZERO = "-zero"

The kind of a term representing a floating-point negative zero value.

static const SpecialValueKind SPECIAL_VALUE_RM_RNA = "rna"

The kind of a term representing a rounding mode round nearest ties to away value.

static const SpecialValueKind SPECIAL_VALUE_RM_RNE = "rne"

The kind of a term representing a rounding mode round nearest ties to even value.

static const SpecialValueKind SPECIAL_VALUE_RM_RTN = "rtn"

The kind of a term representing a rounding mode round toward negative value.

static const SpecialValueKind SPECIAL_VALUE_RM_RTP = "rtp"

The kind of a term representing a rounding mode round toward positive value.

static const SpecialValueKind SPECIAL_VALUE_RM_RTZ = "rtz"

The kind of a term representing a rounding mode round toward zero value.

static const SpecialValueKind SPECIAL_VALUE_SEQ_EMPTY = "seq.empty"

The kind of a term representing the empty sequence.

static const SpecialValueKind SPECIAL_VALUE_SET_EMPTY = "set.empty"

The kind of a term representing the empty set.

static const SpecialValueKind SPECIAL_VALUE_SET_UNIVERSE = "set.universe"

The kind of a term representing the universe set.

template<>
struct std::hash<murxla::Term>

Specialization of std::hash for Term.

Public Functions

size_t operator()(const murxla::Term &t) const

Operator overload to get the hash value of a term.

Parameters

t – The term to compute the hash value for.

Returns

The hash value of a term.