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 () override
	operator Z3_ast () const
	operator bool () const
ast &	operator= (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)
virtual	~object ()=default
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 657 of file z3++.h.

Constructor & Destructor Documentation

sort() [1/3]

sort ( context &  c )

inline

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

:ast(c) {}

Referenced by sort::array_domain(), sort::array_range(), FPNumRef::as_string(), ArrayRef::domain(), ArrayRef::domain_n(), 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 660 of file z3++.h.

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

Referenced by FPNumRef::as_string(), ArrayRef::domain(), ArrayRef::domain_n(), 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 661 of file z3++.h.

:ast(c, a) {}

Referenced by FPNumRef::as_string(), ArrayRef::domain(), ArrayRef::domain_n(), 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 741 of file z3++.h.

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

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

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

constructors()

func_decl_vector constructors ( )

inline

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

                                               {
        assert(is_datatype()); 
        func_decl_vector cs(ctx());
        unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
        for (unsigned i = 0; i < n; ++i) 
            cs.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor(ctx(), *this, i)));
        return cs;
    }

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

fpa_ebits()

unsigned fpa_ebits ( ) const

inline

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

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

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

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

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

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

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

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

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

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

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

{ return sort_kind() == Z3_INT_SORT; }

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

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

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

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

{ return sort_kind() == Z3_SEQ_SORT; }

Referenced by expr::is_seq().

name()

symbol name ( ) const

inline

Return name of sort.

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

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

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

operator Z3_sort()

operator Z3_sort ( ) const

inline

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

{ return reinterpret_cast<Z3_sort>(m_ast); }

recognizers()

func_decl_vector recognizers ( )

inline

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

                                              {
        assert(is_datatype()); 
        func_decl_vector rs(ctx());
        unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
        for (unsigned i = 0; i < n; ++i) 
            rs.push_back(func_decl(ctx(), Z3_get_datatype_sort_recognizer(ctx(), *this, i)));
        return rs;
    }

sort_kind()

Z3_sort_kind sort_kind ( ) const

inline

Return the internal sort kind.

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

{ return Z3_get_sort_kind(*m_ctx, *this); }

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

{ return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }