A Context manages all other Z3 objects, global configuration options, etc. More...
#include <z3++.h>
Public Member Functions | |
context () | |
context (config &c) | |
~context () | |
operator Z3_context () const | |
Z3_error_code | check_error () const |
Auxiliary method used to check for API usage errors. | |
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. | |
bool | enable_exceptions () const |
void | set (char const *param, char const *value) |
Update global parameter param with string value . | |
void | set (char const *param, bool value) |
Update global parameter param with Boolean value . | |
void | set (char const *param, int value) |
Update global parameter param with Integer value . | |
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. | |
symbol | str_symbol (char const *s) |
Create a Z3 symbol based on the given string. | |
symbol | int_symbol (int n) |
Create a Z3 symbol based on the given integer. | |
sort | bool_sort () |
Return the Boolean sort. | |
sort | int_sort () |
Return the integer sort. | |
sort | real_sort () |
Return the Real sort. | |
sort | bv_sort (unsigned sz) |
Return the Bit-vector sort of size sz . That is, the sort for bit-vectors of size sz . | |
sort | char_sort () |
Return the sort for Unicode characters. | |
sort | string_sort () |
Return the sort for Unicode strings. | |
sort | seq_sort (sort &s) |
Return a sequence sort over base sort s . | |
sort | re_sort (sort &seq_sort) |
Return a regular expression sort over sequences seq_sort . | |
sort | array_sort (sort d, sort r) |
Return an array sort for arrays from d to r . | |
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,. | |
template<size_t precision> | |
sort | fpa_sort () |
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128). | |
sort | fpa_rounding_mode_sort () |
Return a RoundingMode sort. | |
void | set_rounding_mode (rounding_mode rm) |
Sets RoundingMode of FloatingPoints. | |
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. | |
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. | |
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. | |
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. | |
sort | datatype_sort (symbol const &name) |
a reference to a recursively defined datatype. Expect that it gets defined as a datatype. | |
sort | uninterpreted_sort (char const *name) |
create an uninterpreted sort with the name given by the string or symbol. | |
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. | |
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. | |
expr | constant (char const *name, sort const &s) |
expr | bool_const (char const *name) |
create uninterpreted constants of a given sort. | |
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. | |
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 | |
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 () |
Friends | |
class | user_propagator_base |
A Context manages all other Z3 objects, global configuration options, etc.
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 3454 of file z3++.h.
|
inline |
Definition at line 3455 of file z3++.h.
|
inline |
create uninterpreted constants of a given sort.
Definition at line 3717 of file z3++.h.
|
inline |
Return the Boolean sort.
Definition at line 3430 of file z3++.h.
Referenced by context::bool_const().
|
inline |
Definition at line 3740 of file z3++.h.
Referenced by goal::as_expr(), user_propagator_base::conflict(), user_propagator_base::conflict(), and solver::to_smt2().
|
inline |
Definition at line 3721 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 3433 of file z3++.h.
Referenced by context::bv_const(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), and context::bv_val().
|
inline |
Definition at line 3759 of file z3++.h.
|
inline |
|
inline |
Definition at line 3757 of file z3++.h.
|
inline |
Definition at line 3758 of file z3++.h.
|
inline |
|
inline |
Definition at line 3756 of file z3++.h.
|
inline |
|
inline |
Auxiliary method used to check for API usage errors.
Definition at line 192 of file z3++.h.
Referenced by context::array_sort(), context::array_sort(), expr::bit2bool(), context::bool_sort(), context::bv_sort(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), 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(), context::fpa_inf(), context::fpa_nan(), context::fpa_rounding_mode_sort(), context::fpa_sort(), context::fpa_val(), context::fpa_val(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), context::num_val(), on_clause::on_clause(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), context::parse_file(), context::parse_file(), context::parse_string(), context::parse_string(), z3::re_diff(), z3::re_intersect(), context::re_sort(), context::real_sort(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::recfun(), context::recfun(), expr::repeat(), expr::rotate_left(), expr::rotate_right(), context::seq_sort(), context::str_symbol(), context::string_sort(), context::string_val(), context::string_val(), context::string_val(), context::string_val(), z3::to_expr(), z3::to_func_decl(), z3::to_sort(), context::tuple_sort(), context::user_propagate_function(), and context::variable().
|
inline |
Definition at line 199 of file z3++.h.
Referenced by solver::from_file(), and solver::from_string().
Definition at line 3711 of file z3++.h.
create an uninterpreted constant.
Definition at line 3706 of file z3++.h.
Referenced by context::bool_const(), context::bv_const(), context::constant(), context::fpa_const(), context::fpa_const(), context::int_const(), context::real_const(), and context::string_const().
|
inline |
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 3544 of file z3++.h.
a reference to a recursively defined datatype. Expect that it gets defined as a datatype.
Definition at line 3568 of file z3++.h.
|
inline |
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 3552 of file z3++.h.
|
inline |
Definition at line 212 of file z3++.h.
Referenced by context::check_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 3459 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 3729 of file z3++.h.
|
inline |
sort fpa_sort | ( | ) |
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
Referenced by context::fpa_const().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Return a floating point sort. ebits
is a number of exponent bits, sbits
is a number of significand bits,.
Definition at line 3438 of file z3++.h.
|
inline |
Definition at line 3766 of file z3++.h.
Referenced by z3::operator!=(), z3::operator!=(), z3::operator==(), and z3::operator==().
|
inline |
Definition at line 3767 of file z3++.h.
|
inline |
Definition at line 3646 of file z3++.h.
|
inline |
Definition at line 3638 of file z3++.h.
|
inline |
Definition at line 3630 of file z3++.h.
|
inline |
Definition at line 3622 of file z3++.h.
Definition at line 3614 of file z3++.h.
|
inline |
Definition at line 3609 of file z3++.h.
|
inline |
Definition at line 3598 of file z3++.h.
|
inline |
Definition at line 3583 of file z3++.h.
Referenced by z3::function(), z3::function(), z3::function(), z3::function(), z3::function(), context::function(), z3::function(), context::function(), z3::function(), z3::function(), and z3::function().
|
inline |
Return the integer sort.
Definition at line 3431 of file z3++.h.
Referenced by context::int_const(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), and context::int_val().
|
inline |
|
inline |
Definition at line 3745 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 234 of file z3++.h.
Definition at line 3776 of file z3++.h.
Referenced by z3::ashr(), z3::ashr(), z3::lshr(), z3::lshr(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), z3::select(), z3::sge(), z3::sge(), z3::sgt(), z3::sgt(), z3::shl(), z3::shl(), z3::sle(), z3::sle(), z3::slt(), z3::slt(), z3::smod(), z3::smod(), z3::srem(), z3::srem(), z3::store(), z3::store(), z3::store(), z3::udiv(), z3::udiv(), z3::uge(), z3::uge(), z3::ugt(), z3::ugt(), z3::ule(), z3::ule(), z3::ult(), z3::ult(), z3::urem(), and z3::urem().
|
inline |
Definition at line 4102 of file z3++.h.
|
inline |
Definition at line 4125 of file z3++.h.
|
inline |
parsing
Definition at line 4096 of file z3++.h.
|
inline |
Definition at line 4108 of file z3++.h.
|
inline |
Return the Real sort.
Definition at line 3432 of file z3++.h.
Referenced by context::real_const(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), and context::real_val().
|
inline |
|
inline |
Definition at line 3752 of file z3++.h.
|
inline |
add function definition body to declaration decl. decl needs to be declared using context::recfun.
decl | |
args | |
body |
Definition at line 3692 of file z3++.h.
Definition at line 3687 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 3666 of file z3++.h.
|
inline |
Definition at line 3654 of file z3++.h.
Referenced by context::recfun(), z3::recfun(), z3::recfun(), context::recfun(), context::recfun(), context::recfun(), z3::recfun(), and z3::recfun().
|
inline |
|
inline |
Update global parameter param
with string value
.
Definition at line 217 of file z3++.h.
|
inline |
Update global parameter param
with Integer value
.
Definition at line 225 of file z3++.h.
|
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.
|
inline |
|
inline |
Create a Z3 symbol based on the given string.
Definition at line 3427 of file z3++.h.
Referenced by context::constant(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::recfun(), context::recfun(), context::recfun(), context::recfun(), and solver::solver().
|
inline |
Definition at line 3720 of file z3++.h.
|
inline |
Return the sort for Unicode strings.
Definition at line 3434 of file z3++.h.
Referenced by context::string_const().
|
inline |
|
inline |
|
inline |
Definition at line 3774 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 parameter. It contains the set of projection functions.
Definition at line 3470 of file z3++.h.
|
inline |
|
inline |
Definition at line 3698 of file z3++.h.
create a de-Bruijn variable.
Definition at line 3712 of file z3++.h.
|
friend |