Pre-Defined Special Value Kinds
The list of special value kinds globally defined in
murxla::AbsTerm.
Special values are created via murxla::Solver::mk_special_value().
The set of special value kinds can be extended with solver-specific special
value kinds via overriding murxla::Solver::add_special_value().
-
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_FF_ZERO = "ff.zero"
The kind of a term representing a finite-field zero value.
-
static const SpecialValueKind SPECIAL_VALUE_FF_ONE = "ff.one"
The kind of a term representing a finite-field zero value.
-
static const SpecialValueKind SPECIAL_VALUE_FF_NEG_ONE = "ff.negone"
The kind of a term representing a finite-field zero 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.