Z3
Public Member Functions | Friends
context Class Reference

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

Public Member Functions

 context ()
 
 context (config &c)
 
 ~context ()
 
 operator Z3_context () const
 
Z3_error_code check_error () const
 Auxiliary method used to check for API usage errors. More...
 
void check_parser_error () const
 
void set_enable_exceptions (bool f)
 The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications have to be very careful about using check_error() after calls that may result in an erroneous state. More...
 
bool enable_exceptions () const
 
void set (char const *param, char const *value)
 Update global parameter param with string value. More...
 
void set (char const *param, bool value)
 Update global parameter param with Boolean value. More...
 
void set (char const *param, int value)
 Update global parameter param with Integer value. More...
 
void interrupt ()
 Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop. More...
 
symbol str_symbol (char const *s)
 Create a Z3 symbol based on the given string. More...
 
symbol int_symbol (int n)
 Create a Z3 symbol based on the given integer. More...
 
sort bool_sort ()
 Return the Boolean sort. More...
 
sort int_sort ()
 Return the integer sort. More...
 
sort real_sort ()
 Return the Real sort. More...
 
sort bv_sort (unsigned sz)
 Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz. More...
 
sort char_sort ()
 Return the sort for Unicode characters. More...
 
sort string_sort ()
 Return the sort for Unicode strings. More...
 
sort seq_sort (sort &s)
 Return a sequence sort over base sort s. More...
 
sort re_sort (sort &seq_sort)
 Return a regular expression sort over sequences seq_sort. More...
 
sort array_sort (sort d, sort r)
 Return an array sort for arrays from d to r. More...
 
sort array_sort (sort_vector const &d, sort r)
 
sort fpa_sort (unsigned ebits, unsigned sbits)
 Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,. More...
 
template<size_t precision>
sort fpa_sort ()
 Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128). More...
 
sort fpa_rounding_mode_sort ()
 Return a RoundingMode sort. More...
 
void set_rounding_mode (rounding_mode rm)
 Sets RoundingMode of FloatingPoints. More...
 
sort enumeration_sort (char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts)
 Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters. The method stores in cs the constants corresponding to the enumerated elements, and in ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. More...
 
func_decl tuple_sort (char const *name, unsigned n, char const *const *names, sort const *sorts, func_decl_vector &projs)
 Return a tuple constructor. name is the name of the returned constructor, n are the number of arguments, names and sorts are their projected sorts. projs is an output parameter. It contains the set of projection functions. More...
 
sort datatype (symbol const &name, constructors const &cs)
 Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the numer of constructors of the datatype cs - the n constructors used to define the datatype. More...
 
sort_vector datatypes (unsigned n, symbol const *names, constructor_list *const *cons)
 Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of names of length n cons - array of constructor lists of length n. More...
 
sort datatype_sort (symbol const &name)
 a reference to a recursively defined datatype. Expect that it gets defined as a datatype. More...
 
sort uninterpreted_sort (char const *name)
 create an uninterpreted sort with the name given by the string or symbol. More...
 
sort uninterpreted_sort (symbol const &name)
 
func_decl function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (symbol const &name, sort_vector const &domain, sort const &range)
 
func_decl function (char const *name, sort_vector const &domain, sort const &range)
 
