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

sort &	operator= (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...

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

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

ast &	operator= (ast const &s)

Z3_ast_kind	kind () const

unsigned	hash () const

Public Member Functions inherited from object
	object (context &c)

	object (object const &s)

context &	ctx () const

void	check_error () const

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

Constructor & Destructor Documentation

§ sort() [1/3]

sort ( context & c )

inline

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

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

441 :ast(c) {}

z3::ast::ast

ast(context &c)

Definition: z3++.h:413

§ sort() [2/3]

sort	(	context &	c,
		Z3_sort	s
	)

inline

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

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

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

z3::ast::ast

ast(context &c)

Definition: z3++.h:413

§ sort() [3/3]

sort ( sort const & s )

inline

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

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

443 :ast(s) {}

z3::ast::ast

ast(context &c)

Definition: z3++.h:413

Member Function Documentation

§ array_domain()

sort array_domain ( ) const

inline

Return the domain of this Array sort.

Precondition: is_array()

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

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

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:332

z3::sort::is_array

bool is_array() const

Return true if this sort is a Array sort.

Definition: z3++.h:480

z3::sort::sort

sort(context &c)

Definition: z3++.h:441

z3::object::check_error

void check_error() const

Definition: z3++.h:333

§ array_range()

sort array_range ( ) const

inline

Return the range of this Array sort.

Precondition: is_array()

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

Referenced by z3::store().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:332

z3::sort::is_array

bool is_array() const

Return true if this sort is a Array sort.

Definition: z3++.h:480

z3::sort::sort

sort(context &c)

Definition: z3++.h:441

z3::object::check_error

void check_error() const

Definition: z3++.h:333

§ bv_size()

unsigned bv_size ( ) const

inline

Return the size of this Bit-vector sort.

Precondition: is_bv()

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

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:332

z3::sort::is_bv

bool is_bv() const

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

Definition: z3++.h:476

z3::object::check_error

void check_error() const

Definition: z3++.h:333

§ is_arith()

bool is_arith ( ) const

inline

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

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

472 { 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:464

z3::sort::is_real

bool is_real() const

Return true if this sort is the Real sort.

Definition: z3++.h:468

§ is_array()

bool is_array ( ) const

inline

Return true if this sort is a Array sort.

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

480 { return sort_kind() == Z3_ARRAY_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_ARRAY_SORT

Definition: z3_api.h:160

§ is_bool()

bool is_bool ( ) const

inline

Return true if this sort is the Boolean sort.

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

460 { return sort_kind() == Z3_BOOL_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_BOOL_SORT

Definition: z3_api.h:156

§ is_bv()

bool is_bv ( ) const

inline

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

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

476 { return sort_kind() == Z3_BV_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_BV_SORT

Definition: z3_api.h:159

§ is_datatype()

bool is_datatype ( ) const

inline

Return true if this sort is a Datatype sort.

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

484 { return sort_kind() == Z3_DATATYPE_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_DATATYPE_SORT

Definition: z3_api.h:161

§ is_finite_domain()

bool is_finite_domain ( ) const

inline

Return true if this sort is a Finite domain sort.

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

500 { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_FINITE_DOMAIN_SORT

Definition: z3_api.h:163

§ is_int()

bool is_int ( ) const

inline

Return true if this sort is the Integer sort.

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

464 { return sort_kind() == Z3_INT_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_INT_SORT

Definition: z3_api.h:157

§ is_re()

bool is_re ( ) const

inline

Return true if this sort is a regular expression sort.

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

496 { return sort_kind() == Z3_RE_SORT; }

Z3_RE_SORT

Definition: z3_api.h:167

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

§ is_real()

bool is_real ( ) const

inline

Return true if this sort is the Real sort.

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

468 { return sort_kind() == Z3_REAL_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_REAL_SORT

Definition: z3_api.h:158

§ is_relation()

bool is_relation ( ) const

inline

Return true if this sort is a Relation sort.

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

488 { return sort_kind() == Z3_RELATION_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_RELATION_SORT

Definition: z3_api.h:162

§ is_seq()

bool is_seq ( ) const

inline

Return true if this sort is a Sequence sort.

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

492 { return sort_kind() == Z3_SEQ_SORT; }

z3::sort::sort_kind

Z3_sort_kind sort_kind() const

Return the internal sort kind.

Definition: z3++.h:452

Z3_SEQ_SORT

Definition: z3_api.h:166

§ name()

symbol name ( ) const

inline

Return name of sort.

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

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:332

z3::object::check_error

void check_error() const

Definition: z3++.h:333

§ operator Z3_sort()

operator Z3_sort ( ) const

inline

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

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

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:411

§ operator=()

sort& operator= ( sort const & s )

inline

Return true if this sort and s are equal.

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

448 { return static_cast<sort&>(ast::operator=(s)); }

z3::sort::sort

sort(context &c)

Definition: z3++.h:441

z3::ast::operator=

ast & operator=(ast const &s)

Definition: z3++.h:419

§ sort_kind()

Z3_sort_kind sort_kind ( ) const

inline

Return the internal sort kind.

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

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

z3::object::m_ctx

context * m_ctx

Definition: z3++.h:328

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

§ sort() [1/3]

§ sort() [2/3]

§ sort() [3/3]

Member Function Documentation

§ array_domain()

§ array_range()

§ bv_size()

§ is_arith()

§ is_array()

§ is_bool()

§ is_bv()

§ is_datatype()

§ is_finite_domain()

§ is_int()

§ is_re()

§ is_real()

§ is_relation()

§ is_seq()

§ name()

§ operator Z3_sort()

§ operator=()

§ sort_kind()