A Context manages all other Z3 objects, global configuration options, etc. More...
Data Structures | |
struct | interpolation |
Public Member Functions | |
context () | |
context (config &c) | |
context (config &c, interpolation) | |
~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 very careful about using check_error() after calls that may result in an errornous 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 actualy 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 | string_sort () |
Return the sort for ASCII 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 | 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... | |
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) |
expr | constant (symbol const &name, sort const &s) |
expr | constant (char const *name, sort const &s) |
expr | bool_const (char const *name) |
expr | int_const (char const *name) |
expr | real_const (char const *name) |
expr | bv_const (char const *name, unsigned sz) |
expr | bool_val (bool b) |
expr | int_val (int n) |
expr | int_val (unsigned n) |
expr | int_val (__int64 n) |
expr | int_val (__uint64 n) |
expr | int_val (char const *n) |
expr | real_val (int n, int d) |
expr | real_val (int n) |
expr | real_val (unsigned n) |
expr | real_val (__int64 n) |
expr | real_val (__uint64 n) |
expr | real_val (char const *n) |
expr | bv_val (int n, unsigned sz) |
expr | bv_val (unsigned n, unsigned sz) |
expr | bv_val (__int64 n, unsigned sz) |
expr | bv_val (__uint64 n, unsigned sz) |
expr | bv_val (char const *n, unsigned sz) |
expr | bv_val (unsigned n, bool const *bits) |
expr | string_val (char const *s) |
expr | string_val (std::string const &s) |
expr | num_val (int n, sort const &s) |
expr | parse_string (char const *s) |
parsing More... | |
expr | parse_file (char const *file) |
expr | parse_string (char const *s, sort_vector const &sorts, func_decl_vector const &decls) |
expr | parse_file (char const *s, sort_vector const &sorts, func_decl_vector const &decls) |
check_result | compute_interpolant (expr const &pat, params const &p, expr_vector &interp, model &m) |
Interpolation support. More... | |
expr_vector | get_interpolant (expr const &proof, expr const &pat, params const &p) |
A Context manages all other Z3 objects, global configuration options, etc.
|
inline |
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 2403 of file z3++.h.
|
inline |
Definition at line 2404 of file z3++.h.
|
inline |
Return the Boolean sort.
Definition at line 2395 of file z3++.h.
|
inline |
Definition at line 2510 of file z3++.h.
Referenced by z3::implies(), z3::operator &&(), and z3::operator||().
|
inline |
Definition at line 2508 of file z3++.h.
|
inline |
Return the Bit-vector sort of size sz
. That is, the sort for bit-vectors of size sz
.
Definition at line 2398 of file z3++.h.
|
inline |
Definition at line 2525 of file z3++.h.
|
inline |
Definition at line 2526 of file z3++.h.
Definition at line 2527 of file z3++.h.
Definition at line 2528 of file z3++.h.
|
inline |
Definition at line 2529 of file z3++.h.
|
inline |
Definition at line 2530 of file z3++.h.
|
inline |
Auxiliary method used to check for API usage errors.
Definition at line 170 of file z3++.h.
Referenced by object::check_error(), z3::concat(), z3::to_expr(), z3::to_func_decl(), and z3::to_sort().
|
inline |
Definition at line 177 of file z3++.h.
|
inline |
Interpolation support.
Definition at line 2872 of file z3++.h.
Definition at line 2499 of file z3++.h.
Definition at line 2504 of file z3++.h.
|
inline |
|
inline |
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 2409 of file z3++.h.
|
inline |
Definition at line 2428 of file z3++.h.
Referenced by z3::function().
|
inline |
Definition at line 2439 of file z3++.h.
|
inline |
Definition at line 2443 of file z3++.h.
|
inline |
Definition at line 2454 of file z3++.h.
Definition at line 2459 of file z3++.h.
|
inline |
Definition at line 2467 of file z3++.h.
|
inline |
Definition at line 2475 of file z3++.h.
|
inline |
Definition at line 2483 of file z3++.h.
|
inline |
Definition at line 2491 of file z3++.h.
|
inline |
|
inline |
Return the integer sort.
Definition at line 2396 of file z3++.h.
|
inline |
Create a Z3 symbol based on the given integer.
Definition at line 2393 of file z3++.h.
|
inline |
Definition at line 2512 of file z3++.h.
|
inline |
Definition at line 2513 of file z3++.h.
Definition at line 2514 of file z3++.h.
Definition at line 2515 of file z3++.h.
|
inline |
Definition at line 2516 of file z3++.h.
|
inline |
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 actualy stop.
Definition at line 218 of file z3++.h.
Definition at line 2539 of file z3++.h.
Referenced by z3::ashr(), z3::lshr(), z3::mod(), z3::operator &(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::pw(), z3::rem(), z3::select(), z3::shl(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
|
inline |
Definition at line 2833 of file z3++.h.
|
inline |
Definition at line 2855 of file z3++.h.
|
inline |
parsing
Definition at line 2828 of file z3++.h.
|
inline |
Definition at line 2839 of file z3++.h.
Return a regular expression sort over sequences seq_sort
.
Definition at line 2401 of file z3++.h.
|
inline |
Return the Real sort.
Definition at line 2397 of file z3++.h.
|
inline |
Definition at line 2518 of file z3++.h.
|
inline |
Definition at line 2519 of file z3++.h.
|
inline |
Definition at line 2520 of file z3++.h.
Definition at line 2521 of file z3++.h.
Definition at line 2522 of file z3++.h.
|
inline |
Definition at line 2523 of file z3++.h.
Return a sequence sort over base sort s
.
Definition at line 2400 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
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 very careful about using check_error() after calls that may result in an errornous state.
|
inline |
Create a Z3 symbol based on the given string.
Definition at line 2392 of file z3++.h.
Referenced by context::function(), and solver::solver().
|
inline |
Return the sort for ASCII strings.
Definition at line 2399 of file z3++.h.
|
inline |
Definition at line 2536 of file z3++.h.
|
inline |
Definition at line 2537 of file z3++.h.
|
inline |
create an uninterpreted sort with the name given by the string or symbol.
Definition at line 2420 of file z3++.h.