A Context manages all other Z3 objects, global configuration options, etc. More...
Public Member Functions | |
context () | |
context (config &c) | |
~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 | 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... | |
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 | num_val (int n, sort const &s) |
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 1564 of file z3++.h.
|
inline |
Return the Boolean sort.
Definition at line 1560 of file z3++.h.
Referenced by context::bool_const().
|
inline |
Definition at line 1659 of file z3++.h.
Referenced by goal::as_expr(), z3::implies(), and solver::to_smt2().
|
inline |
Definition at line 1657 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 1563 of file z3++.h.
Referenced by context::bv_const(), and context::bv_val().
|
inline |
Definition at line 1674 of file z3++.h.
|
inline |
Definition at line 1675 of file z3++.h.
Definition at line 1676 of file z3++.h.
Definition at line 1677 of file z3++.h.
|
inline |
Definition at line 1678 of file z3++.h.
|
inline |
Auxiliary method used to check for API usage errors.
Definition at line 141 of file z3++.h.
Referenced by context::array_sort(), context::bool_sort(), context::bv_sort(), context::bv_val(), object::check_error(), context::constant(), context::enumeration_sort(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::num_val(), func_decl::operator()(), context::real_sort(), context::real_val(), context::str_symbol(), z3::to_expr(), z3::to_func_decl(), and z3::to_sort().
Definition at line 1648 of file z3++.h.
Referenced by context::bool_const(), context::bv_const(), context::constant(), context::int_const(), and context::real_const().
Definition at line 1653 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 1565 of file z3++.h.
|
inline |
Definition at line 1577 of file z3++.h.
Referenced by z3::function().
|
inline |
Definition at line 1592 of file z3++.h.
|
inline |
Definition at line 1608 of file z3++.h.
|
inline |
Definition at line 1616 of file z3++.h.
|
inline |
Definition at line 1624 of file z3++.h.
|
inline |
Definition at line 1632 of file z3++.h.
|
inline |
Definition at line 1640 of file z3++.h.
|
inline |
Return the integer sort.
Definition at line 1561 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 1558 of file z3++.h.
|
inline |
Definition at line 1661 of file z3++.h.
|
inline |
Definition at line 1662 of file z3++.h.
Definition at line 1663 of file z3++.h.
Definition at line 1664 of file z3++.h.
|
inline |
Definition at line 1665 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 168 of file z3++.h.
Definition at line 1680 of file z3++.h.
Referenced by func_decl::operator()(), z3::pw(), z3::select(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), and z3::ult().
|
inline |
Return the Real sort.
Definition at line 1562 of file z3++.h.
Referenced by context::real_const(), and context::real_val().
|
inline |
Definition at line 1667 of file z3++.h.
|
inline |
Definition at line 1668 of file z3++.h.
|
inline |
Definition at line 1669 of file z3++.h.
Definition at line 1670 of file z3++.h.
Definition at line 1671 of file z3++.h.
|
inline |
Definition at line 1672 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
Create a Z3 symbol based on the given string.
Definition at line 1557 of file z3++.h.
Referenced by context::constant(), context::function(), and solver::solver().