Z3
Public Member Functions | Friends
context Class Reference

A Context manages all other Z3 objects, global configuration options, etc. More...

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. 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 char_sort ()
 Return the sort for Unicode characters. More...
 
sort string_sort ()
 Return the sort for Unicode 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_sort ()
 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 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 numer of constructors of the datatype cs - the n constructors used to define the datatype. More...
 
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. More...
 
sort datatype_sort (symbol const &name)
 a reference to a recursively defined datatype. Expect that it gets defined as a datatype. 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 (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>. More...
 
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. More...
 
expr constant (char const *name, sort const &s)
 
expr bool_const (char const *name)
 create uninterpreted constants of a given sort. More...
 
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. More...
 
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 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 ()
 

Friends

class user_propagator_base
 

Detailed Description

A Context manages all other Z3 objects, global configuration options, etc.

Definition at line 160 of file z3++.h.

Constructor & Destructor Documentation

context ( )
inline

Definition at line 184 of file z3++.h.

184 { config c; init(c); }
context ( config c)
inline

Definition at line 185 of file z3++.h.

185 { init(c); }
~context ( )
inline

Definition at line 186 of file z3++.h.

186 { if (m_ctx) Z3_del_context(m_ctx); }
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.

Member Function Documentation

sort array_sort ( sort  d,
sort  r 
)
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 3454 of file z3++.h.

3454 { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort array_sort ( sort_vector const &  d,
sort  r 
)
inline

Definition at line 3455 of file z3++.h.

3455  {
3456  array<Z3_sort> dom(d);
3457  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3458  }
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.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bool_const ( char const *  name)
inline

create uninterpreted constants of a given sort.

Definition at line 3717 of file z3++.h.

3717 { return constant(name, bool_sort()); }
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:3430
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort bool_sort ( )
inline

Return the Boolean sort.

Definition at line 3430 of file z3++.h.

Referenced by context::bool_const().

3430 { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bool_val ( bool  b)
inline

Definition at line 3740 of file z3++.h.

Referenced by goal::as_expr(), user_propagator_base::conflict(), z3::implies(), z3::mk_xor(), z3::operator&&(), z3::operator||(), and solver::to_smt2().

3740 { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
expr bv_const ( char const *  name,
unsigned  sz 
)
inline

Definition at line 3721 of file z3++.h.

3721 { return constant(name, bv_sort(sz)); }
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3433
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort bv_sort ( unsigned  sz)
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(), and context::bv_val().

3433 { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bv_val ( int  n,
unsigned  sz 
)
inline

Definition at line 3755 of file z3++.h.

3755 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3433
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

Definition at line 3756 of file z3++.h.

3756 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
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.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3433
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bv_val ( int64_t  n,
unsigned  sz 
)
inline

Definition at line 3757 of file z3++.h.

3757 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
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.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3433
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bv_val ( uint64_t  n,
unsigned  sz 
)
inline

Definition at line 3758 of file z3++.h.

3758 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3433
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.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr bv_val ( char const *  n,
unsigned  sz 
)
inline

Definition at line 3759 of file z3++.h.

3759 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3433
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
expr bv_val ( unsigned  n,
bool const *  bits 
)
inline

Definition at line 3760 of file z3++.h.

3760  {
3761  array<bool> _bits(n);
3762  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3763  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3764  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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.
sort char_sort ( )
inline

Return the sort for Unicode characters.

Definition at line 3435 of file z3++.h.

3435 { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
Z3_error_code check_error ( ) const
inline

Auxiliary method used to check for API usage errors.

Definition at line 192 of file z3++.h.

Referenced by context::array_sort(), expr::bit2bool(), context::bool_sort(), context::bv_sort(), context::bv_val(), context::char_sort(), object::check_error(), context::check_parser_error(), z3::concat(), 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::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::num_val(), on_clause::on_clause(), func_decl::operator()(), context::parse_file(), context::parse_string(), z3::re_diff(), 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::to_expr(), z3::to_func_decl(), z3::to_sort(), context::tuple_sort(), context::user_propagate_function(), and context::variable().

192  {
193  Z3_error_code e = Z3_get_error_code(m_ctx);
194  if (e != Z3_OK && enable_exceptions())
195  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
196  return e;
197  }
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
#define Z3_THROW(x)
Definition: z3++.h:103
Definition: z3_api.h:1344
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1342
bool enable_exceptions() const
Definition: z3++.h:212
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
void check_parser_error ( ) const
inline

Definition at line 199 of file z3++.h.

Referenced by solver::from_file(), and solver::from_string().

199  {
200  check_error();
201  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr constant ( symbol const &  name,
sort const &  s 
)
inline

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::int_const(), context::real_const(), and context::string_const().

3706  {
3707  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3708  check_error();
3709  return expr(*this, r);
3710  }
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr constant ( char const *  name,
sort const &  s 
)
inline

Definition at line 3711 of file z3++.h.

3711 { return constant(str_symbol(name), s); }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort datatype ( symbol const &  name,
constructors const &  cs 
)
inline

Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the numer 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.

3544  {
3545  array<Z3_constructor> _cs(cs.size());
3546  for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
3547  Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
3548  check_error();
3549  return sort(*this, s);
3550  }
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort datatype_sort ( symbol const &  name)
inline

a reference to a recursively defined datatype. Expect that it gets defined as a datatype.

Definition at line 3568 of file z3++.h.

3568  {
3569  Z3_sort s = Z3_mk_datatype_sort(*this, name);
3570  check_error();
3571  return sort(*this, s);
3572  }
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort_vector datatypes ( unsigned  n,
symbol const *  names,
constructor_list *const *  cons 
)
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.

3554  {
3555  sort_vector result(*this);
3556  array<Z3_symbol> _names(n);
3557  array<Z3_sort> _sorts(n);
3558  array<Z3_constructor_list> _cons(n);
3559  for (unsigned i = 0; i < n; ++i)
3560  _names[i] = names[i], _cons[i] = *cons[i];
3561  Z3_mk_datatypes(*this, n, _names.ptr(), _sorts.ptr(), _cons.ptr());
3562  for (unsigned i = 0; i < n; ++i)
3563  result.push_back(sort(*this, _sorts[i]));
3564  return result;
3565  }
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:77
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
bool enable_exceptions ( ) const
inline

Definition at line 212 of file z3++.h.

Referenced by context::check_error().

212 { return m_enable_exceptions; }
sort enumeration_sort ( char const *  name,
unsigned  n,
char const *const *  enum_names,
func_decl_vector cs,
func_decl_vector ts 
)
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.

3459  {
3460  array<Z3_symbol> _enum_names(n);
3461  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3462  array<Z3_func_decl> _cs(n);
3463  array<Z3_func_decl> _ts(n);
3464  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3465  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3466  check_error();
3467  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3468  return s;
3469  }
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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 to_sort(context &c, Z3_sort s)
Definition: z3++.h:2115
expr fpa_const ( char const *  name,
unsigned  ebits,
unsigned  sbits 
)
inline

Definition at line 3722 of file z3++.h.

3722 { return constant(name, fpa_sort(ebits, sbits)); }
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
expr fpa_const ( char const *  name)
inline

Definition at line 3725 of file z3++.h.

3725 { return constant(name, fpa_sort<precision>()); }
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
expr fpa_inf ( sort const &  s,
bool  sgn 
)
inline

Definition at line 3769 of file z3++.h.

3769 { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
expr fpa_nan ( sort const &  s)
inline

Definition at line 3768 of file z3++.h.

3768 { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
expr fpa_rounding_mode ( )
inline

Definition at line 3729 of file z3++.h.

Referenced by z3::fpa_to_fpa(), z3::fpa_to_sbv(), z3::fpa_to_ubv(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::round_fpa_to_closest_integer(), z3::sbv_to_fpa(), and z3::ubv_to_fpa().

3729  {
3730  switch (m_rounding_mode) {
3731  case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3732  case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3733  case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3734  case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3735  case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3736  default: return expr(*this);
3737  }
3738  }
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Definition: z3++.h:143
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_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode...
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode...
Definition: z3++.h:140
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: z3++.h:144
Definition: z3++.h:142
Definition: z3++.h:141
sort fpa_rounding_mode_sort ( )
inline

Return a RoundingMode sort.

Definition at line 3452 of file z3++.h.

3452 { Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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 3438 of file z3++.h.

3438 { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort fpa_sort ( )

Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

Referenced by context::fpa_const().

sort fpa_sort ( )
inline

Definition at line 3441 of file z3++.h.

Referenced by context::fpa_sort().

3441 { return fpa_sort(5, 11); }
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
sort fpa_sort ( )
inline

Definition at line 3444 of file z3++.h.

Referenced by context::fpa_sort().

3444 { return fpa_sort(8, 24); }
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
sort fpa_sort ( )
inline

Definition at line 3447 of file z3++.h.

Referenced by context::fpa_sort().

3447 { return fpa_sort(11, 53); }
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
sort fpa_sort ( )
inline

Definition at line 3450 of file z3++.h.

Referenced by context::fpa_sort().

3450 { return fpa_sort(15, 113); }
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
expr fpa_val ( double  n)
inline

Definition at line 3766 of file z3++.h.

Referenced by z3::operator!=(), and z3::operator==().

3766 { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr fpa_val ( float  n)
inline

Definition at line 3767 of file z3++.h.

3767 { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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.
func_decl function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

Definition at line 3583 of file z3++.h.

Referenced by z3::function().

3583  {
3584  array<Z3_sort> args(arity);
3585  for (unsigned i = 0; i < arity; i++) {
3586  check_context(domain[i], range);
3587  args[i] = domain[i];
3588  }
3589  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3590  check_error();
3591  return func_decl(*this, f);
3592  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

Definition at line 3594 of file z3++.h.

3594  {
3595  return function(range.ctx().str_symbol(name), arity, domain, range);
3596  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
context & ctx() const
Definition: z3++.h:473
func_decl function ( symbol const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

Definition at line 3598 of file z3++.h.

3598  {
3599  array<Z3_sort> args(domain.size());
3600  for (unsigned i = 0; i < domain.size(); i++) {
3601  check_context(domain[i], range);
3602  args[i] = domain[i];
3603  }
3604  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3605  check_error();
3606  return func_decl(*this, f);
3607  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl function ( char const *  name,
sort_vector const &  domain,
sort const &  range 
)
inline

Definition at line 3609 of file z3++.h.

3609  {
3610  return function(range.ctx().str_symbol(name), domain, range);
3611  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
context & ctx() const
Definition: z3++.h:473
func_decl function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

Definition at line 3614 of file z3++.h.

3614  {
3615  check_context(domain, range);
3616  Z3_sort args[1] = { domain };
3617  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3618  check_error();
3619  return func_decl(*this, f);
3620  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

Definition at line 3622 of file z3++.h.

3622  {
3624  Z3_sort args[2] = { d1, d2 };
3625  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3626  check_error();
3627  return func_decl(*this, f);
3628  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

Definition at line 3630 of file z3++.h.

3630  {
3632  Z3_sort args[3] = { d1, d2, d3 };
3633  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3634  check_error();
3635  return func_decl(*this, f);
3636  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  d4,
sort const &  range 
)
inline

Definition at line 3638 of file z3++.h.

3638  {
3640  Z3_sort args[4] = { d1, d2, d3, d4 };
3641  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3642  check_error();
3643  return func_decl(*this, f);
3644  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  d4,
sort const &  d5,
sort const &  range 
)
inline

Definition at line 3646 of file z3++.h.

3646  {
3648  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3649  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3650  check_error();
3651  return func_decl(*this, f);
3652  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr int_const ( char const *  name)
inline

Definition at line 3718 of file z3++.h.

3718 { return constant(name, int_sort()); }
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort int_sort()
Return the integer sort.
Definition: z3++.h:3431
sort int_sort ( )
inline

Return the integer sort.

Definition at line 3431 of file z3++.h.

Referenced by context::int_const(), and context::int_val().

3431 { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
symbol int_symbol ( int  n)
inline

Create a Z3 symbol based on the given integer.

Definition at line 3428 of file z3++.h.

3428 { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr int_val ( int  n)
inline

Definition at line 3742 of file z3++.h.

Referenced by z3::abs().

3742 { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort int_sort()
Return the integer sort.
Definition: z3++.h:3431
expr int_val ( unsigned  n)
inline

Definition at line 3743 of file z3++.h.

3743 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort int_sort()
Return the integer sort.
Definition: z3++.h:3431
expr int_val ( int64_t  n)
inline

Definition at line 3744 of file z3++.h.

3744 { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
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.
Definition: z3++.h:192
sort int_sort()
Return the integer sort.
Definition: z3++.h:3431
expr int_val ( uint64_t  n)
inline

Definition at line 3745 of file z3++.h.

3745 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
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.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort int_sort()
Return the integer sort.
Definition: z3++.h:3431
expr int_val ( char const *  n)
inline

Definition at line 3746 of file z3++.h.

3746 { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
sort int_sort()
Return the integer sort.
Definition: z3++.h:3431
void interrupt ( )
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.

234 { Z3_interrupt(m_ctx); }
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
expr num_val ( int  n,
sort const &  s 
)
inline

Definition at line 3776 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::sge(), z3::sgt(), 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().

3776 { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
operator Z3_context ( ) const
inline

Definition at line 187 of file z3++.h.

187 { return m_ctx; }
expr_vector parse_file ( char const *  file)
inline

Definition at line 4102 of file z3++.h.

4102  {
4103  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
4104  check_error();
4105  return expr_vector(*this, r);
4106  }
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.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr_vector parse_file ( char const *  s,
sort_vector const &  sorts,
func_decl_vector const &  decls 
)
inline

Definition at line 4125 of file z3++.h.

4125  {
4126  array<Z3_symbol> sort_names(sorts.size());
4127  array<Z3_symbol> decl_names(decls.size());
4128  array<Z3_sort> sorts1(sorts);
4129  array<Z3_func_decl> decls1(decls);
4130  for (unsigned i = 0; i < sorts.size(); ++i) {
4131  sort_names[i] = sorts[i].name();
4132  }
4133  for (unsigned i = 0; i < decls.size(); ++i) {
4134  decl_names[i] = decls[i].name();
4135  }
4136  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
4137  check_error();
4138  return expr_vector(*this, r);
4139  }
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.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr_vector parse_string ( char const *  s)
inline

parsing

Definition at line 4096 of file z3++.h.

4096  {
4097  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
4098  check_error();
4099  return expr_vector(*this, r);
4100 
4101  }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr_vector parse_string ( char const *  s,
sort_vector const &  sorts,
func_decl_vector const &  decls 
)
inline

Definition at line 4108 of file z3++.h.

4108  {
4109  array<Z3_symbol> sort_names(sorts.size());
4110  array<Z3_symbol> decl_names(decls.size());
4111  array<Z3_sort> sorts1(sorts);
4112  array<Z3_func_decl> decls1(decls);
4113  for (unsigned i = 0; i < sorts.size(); ++i) {
4114  sort_names[i] = sorts[i].name();
4115  }
4116  for (unsigned i = 0; i < decls.size(); ++i) {
4117  decl_names[i] = decls[i].name();
4118  }
4119 
4120  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
4121  check_error();
4122  return expr_vector(*this, r);
4123  }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
sort re_sort ( sort seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

Definition at line 3437 of file z3++.h.

3437 { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
expr real_const ( char const *  name)
inline

Definition at line 3719 of file z3++.h.

3719 { return constant(name, real_sort()); }
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort real_sort()
Return the Real sort.
Definition: z3++.h:3432
sort real_sort ( )
inline

Return the Real sort.

Definition at line 3432 of file z3++.h.

Referenced by context::real_const(), and context::real_val().

3432 { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr real_val ( int  n)
inline

Definition at line 3749 of file z3++.h.

Referenced by z3::abs().

3749 { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
sort real_sort()
Return the Real sort.
Definition: z3++.h:3432
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr real_val ( unsigned  n)
inline

Definition at line 3750 of file z3++.h.

3750 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
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.
sort real_sort()
Return the Real sort.
Definition: z3++.h:3432
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr real_val ( int64_t  n)
inline

Definition at line 3751 of file z3++.h.

3751 { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
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.
sort real_sort()
Return the Real sort.
Definition: z3++.h:3432
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr real_val ( uint64_t  n)
inline

Definition at line 3752 of file z3++.h.

3752 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
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.
sort real_sort()
Return the Real sort.
Definition: z3++.h:3432
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr real_val ( int64_t  n,
int64_t  d 
)
inline

Definition at line 3748 of file z3++.h.

3748 { Z3_ast r = Z3_mk_real_int64(m_ctx, n, d); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)
Create a real from a fraction of int64.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr real_val ( char const *  n)
inline

Definition at line 3753 of file z3++.h.

3753 { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
sort real_sort()
Return the Real sort.
Definition: z3++.h:3432
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
void recdef ( func_decl  decl,
expr_vector const &  args,
expr const &  body 
)
inline

add function definition body to declaration decl. decl needs to be declared using context::<recfun>.

Parameters
decl
args
body

Definition at line 3692 of file z3++.h.

3692  {
3693  check_context(f, args); check_context(f, body);
3694  array<Z3_ast> vars(args);
3695  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3696  }
void check_context(object const &a, object const &b)
Definition: z3++.h:477
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.
func_decl recfun ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

Definition at line 3654 of file z3++.h.

Referenced by context::recfun(), and z3::recfun().

3654  {
3655  array<Z3_sort> args(arity);
3656  for (unsigned i = 0; i < arity; i++) {
3657  check_context(domain[i], range);
3658  args[i] = domain[i];
3659  }
3660  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3661  check_error();
3662  return func_decl(*this, f);
3663 
3664  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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.
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 
)
inline

Definition at line 3674 of file z3++.h.

3674  {
3675  return recfun(str_symbol(name), domain, range);
3676 
3677  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3654
func_decl recfun ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

Definition at line 3679 of file z3++.h.

3679  {
3680  return recfun(str_symbol(name), arity, domain, range);
3681  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3654
func_decl recfun ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

Definition at line 3683 of file z3++.h.

3683  {
3684  return recfun(str_symbol(name), 1, &d1, range);
3685  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3654
func_decl recfun ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

Definition at line 3687 of file z3++.h.

3687  {
3688  sort dom[2] = { d1, d2 };
3689  return recfun(str_symbol(name), 2, dom, range);
3690  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3427
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3654
sort seq_sort ( sort s)
inline

Return a sequence sort over base sort s.

Definition at line 3436 of file z3++.h.

3436 { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
void set ( char const *  param,
char const *  value 
)
inline

Update global parameter param with string value.

Definition at line 217 of file z3++.h.

217 { Z3_update_param_value(m_ctx, param, value); }
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.
void set ( char const *  param,
bool  value 
)
inline

Update global parameter param with Boolean value.

Definition at line 221 of file z3++.h.

221 { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
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.
void set ( char const *  param,
int  value 
)
inline

Update global parameter param with Integer value.

Definition at line 225 of file z3++.h.

225  {
226  auto str = std::to_string(value);
227  Z3_update_param_value(m_ctx, param, str.c_str());
228  }
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.
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 210 of file z3++.h.

210 { m_enable_exceptions = f; }
void set_rounding_mode ( rounding_mode  rm)
inline

Sets RoundingMode of FloatingPoints.

Definition at line 3727 of file z3++.h.

3727 { m_rounding_mode = rm; }
symbol str_symbol ( char const *  s)
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::recfun(), and solver::solver().

3427 { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr string_const ( char const *  name)
inline

Definition at line 3720 of file z3++.h.

3720 { return constant(name, string_sort()); }
expr constant(symbol const &name, sort const &s)
create an uninterpreted constant.
Definition: z3++.h:3706
sort string_sort()
Return the sort for Unicode strings.
Definition: z3++.h:3434
sort string_sort ( )
inline

Return the sort for Unicode strings.

Definition at line 3434 of file z3++.h.

Referenced by context::string_const().

3434 { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr string_val ( char const *  s)
inline

Definition at line 3772 of file z3++.h.

3772 { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
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 The string may contain escape encoding f...
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr string_val ( char const *  s,
unsigned  n 
)
inline

Definition at line 3771 of file z3++.h.

3771 { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr string_val ( std::string const &  s)
inline

Definition at line 3773 of file z3++.h.

3773 { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
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 The string may contain escape encoding f...
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr string_val ( std::u32string const &  s)
inline

Definition at line 3774 of file z3++.h.

3774 { Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)s.c_str()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[])
Create a string constant out of the string that is passed in It takes the length of the string as wel...
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
func_decl tuple_sort ( char const *  name,
unsigned  n,
char const *const *  names,
sort const *  sorts,
func_decl_vector projs 
)
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.

3470  {
3471  array<Z3_symbol> _names(n);
3472  array<Z3_sort> _sorts(n);
3473  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3474  array<Z3_func_decl> _projs(n);
3475  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3476  Z3_func_decl tuple;
3477  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3478  check_error();
3479  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3480  return func_decl(*this, tuple);
3481  }
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_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2115
sort uninterpreted_sort ( char const *  name)
inline

create an uninterpreted sort with the name given by the string or symbol.

Definition at line 3575 of file z3++.h.

3575  {
3576  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3577  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3578  }
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2115
sort uninterpreted_sort ( symbol const &  name)
inline

Definition at line 3579 of file z3++.h.

3579  {
3580  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3581  }
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2115
func_decl user_propagate_function ( symbol const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

Definition at line 3698 of file z3++.h.

3698  {
3699  check_context(domain, range);
3700  array<Z3_sort> domain1(domain);
3701  Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
3702  check_error();
3703  return func_decl(*this, f);
3704  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
context & ctx() const
Definition: z3++.h:473
void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
expr variable ( unsigned  index,
sort const &  s 
)
inline

create a de-Bruijn variable.

Definition at line 3712 of file z3++.h.

3712  {
3713  Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
3714  check_error();
3715  return expr(*this, r);
3716  }
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192

Friends And Related Function Documentation

friend class user_propagator_base
friend

Definition at line 162 of file z3++.h.