RetroSearch Browse

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

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

Z3: context Class Reference

A Context manages all other Z3 objects, global configuration options, etc. More...

context () context (config &c) ~context () operator Z3_context () const Z3_error_code check_error () const Auxiliary method used to check for API usage errors. More...
void check_parser_error () const void set_enable_exceptions (bool f) The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications have to be very careful about using check_error() after calls that may result in an erroneous state. More...
bool enable_exceptions () const void set (char const *param, char const *value) Update global parameter param with string value. More...
void set (char const *param, bool value) Update global parameter param with Boolean value. More...
void set (char const *param, int value) Update global parameter param with Integer value. More...
void interrupt () Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop. More...
symbol str_symbol (char const *s) Create a Z3 symbol based on the given string. More...
symbol int_symbol (int n) Create a Z3 symbol based on the given integer. More...
sort bool_sort () Return the Boolean sort. More...
sort int_sort () Return the integer sort. More...
sort real_sort () Return the Real sort. More...
sort bv_sort (unsigned sz) Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz. More...
sort char_sort () Return the sort for Unicode characters. More...
sort string_sort () Return the sort for Unicode strings. More...
sort seq_sort (sort &s) Return a sequence sort over base sort s. More...
sort re_sort (sort &seq_sort) Return a regular expression sort over sequences seq_sort. More...
sort array_sort (sort d, sort r) Return an array sort for arrays from d to r. More...
sort array_sort (sort_vector const &d, sort r) sort fpa_sort (unsigned ebits, unsigned sbits) Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,. More...
template<size_t precision> sort fpa_sort () Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128). More...
sort fpa_rounding_mode_sort () Return a RoundingMode sort. More...
void set_rounding_mode (rounding_mode rm) Sets RoundingMode of FloatingPoints. More...
sort enumeration_sort (char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts) Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters. The method stores in cs the constants corresponding to the enumerated elements, and in ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. More...
func_decl tuple_sort (char const *name, unsigned n, char const *const *names, sort const *sorts, func_decl_vector &projs) Return a tuple constructor. name is the name of the returned constructor, n are the number of arguments, names and sorts are their projected sorts. projs is an output parameter. It contains the set of projection functions. More...
sort datatype (symbol const &name, constructors const &cs) Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the number of constructors of the datatype cs - the n constructors used to define the datatype. More...
sort_vector datatypes (unsigned n, symbol const *names, constructor_list *const *cons) Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of names of length n cons - array of constructor lists of length n. More...
sort datatype_sort (symbol const &name) a reference to a recursively defined datatype. Expect that it gets defined as a datatype. More...
sort uninterpreted_sort (char const *name) create an uninterpreted sort with the name given by the string or symbol. More...
sort uninterpreted_sort (symbol const &name) func_decl function (symbol const &name, unsigned arity, sort const *domain, sort const &range) func_decl function (char const *name, unsigned arity, sort const *domain, sort const &range) func_decl function (symbol const &name, sort_vector const &domain, sort const &range) func_decl function (char const *name, sort_vector const &domain, sort const &range) func_decl function (char const *name, sort const &domain, sort const &range) func_decl function (char const *name, sort const &d1, sort const &d2, sort const &range) func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range) func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range) func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range) func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range) func_decl recfun (symbol const &name, const sort_vector &domain, sort const &range) func_decl recfun (char const *name, sort_vector const &domain, sort const &range) func_decl recfun (char const *name, unsigned arity, sort const *domain, sort const &range) func_decl recfun (char const *name, sort const &domain, sort const &range) func_decl recfun (char const *name, sort const &d1, sort const &d2, sort const &range) void recdef (func_decl decl, expr_vector const &args, expr const &body) add function definition body to declaration decl. decl needs to be declared using context::recfun. More...
func_decl user_propagate_function (symbol const &name, sort_vector const &domain, sort const &range) expr constant (symbol const &name, sort const &s) create an uninterpreted constant. More...
expr constant (char const *name, sort const &s) expr bool_const (char const *name) create uninterpreted constants of a given sort. More...
expr int_const (char const *name) expr real_const (char const *name) expr string_const (char const *name) expr bv_const (char const *name, unsigned sz) expr fpa_const (char const *name, unsigned ebits, unsigned sbits) template<size_t precision> expr fpa_const (char const *name) expr variable (unsigned index, sort const &s) create a de-Bruijn variable. More...
expr fpa_rounding_mode () expr bool_val (bool b) expr int_val (int n) expr int_val (unsigned n) expr int_val (int64_t n) expr int_val (uint64_t n) expr int_val (char const *n) expr real_val (int n) expr real_val (unsigned n) expr real_val (int64_t n) expr real_val (uint64_t n) expr real_val (int64_t n, int64_t d) expr real_val (char const *n) expr bv_val (int n, unsigned sz) expr bv_val (unsigned n, unsigned sz) expr bv_val (int64_t n, unsigned sz) expr bv_val (uint64_t n, unsigned sz) expr bv_val (char const *n, unsigned sz) expr bv_val (unsigned n, bool const *bits) expr fpa_val (double n) expr fpa_val (float n) expr fpa_nan (sort const &s) expr fpa_inf (sort const &s, bool sgn) expr string_val (char const *s) expr string_val (char const *s, unsigned n) expr string_val (std::string const &s) expr string_val (std::u32string const &s) expr num_val (int n, sort const &s) expr_vector parse_string (char const *s) parsing More...
expr_vector parse_file (char const *file) expr_vector parse_string (char const *s, sort_vector const &sorts, func_decl_vector const &decls) expr_vector parse_file (char const *s, sort_vector const &sorts, func_decl_vector const &decls) template<> sort fpa_sort () template<> sort fpa_sort () template<> sort fpa_sort () template<> sort fpa_sort ()

