Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
sort Class Reference

A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...

+ Inheritance diagram for sort:

Public Member Functions

 sort (context &c)
 sort (context &c, Z3_sort s)
 sort (sort const &s)
 operator Z3_sort () const
sortoperator= (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.

Detailed Description

A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.

Definition at line 350 of file z3++.h.


Constructor & Destructor Documentation

sort ( context c) [inline]
sort ( context c,
Z3_sort  s 
) [inline]

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)) {}
sort ( sort const &  s) [inline]

Definition at line 354 of file z3++.h.

Referenced by ArrayRef::domain(), ArrayRef::range(), and ExprRef::sort_kind().

:ast(s) {}

Member Function Documentation

sort array_domain ( ) const [inline]

Return the domain of this Array sort.

Precondition:
is_array()

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.

Precondition:
is_array()

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.

Precondition:
is_bv()

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().

{ return is_int() || is_real(); }
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().

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]

Definition at line 355 of file z3++.h.

{ return reinterpret_cast<Z3_sort>(m_ast); }
sort& operator= ( sort const &  s) [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); }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines