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

+ 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...
 
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 ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (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)
 
contextctx () 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
contextm_ctx
 

Detailed Description

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

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

Constructor & Destructor Documentation

◆ sort() [1/3]

sort ( context c)
inline

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

636 :ast(c) {}

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

◆ sort() [2/3]

sort ( context c,
Z3_sort  s 
)
inline

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

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

◆ sort() [3/3]

sort ( context c,
Z3_ast  a 
)
inline

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

638 :ast(c, a) {}

Member Function Documentation

◆ array_domain()

sort array_domain ( ) const
inline

Return the domain of this Array sort.

Precondition
is_array()

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

718 { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }

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 724 of file z3++.h.

724 { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }

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 708 of file z3++.h.

708 { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }

◆ constructors()

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

4002  {
4003  assert(is_datatype());
4004  func_decl_vector cs(ctx());
4005  unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
4006  for (unsigned i = 0; i < n; ++i)
4007  cs.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor(ctx(), *this, i)));
4008  return cs;
4009  }

◆ fpa_ebits()

unsigned fpa_ebits ( ) const
inline

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

710 { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }

◆ fpa_sbits()

unsigned fpa_sbits ( ) const
inline

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

712 { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

644 { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }

◆ is_arith()

bool is_arith ( ) const
inline

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

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

669 { return is_int() || is_real(); }

Referenced by expr::is_arith().

◆ is_array()

bool is_array ( ) const
inline

Return true if this sort is a Array sort.

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

677 { return sort_kind() == Z3_ARRAY_SORT; }

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 657 of file z3++.h.

657 { return sort_kind() == Z3_BOOL_SORT; }

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 673 of file z3++.h.

673 { return sort_kind() == Z3_BV_SORT; }

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 681 of file z3++.h.

681 { return sort_kind() == Z3_DATATYPE_SORT; }

Referenced by func_decl::accessors(), sort::constructors(), expr::is_datatype(), and sort::recognizers().

◆ is_finite_domain()

bool is_finite_domain ( ) const
inline

Return true if this sort is a Finite domain sort.

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

697 { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }

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 701 of file z3++.h.

701 { return sort_kind() == Z3_FLOATING_POINT_SORT; }

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 661 of file z3++.h.

661 { return sort_kind() == Z3_INT_SORT; }

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

◆ is_re()

bool is_re ( ) const
inline

Return true if this sort is a regular expression sort.

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

693 { return sort_kind() == Z3_RE_SORT; }

Referenced by expr::is_re().

◆ is_real()

bool is_real ( ) const
inline

Return true if this sort is the Real sort.

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

665 { return sort_kind() == Z3_REAL_SORT; }

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 685 of file z3++.h.

685 { return sort_kind() == Z3_RELATION_SORT; }

Referenced by expr::is_relation().

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this sort is a Sequence sort.

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

689 { return sort_kind() == Z3_SEQ_SORT; }

Referenced by expr::is_seq().

◆ name()

symbol name ( ) const
inline

Return name of sort.

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

653 { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }

◆ operator Z3_sort()

operator Z3_sort ( ) const
inline

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

639 { return reinterpret_cast<Z3_sort>(m_ast); }

◆ recognizers()

func_decl_vector recognizers ( )
inline

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

4011  {
4012  assert(is_datatype());
4013  func_decl_vector rs(ctx());
4014  unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
4015  for (unsigned i = 0; i < n; ++i)
4016  rs.push_back(func_decl(ctx(), Z3_get_datatype_sort_recognizer(ctx(), *this, i)));
4017  return rs;
4018  }

◆ sort_kind()

Z3_sort_kind sort_kind ( ) const
inline

Friends And Related Function Documentation

◆ operator<<

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

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

726 { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
Z3_FINITE_DOMAIN_SORT
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:117
Z3_sort_to_string
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
z3::sort::sort_kind
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:649
z3::sort::is_fpa
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:701
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.
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.
Z3_get_datatype_sort_recognizer
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
z3::sort::is_array
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:677
Z3_RE_SORT
@ Z3_RE_SORT
Definition: z3_api.h:121
Microsoft.Z3.Z3_sort
System.IntPtr Z3_sort
Definition: NativeContext.cs:33
Z3_get_sort_id
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
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.
z3::sort::is_bv
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:673
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).
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:448
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:530
Z3_FLOATING_POINT_SORT
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:118
z3::sort::is_datatype
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:681
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,...
z3::func_decl_vector
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:77
Z3_RELATION_SORT
@ Z3_RELATION_SORT
Definition: z3_api.h:116
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.
Z3_get_datatype_sort_num_constructors
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_DATATYPE_SORT
@ Z3_DATATYPE_SORT
Definition: z3_api.h:115
z3::sort::is_int
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:661
Z3_SEQ_SORT
@ Z3_SEQ_SORT
Definition: z3_api.h:120
Z3_get_datatype_sort_constructor
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
Z3_REAL_SORT
@ Z3_REAL_SORT
Definition: z3_api.h:112
Z3_BV_SORT
@ Z3_BV_SORT
Definition: z3_api.h:113
z3::sort::is_real
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:665
z3::ast::ast
ast(context &c)
Definition: z3++.h:532
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
Z3_BOOL_SORT
@ Z3_BOOL_SORT
Definition: z3_api.h:110
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:452
Z3_INT_SORT
@ Z3_INT_SORT
Definition: z3_api.h:111
Z3_ARRAY_SORT
@ Z3_ARRAY_SORT
Definition: z3_api.h:114
Microsoft.Z3.Z3_symbol
System.IntPtr Z3_symbol
Definition: NativeContext.cs:35
z3::object::ctx
context & ctx() const
Definition: z3++.h:451
z3::sort::sort
sort(context &c)
Definition: z3++.h:636
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.