A Context manages all other Z3 objects, global configuration options, etc.

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

◆ context() [1/2]

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

184

{ config c; init(c); }

◆ context() [2/2] ◆ ~context()

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

void Z3_API Z3_del_context(Z3_context c)

Delete the given logical context.

◆ array_sort() [1/2]

Return an array sort for arrays from d to r.

Example: Given a context c, c.array_sort(c.int_sort(), c.bool_sort()) is an array sort from integer to Boolean.

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

Z3_error_code check_error() const

Auxiliary method used to check for API usage errors.

Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)

Create an array type.

◆ array_sort() [2/2]

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

3507

array<Z3_sort> dom(d);

Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)

Create an array type with N arguments.

◆ bool_const() expr bool_const ( char const * name ) inline

create uninterpreted constants of a given sort.

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

sort bool_sort()

Return the Boolean sort.

expr constant(symbol const &name, sort const &s)

create an uninterpreted constant.

◆ bool_sort()

Return the Boolean sort.

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

Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)

Create the Boolean type.

Referenced by context::bool_const().

◆ bool_val() ◆ bv_const() expr bv_const ( char const * name, unsigned sz ) inline

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

sort bv_sort(unsigned sz)

Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.

◆ bv_sort() sort bv_sort ( unsigned sz ) inline

Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.

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

Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)

Create a bit-vector type of the given size.

Referenced by context::bv_const(), and context::bv_val().

◆ bv_val() [1/6] expr bv_val ( char const * n, unsigned sz ) inline

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

Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)

Create a numeral of a given sort.

◆ bv_val() [2/6] expr bv_val ( int n, unsigned sz ) inline

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

Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)

Create a numeral of an int, bit-vector, or finite-domain sort.

◆ bv_val() [3/6] expr bv_val ( int64_t n, unsigned sz ) inline

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

Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)

Create a numeral of a int, bit-vector, or finite-domain sort.

◆ bv_val() [4/6] expr bv_val ( uint64_t n, unsigned sz ) inline

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

Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)

Create a numeral of a int, bit-vector, or finite-domain sort.

◆ bv_val() [5/6] expr bv_val ( unsigned n, bool const * bits ) inline

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

3812

array<bool> _bits(n);

3813 for

(

unsigned

i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;

Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)

create a bit-vector numeral from a vector of Booleans.

◆ bv_val() [6/6] expr bv_val ( unsigned n, unsigned sz ) inline

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

Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)

Create a numeral of a int, bit-vector, or finite-domain sort.

◆ char_sort()

Return the sort for Unicode characters.

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

Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)

Create a sort for unicode characters.

◆ check_error()

Auxiliary method used to check for API usage errors.

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

bool enable_exceptions() const

Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)

Return a string describing the given error code.

Z3_error_code

Z3 error codes (See Z3_get_error_code).

Z3_error_code Z3_API Z3_get_error_code(Z3_context c)

Return the error code for the last API call.

