A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
Public Member Functions | |
sort (context &c) | |
sort (context &c, Z3_sort s) | |
sort (sort const &s) | |
operator Z3_sort () const | |
sort & | operator= (sort const &s) |
Return true if this sort and s are equal. More... | |
Z3_sort_kind | sort_kind () const |
Return the internal sort kind. More... | |
symbol | name () const |
Return name of sort. More... | |
bool | is_bool () const |
Return true if this sort is the Boolean sort. More... | |
bool | is_int () const |
Return true if this sort is the Integer sort. More... | |
bool | is_real () const |
Return true if this sort is the Real sort. More... | |
bool | is_arith () const |
Return true if this sort is the Integer or Real sort. More... | |
bool | is_bv () const |
Return true if this sort is a Bit-vector sort. More... | |
bool | is_array () const |
Return true if this sort is a Array sort. More... | |
bool | is_datatype () const |
Return true if this sort is a Datatype sort. More... | |
bool | is_relation () const |
Return true if this sort is a Relation sort. More... | |
bool | is_seq () const |
Return true if this sort is a Sequence sort. More... | |
bool | is_re () const |
Return true if this sort is a regular expression sort. More... | |
bool | is_finite_domain () const |
Return true if this sort is a Finite domain sort. More... | |
unsigned | bv_size () const |
Return the size of this Bit-vector sort. More... | |
sort | array_domain () const |
Return the domain of this Array sort. More... | |
sort | array_range () const |
Return the range of this Array sort. More... | |
![]() | |
ast (context &c) | |
ast (context &c, Z3_ast n) | |
ast (ast const &s) | |
~ast () | |
operator Z3_ast () const | |
operator bool () const | |
ast & | operator= (ast const &s) |
Z3_ast_kind | kind () const |
unsigned | hash () const |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | check_error () const |
Additional Inherited Members | |
![]() | |
Z3_ast | m_ast |
![]() | |
context * | m_ctx |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition at line 441 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
Definition at line 442 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
Definition at line 443 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
|
inline |
Return the domain of this Array sort.
Definition at line 514 of file z3++.h.
Referenced by z3::select(), and z3::store().
|
inline |
Return the range of this Array sort.
Definition at line 520 of file z3++.h.
Referenced by z3::store().
|
inline |
Return the size of this Bit-vector sort.
Definition at line 507 of file z3++.h.
|
inline |
Return true if this sort is the Integer or Real sort.
Definition at line 472 of file z3++.h.
|
inline |
Return true if this sort is a Array sort.
Definition at line 480 of file z3++.h.
|
inline |
Return true if this sort is the Boolean sort.
Definition at line 460 of file z3++.h.
|
inline |
Return true if this sort is a Bit-vector sort.
Definition at line 476 of file z3++.h.
|
inline |
Return true if this sort is a Datatype sort.
Definition at line 484 of file z3++.h.
|
inline |
Return true if this sort is a Finite domain sort.
Definition at line 500 of file z3++.h.
|
inline |
Return true if this sort is the Integer sort.
Definition at line 464 of file z3++.h.
|
inline |
Return true if this sort is a regular expression sort.
Definition at line 496 of file z3++.h.
|
inline |
Return true if this sort is the Real sort.
Definition at line 468 of file z3++.h.
|
inline |
Return true if this sort is a Relation sort.
Definition at line 488 of file z3++.h.
|
inline |
Return true if this sort is a Sequence sort.
Definition at line 492 of file z3++.h.
|
inline |