A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
#include <z3++.h>
Public Member Functions | |
sort (context &c) | |
sort (context &c, Z3_sort s) | |
sort (context &c, Z3_ast a) | |
operator Z3_sort () const | |
unsigned | id () const |
retrieve unique identifier for func_decl. | |
Z3_sort_kind | sort_kind () const |
Return the internal sort kind. | |
symbol | name () const |
Return name of sort. | |
bool | is_bool () const |
Return true if this sort is the Boolean sort. | |
bool | is_int () const |
Return true if this sort is the Integer sort. | |
bool | is_real () const |
Return true if this sort is the Real sort. | |
bool | is_arith () const |
Return true if this sort is the Integer or Real sort. | |
bool | is_bv () const |
Return true if this sort is a Bit-vector sort. | |
bool | is_array () const |
Return true if this sort is a Array sort. | |
bool | is_datatype () const |
Return true if this sort is a Datatype sort. | |
bool | is_relation () const |
Return true if this sort is a Relation sort. | |
bool | is_seq () const |
Return true if this sort is a Sequence sort. | |
bool | is_re () const |
Return true if this sort is a regular expression sort. | |
bool | is_finite_domain () const |
Return true if this sort is a Finite domain sort. | |
bool | is_fpa () const |
Return true if this sort is a Floating point sort. | |
unsigned | bv_size () const |
Return the size of this Bit-vector sort. | |
unsigned | fpa_ebits () const |
unsigned | fpa_sbits () const |
sort | array_domain () const |
Return the domain of this Array sort. | |
sort | array_range () const |
Return the range of this Array sort. | |
func_decl_vector | constructors () |
func_decl_vector | recognizers () |
Public Member Functions inherited from ast | |
ast (context &c) | |
ast (context &c, Z3_ast n) | |
ast (ast const &s) | |
~ast () override | |
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 |
Public Member Functions inherited from object | |
object (context &c) | |
virtual | ~object ()=default |
context & | ctx () const |
Z3_error_code | check_error () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, sort const &s) |
Additional Inherited Members | |
Protected Attributes inherited from ast | |
Z3_ast | m_ast |
Protected Attributes inherited from object | |
context * | m_ctx |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition at line 659 of file z3++.h.
Referenced by array_domain(), array_range(), and operator<<.
|
inline |
Return the domain of this Array sort.
Definition at line 741 of file z3++.h.
Referenced by z3::select(), z3::store(), and z3::store().
|
inline |
Return the range of this Array sort.
Definition at line 747 of file z3++.h.
Referenced by z3::store(), and z3::store().
|
inline |
|
inline |
Definition at line 4192 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
Return true if this sort is the Integer or Real sort.
Definition at line 692 of file z3++.h.
Referenced by expr::is_arith().
|
inline |
Return true if this sort is a Array sort.
Definition at line 700 of file z3++.h.
Referenced by array_domain(), array_range(), and expr::is_array().
|
inline |
Return true if this sort is the Boolean sort.
Definition at line 680 of file z3++.h.
Referenced by expr::is_bool().
|
inline |
Return true if this sort is a Bit-vector sort.
Definition at line 696 of file z3++.h.
Referenced by bv_size(), and expr::is_bv().
|
inline |
Return true if this sort is a Datatype sort.
Definition at line 704 of file z3++.h.
Referenced by func_decl::accessors(), constructors(), expr::is_datatype(), and recognizers().
|
inline |
Return true if this sort is a Finite domain sort.
Definition at line 720 of file z3++.h.
Referenced by expr::is_finite_domain().
|
inline |
Return true if this sort is a Floating point sort.
Definition at line 724 of file z3++.h.
Referenced by fpa_ebits(), fpa_sbits(), and expr::is_fpa().
|
inline |
Return true if this sort is the Integer sort.
Definition at line 684 of file z3++.h.
Referenced by is_arith(), and expr::is_int().
|
inline |
Return true if this sort is a regular expression sort.
Definition at line 716 of file z3++.h.
Referenced by expr::is_re().
|
inline |
Return true if this sort is the Real sort.
Definition at line 688 of file z3++.h.
Referenced by is_arith(), and expr::is_real().
|
inline |
Return true if this sort is a Relation sort.
Definition at line 708 of file z3++.h.
Referenced by expr::is_relation().
|
inline |
Return true if this sort is a Sequence sort.
Definition at line 712 of file z3++.h.
Referenced by expr::is_seq().
|
inline |
|
inline |
|
inline |
Definition at line 4201 of file z3++.h.
|
inline |
Return the internal sort kind.
Definition at line 672 of file z3++.h.
Referenced by is_array(), is_bool(), is_bv(), is_datatype(), is_finite_domain(), is_fpa(), is_int(), is_re(), is_real(), is_relation(), and is_seq().