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
-
enumerator NONE
-
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.
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.
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.
-
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.
-
enum LeafKind