Op
-
class
Op
-
A cvc5 operator.
An operator is a term that represents certain operators, instantiated with its required parameters, e.g., a Term of kind #BITVECTOR_EXTRACT.
Public Functions
-
Op
(
)
-
Constructor.
-
~Op
(
)
-
Destructor.
-
bool
operator
==
(
const
Op
&
t
)
const
-
Syntactic equality operator.
- Parameters :
-
t – The operator to compare to for equality.
- Returns :
-
True if both operators are syntactically identical.
-
bool
operator
!=
(
const
Op
&
t
)
const
-
Syntactic disequality operator.
- Parameters :
-
t – The operator to compare to for disequality.
- Returns :
-
True if operators differ syntactically.
-
Kind
getKind
(
)
const
-
Get the kind of this operator.
- Returns :
-
The kind of this operator.
-
bool
isNull
(
)
const
-
Determine if this operator is nullary.
- Returns :
-
True if this operator is a nullary operator.
-
bool
isIndexed
(
)
const
-
Determine if this operator is indexed.
- Returns :
-
True iff this operator is indexed.
-
size_t
getNumIndices
(
)
const
-
Get the number of indices of this operator.
- Returns :
-
The number of indices of this operator.
-
Term
operator
[]
(
size_t
i
)
const
-
Get the index at position
iof an indexed operator.- Parameters :
-
i – The position of the index to return.
- Returns :
-
The index at position i.
-
std
::
string
toString
(
)
const
-
Get the string representation of this operator.
- Returns :
-
A string representation of this operator.
-
Op
(
)