func_decl function (char const *name, sort const &domain, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
 
func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (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)
 
func_decl user_propagate_function (symbol const &name, sort_vector const &domain, sort const &range)
 
expr constant (symbol const &name, sort const &s)
 
expr constant (char const *name, sort const &s)
 
expr bool_const (char const *name)
 
expr int_const (char const *name)
 
expr real_const (char const *name)
 
expr 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 user_propagator_base
 

Detailed Description

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

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

Constructor & Destructor Documentation

◆ context() [1/2]

context ( )
inline

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

182 { config c; init(c); }

◆ context() [2/2]

context ( config c)
inline

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

183 { init(c); }

◆ ~context()

~context ( )
inline

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

184 { if (m_ctx) 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 3333 of file z3++.h.

3333 { 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 3334 of file z3++.h.

3334  {
3335  array<Z3_sort> dom(d);
3336  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3337  }

◆ bool_const()

expr bool_const ( char const *  name)
inline

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

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

◆ bool_sort()

sort bool_sort ( )
inline

Return the Boolean sort.

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

3309 { 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 3601 of file z3++.h.

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

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

◆ bv_const()

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

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

3582 { 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 3312 of file z3++.h.

3312 { 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 3620 of file z3++.h.

3620 { 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 3616 of file z3++.h.

3616 { 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 3618 of file z3++.h.

3618 { 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 3619 of file z3++.h.

3619 { 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 3621 of file z3++.h.

3621  {
3622  array<bool> _bits(n);
3623  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3624  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3625  }

◆ bv_val() [6/6]

expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

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

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

◆ char_sort()

sort char_sort ( )
inline

Return the sort for Unicode characters.

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

3314 { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }

◆ check_error()

Z3_error_code check_error ( ) const
inline

◆ check_parser_error()

void check_parser_error ( ) const
inline

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

197  {
198  check_error();
199  }

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

◆ constant() [1/2]

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

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

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

◆ constant() [2/2]

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

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

3572  {
3573  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3574  check_error();
3575  return expr(*this, r);
3576  }

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

◆ datatype()

sort datatype ( symbol const &  name,
constructors const &  cs 
)
inline

Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the numer of constructors of the datatype cs - the n constructors used to define the datatype.

References to the datatype can be created using datatype_sort.

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

3423  {
3424  array<Z3_constructor> _cs(cs.size());
3425  for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
3426  Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
3427  check_error();
3428  return sort(*this, s);
3429  }

◆ datatype_sort()

sort datatype_sort ( symbol const &  name)
inline

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

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

3447  {
3448  Z3_sort s = Z3_mk_datatype_sort(*this, name);
3449  check_error();
3450  return sort(*this, s);
3451  }

◆ datatypes()

sort_vector datatypes ( unsigned  n,
symbol const *  names,
constructor_list *const *  cons 
)
inline

Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of names of length n cons - array of constructor lists of length n.

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

3433  {
3434  sort_vector result(*this);
3435  array<Z3_symbol> _names(n);
3436  array<Z3_sort> _sorts(n);
3437  array<Z3_constructor_list> _cons(n);
3438  for (unsigned i = 0; i < n; ++i)
3439  _names[i] = names[i], _cons[i] = *cons[i];
3440  Z3_mk_datatypes(*this, n, _names.ptr(), _sorts.ptr(), _cons.ptr());
3441  for (unsigned i = 0; i < n; ++i)
3442  result.push_back(sort(*this, _sorts[i]));
3443  return result;
3444  }

◆ enable_exceptions()

bool enable_exceptions ( ) const
inline

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

210 { 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 3338 of file z3++.h.

3338  {
3339  array<Z3_symbol> _enum_names(n);
3340  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3341  array<Z3_func_decl> _cs(n);
3342  array<Z3_func_decl> _ts(n);
3343  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3344  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3345  check_error();
3346  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3347  return s;
3348  }

◆ fpa_const() [1/2]

expr fpa_const ( char const *  name)
inline

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

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

◆ fpa_const() [2/2]

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

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

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

◆ fpa_inf()

expr fpa_inf ( sort const &  s,
bool  sgn 
)
inline

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

3630 { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }

◆ fpa_nan()

expr fpa_nan ( sort const &  s)
inline

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

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

◆ fpa_rounding_mode()

expr fpa_rounding_mode ( )
inline

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

3590  {
3591  switch (m_rounding_mode) {
3592  case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3593  case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3594  case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3595  case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3596  case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3597  default: return expr(*this);
3598  }
3599  }

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().

◆ fpa_rounding_mode_sort()

sort fpa_rounding_mode_sort ( )
inline

Return a RoundingMode sort.

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

3331 { Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }

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

3320 { return fpa_sort(5, 11); }

Referenced by context::fpa_sort().

◆ fpa_sort() [3/6]

sort fpa_sort ( )
inline

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

3323 { return fpa_sort(8, 24); }

Referenced by context::fpa_sort().

◆ fpa_sort() [4/6]

sort fpa_sort ( )
inline

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

3326 { return fpa_sort(11, 53); }

Referenced by context::fpa_sort().

◆ fpa_sort() [5/6]

sort fpa_sort ( )
inline

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

3329 { 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 3317 of file z3++.h.

3317 { 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 3627 of file z3++.h.

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

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

◆ fpa_val() [2/2]

expr fpa_val ( float  n)
inline

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

3628 { 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 3525 of file z3++.h.

3525  {
3527  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3528  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3529  check_error();
3530  return func_decl(*this, f);
3531  }

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

3517  {
3519  Z3_sort args[4] = { d1, d2, d3, d4 };
3520  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3521  check_error();
3522  return func_decl(*this, f);
3523  }

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

3509  {
3511  Z3_sort args[3] = { d1, d2, d3 };
3512  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3513  check_error();
3514  return func_decl(*this, f);
3515  }

◆ function() [4/9]

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

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

3501  {
3503  Z3_sort args[2] = { d1, d2 };
3504  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3505  check_error();
3506  return func_decl(*this, f);
3507  }

◆ function() [5/9]

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

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

3493  {
3494  check_context(domain, range);
3495  Z3_sort args[1] = { domain };
3496  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3497  check_error();
3498  return func_decl(*this, f);
3499  }

◆ function() [6/9]

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

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

3488  {
3489  return function(range.ctx().str_symbol(name), domain, range);
3490  }

◆ function() [7/9]

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

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

3473  {
3474  return function(range.ctx().str_symbol(name), arity, domain, range);
3475  }

◆ function() [8/9]

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

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

3477  {
3478  array<Z3_sort> args(domain.size());
3479  for (unsigned i = 0; i < domain.size(); i++) {
3480  check_context(domain[i], range);
3481  args[i] = domain[i];
3482  }
3483  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3484  check_error();
3485  return func_decl(*this, f);
3486  }

◆ function() [9/9]

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

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

3462  {
3463  array<Z3_sort> args(arity);
3464  for (unsigned i = 0; i < arity; i++) {
3465  check_context(domain[i], range);
3466  args[i] = domain[i];
3467  }
3468  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3469  check_error();
3470  return func_decl(*this, f);
3471  }

Referenced by z3::function().

◆ int_const()

expr int_const ( char const *  name)
inline

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

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

◆ int_sort()

sort int_sort ( )
inline

Return the integer sort.

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

3310 { 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 3307 of file z3++.h.

3307 { 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 3607 of file z3++.h.

3607 { 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 3603 of file z3++.h.

3603 { 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 3605 of file z3++.h.

3605 { 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 3606 of file z3++.h.

3606 { 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 3604 of file z3++.h.

3604 { 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 232 of file z3++.h.

232 { 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 185 of file z3++.h.

185 { return m_ctx; }

◆ parse_file() [1/2]

expr_vector parse_file ( char const *  file)
inline

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

3963  {
3964  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3965  check_error();
3966  return expr_vector(*this, r);
3967  }

◆ parse_file() [2/2]

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

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

3986  {
3987  array<Z3_symbol> sort_names(sorts.size());
3988  array<Z3_symbol> decl_names(decls.size());
3989  array<Z3_sort> sorts1(sorts);
3990  array<Z3_func_decl> decls1(decls);
3991  for (unsigned i = 0; i < sorts.size(); ++i) {
3992  sort_names[i] = sorts[i].name();
3993  }
3994  for (unsigned i = 0; i < decls.size(); ++i) {
3995  decl_names[i] = decls[i].name();
3996  }
3997  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3998  check_error();
3999  return expr_vector(*this, r);
4000  }

◆ parse_string() [1/2]

expr_vector parse_string ( char const *  s)
inline

parsing

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

3957  {
3958  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3959  check_error();
3960  return expr_vector(*this, r);
3961 
3962  }

◆ parse_string() [2/2]

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

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

3969  {
3970  array<Z3_symbol> sort_names(sorts.size());
3971  array<Z3_symbol> decl_names(decls.size());
3972  array<Z3_sort> sorts1(sorts);
3973  array<Z3_func_decl> decls1(decls);
3974  for (unsigned i = 0; i < sorts.size(); ++i) {
3975  sort_names[i] = sorts[i].name();
3976  }
3977  for (unsigned i = 0; i < decls.size(); ++i) {
3978  decl_names[i] = decls[i].name();
3979  }
3980 
3981  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3982  check_error();
3983  return expr_vector(*this, r);
3984  }

◆ re_sort()

sort re_sort ( sort seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

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

3316 { 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 3580 of file z3++.h.

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

◆ real_sort()

sort real_sort ( )
inline

Return the Real sort.

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

3311 { 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 3614 of file z3++.h.

3614 { 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 3610 of file z3++.h.

3610 { 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 3609 of file z3++.h.

3609 { 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 3612 of file z3++.h.

3612 { 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 3613 of file z3++.h.

3613 { 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 3611 of file z3++.h.

3611 { 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 3558 of file z3++.h.

3558  {
3559  check_context(f, args); check_context(f, body);
3560  array<Z3_ast> vars(args);
3561  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3562  }

◆ recfun() [1/4]

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

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

3553  {
3554  sort dom[2] = { d1, d2 };
3555  return recfun(str_symbol(name), 2, dom, range);
3556  }

◆ recfun() [2/4]

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

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

3549  {
3550  return recfun(str_symbol(name), 1, &d1, range);
3551  }

◆ recfun() [3/4]

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

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

3545  {
3546  return recfun(str_symbol(name), arity, domain, range);
3547  }

◆ recfun() [4/4]

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

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

3533  {
3534  array<Z3_sort> args(arity);
3535  for (unsigned i = 0; i < arity; i++) {
3536  check_context(domain[i], range);
3537  args[i] = domain[i];
3538  }
3539  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3540  check_error();
3541  return func_decl(*this, f);
3542 
3543  }

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

3315 { 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 219 of file z3++.h.

219 { 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 215 of file z3++.h.

215 { 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 223 of file z3++.h.

223  {
224  auto str = std::to_string(value);
225  Z3_update_param_value(m_ctx, param, str.c_str());
226  }

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

208 { m_enable_exceptions = f; }

◆ set_rounding_mode()

void set_rounding_mode ( rounding_mode  rm)
inline

Sets RoundingMode of FloatingPoints.

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

3588 { 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 3306 of file z3++.h.

3306 { 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_const()

expr string_const ( char const *  name)
inline

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

3581 { return constant(name, string_sort()); }

◆ string_sort()

sort string_sort ( )
inline

Return the sort for Unicode strings.

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

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

Referenced by context::string_const().

◆ string_val() [1/4]

expr string_val ( char const *  s)
inline

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

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

◆ string_val() [2/4]

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

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

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

◆ string_val() [3/4]

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

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

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

◆ string_val() [4/4]

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

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

3635 { Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)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 3349 of file z3++.h.

3349  {
3350  array<Z3_symbol> _names(n);
3351  array<Z3_sort> _sorts(n);
3352  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3353  array<Z3_func_decl> _projs(n);
3354  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3355  Z3_func_decl tuple;
3356  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3357  check_error();
3358  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3359  return func_decl(*this, tuple);
3360  }

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

3454  {
3455  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3456  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3457  }

◆ uninterpreted_sort() [2/2]

sort uninterpreted_sort ( symbol const &  name)
inline

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

3458  {
3459  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3460  }

◆ user_propagate_function()

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

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

3564  {
3565  check_context(domain, range);
3566  array<Z3_sort> domain1(domain);
3567  Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
3568  check_error();
3569  return func_decl(*this, f);
3570  }

Friends And Related Function Documentation

◆ user_propagator_base

friend class user_propagator_base
friend

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

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.
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.
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::sort_vector
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:76
z3::context::string_sort
sort string_sort()
Return the sort for Unicode strings.
Definition: z3++.h:3313
z3::context::int_sort
sort int_sort()
Return the integer sort.
Definition: z3++.h:3310
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::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3306
Z3_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1341
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_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::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3946
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_OK
@ Z3_OK
Definition: z3_api.h:1343
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:102
Z3_del_context
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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_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.
Microsoft.Z3.Z3_sort
System.IntPtr Z3_sort
Definition: NativeContext.cs:33
Z3_mk_bool_sort
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3572
Microsoft.Z3.Z3_func_decl
System.IntPtr Z3_func_decl
Definition: NativeContext.cs:30
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_mk_int_symbol
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
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_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_string_sort
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
z3::RTN
@ RTN
Definition: z3++.h:142
z3::context::enable_exceptions
bool enable_exceptions() const
Definition: z3++.h:210
z3::context::fpa_sort
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
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_real_sort
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_mk_fpa_rounding_mode_sort
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.
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::RTP
@ RTP
Definition: z3++.h:141
z3::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:2083
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_mk_datatype
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records....
Microsoft.Z3.Z3_ast_vector
System.IntPtr Z3_ast_vector
Definition: NativeContext.cs:29
Z3_solver_propagate_declare
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
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:3312
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3533
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_false
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
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_datatypes
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
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_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_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_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::real_sort
sort real_sort()
Return the Real sort.
Definition: z3++.h:3311
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:75
Z3_mk_datatype_sort
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
Z3_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_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_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::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:455
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_fpa_sort
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
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_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_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_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_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.
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
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_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_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_int_sort
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
z3::context::bool_sort
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:3309
z3::RTZ
@ RTZ
Definition: z3++.h:143
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_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::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:190
Z3_mk_char_sort
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
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.
Microsoft.Z3.Z3_symbol
System.IntPtr Z3_symbol
Definition: NativeContext.cs:35
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::object::ctx
context & ctx() const
Definition: z3++.h:451
Z3_mk_true
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
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::RNA
@ RNA
Definition: z3++.h:139
z3::RNE
@ RNE
Definition: z3++.h:140