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. | |
Z3_sort_kind | sort_kind () const |
Return the internal sort kind. | |
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_finite_domain () const |
Return true if this sort is a Finite domain sort. | |
unsigned | bv_size () const |
Return the size of this Bit-vector sort. | |
sort | array_domain () const |
Return the domain of this Array sort. | |
sort | array_range () const |
Return the range of this Array sort. |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition at line 352 of file z3++.h.
Referenced by sort::array_domain(), sort::array_range(), ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
:ast(c) {}
Definition at line 353 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
:ast(c, reinterpret_cast<Z3_ast>(s)) {}
Definition at line 354 of file z3++.h.
Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().
:ast(s) {}
sort array_domain | ( | ) | const [inline] |
Return the domain of this Array sort.
Definition at line 414 of file z3++.h.
Referenced by z3::select(), and z3::store().
{ assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
sort array_range | ( | ) | const [inline] |
Return the range of this Array sort.
Definition at line 420 of file z3++.h.
Referenced by z3::store().
{ assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
unsigned bv_size | ( | ) | const [inline] |
Return the size of this Bit-vector sort.
Definition at line 407 of file z3++.h.
{ assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
bool is_arith | ( | ) | const [inline] |
Return true if this sort is the Integer or Real sort.
Definition at line 380 of file z3++.h.
Referenced by expr::is_arith().
bool is_array | ( | ) | const [inline] |
Return true if this sort is a Array sort.
Definition at line 388 of file z3++.h.
Referenced by sort::array_domain(), sort::array_range(), and expr::is_array().
{ return sort_kind() == Z3_ARRAY_SORT; }
bool is_bool | ( | ) | const [inline] |
Return true if this sort is the Boolean sort.
Definition at line 368 of file z3++.h.
Referenced by expr::is_bool().
{ return sort_kind() == Z3_BOOL_SORT; }
bool is_bv | ( | ) | const [inline] |
Return true if this sort is a Bit-vector sort.
Definition at line 384 of file z3++.h.
Referenced by sort::bv_size(), and expr::is_bv().
{ return sort_kind() == Z3_BV_SORT; }
bool is_datatype | ( | ) | const [inline] |
Return true if this sort is a Datatype sort.
Definition at line 392 of file z3++.h.
Referenced by expr::is_datatype().
{ return sort_kind() == Z3_DATATYPE_SORT; }
bool is_finite_domain | ( | ) | const [inline] |
Return true if this sort is a Finite domain sort.
Definition at line 400 of file z3++.h.
Referenced by expr::is_finite_domain().
{ return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
bool is_int | ( | ) | const [inline] |
Return true if this sort is the Integer sort.
Definition at line 372 of file z3++.h.
Referenced by sort::is_arith(), and expr::is_int().
{ return sort_kind() == Z3_INT_SORT; }
bool is_real | ( | ) | const [inline] |
Return true if this sort is the Real sort.
Definition at line 376 of file z3++.h.
Referenced by sort::is_arith(), and expr::is_real().
{ return sort_kind() == Z3_REAL_SORT; }
bool is_relation | ( | ) | const [inline] |
Return true if this sort is a Relation sort.
Definition at line 396 of file z3++.h.
Referenced by expr::is_relation().
{ return sort_kind() == Z3_RELATION_SORT; }
operator Z3_sort | ( | ) | const [inline] |
Return true if this sort and s
are equal.
Definition at line 359 of file z3++.h.
{ return static_cast<sort&>(ast::operator=(s)); }
Z3_sort_kind sort_kind | ( | ) | const [inline] |
Return the internal sort kind.
Definition at line 363 of file z3++.h.
Referenced by sort::is_array(), sort::is_bool(), sort::is_bv(), sort::is_datatype(), sort::is_finite_domain(), sort::is_int(), sort::is_real(), and sort::is_relation().
{ return Z3_get_sort_kind(*m_ctx, *this); }