A Context manages all other Z3 objects, global configuration options, etc.
More...
|
| context () |
|
| context (config &c) |
|
| ~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 be 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 | 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,. More...
|
|
template<size_t precision> |
sort | fpa_sort () |
| Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128). More...
|
|
sort | fpa_rounding_mode () |
| Return a RoundingMode sort. More...
|
|
void | set_rounding_mode (rounding_mode rm) |
| Sets RoundingMode of FloatingPoints. 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 | 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. 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) |
|
func_decl | recfun (symbol const &name, unsigned arity, sort 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, expr_vector const &args, expr const &body) |
|
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 | fpa_const (char const *name, unsigned ebits, unsigned sbits) |
|
template<size_t precision> |
expr | fpa_const (char const *name) |
|
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 | fpa_val (double n) |
|
expr | fpa_val (float n) |
|
expr | string_val (char const *s) |
|
expr | string_val (char const *s, unsigned n) |
|
expr | string_val (std::string const &s) |
|
expr | num_val (int n, sort const &s) |
|
expr_vector | parse_string (char const *s) |
| parsing More...
|
|
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 () |
|
A Context manages all other Z3 objects, global configuration options, etc.
Definition at line 156 of file z3++.h.
◆ context() [1/2]
Definition at line 173 of file z3++.h.
173 { config c; init(c); }
◆ context() [2/2]
◆ ~context()
◆ array_sort() [1/2]
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 2999 of file z3++.h.
◆ array_sort() [2/2]
Definition at line 3000 of file z3++.h.
3001 array<Z3_sort> dom(d);
◆ bool_const()
expr bool_const |
( |
char const * |
name | ) |
|
|
inline |
◆ bool_sort()
◆ bool_val()
◆ bv_const()
expr bv_const |
( |
char const * |
name, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
◆ bv_sort()
sort bv_sort |
( |
unsigned |
sz | ) |
|
|
inline |
◆ bv_val() [1/6]
expr bv_val |
( |
char const * |
n, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
◆ bv_val() [2/6]
expr bv_val |
( |
int |
n, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
◆ bv_val() [3/6]
expr bv_val |
( |
int64_t |
n, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
◆ bv_val() [4/6]
expr bv_val |
( |
uint64_t |
n, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
◆ bv_val() [5/6]
expr bv_val |
( |
unsigned |
n, |
|
|
bool const * |
bits |
|
) |
| |
|
inline |
Definition at line 3173 of file z3++.h.
3174 array<bool> _bits(n);
3175 for (
unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
◆ bv_val() [6/6]
expr bv_val |
( |
unsigned |
n, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
◆ check_error()
Auxiliary method used to check for API usage errors.
Definition at line 181 of file z3++.h.
Referenced by context::array_sort(), z3::atleast(), z3::atmost(), context::bool_sort(), context::bv_sort(), context::bv_val(), object::check_error(), context::check_parser_error(), z3::concat(), context::constant(), z3::distinct(), context::enumeration_sort(), expr::extract(), context::fpa_sort(), context::fpa_val(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::num_val(), func_decl::operator()(), context::parse_file(), context::parse_string(), z3::pbeq(), z3::pbge(), z3::pble(), z3::re_intersect(), context::re_sort(), context::real_sort(), context::real_val(), context::recfun(), expr::repeat(), expr::rotate_left(), expr::rotate_right(), context::seq_sort(), context::str_symbol(), context::string_sort(), context::string_val(), z3::sum(), z3::to_expr(), z3::to_func_decl(), z3::to_sort(), and context::tuple_sort().
◆ check_parser_error()
void check_parser_error |
( |
| ) |
const |
|
inline |
◆ constant() [1/2]
expr constant |
( |
char const * |
name, |
|
|
sort const & |
s |
|
) |
| |
|
inline |
◆ constant() [2/2]
◆ enable_exceptions()
bool enable_exceptions |
( |
| ) |
const |
|
inline |
◆ enumeration_sort()
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 3004 of file z3++.h.
3005 array<Z3_symbol> _enum_names(n);
3006 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
3007 array<Z3_func_decl> _cs(n);
3008 array<Z3_func_decl> _ts(n);
3012 for (
unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*
this, _cs[i])); ts.push_back(func_decl(*
this, _ts[i])); }
◆ fpa_const() [1/2]
expr fpa_const |
( |
char const * |
name | ) |
|
|
inline |
Definition at line 3151 of file z3++.h.
3151 {
return constant(name, fpa_sort<precision>()); }
◆ fpa_const() [2/2]
expr fpa_const |
( |
char const * |
name, |
|
|
unsigned |
ebits, |
|
|
unsigned |
sbits |
|
) |
| |
|
inline |
◆ fpa_rounding_mode()
sort fpa_rounding_mode |
( |
| ) |
|
|
inline |
◆ fpa_sort() [1/6]
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
Referenced by context::fpa_const().
◆ fpa_sort() [2/6]
◆ fpa_sort() [3/6]
◆ fpa_sort() [4/6]
◆ fpa_sort() [5/6]
◆ fpa_sort() [6/6]
sort fpa_sort |
( |
unsigned |
ebits, |
|
|
unsigned |
sbits |
|
) |
| |
|
inline |
Return a floating point sort. ebits
is a number of exponent bits, sbits
is a number of significand bits,.
- Precondition
- where ebits must be larger than 1 and sbits must be larger than 2.
Definition at line 2972 of file z3++.h.
◆ fpa_val() [1/2]
◆ fpa_val() [2/2]
◆ function() [1/9]
Definition at line 3099 of file z3++.h.
3101 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3104 return func_decl(*
this, f);
◆ function() [2/9]
Definition at line 3091 of file z3++.h.
3093 Z3_sort args[4] = { d1, d2, d3, d4 };
3096 return func_decl(*
this, f);
◆ function() [3/9]
Definition at line 3083 of file z3++.h.
3085 Z3_sort args[3] = { d1, d2, d3 };
3088 return func_decl(*
this, f);
◆ function() [4/9]
Definition at line 3075 of file z3++.h.
3077 Z3_sort args[2] = { d1, d2 };
3080 return func_decl(*
this, f);
◆ function() [5/9]
Definition at line 3067 of file z3++.h.
3069 Z3_sort args[1] = { domain };
3072 return func_decl(*
this, f);
◆ function() [6/9]
◆ function() [7/9]
func_decl function |
( |
char const * |
name, |
|
|
unsigned |
arity, |
|
|
sort const * |
domain, |
|
|
sort const & |
range |
|
) |
| |
|
inline |
◆ function() [8/9]
Definition at line 3051 of file z3++.h.
3052 array<Z3_sort> args(domain.size());
3053 for (
unsigned i = 0; i < domain.size(); i++) {
3055 args[i] = domain[i];
3059 return func_decl(*
this, f);
◆ function() [9/9]
Definition at line 3036 of file z3++.h.
3037 array<Z3_sort> args(arity);
3038 for (
unsigned i = 0; i < arity; i++) {
3040 args[i] = domain[i];
3044 return func_decl(*
this, f);
Referenced by z3::function().
◆ int_const()
expr int_const |
( |
char const * |
name | ) |
|
|
inline |
◆ int_sort()
◆ int_symbol()
Create a Z3 symbol based on the given integer.
Definition at line 2963 of file z3++.h.
◆ int_val() [1/5]
expr int_val |
( |
char const * |
n | ) |
|
|
inline |
◆ int_val() [2/5]
◆ int_val() [3/5]
expr int_val |
( |
int64_t |
n | ) |
|
|
inline |
◆ int_val() [4/5]
expr int_val |
( |
uint64_t |
n | ) |
|
|
inline |
◆ int_val() [5/5]
expr int_val |
( |
unsigned |
n | ) |
|
|
inline |
◆ 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.
Definition at line 224 of file z3++.h.
◆ num_val()
Definition at line 3186 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::sle(), z3::slt(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
◆ operator Z3_context()
operator Z3_context |
( |
| ) |
const |
|
inline |
◆ parse_file() [1/2]
◆ parse_file() [2/2]
Definition at line 3528 of file z3++.h.
3529 array<Z3_symbol> sort_names(sorts.size());
3530 array<Z3_symbol> decl_names(decls.size());
3531 array<Z3_sort> sorts1(sorts);
3532 array<Z3_func_decl> decls1(decls);
3533 for (
unsigned i = 0; i < sorts.size(); ++i) {
3534 sort_names[i] = sorts[i].name();
3536 for (
unsigned i = 0; i < decls.size(); ++i) {
3537 decl_names[i] = decls[i].name();
3539 Z3_ast_vector r =
Z3_parse_smtlib2_file(*
this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
◆ parse_string() [1/2]
◆ parse_string() [2/2]
Definition at line 3511 of file z3++.h.
3512 array<Z3_symbol> sort_names(sorts.size());
3513 array<Z3_symbol> decl_names(decls.size());
3514 array<Z3_sort> sorts1(sorts);
3515 array<Z3_func_decl> decls1(decls);
3516 for (
unsigned i = 0; i < sorts.size(); ++i) {
3517 sort_names[i] = sorts[i].name();
3519 for (
unsigned i = 0; i < decls.size(); ++i) {
3520 decl_names[i] = decls[i].name();
3523 Z3_ast_vector r =
Z3_parse_smtlib2_string(*
this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
◆ re_sort()
Return a regular expression sort over sequences seq_sort
.
Definition at line 2971 of file z3++.h.
◆ real_const()
expr real_const |
( |
char const * |
name | ) |
|
|
inline |
◆ real_sort()
◆ real_val() [1/6]
expr real_val |
( |
char const * |
n | ) |
|
|
inline |
◆ real_val() [2/6]
◆ real_val() [3/6]
expr real_val |
( |
int |
n, |
|
|
int |
d |
|
) |
| |
|
inline |
◆ real_val() [4/6]
expr real_val |
( |
int64_t |
n | ) |
|
|
inline |
◆ real_val() [5/6]
expr real_val |
( |
uint64_t |
n | ) |
|
|
inline |
◆ real_val() [6/6]
expr real_val |
( |
unsigned |
n | ) |
|
|
inline |
◆ recdef()
Definition at line 3132 of file z3++.h.
3134 array<Z3_ast> vars(args);
◆ recfun() [1/4]
Definition at line 3127 of file z3++.h.
3128 sort dom[2] = { d1, d2 };
◆ recfun() [2/4]
◆ recfun() [3/4]
func_decl recfun |
( |
char const * |
name, |
|
|
unsigned |
arity, |
|
|
sort const * |
domain, |
|
|
sort const & |
range |
|
) |
| |
|
inline |
◆ recfun() [4/4]
Definition at line 3107 of file z3++.h.
3108 array<Z3_sort> args(arity);
3109 for (
unsigned i = 0; i < arity; i++) {
3111 args[i] = domain[i];
3115 return func_decl(*
this, f);
Referenced by context::recfun(), and z3::recfun().
◆ seq_sort()
Return a sequence sort over base sort s
.
Definition at line 2970 of file z3++.h.
◆ set() [1/3]
void set |
( |
char const * |
param, |
|
|
bool |
value |
|
) |
| |
|
inline |
Update global parameter param
with Boolean value
.
Definition at line 210 of file z3++.h.
◆ set() [2/3]
void set |
( |
char const * |
param, |
|
|
char const * |
value |
|
) |
| |
|
inline |
Update global parameter param
with string value
.
Definition at line 206 of file z3++.h.
◆ set() [3/3]
void set |
( |
char const * |
param, |
|
|
int |
value |
|
) |
| |
|
inline |
Update global parameter param
with Integer value
.
Definition at line 214 of file z3++.h.
215 std::ostringstream oss;
◆ set_enable_exceptions()
void set_enable_exceptions |
( |
bool |
f | ) |
|
|
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 199 of file z3++.h.
199 { m_enable_exceptions = f; }
◆ set_rounding_mode()
Sets RoundingMode of FloatingPoints.
Definition at line 2997 of file z3++.h.
2997 { m_rounding_mode = rm; }
◆ str_symbol()
symbol str_symbol |
( |
char const * |
s | ) |
|
|
inline |
◆ string_sort()
Return the sort for ASCII strings.
Definition at line 2969 of file z3++.h.
◆ string_val() [1/3]
expr string_val |
( |
char const * |
s | ) |
|
|
inline |
◆ string_val() [2/3]
expr string_val |
( |
char const * |
s, |
|
|
unsigned |
n |
|
) |
| |
|
inline |
◆ string_val() [3/3]
expr string_val |
( |
std::string const & |
s | ) |
|
|
inline |
◆ tuple_sort()
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 3015 of file z3++.h.
3016 array<Z3_symbol> _names(n);
3017 array<Z3_sort> _sorts(n);
3018 for (
unsigned i = 0; i < n; i++) { _names[i] =
Z3_mk_string_symbol(*
this, names[i]); _sorts[i] = sorts[i]; }
3019 array<Z3_func_decl> _projs(n);
3022 sort _ignore_s =
to_sort(*
this,
Z3_mk_tuple_sort(*
this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3024 for (
unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*
this, _projs[i])); }
3025 return func_decl(*
this, tuple);
◆ uninterpreted_sort() [1/2]
sort uninterpreted_sort |
( |
char const * |
name | ) |
|
|
inline |
create an uninterpreted sort with the name given by the string or symbol.
Definition at line 3028 of file z3++.h.
◆ uninterpreted_sort() [2/2]
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)
create a bit-vector numeral from a vector of Booleans.
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
sort int_sort()
Return the integer sort.
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
expr range(expr const &lo, expr const &hi)
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
expr constant(symbol const &name, sort const &s)
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)
Create a string constant out of the string that is passed in.
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
bool enable_exceptions() const
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
sort to_sort(context &c, Z3_sort s)
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a float.
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a double.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
sort real_sort()
Return the Real sort.
ast_vector_tpl< expr > expr_vector
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
void check_context(object const &a, object const &b)
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
sort bool_sort()
Return the Boolean sort.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.