Referenced by context::array_sort(), expr::bit2bool(), context::bool_sort(), context::bv_sort(), context::bv_val(), context::char_sort(), object::check_error(), context::check_parser_error(), context::constant(), context::datatype(), context::datatype_sort(), context::enumeration_sort(), expr::extract(), z3::foldl(), z3::foldli(), context::fpa_inf(), context::fpa_nan(), context::fpa_rounding_mode_sort(), context::fpa_sort(), context::fpa_val(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), z3::map(), z3::mapi(), context::num_val(), on_clause::on_clause(), func_decl::operator()(), context::parse_file(), context::parse_string(), z3::re_diff(), z3::re_intersect(), context::re_sort(), context::real_sort(), context::real_val(), context::recfun(), expr::repeat(), expr::rotate_left(), expr::rotate_right(), context::seq_sort(), context::str_symbol(), context::string_sort(), context::string_val(), z3::to_expr(), z3::to_func_decl(), z3::to_sort(), context::tuple_sort(), context::user_propagate_function(), and context::variable().

◆ check_parser_error() void check_parser_error ( ) const inline ◆ constant() [1/2] expr constant ( char const * name, sort const & s ) inline

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

symbol str_symbol(char const *s)

Create a Z3 symbol based on the given string.

◆ constant() [2/2] ◆ datatype()

Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the number of constructors of the datatype cs - the n constructors used to define the datatype.

References to the datatype can be created using datatype_sort.

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

3596

array<Z3_constructor> _cs(cs.size());

3597 for

(

unsigned

i = 0; i < cs.size(); ++i) _cs[i] = cs[i];

3600 return

sort(*

this

, s);

Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])

Create datatype, such as lists, trees, records, enumerations or unions of records....

◆ datatype_sort()

a reference to a recursively defined datatype. Expect that it gets defined as a datatype.

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

3622 return

sort(*

this

, s);

Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)

create a forward reference to a recursive datatype being declared. The forward reference can be used ...

◆ datatypes()

Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of names of length n cons - array of constructor lists of length n.

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

3607

array<Z3_symbol> _names(n);

3608

array<Z3_sort> _sorts(n);

3609

array<Z3_constructor_list> _cons(n);

3610 for

(

unsigned

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

3611

_names[i] = names[i], _cons[i] = *cons[i];

3612 Z3_mk_datatypes

this

, n, _names.ptr(), _sorts.ptr(), _cons.ptr());

3613 for

(

unsigned

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

3614

result.push_back(sort(*

this

, _sorts[i]));

void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])

Create mutually recursive datatypes.

ast_vector_tpl< sort > sort_vector

◆ enable_exceptions() bool enable_exceptions ( ) const inline ◆ enumeration_sort()

Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters. The method stores in cs the constants corresponding to the enumerated elements, and in ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.

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

3511

array<Z3_symbol> _enum_names(n);

3512 for

(

unsigned

i = 0; i < n; i++) { _enum_names[i] =

Z3_mk_string_symbol

this

, enum_names[i]); }

3513

array<Z3_func_decl> _cs(n);

3514

array<Z3_func_decl> _ts(n);

3518 for

(

unsigned

i = 0; i < n; i++) { cs.push_back(func_decl(*

this

, _cs[i])); ts.push_back(func_decl(*

this

, _ts[i])); }

Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])

Create a enumeration sort.

Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)

Create a Z3 symbol using a C string.

sort to_sort(context &c, Z3_sort s)

◆ fpa_const() [1/2] expr fpa_const ( char const * name ) inline

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

3776

{

return constant

(name, fpa_sort<precision>()); }

◆ fpa_const() [2/2] expr fpa_const ( char const * name, unsigned ebits, unsigned sbits ) inline

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

sort fpa_sort()

Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

◆ fpa_inf() expr fpa_inf ( sort const & s, bool sgn ) inline

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

Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)

Create a floating-point infinity of sort s.

◆ fpa_nan()

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

Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)

Create a floating-point NaN of sort s.

◆ fpa_rounding_mode() expr fpa_rounding_mode ( ) inline

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

3781 switch

(m_rounding_mode) {

3787 default

return

expr(*

this

);

Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

◆ fpa_rounding_mode_sort() sort fpa_rounding_mode_sort ( ) inline

Return a RoundingMode sort.

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

Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)

Create the RoundingMode sort.

◆ fpa_sort() [1/6]

Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

Referenced by context::fpa_const().

◆ fpa_sort() [2/6] ◆ fpa_sort() [3/6] ◆ fpa_sort() [4/6] ◆ fpa_sort() [5/6] ◆ fpa_sort() [6/6] sort fpa_sort ( unsigned ebits, unsigned sbits ) inline

Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,.

