Z3
Public Member Functions
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 string_sort ()
 Return the sort for ASCII strings. More...
 
sort seq_sort (sort &s)
 Return a sequence sort over base sort s. More...
 
sort re_sort (sort &seq_sort)
 Return a regular expression sort over sequences seq_sort. More...
 
sort array_sort (sort d, sort r)
 Return an array sort for arrays from d to r. More...
 
sort array_sort (sort_vector const &d, sort r)
 
sort fpa_sort (unsigned ebits, unsigned sbits)
 Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,. More...
 
template<size_t precision>
sort fpa_sort ()
 Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128). More...
 
sort fpa_rounding_mode ()
 Return a RoundingMode sort. More...
 
void set_rounding_mode (rounding_mode rm)
 Sets RoundingMode of FloatingPoints. More...
 
sort enumeration_sort (char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts)
 Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters. The method stores in cs the constants corresponding to the enumerated elements, and in ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. More...
 
func_decl tuple_sort (char const *name, unsigned n, char const *const *names, sort const *sorts, func_decl_vector &projs)
 Return a tuple constructor. name is the name of the returned constructor, n are the number of arguments, names and sorts are their projected sorts. projs is an output parameter. It contains the set of projection functions. More...
 
sort uninterpreted_sort (char const *name)
 create an uninterpreted sort with the name given by the string or symbol. More...
 
sort uninterpreted_sort (symbol const &name)
 
func_decl function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (symbol const &name, sort_vector const &domain, sort const &range)
 
func_decl function (char const *name, sort_vector const &domain, sort const &range)
 
