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 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 | 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... | |
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 paramter. It contains the set of projection functions. 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_t n) |
expr | int_val (uint64_t 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_t n) |
expr | real_val (uint64_t 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_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 | 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 2439 of file z3++.h.
|
inline |
Definition at line 2440 of file z3++.h.
|
inline |
Return the Boolean sort.
Definition at line 2431 of file z3++.h.
Referenced by context::bool_const().
|
inline |
Definition at line 2559 of file z3++.h.
Referenced by goal::as_expr(), apply_result::as_expr(), z3::implies(), z3::operator &&(), z3::operator||(), and solver::to_smt2().
|
inline |
Definition at line 2557 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 2434 of file z3++.h.
Referenced by context::bv_const(), and context::bv_val().
|
inline |
Definition at line 2574 of file z3++.h.
|
inline |
Definition at line 2575 of file z3++.h.
|
inline |
Definition at line 2576 of file z3++.h.
|
inline |
Definition at line 2577 of file z3++.h.
|
inline |
Definition at line 2578 of file z3++.h.
|
inline |
Definition at line 2579 of file z3++.h.
|
inline |
Auxiliary method used to check for API usage errors.
Definition at line 170 of file z3++.h.
Referenced by context::array_sort(), context::bool_sort(), context::bv_sort(), context::bv_val(), object::check_error(), context::check_parser_error(), z3::concat(), context::constant(), context::enumeration_sort(), expr::extract(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::num_val(), func_decl::operator()(), context::re_sort(), context::real_sort(), context::real_val(), 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(), and context::tuple_sort().
|
inline |
Definition at line 177 of file z3++.h.
Referenced by solver::from_file(), solver::from_string(), context::parse_file(), and context::parse_string().
|
inline |
Interpolation support.
Definition at line 2927 of file z3++.h.
Definition at line 2548 of file z3++.h.
Referenced by context::bool_const(), context::bv_const(), context::constant(), context::int_const(), and context::real_const().
Definition at line 2553 of file z3++.h.
|
inline |
Definition at line 195 of file z3++.h.
Referenced by context::check_error(), and context::check_parser_error().
|
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 2445 of file z3++.h.
|
inline |
Definition at line 2477 of file z3++.h.
Referenced by z3::function().
|
inline |
Definition at line 2488 of file z3++.h.
|
inline |
Definition at line 2492 of file z3++.h.
|
inline |
Definition at line 2503 of file z3++.h.
Definition at line 2508 of file z3++.h.
|
inline |
Definition at line 2516 of file z3++.h.
|
inline |
Definition at line 2524 of file z3++.h.
|
inline |
Definition at line 2532 of file z3++.h.
|
inline |
Definition at line 2540 of file z3++.h.
|
inline |
|
inline |
Return the integer sort.
Definition at line 2432 of file z3++.h.
Referenced by context::int_const(), and context::int_val().
|
inline |
Create a Z3 symbol based on the given integer.
Definition at line 2429 of file z3++.h.
|
inline |
Definition at line 2561 of file z3++.h.
|
inline |
Definition at line 2562 of file z3++.h.
|
inline |
Definition at line 2563 of file z3++.h.
|
inline |
Definition at line 2564 of file z3++.h.
|
inline |
Definition at line 2565 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 actually stop.
Definition at line 218 of file z3++.h.
Definition at line 2588 of file z3++.h.
Referenced by z3::ashr(), z3::lshr(), z3::mod(), z3::operator &(), z3::operator!=(), func_decl::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 2888 of file z3++.h.
|
inline |
Definition at line 2910 of file z3++.h.
|
inline |
parsing
Definition at line 2883 of file z3++.h.
|
inline |
Definition at line 2894 of file z3++.h.
Return a regular expression sort over sequences seq_sort
.
Definition at line 2437 of file z3++.h.
|
inline |
Return the Real sort.
Definition at line 2433 of file z3++.h.
Referenced by context::real_const(), and context::real_val().
|
inline |
Definition at line 2567 of file z3++.h.
|
inline |
Definition at line 2568 of file z3++.h.
|
inline |
Definition at line 2569 of file z3++.h.
|
inline |
Definition at line 2570 of file z3++.h.
|
inline |
Definition at line 2571 of file z3++.h.
|
inline |
Definition at line 2572 of file z3++.h.
Return a sequence sort over base sort s
.
Definition at line 2436 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 erroneous state.
|
inline |
Create a Z3 symbol based on the given string.
Definition at line 2428 of file z3++.h.
Referenced by context::constant(), context::function(), and solver::solver().
|
inline |
Return the sort for ASCII strings.
Definition at line 2435 of file z3++.h.
|
inline |
Definition at line 2585 of file z3++.h.
|
inline |
Definition at line 2586 of file z3++.h.
|
inline |
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 paramter. It contains the set of projection functions.
Definition at line 2456 of file z3++.h.
|
inline |
create an uninterpreted sort with the name given by the string or symbol.
Definition at line 2469 of file z3++.h.