Z3 |

Public Member Functions | Friends
sort Class Reference

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

`#include <z3++.h>`

Inheritance diagram for sort:

## 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. 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...
bool | is_fpa () const
| Return true if this sort is a Floating point sort. More...
unsigned | bv_size () const
| Return the size of this Bit-vector sort. More...
unsigned | fpa_ebits () const
unsigned | fpa_sbits () const
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 (ast &&s) noexcept
| ~ast ()
| operator Z3_ast () const
| operator bool () const
ast & | operator= (ast const &s)
ast & | operator= (ast &&s) noexcept
Z3_ast_kind | kind () const
unsigned | hash () const
std::string | to_string () const
Public Member Functions inherited from object
| object (context &c)
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

## Detailed Description

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

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

## Constructor & Destructor Documentation

## ◆ sort() [1/3]

sort | ( | context & | c | ) |
| inline

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

614:ast(c) {}
z3::ast::ast
ast(context &c)
Definition: z3++.h:502

Referenced by QuantifierRef::__getitem__(), sort::array_domain(), sort::array_range(), FPNumRef::as_string(), ArrayRef::domain(), FPRef::ebits(), ArithRef::is_int(), ArithRef::is_real(), ArrayRef::range(), FPRef::sbits(), BitVecRef::size(), and ExprRef::sort_kind().

## ◆ sort() [2/3]

sort | ( | context & | c,
|  | Z3_sort | s
| ) |  |
| inline

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

615:ast(c, reinterpret_cast<Z3_ast>(s)) {}

Referenced by QuantifierRef::__getitem__(), FPNumRef::as_string(), ArrayRef::domain(), FPRef::ebits(), ArithRef::is_int(), ArithRef::is_real(), ArrayRef::range(), FPRef::sbits(), BitVecRef::size(), and ExprRef::sort_kind().

## ◆ sort() [3/3]

sort | ( | context & | c,
|  | Z3_ast | a
| ) |  |
| inline

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

616:ast(c, a) {}

Referenced by QuantifierRef::__getitem__(), FPNumRef::as_string(), ArrayRef::domain(), FPRef::ebits(), ArithRef::is_int(), ArithRef::is_real(), ArrayRef::range(), FPRef::sbits(), BitVecRef::size(), and ExprRef::sort_kind().

## Member Function Documentation

## ◆ array_domain()

sort array_domain | ( |  | ) | const
| inline

Return the domain of this Array sort.

Precondition
  is_array()

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