func_decl function (char const *name, sort const &domain, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
 
func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, sort const &domain, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
 
void recdef (func_decl, expr_vector const &args, expr const &body)
 
expr constant (symbol const &name, sort const &s)
 
expr constant (char const *name, sort const &s)
 
expr bool_const (char const *name)
 
expr int_const (char const *name)
 
expr real_const (char const *name)
 
expr bv_const (char const *name, unsigned sz)
 
expr fpa_const (char const *name, unsigned ebits, unsigned sbits)
 
template<size_t precision>
expr fpa_const (char const *name)
 
expr bool_val (bool b)
 
expr int_val (int n)
 
expr int_val (unsigned n)
 
expr int_val (int64_t n)
 
expr int_val (uint64_t n)
 
expr int_val (char const *n)
 
expr real_val (int n, int d)
 
expr real_val (int n)
 
expr real_val (unsigned n)
 
expr real_val (int64_t n)
 
expr real_val (uint64_t n)
 
expr real_val (char const *n)
 
expr bv_val (int n, unsigned sz)
 
expr bv_val (unsigned n, unsigned sz)
 
expr bv_val (int64_t n, unsigned sz)
 
expr bv_val (uint64_t n, unsigned sz)
 
expr bv_val (char const *n, unsigned sz)
 
expr bv_val (unsigned n, bool const *bits)
 
expr fpa_val (double n)
 
expr fpa_val (float n)
 
expr string_val (char const *s)
 
expr string_val (char const *s, unsigned n)
 
expr string_val (std::string const &s)
 
expr num_val (int n, sort const &s)
 
expr_vector parse_string (char const *s)
 parsing More...
 
expr_vector parse_file (char const *file)
 
expr_vector parse_string (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
 
expr_vector parse_file (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
 
template<>
sort fpa_sort ()
 
template<>
sort fpa_sort ()
 
template<>
sort fpa_sort ()
 
template<>
sort fpa_sort ()
 

Detailed Description

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

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

Constructor & Destructor Documentation

◆ context() [1/2]

context ( )
inline

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

170 { config c; init(c); }

◆ context() [2/2]

context ( config c)
inline

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

171 { init(c); }

◆ ~context()

~context ( )
inline

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

172 { Z3_del_context(m_ctx); }

Member Function Documentation

◆ array_sort() [1/2]

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 2942 of file z3++.h.

2942 { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }

◆ array_sort() [2/2]

sort array_sort ( sort_vector const &  d,
sort  r 
)
inline

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

2943  {
2944  array<Z3_sort> dom(d);
2945  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2946  }

◆ bool_const()

expr bool_const ( char const *  name)
inline

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

3087 { return constant(name, bool_sort()); }

◆ bool_sort()

sort bool_sort ( )
inline

Return the Boolean sort.

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

2908 { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }

Referenced by context::bool_const().

◆ bool_val()

expr bool_val ( bool  b)
inline

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

3096 { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }

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

◆ bv_const()

expr bv_const ( char const *  name,
unsigned  sz 
)
inline

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

3090 { return constant(name, bv_sort(sz)); }

◆ bv_sort()

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 2911 of file z3++.h.

2911 { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }

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

◆ bv_val() [1/6]

expr bv_val ( char const *  n,
unsigned  sz 
)
inline

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

3115 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ bv_val() [2/6]

expr bv_val ( int  n,
unsigned  sz 
)
inline

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

3111 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ bv_val() [3/6]

expr bv_val ( int64_t  n,
unsigned  sz 
)
inline

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

3113 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ bv_val() [4/6]

expr bv_val ( uint64_t  n,
unsigned  sz 
)
inline

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

3114 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ bv_val() [5/6]

expr bv_val ( unsigned  n,
bool const *  bits 
)
inline

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

3116  {
3117  array<bool> _bits(n);
3118  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3119  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3120  }

◆ bv_val() [6/6]

expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

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

3112 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ check_error()

Z3_error_code check_error ( ) const
inline

◆ check_parser_error()

void check_parser_error ( ) const
inline

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

185  {
186  check_error();
187  }

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

◆ constant() [1/2]

expr constant ( char const *  name,
sort const &  s 
)
inline

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

3086 { return constant(str_symbol(name), s); }

◆ constant() [2/2]

expr constant ( symbol const &  name,
sort const &  s 
)
inline

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

3081  {
3082  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3083  check_error();
3084  return expr(*this, r);
3085  }

Referenced by context::bool_const(), context::bv_const(), context::constant(), context::fpa_const(), context::int_const(), and context::real_const().

◆ enable_exceptions()

bool enable_exceptions ( ) const
inline

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

198 { return m_enable_exceptions; }

Referenced by context::check_error().

◆ enumeration_sort()

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 2947 of file z3++.h.

2947  {
2948  array<Z3_symbol> _enum_names(n);
2949  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2950  array<Z3_func_decl> _cs(n);
2951  array<Z3_func_decl> _ts(n);
2952  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2953  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2954  check_error();
2955  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2956  return s;
2957  }

◆ fpa_const() [1/2]

expr fpa_const ( char const *  name)
inline

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

3094 { return constant(name, fpa_sort<precision>()); }

◆ fpa_const() [2/2]

expr fpa_const ( char const *  name,
unsigned  ebits,
unsigned  sbits 
)
inline

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

3091 { return constant(name, fpa_sort(ebits, sbits)); }

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )
inline

Return a RoundingMode sort.

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

2929  {
2930  switch (m_rounding_mode) {
2931  case RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
2932  case RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
2933  case RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
2934  case RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
2935  case RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
2936  default: return sort(*this);
2937  }
2938  }

Referenced by expr::fpa_rounding_mode(), z3::operator*(), z3::operator+(), z3::operator-(), and z3::operator/().

◆ fpa_sort() [1/6]

sort fpa_sort ( )

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

Referenced by context::fpa_const().

◆ fpa_sort() [2/6]

sort fpa_sort ( )
inline

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

2918 { return fpa_sort(5, 11); }

Referenced by context::fpa_sort().

◆ fpa_sort() [3/6]

sort fpa_sort ( )
inline

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

2921 { return fpa_sort(8, 24); }

Referenced by context::fpa_sort().

◆ fpa_sort() [4/6]

sort fpa_sort ( )
inline

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

2924 { return fpa_sort(11, 53); }

Referenced by context::fpa_sort().

◆ fpa_sort() [5/6]

sort fpa_sort ( )
inline

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

2927 { return fpa_sort(15, 113); }

Referenced by context::fpa_sort().

◆ fpa_sort() [6/6]

sort fpa_sort ( unsigned  ebits,
unsigned  sbits 
)
inline

Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,.

Precondition
where ebits must be larger than 1 and sbits must be larger than 2.

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

2915 { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }

◆ fpa_val() [1/2]

expr fpa_val ( double  n)
inline

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

3122 { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ fpa_val() [2/2]

expr fpa_val ( float  n)
inline

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

3123 { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ function() [1/9]

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 3042 of file z3++.h.

3042  {
3044  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3045  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3046  check_error();
3047  return func_decl(*this, f);
3048  }

◆ function() [2/9]

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 3034 of file z3++.h.

3034  {
3036  Z3_sort args[4] = { d1, d2, d3, d4 };
3037  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3038  check_error();
3039  return func_decl(*this, f);
3040  }

◆ function() [3/9]

func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

3026  {
3028  Z3_sort args[3] = { d1, d2, d3 };
3029  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3030  check_error();
3031  return func_decl(*this, f);
3032  }

◆ function() [4/9]

func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3018  {
3020  Z3_sort args[2] = { d1, d2 };
3021  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3022  check_error();
3023  return func_decl(*this, f);
3024  }

◆ function() [5/9]

func_decl function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

3010  {
3011  check_context(domain, range);
3012  Z3_sort args[1] = { domain };
3013  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3014  check_error();
3015  return func_decl(*this, f);
3016  }

◆ function() [6/9]

func_decl function ( char const *  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

3005  {
3006  return function(range.ctx().str_symbol(name), domain, range);
3007  }

◆ function() [7/9]

func_decl function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

2990  {
2991  return function(range.ctx().str_symbol(name), arity, domain, range);
2992  }

◆ function() [8/9]

func_decl function ( symbol const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

2994  {
2995  array<Z3_sort> args(domain.size());
2996  for (unsigned i = 0; i < domain.size(); i++) {
2997  check_context(domain[i], range);
2998  args[i] = domain[i];
2999  }
3000  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3001  check_error();
3002  return func_decl(*this, f);
3003  }

◆ function() [9/9]

func_decl function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

2979  {
2980  array<Z3_sort> args(arity);
2981  for (unsigned i = 0; i < arity; i++) {
2982  check_context(domain[i], range);
2983  args[i] = domain[i];
2984  }
2985  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2986  check_error();
2987  return func_decl(*this, f);
2988  }

Referenced by z3::function().

◆ int_const()

expr int_const ( char const *  name)
inline

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

3088 { return constant(name, int_sort()); }

◆ int_sort()

sort int_sort ( )
inline

Return the integer sort.

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

2909 { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }

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

◆ int_symbol()

symbol int_symbol ( int  n)
inline

Create a Z3 symbol based on the given integer.

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

2906 { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }

◆ int_val() [1/5]

expr int_val ( char const *  n)
inline

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

3102 { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

◆ int_val() [2/5]

expr int_val ( int  n)
inline

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

3098 { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

Referenced by z3::abs().

◆ int_val() [3/5]

expr int_val ( int64_t  n)
inline

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

3100 { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

◆ int_val() [4/5]

expr int_val ( uint64_t  n)
inline

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

3101 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

◆ int_val() [5/5]

expr int_val ( unsigned  n)
inline

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

3099 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

◆ interrupt()

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 221 of file z3++.h.

221 { Z3_interrupt(m_ctx); }

◆ num_val()

expr num_val ( int  n,
sort const &  s 
)
inline

◆ operator Z3_context()

operator Z3_context ( ) const
inline

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

173 { return m_ctx; }

◆ parse_file() [1/2]

expr_vector parse_file ( char const *  file)
inline

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

3448  {
3449  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3450  check_error();
3451  return expr_vector(*this, r);
3452  }

◆ parse_file() [2/2]

expr_vector parse_file ( char const *  s,
sort_vector const &  sorts,
func_decl_vector const &  decls 
)
inline

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

3471  {
3472  array<Z3_symbol> sort_names(sorts.size());
3473  array<Z3_symbol> decl_names(decls.size());
3474  array<Z3_sort> sorts1(sorts);
3475  array<Z3_func_decl> decls1(decls);
3476  for (unsigned i = 0; i < sorts.size(); ++i) {
3477  sort_names[i] = sorts[i].name();
3478  }
3479  for (unsigned i = 0; i < decls.size(); ++i) {
3480  decl_names[i] = decls[i].name();
3481  }
3482  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3483  check_error();
3484  return expr_vector(*this, r);
3485  }

◆ parse_string() [1/2]

expr_vector parse_string ( char const *  s)
inline

parsing

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

3442  {
3443  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3444  check_error();
3445  return expr_vector(*this, r);
3446 
3447  }

◆ parse_string() [2/2]

expr_vector parse_string ( char const *  s,
sort_vector const &  sorts,
func_decl_vector const &  decls 
)
inline

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

3454  {
3455  array<Z3_symbol> sort_names(sorts.size());
3456  array<Z3_symbol> decl_names(decls.size());
3457  array<Z3_sort> sorts1(sorts);
3458  array<Z3_func_decl> decls1(decls);
3459  for (unsigned i = 0; i < sorts.size(); ++i) {
3460  sort_names[i] = sorts[i].name();
3461  }
3462  for (unsigned i = 0; i < decls.size(); ++i) {
3463  decl_names[i] = decls[i].name();
3464  }
3465 
3466  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3467  check_error();
3468  return expr_vector(*this, r);
3469  }

◆ re_sort()

sort re_sort ( sort seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

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

2914 { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }

◆ real_const()

expr real_const ( char const *  name)
inline

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

3089 { return constant(name, real_sort()); }

◆ real_sort()

sort real_sort ( )
inline

Return the Real sort.

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

2910 { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }

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

◆ real_val() [1/6]

expr real_val ( char const *  n)
inline

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

3109 { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

◆ real_val() [2/6]

expr real_val ( int  n)
inline

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

3105 { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

◆ real_val() [3/6]

expr real_val ( int  n,
int  d 
)
inline

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

3104 { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); }

Referenced by z3::abs().

◆ real_val() [4/6]

expr real_val ( int64_t  n)
inline

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

3107 { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

◆ real_val() [5/6]

expr real_val ( uint64_t  n)
inline

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

3108 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

◆ real_val() [6/6]

expr real_val ( unsigned  n)
inline

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

3106 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

◆ recdef()

void recdef ( func_decl  f,
expr_vector const &  args,
expr const &  body 
)
inline

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

3075  {
3076  check_context(f, args); check_context(f, body);
3077  array<Z3_ast> vars(args);
3078  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3079  }

◆ recfun() [1/4]

func_decl recfun ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3070  {
3071  sort dom[2] = { d1, d2 };
3072  return recfun(str_symbol(name), 2, dom, range);
3073  }

◆ recfun() [2/4]

func_decl recfun ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

3066  {
3067  return recfun(str_symbol(name), 1, &d1, range);
3068  }

◆ recfun() [3/4]

func_decl recfun ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3062  {
3063  return recfun(str_symbol(name), arity, domain, range);
3064  }

◆ recfun() [4/4]

func_decl recfun ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3050  {
3051  array<Z3_sort> args(arity);
3052  for (unsigned i = 0; i < arity; i++) {
3053  check_context(domain[i], range);
3054  args[i] = domain[i];
3055  }
3056  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3057  check_error();
3058  return func_decl(*this, f);
3059 
3060  }

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

◆ seq_sort()

sort seq_sort ( sort s)
inline

Return a sequence sort over base sort s.

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

2913 { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }

◆ set() [1/3]

void set ( char const *  param,
bool  value 
)
inline

Update global parameter param with Boolean value.

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

207 { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }

◆ set() [2/3]

void set ( char const *  param,
char const *  value 
)
inline

Update global parameter param with string value.

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

203 { Z3_update_param_value(m_ctx, param, value); }

◆ set() [3/3]

void set ( char const *  param,
int  value 
)
inline

Update global parameter param with Integer value.

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

211  {
212  std::ostringstream oss;
213  oss << value;
214  Z3_update_param_value(m_ctx, param, oss.str().c_str());
215  }

◆ set_enable_exceptions()

void set_enable_exceptions ( bool  f)
inline

The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications have to be very careful about using check_error() after calls that may result in an erroneous state.

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

196 { m_enable_exceptions = f; }

◆ set_rounding_mode()

void set_rounding_mode ( rounding_mode  rm)
inline

Sets RoundingMode of FloatingPoints.

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

2940 { m_rounding_mode = rm; }

◆ str_symbol()

symbol str_symbol ( char const *  s)
inline

Create a Z3 symbol based on the given string.

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

2905 { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }

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

◆ string_sort()

sort string_sort ( )
inline

Return the sort for ASCII strings.

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

2912 { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }

◆ string_val() [1/3]

expr string_val ( char const *  s)
inline

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

3126 { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }

◆ string_val() [2/3]

expr string_val ( char const *  s,
unsigned  n 
)
inline

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

3125 { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }

◆ string_val() [3/3]

expr string_val ( std::string const &  s)
inline

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

3127 { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }

◆ tuple_sort()

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 2958 of file z3++.h.

2958  {
2959  array<Z3_symbol> _names(n);
2960  array<Z3_sort> _sorts(n);
2961  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
2962  array<Z3_func_decl> _projs(n);
2963  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2964  Z3_func_decl tuple;
2965  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
2966  check_error();
2967  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
2968  return func_decl(*this, tuple);
2969  }

◆ uninterpreted_sort() [1/2]

sort uninterpreted_sort ( char const *  name)
inline

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

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

2971  {
2972  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2973  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2974  }

◆ uninterpreted_sort() [2/2]

sort uninterpreted_sort ( symbol const &  name)
inline

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

2975  {
2976  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2977  }
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_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.
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_true
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_del_context
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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_OK
@ Z3_OK
Definition: z3_api.h:1365
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.
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::context::int_sort
sort int_sort()
Return the integer sort.
Definition: z3++.h:2909
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::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2905
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:96
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.
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,...
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.
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3081
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_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_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_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.
Z3_mk_fpa_sort
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
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::RTN
@ RTN
Definition: z3++.h:137
z3::context::enable_exceptions
bool enable_exceptions() const
Definition: z3++.h:198
z3::context::fpa_sort
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
z3::RTP
@ RTP
Definition: z3++.h:136
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::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1667
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:2911
Z3_mk_bool_sort
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
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.
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_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_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_mk_const
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
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_mk_int_sort
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
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::context::real_sort
sort real_sort()
Return the Real sort.
Definition: z3++.h:2910
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
Z3_mk_string_sort
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
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_array_sort
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_mk_false
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
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_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::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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.
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.
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_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_mk_real
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
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::bool_sort
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:2908
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::RTZ
@ RTZ
Definition: z3++.h:138
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:178
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1363
Z3_mk_real_sort
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
z3::object::ctx
context & ctx() const
Definition: z3++.h:406
z3::RNA
@ RNA
Definition: z3++.h:134
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::RNE
@ RNE
Definition: z3++.h:135