Solver Wrapper Interface: AbsTerm

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

Determine if this term is a finite-field term.

Returns:

True if this term is a finite-field 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_ff_value() const

Determine if this term is a finite-field value.

Returns:

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

Get the size of this finite-field term’s field.

Returns:

The finite-field size of this finite-field term, or 0 by default.

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.

template<>
struct 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.