RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3_1_1sort.html below:

Z3: sort Class Reference

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

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.

◆ sort() [1/3]

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

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]

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

660

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

Z3_error_code check_error() const

bool is_array() const

Return true if this sort is a Array sort.

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

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

bool is_bv() const

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

unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)

Return the size of the given bit-vector sort.

◆ constructors()

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

4196 for

(

unsigned

i = 0; i < n; ++i)

bool is_datatype() const

Return true if this sort is a Datatype sort.

unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)

Return number of constructors for datatype.

Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)

Return idx'th constructor.

ast_vector_tpl< func_decl > func_decl_vector

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.

bool is_fpa() const

Return true if this sort is a Floating point sort.

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

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()

retrieve unique identifier for func_decl.

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

unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)

Return a unique identifier for s.

◆ is_arith()

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

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

bool is_int() const

Return true if this sort is the Integer sort.

bool is_real() const

Return true if this sort is the Real sort.

Referenced by expr::is_arith().

◆ is_array() ◆ is_bool() ◆ is_bv() ◆ is_datatype() bool is_datatype ( ) const inline ◆ is_finite_domain() bool is_finite_domain ( ) const inline ◆ is_fpa() ◆ is_int() ◆ is_re()

Return true if this sort is a regular expression sort.

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

Referenced by expr::is_re().

◆ is_real() ◆ is_relation() bool is_relation ( ) const inline ◆ is_seq() ◆ name() ◆ operator Z3_sort() operator Z3_sort ( ) const inline ◆ recognizers()

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

4205 for

(

unsigned

i = 0; i < n; ++i)

Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)

Return idx'th recognizer.

◆ sort_kind()

Return the internal sort kind.

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

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

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

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

Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4