Precondition: where ebits must be larger than 1 and sbits must be larger than 2.

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

Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)

Create a FloatingPoint sort.

◆ fpa_val() [1/2] expr fpa_val ( double n ) inline

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

Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)

Create a numeral of FloatingPoint sort from a double.

Referenced by z3::operator!=(), and z3::operator==().

◆ fpa_val() [2/2]

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

Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty)

Create a numeral of FloatingPoint sort from a float.

◆ function() [1/9]

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

3699 Z3_sort

args[5] = { d1, d2, d3, d4, d5 };

3702 return

func_decl(*

this

, f);

Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a constant or function.

System.IntPtr Z3_func_decl

void check_context(object const &a, object const &b)

expr range(expr const &lo, expr const &hi)

◆ function() [2/9]

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

3691 Z3_sort

args[4] = { d1, d2, d3, d4 };

3694 return

func_decl(*

this

, f);

◆ function() [3/9]

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

3683 Z3_sort

args[3] = { d1, d2, d3 };

3686 return

func_decl(*

this

, f);

◆ function() [4/9]

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

3678 return

func_decl(*

this

, f);

◆ function() [5/9]

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

3670 return

func_decl(*

this

, f);

◆ function() [6/9] ◆ function() [7/9] func_decl function ( char const * name, unsigned arity, sort const * domain, sort const & range ) inline ◆ function() [8/9]

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

3650

array<Z3_sort> args(domain.size());

3651 for

(

unsigned

i = 0; i < domain.size(); i++) {

3653

args[i] = domain[i];

3657 return

func_decl(*

this

, f);

◆ function() [9/9]

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

3635

array<Z3_sort> args(arity);

3636 for

(

unsigned

i = 0; i < arity; i++) {

3638

args[i] = domain[i];

3642 return

func_decl(*

this

, f);

Referenced by z3::function().

◆ int_const() expr int_const ( char const * name ) inline

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

sort int_sort()

Return the integer sort.

◆ int_sort() ◆ int_symbol()

Create a Z3 symbol based on the given integer.

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

Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)

Create a Z3 symbol using an integer.

◆ int_val() [1/5] expr int_val ( char const * n ) inline ◆ int_val() [2/5] ◆ int_val() [3/5] expr int_val ( int64_t n ) inline ◆ int_val() [4/5] expr int_val ( uint64_t n ) inline ◆ int_val() [5/5] expr int_val ( unsigned n ) inline ◆ interrupt()

Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop.

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

void Z3_API Z3_interrupt(Z3_context c)

Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...

◆ num_val()

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

Referenced by z3::ashr(), z3::lshr(), func_decl::operator()(), z3::select(), z3::sge(), z3::sgt(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

◆ operator Z3_context() operator Z3_context ( ) const inline ◆ parse_file() [1/2]

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

Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])

Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.

System.IntPtr Z3_ast_vector

ast_vector_tpl< expr > expr_vector

◆ parse_file() [2/2]

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

4177

array<Z3_symbol> sort_names(sorts.size());

4178

array<Z3_symbol> decl_names(decls.size());

4179

array<Z3_sort> sorts1(sorts);

4180

array<Z3_func_decl> decls1(decls);

4181 for

(

unsigned

i = 0; i < sorts.size(); ++i) {

4182

sort_names[i] = sorts[i].name();

4184 for

(

unsigned

i = 0; i < decls.size(); ++i) {

4185

decl_names[i] = decls[i].name();

◆ parse_string() [1/2]

parsing

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

Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])

Parse the given string using the SMT-LIB2 parser.

◆ parse_string() [2/2]

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

4160

array<Z3_symbol> sort_names(sorts.size());

4161

array<Z3_symbol> decl_names(decls.size());

4162

array<Z3_sort> sorts1(sorts);

4163

array<Z3_func_decl> decls1(decls);

4164 for

(

unsigned

i = 0; i < sorts.size(); ++i) {

4165

sort_names[i] = sorts[i].name();

4167 for

(

unsigned

i = 0; i < decls.size(); ++i) {

4168

decl_names[i] = decls[i].name();

◆ re_sort()

Return a regular expression sort over sequences seq_sort.

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

Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)

Create a regular expression sort out of a sequence sort.

◆ real_const() expr real_const ( char const * name ) inline

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

sort real_sort()

Return the Real sort.

◆ real_sort() ◆ real_val() [1/6] expr real_val ( char const * n ) inline ◆ real_val() [2/6] ◆ real_val() [3/6] expr real_val ( int64_t n ) inline ◆ real_val() [4/6] expr real_val ( int64_t n, int64_t d ) inline

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

Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)

