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... | |
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_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 357 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
Definition at line 358 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
Definition at line 359 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 419 of file z3++.h.
Referenced by z3::select(), and z3::store().
|
inline |
Return the range of this Array sort.
Definition at line 425 of file z3++.h.
Referenced by z3::store().
|
inline |
Return the size of this Bit-vector sort.
Definition at line 412 of file z3++.h.
|
inline |
Return true if this sort is the Integer or Real sort.
Definition at line 385 of file z3++.h.
|
inline |
Return true if this sort is a Array sort.
Definition at line 393 of file z3++.h.
|
inline |
Return true if this sort is the Boolean sort.
Definition at line 373 of file z3++.h.
|
inline |
Return true if this sort is a Bit-vector sort.
Definition at line 389 of file z3++.h.
|
inline |
Return true if this sort is a Datatype sort.
Definition at line 397 of file z3++.h.
|
inline |
Return true if this sort is a Finite domain sort.
Definition at line 405 of file z3++.h.
|
inline |
Return true if this sort is the Integer sort.
Definition at line 377 of file z3++.h.
|
inline |
Return true if this sort is the Real sort.
Definition at line 381 of file z3++.h.
|
inline |
Return true if this sort is a Relation sort.
Definition at line 401 of file z3++.h.
|
inline |