Z3
Public Member Functions | Friends
context Class Reference
C++ API

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 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 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 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, 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 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 scoped_context
 

Detailed Description

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

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

Constructor & Destructor Documentation

context ( )
inline

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

180 { config c; init(c); }
context ( config &  c)
inline

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

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

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

182 { if (m_ctx) Z3_del_context(m_ctx); }
Z3_del_context
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 3288 of file z3++.h.

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

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

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

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

3433 { return constant(name, bool_sort()); }
z3::context::bool_sort
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:3264
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
sort bool_sort ( )
inline

Return the Boolean sort.

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

Referenced by context::bool_const().

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

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

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

3456 { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
Z3_mk_true
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_mk_false
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 3437 of file z3++.h.

3437 { return constant(name, bv_sort(sz)); }
z3::context::bv_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:3267
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
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 3267 of file z3++.h.

Referenced by context::bv_const(), and context::bv_val().

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

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

3471 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
z3::context::bv_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:3267
Z3_mk_int
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

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

3472 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_unsigned_int
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::context::bv_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:3267
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr bv_val ( int64_t  n,
unsigned  sz 
)
inline

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

3473 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_int64
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::context::bv_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:3267
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr bv_val ( uint64_t  n,
unsigned  sz 
)
inline

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

3474 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
z3::context::bv_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:3267
Z3_mk_unsigned_int64
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr bv_val ( char const *  n,
unsigned  sz 
)
inline

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

3475 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
z3::context::bv_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:3267
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_numeral
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 3476 of file z3++.h.

3476  {
3477  array<bool> _bits(n);
3478  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3479  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3480  }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_bv_numeral
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 3269 of file z3++.h.

3269 { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_char_sort
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 188 of file z3++.h.

Referenced by context::array_sort(), context::bool_sort(), context::bv_sort(), context::bv_val(), context::char_sort(), object::check_error(), context::check_parser_error(), z3::concat(), context::constant(), 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(), func_decl::operator()(), context::parse_file(), context::parse_string(), 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(), and context::tuple_sort().

188  {
189  Z3_error_code e = Z3_get_error_code(m_ctx);
190  if (e != Z3_OK && enable_exceptions())
191  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
192  return e;
193  }
Z3_get_error_msg
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:100
Z3_OK
Definition: z3_api.h:1370
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1368
z3::context::enable_exceptions
bool enable_exceptions() const
Definition: z3++.h:208
Z3_get_error_code
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 195 of file z3++.h.

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

195  {
196  check_error();
197  }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr constant ( symbol const &  name,
sort const &  s 
)
inline

Definition at line 3427 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().

3427  {
3428  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3429  check_error();
3430  return expr(*this, r);
3431  }
Z3_mk_const
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr constant ( char const *  name,
sort const &  s 
)
inline

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

3432 { return constant(str_symbol(name), s); }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
bool enable_exceptions ( ) const
inline

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

Referenced by context::check_error().

208 { 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 3293 of file z3++.h.

3293  {
3294  array<Z3_symbol> _enum_names(n);
3295  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3296  array<Z3_func_decl> _cs(n);
3297  array<Z3_func_decl> _ts(n);
3298  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3299  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3300  check_error();
3301  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3302  return s;
3303  }
Z3_mk_string_symbol
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_enumeration_sort
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.
z3::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2039
expr fpa_const ( char const *  name,
unsigned  ebits,
unsigned  sbits 
)
inline

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

3438 { return constant(name, fpa_sort(ebits, sbits)); }
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
z3::context::fpa_sort
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 3441 of file z3++.h.

3441 { return constant(name, fpa_sort<precision>()); }
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
expr fpa_inf ( sort const &  s,
bool  sgn 
)
inline

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

3485 { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_fpa_inf
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 3484 of file z3++.h.

3484 { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_fpa_nan
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 3445 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().

3445  {
3446  switch (m_rounding_mode) {
3447  case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3448  case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3449  case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3450  case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3451  case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3452  default: return expr(*this);
3453  }
3454  }
Z3_mk_fpa_rtz
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
z3::RTN
Definition: z3++.h:140
Z3_mk_fpa_rne
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Z3_mk_fpa_rtn
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode...
Z3_mk_fpa_rtp
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode...
z3::RNA
Definition: z3++.h:137
Z3_mk_fpa_rna
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
z3::RTZ
Definition: z3++.h:141
z3::RTP
Definition: z3++.h:139
z3::RNE
Definition: z3++.h:138
sort fpa_rounding_mode_sort ( )
inline

Return a RoundingMode sort.

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

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

3272 { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
Z3_mk_fpa_sort
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
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 3275 of file z3++.h.

Referenced by context::fpa_sort().

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

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

Referenced by context::fpa_sort().

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

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

Referenced by context::fpa_sort().

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

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

Referenced by context::fpa_sort().

3284 { return fpa_sort(15, 113); }
z3::context::fpa_sort
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 3482 of file z3++.h.

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

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

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

3483 { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_fpa_numeral_float
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 3325 of file z3++.h.

Referenced by z3::function().

3325  {
3326  array<Z3_sort> args(arity);
3327  for (unsigned i = 0; i < arity; i++) {
3328  check_context(domain[i], range);
3329  args[i] = domain[i];
3330  }
3331  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3332  check_error();
3333  return func_decl(*this, f);
3334  }
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
func_decl function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3336  {
3337  return function(range.ctx().str_symbol(name), arity, domain, range);
3338  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
z3::object::ctx
context & ctx() const
Definition: z3++.h:428
func_decl function ( symbol const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

3340  {
3341  array<Z3_sort> args(domain.size());
3342  for (unsigned i = 0; i < domain.size(); i++) {
3343  check_context(domain[i], range);
3344  args[i] = domain[i];
3345  }
3346  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3347  check_error();
3348  return func_decl(*this, f);
3349  }
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
func_decl function ( char const *  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

3351  {
3352  return function(range.ctx().str_symbol(name), domain, range);
3353  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
z3::object::ctx
context & ctx() const
Definition: z3++.h:428
func_decl function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

3356  {
3357  check_context(domain, range);
3358  Z3_sort args[1] = { domain };
3359  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3360  check_error();
3361  return func_decl(*this, f);
3362  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3364  {
3365  check_context(d1, range); check_context(d2, range);
3366  Z3_sort args[2] = { d1, d2 };
3367  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3368  check_error();
3369  return func_decl(*this, f);
3370  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

3372  {
3373  check_context(d1, range); check_context(d2, range); check_context(d3, range);
3374  Z3_sort args[3] = { d1, d2, d3 };
3375  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3376  check_error();
3377  return func_decl(*this, f);
3378  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
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 3380 of file z3++.h.

3380  {
3381  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
3382  Z3_sort args[4] = { d1, d2, d3, d4 };
3383  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3384  check_error();
3385  return func_decl(*this, f);
3386  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
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 3388 of file z3++.h.

3388  {
3389  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
3390  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3391  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3392  check_error();
3393  return func_decl(*this, f);
3394  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
Z3_mk_func_decl
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr int_const ( char const *  name)
inline

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

3434 { return constant(name, int_sort()); }
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
z3::context::int_sort
sort int_sort()
Return the integer sort.
Definition: z3++.h:3265
sort int_sort ( )
inline

Return the integer sort.

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

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

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

Create a Z3 symbol based on the given integer.

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

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

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

Referenced by z3::abs().

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

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

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

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

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

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

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

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

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

230 { Z3_interrupt(m_ctx); }
Z3_interrupt
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 3492 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().

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

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

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

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

3811  {
3812  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3813  check_error();
3814  return expr_vector(*this, r);
3815  }
Z3_parse_smtlib2_file
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
expr_vector parse_file ( char const *  s,
sort_vector const &  sorts,
func_decl_vector const &  decls 
)
inline

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

3834  {
3835  array<Z3_symbol> sort_names(sorts.size());
3836  array<Z3_symbol> decl_names(decls.size());
3837  array<Z3_sort> sorts1(sorts);
3838  array<Z3_func_decl> decls1(decls);
3839  for (unsigned i = 0; i < sorts.size(); ++i) {
3840  sort_names[i] = sorts[i].name();
3841  }
3842  for (unsigned i = 0; i < decls.size(); ++i) {
3843  decl_names[i] = decls[i].name();
3844  }
3845  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3846  check_error();
3847  return expr_vector(*this, r);
3848  }
Z3_parse_smtlib2_file
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
expr_vector parse_string ( char const *  s)
inline

parsing

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

3805  {
3806  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3807  check_error();
3808  return expr_vector(*this, r);
3809 
3810  }
Z3_parse_smtlib2_string
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
expr_vector parse_string ( char const *  s,
sort_vector const &  sorts,
func_decl_vector const &  decls 
)
inline

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

3817  {
3818  array<Z3_symbol> sort_names(sorts.size());
3819  array<Z3_symbol> decl_names(decls.size());
3820  array<Z3_sort> sorts1(sorts);
3821  array<Z3_func_decl> decls1(decls);
3822  for (unsigned i = 0; i < sorts.size(); ++i) {
3823  sort_names[i] = sorts[i].name();
3824  }
3825  for (unsigned i = 0; i < decls.size(); ++i) {
3826  decl_names[i] = decls[i].name();
3827  }
3828 
3829  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3830  check_error();
3831  return expr_vector(*this, r);
3832  }
Z3_parse_smtlib2_string
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
sort re_sort ( sort &  seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

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

3271 { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_re_sort
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 3435 of file z3++.h.

3435 { return constant(name, real_sort()); }
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
z3::context::real_sort
sort real_sort()
Return the Real sort.
Definition: z3++.h:3266
sort real_sort ( )
inline

Return the Real sort.

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

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

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

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

Referenced by z3::abs().

3464 { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); }
Z3_mk_real
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr real_val ( int  n)
inline

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

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

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

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

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

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

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

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

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

3469 { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
z3::context::real_sort
sort real_sort()
Return the Real sort.
Definition: z3++.h:3266
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_numeral
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  f,
expr_vector const &  args,
expr const &  body 
)
inline

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

3421  {
3422  check_context(f, args); check_context(f, body);
3423  array<Z3_ast> vars(args);
3424  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3425  }
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
Z3_add_rec_def
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 3396 of file z3++.h.

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

3396  {
3397  array<Z3_sort> args(arity);
3398  for (unsigned i = 0; i < arity; i++) {
3399  check_context(domain[i], range);
3400  args[i] = domain[i];
3401  }
3402  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3403  check_error();
3404  return func_decl(*this, f);
3405 
3406  }
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:432
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
Z3_mk_rec_func_decl
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 ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3408  {
3409  return recfun(str_symbol(name), arity, domain, range);
3410  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3396
func_decl recfun ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

3412  {
3413  return recfun(str_symbol(name), 1, &d1, range);
3414  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3396
func_decl recfun ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3416  {
3417  sort dom[2] = { d1, d2 };
3418  return recfun(str_symbol(name), 2, dom, range);
3419  }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3261
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3794
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3396
sort seq_sort ( sort &  s)
inline

Return a sequence sort over base sort s.

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

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

Update global parameter param with string value.

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

213 { Z3_update_param_value(m_ctx, param, value); }
Z3_update_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 217 of file z3++.h.

217 { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
Z3_update_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,
int  value 
)
inline

Update global parameter param with Integer value.

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

221  {
222  auto str = std::to_string(value);
223  Z3_update_param_value(m_ctx, param, str.c_str());
224  }
Z3_update_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_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 206 of file z3++.h.

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

Sets RoundingMode of FloatingPoints.

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

3443 { m_rounding_mode = rm; }
symbol str_symbol ( char const *  s)
inline

Create a Z3 symbol based on the given string.

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

Referenced by context::constant(), context::function(), context::recfun(), and solver::solver().

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

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

3436 { return constant(name, string_sort()); }
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3427
z3::context::string_sort
sort string_sort()
Return the sort for Unicode strings.
Definition: z3++.h:3268
sort string_sort ( )
inline

Return the sort for Unicode strings.

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

Referenced by context::string_const().

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

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

3488 { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
Z3_mk_string
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr string_val ( char const *  s,
unsigned  n 
)
inline

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

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

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

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

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

3490 { Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)s.c_str()); check_error(); return expr(*this, r); }
Z3_mk_u32string
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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
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 3304 of file z3++.h.

3304  {
3305  array<Z3_symbol> _names(n);
3306  array<Z3_sort> _sorts(n);
3307  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3308  array<Z3_func_decl> _projs(n);
3309  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3310  Z3_func_decl tuple;
3311  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3312  check_error();
3313  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3314  return func_decl(*this, tuple);
3315  }
Z3_mk_tuple_sort
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_mk_string_symbol
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
z3::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2039
sort uninterpreted_sort ( char const *  name)
inline

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

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

3317  {
3318  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3319  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3320  }
Z3_mk_string_symbol
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_mk_uninterpreted_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::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2039
sort uninterpreted_sort ( symbol const &  name)
inline

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

3321  {
3322  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3323  }
Z3_mk_uninterpreted_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::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2039

Friends And Related Function Documentation

friend class scoped_context
friend

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

Generated on Mon Dec 20 2021 20:11:57 for Z3 by   doxygen 1.8.10