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 |
std::string | to_string () const |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
Z3_error_code | 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.
|
inline |
Return the domain of this Array sort.
Definition at line 548 of file z3++.h.
Referenced by z3::select(), and z3::store().
|
inline |
Return the range of this Array sort.
Definition at line 554 of file z3++.h.
Referenced by z3::store().
|
inline |
Return the size of this Bit-vector sort.
Definition at line 541 of file z3++.h.
|
inline |
Return true if this sort is the Integer or Real sort.
Definition at line 506 of file z3++.h.
|
inline |
Return true if this sort is a Array sort.
Definition at line 514 of file z3++.h.
|
inline |
Return true if this sort is the Boolean sort.
Definition at line 494 of file z3++.h.
|
inline |
Return true if this sort is a Bit-vector sort.
Definition at line 510 of file z3++.h.
|
inline |
Return true if this sort is a Datatype sort.
Definition at line 518 of file z3++.h.
|
inline |
Return true if this sort is a Finite domain sort.
Definition at line 534 of file z3++.h.
|
inline |
Return true if this sort is the Integer sort.
Definition at line 498 of file z3++.h.
|
inline |
Return true if this sort is a regular expression sort.
Definition at line 530 of file z3++.h.
|
inline |
Return true if this sort is the Real sort.
Definition at line 502 of file z3++.h.
|
inline |
Return true if this sort is a Relation sort.
Definition at line 522 of file z3++.h.
|
inline |
Return true if this sort is a Sequence sort.
Definition at line 526 of file z3++.h.
|
inline |
|
inline |