Create a real from a fraction of int64.

◆ real_val() [5/6] expr real_val ( uint64_t n ) inline ◆ real_val() [6/6] expr real_val ( unsigned n ) inline ◆ recdef()

add function definition body to declaration decl. decl needs to be declared using context::recfun.

Parameters

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

3745

array<Z3_ast> vars(args);

void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)

Define the body of a recursive function.

◆ recfun() [1/6]

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

3739

sort dom[2] = { d1, d2 };

func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)

◆ recfun() [2/6] ◆ recfun() [3/6] ◆ recfun() [4/6] func_decl recfun ( char const * name, unsigned arity, sort const * domain, sort const & range ) inline ◆ recfun() [5/6]

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

3719

array<Z3_sort> domain1(domain);

3722 return

func_decl(*

this

, f);

Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a recursive function.

◆ recfun() [6/6]

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

3706

array<Z3_sort> args(arity);

3707 for

(

unsigned

i = 0; i < arity; i++) {

3709

args[i] = domain[i];

3713 return

func_decl(*

this

, f);

Referenced by context::recfun(), and z3::recfun().

◆ seq_sort()

Return a sequence sort over base sort s.

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

Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)

Create a sequence sort out of the sort for the elements.

◆ set() [1/3] void set ( char const * param, bool value ) inline

Update global parameter param with Boolean value.

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

void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)

Set a value of a context parameter.

◆ set() [2/3] void set ( char const * param, char const * value ) inline

Update global parameter param with string value.

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

◆ set() [3/3] void set ( char const * param, int value ) inline

Update global parameter param with Integer value.

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

226 auto

str = std::to_string(value);

◆ set_enable_exceptions() void set_enable_exceptions ( bool f ) inline

The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications have to be very careful about using check_error() after calls that may result in an erroneous state.

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

210

{ m_enable_exceptions = f; }

◆ set_rounding_mode()

Sets RoundingMode of FloatingPoints.

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

3778

{ m_rounding_mode = rm; }

◆ str_symbol() symbol str_symbol ( char const * s ) inline ◆ string_const() expr string_const ( char const * name ) inline

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

sort string_sort()

Return the sort for Unicode strings.

◆ string_sort()

Return the sort for Unicode strings.

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

Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)

Create a sort for unicode strings.

Referenced by context::string_const().

◆ string_val() [1/4] expr string_val ( char const * s ) inline

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

Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)

Create a string constant out of the string that is passed in The string may contain escape encoding f...

◆ string_val() [2/4] expr string_val ( char const * s, unsigned n ) inline

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

Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)

Create a string constant out of the string that is passed in It takes the length of the string as wel...

◆ string_val() [3/4] expr string_val ( std::string const & s ) inline ◆ string_val() [4/4] expr string_val ( std::u32string const & s ) inline

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

Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[])

Create a string constant out of the string that is passed in It takes the length of the string as wel...

◆ tuple_sort()

Return a tuple constructor. name is the name of the returned constructor, n are the number of arguments, names and sorts are their projected sorts. projs is an output parameter. It contains the set of projection functions.

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

3522

array<Z3_symbol> _names(n);

3523

array<Z3_sort> _sorts(n);

3524 for

(

unsigned

i = 0; i < n; i++) { _names[i] =

Z3_mk_string_symbol

this

, names[i]); _sorts[i] = sorts[i]; }

3525

array<Z3_func_decl> _projs(n);

3528

sort _ignore_s =

to_sort

this

Z3_mk_tuple_sort

this

, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));

3530 for

(

unsigned

i = 0; i < n; i++) { projs.push_back(func_decl(*

this

, _projs[i])); }

3531 return

func_decl(*

this

, tuple);

Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])

Create a tuple type.

◆ uninterpreted_sort() [1/2] sort uninterpreted_sort ( char const * name ) inline

create an uninterpreted sort with the name given by the string or symbol.

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

Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)

Create a free (uninterpreted) type using the given name (symbol).

◆ uninterpreted_sort() [2/2] ◆ user_propagate_function()

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

3751

array<Z3_sort> domain1(domain);

3754 return

func_decl(*

this

, f);

Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)

◆ variable() expr variable ( unsigned index, sort const & s ) inline

create a de-Bruijn variable.

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

3766 return

expr(*

this

, r);

Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)

Create a variable.

◆ user_propagator_base

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