Z3
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. 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...
 
- Public Member Functions inherited from ast
 ast (context &c)
 
 ast (context &c, Z3_ast n)
 
 ast (ast const &s)
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Additional Inherited Members

- Protected Attributes inherited from ast
Z3_ast m_ast
 
- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

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

Constructor & Destructor Documentation

sort ( context c)
inline

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

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

357 :ast(c) {}
ast(context &c)
Definition: z3++.h:330
sort ( context c,
Z3_sort  s 
)
inline

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

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

358 :ast(c, reinterpret_cast<Z3_ast>(s)) {}
ast(context &c)
Definition: z3++.h:330
sort ( sort const &  s)
inline

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

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

359 :ast(s) {}
ast(context &c)
Definition: z3++.h:330

Member Function Documentation

sort array_domain ( ) const
inline

Return the domain of this Array sort.

Precondition
is_array()

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

Referenced by z3::select(), and z3::store().

419 { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort.
sort(context &c)
Definition: z3++.h:357
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:393
sort array_range ( ) const
inline

Return the range of this Array sort.

Precondition
is_array()

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

Referenced by z3::store().

425 { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
sort(context &c)
Definition: z3++.h:357
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:393
unsigned bv_size ( ) const
inline

Return the size of this Bit-vector sort.

Precondition
is_bv()

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

412 { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:389
context & ctx() const
Definition: z3++.h:277
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
void check_error() const
Definition: z3++.h:278
bool is_arith ( ) const
inline

Return true if this sort is the Integer or Real sort.

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

385 { return is_int() || is_real(); }
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:377
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:381
bool is_array ( ) const
inline

Return true if this sort is a Array sort.

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

393 { return sort_kind() == Z3_ARRAY_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_bool ( ) const
inline

Return true if this sort is the Boolean sort.

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

373 { return sort_kind() == Z3_BOOL_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_bv ( ) const
inline

Return true if this sort is a Bit-vector sort.

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

389 { return sort_kind() == Z3_BV_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_datatype ( ) const
inline

Return true if this sort is a Datatype sort.

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

397 { return sort_kind() == Z3_DATATYPE_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_finite_domain ( ) const
inline

Return true if this sort is a Finite domain sort.

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

405 { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_int ( ) const
inline

Return true if this sort is the Integer sort.

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

377 { return sort_kind() == Z3_INT_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_real ( ) const
inline

Return true if this sort is the Real sort.

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

381 { return sort_kind() == Z3_REAL_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_relation ( ) const
inline

Return true if this sort is a Relation sort.

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

401 { return sort_kind() == Z3_RELATION_SORT; }
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
operator Z3_sort ( ) const
inline

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

360 { return reinterpret_cast<Z3_sort>(m_ast); }
Z3_ast m_ast
Definition: z3++.h:328
sort& operator= ( sort const &  s)
inline

Return true if this sort and s are equal.

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

364 { return static_cast<sort&>(ast::operator=(s)); }
sort(context &c)
Definition: z3++.h:357
ast & operator=(ast const &s)
Definition: z3++.h:336
Z3_sort_kind sort_kind ( ) const
inline

Return the internal sort kind.

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

368 { return Z3_get_sort_kind(*m_ctx, *this); }
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
context * m_ctx
Definition: z3++.h:273