696{ assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
z3::sort::sort
sort(context &c)
Definition: z3++.h:614
z3::sort::is_array
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:655
Z3_get_array_sort_domain
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array,...

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

## ◆ array_range()

sort array_range | ( |  | ) | const
| inline

Return the range of this Array sort.

Precondition
  is_array()

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

702{ assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
Z3_get_array_sort_range
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.

Referenced by z3::store().

## ◆ bv_size()

unsigned bv_size | ( |  | ) | const
| inline

Return the size of this Bit-vector sort.

Precondition
  is_bv()

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

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

## ◆ fpa_ebits()

unsigned fpa_ebits | ( |  | ) | const
| inline

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

688{ assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
z3::sort::is_fpa
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:679
Z3_fpa_get_ebits
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

## ◆ fpa_sbits()

unsigned fpa_sbits | ( |  | ) | const
| inline

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

690{ assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
Z3_fpa_get_sbits
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.

## ◆ id()

unsigned id | ( |  | ) | const
| inline

retrieve unique identifier for func_decl.

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

622{ unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
Z3_get_sort_id
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.

## ◆ is_arith()

bool is_arith | ( |  | ) | const
| inline

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

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

647{ return is_int() || is_real(); }
z3::sort::is_int
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:639
z3::sort::is_real
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:643

Referenced by expr::is_arith().

## ◆ is_array()

bool is_array | ( |  | ) | const
| inline

Return true if this sort is a Array sort.

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

655{ return sort_kind() == Z3_ARRAY_SORT; }
z3::sort::sort_kind
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:627
Z3_ARRAY_SORT
@ Z3_ARRAY_SORT
Definition: z3_api.h:156

Referenced by sort::array_domain(), sort::array_range(), and expr::is_array().

## ◆ is_bool()

bool is_bool | ( |  | ) | const
| inline

Return true if this sort is the Boolean sort.

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

635{ return sort_kind() == Z3_BOOL_SORT; }
Z3_BOOL_SORT
@ Z3_BOOL_SORT
Definition: z3_api.h:152

Referenced by expr::is_bool().

## ◆ is_bv()

bool is_bv | ( |  | ) | const
| inline

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

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

651{ return sort_kind() == Z3_BV_SORT; }
Z3_BV_SORT
@ Z3_BV_SORT
Definition: z3_api.h:155

Referenced by sort::bv_size(), and expr::is_bv().

## ◆ is_datatype()

bool is_datatype | ( |  | ) | const
| inline

Return true if this sort is a Datatype sort.

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

659{ return sort_kind() == Z3_DATATYPE_SORT; }
Z3_DATATYPE_SORT
@ Z3_DATATYPE_SORT
Definition: z3_api.h:157

Referenced by expr::is_datatype().

## ◆ is_finite_domain()

bool is_finite_domain | ( |  | ) | const
| inline

Return true if this sort is a Finite domain sort.

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

675{ return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
Z3_FINITE_DOMAIN_SORT
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:159

Referenced by expr::is_finite_domain().

## ◆ is_fpa()

bool is_fpa | ( |  | ) | const
| inline

Return true if this sort is a Floating point sort.

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

679{ return sort_kind() == Z3_FLOATING_POINT_SORT; }
Z3_FLOATING_POINT_SORT
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:160

Referenced by sort::fpa_ebits(), sort::fpa_sbits(), and expr::is_fpa().

## ◆ is_int()

bool is_int | ( |  | ) | const
| inline

Return true if this sort is the Integer sort.

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

639{ return sort_kind() == Z3_INT_SORT; }
Z3_INT_SORT
@ Z3_INT_SORT
Definition: z3_api.h:153

Referenced by IntNumRef::as_long(), sort::is_arith(), expr::is_int(), and ArithSortRef::subsort().

## ◆ is_re()

bool is_re | ( |  | ) | const
| inline

Return true if this sort is a regular expression sort.

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

671{ return sort_kind() == Z3_RE_SORT; }
Z3_RE_SORT
@ Z3_RE_SORT
Definition: z3_api.h:163

Referenced by expr::is_re().

## ◆ is_real()

bool is_real | ( |  | ) | const
| inline

Return true if this sort is the Real sort.

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

643{ return sort_kind() == Z3_REAL_SORT; }
Z3_REAL_SORT
@ Z3_REAL_SORT
Definition: z3_api.h:154

Referenced by sort::is_arith(), and expr::is_real().

## ◆ is_relation()

bool is_relation | ( |  | ) | const
| inline

Return true if this sort is a Relation sort.

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

663{ return sort_kind() == Z3_RELATION_SORT; }
Z3_RELATION_SORT
@ Z3_RELATION_SORT
Definition: z3_api.h:158

Referenced by expr::is_relation().

## ◆ is_seq()

bool is_seq | ( |  | ) | const
| inline

Return true if this sort is a Sequence sort.

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

667{ return sort_kind() == Z3_SEQ_SORT; }
Z3_SEQ_SORT
@ Z3_SEQ_SORT
Definition: z3_api.h:162

Referenced by expr::is_seq().

## ◆ name()

symbol name | ( |  | ) | const
| inline

Return name of sort.

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

631{ Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
Z3_get_sort_name
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.

Referenced by Datatype::__deepcopy__(), and Datatype::__repr__().

## ◆ operator Z3_sort()

operator Z3_sort | ( |  | ) | const
| inline

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

617{ return reinterpret_cast<Z3_sort>(m_ast); }
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:500

## ◆ sort_kind()

Z3_sort_kind sort_kind | ( |  | ) | const
| inline

Return the internal sort kind.

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

627{ return Z3_get_sort_kind(*m_ctx, *this); }
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:419
Z3_get_sort_kind
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).

Referenced by sort::is_array(), sort::is_bool(), sort::is_bv(), sort::is_datatype(), sort::is_finite_domain(), sort::is_fpa(), sort::is_int(), sort::is_re(), sort::is_real(), sort::is_relation(), and sort::is_seq().

## Friends And Related Function Documentation

## ◆ operator<<

std::ostream & operator<< | ( | std::ostream & | out,
|  | sort const & | s
| ) |  |
| friend

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

704{ return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
Z3_sort_to_string
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)