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 | |
void | check_error () const |
Auxiliary method used to check for API usage errors. More... | |
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 | 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 | 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 2095 of file z3++.h.
|
inline |
Return the Boolean sort.
Definition at line 2087 of file z3++.h.
|
inline |
Definition at line 2197 of file z3++.h.
Referenced by z3::implies(), z3::operator &&(), and z3::operator||().
|
inline |
Definition at line 2195 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 2090 of file z3++.h.
|
inline |
Definition at line 2212 of file z3++.h.
|
inline |
Definition at line 2213 of file z3++.h.
Definition at line 2214 of file z3++.h.
Definition at line 2215 of file z3++.h.
|
inline |
Definition at line 2216 of file z3++.h.
|
inline |
Auxiliary method used to check for API usage errors.
Definition at line 162 of file z3++.h.
Referenced by object::check_error(), z3::concat(), z3::to_expr(), z3::to_func_decl(), and z3::to_sort().
|
inline |
Interpolation support.
Definition at line 2514 of file z3++.h.
Definition at line 2186 of file z3++.h.
Definition at line 2191 of file z3++.h.
|
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 2096 of file z3++.h.
|
inline |
Definition at line 2115 of file z3++.h.
Referenced by z3::function().
|
inline |
Definition at line 2130 of file z3++.h.
|
inline |
Definition at line 2146 of file z3++.h.
|
inline |
Definition at line 2154 of file z3++.h.
|
inline |
Definition at line 2162 of file z3++.h.
|
inline |
Definition at line 2170 of file z3++.h.
|
inline |
Definition at line 2178 of file z3++.h.
|
inline |
|
inline |
Return the integer sort.
Definition at line 2088 of file z3++.h.
|
inline |
Create a Z3 symbol based on the given integer.
Definition at line 2085 of file z3++.h.
|
inline |
Definition at line 2199 of file z3++.h.
|
inline |
Definition at line 2200 of file z3++.h.
Definition at line 2201 of file z3++.h.
Definition at line 2202 of file z3++.h.
|
inline |
Definition at line 2203 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 189 of file z3++.h.
Definition at line 2221 of file z3++.h.
Referenced by z3::ashr(), z3::lshr(), 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::select(), z3::shl(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
|
inline |
Definition at line 2475 of file z3++.h.
|
inline |
Definition at line 2497 of file z3++.h.
|
inline |
parsing
Definition at line 2469 of file z3++.h.
|
inline |
Definition at line 2481 of file z3++.h.
Return a regular expression sort over sequences seq_sort
.
Definition at line 2093 of file z3++.h.
|
inline |
Return the Real sort.
Definition at line 2089 of file z3++.h.
|
inline |
Definition at line 2205 of file z3++.h.
|
inline |
Definition at line 2206 of file z3++.h.
|
inline |
Definition at line 2207 of file z3++.h.
Definition at line 2208 of file z3++.h.
Definition at line 2209 of file z3++.h.
|
inline |
Definition at line 2210 of file z3++.h.
Return a sequence sort over base sort s
.
Definition at line 2092 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
Create a Z3 symbol based on the given string.
Definition at line 2084 of file z3++.h.
Referenced by context::function(), and solver::solver().
|
inline |
Return the sort for ASCII strings.
Definition at line 2091 of file z3++.h.
|
inline |
Definition at line 2218 of file z3++.h.
|
inline |
Definition at line 2219 of file z3++.h.
|
inline |
create an uninterpreted sort with the name given by the string or symbol.
Definition at line 2107 of file z3++.h.