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 (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); }
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.

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

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

◆ array_sort() [2/2]

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

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

2763  {
2764  array<Z3_sort> dom(d);
2765  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2766  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.

◆ bool_const()

expr bool_const ( char const *  name)
inline

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

2907 { return constant(name, bool_sort()); }
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:2728
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901

◆ bool_sort()

sort bool_sort ( )
inline

Return the Boolean sort.

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

Referenced by context::bool_const().

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

◆ bool_val()

expr bool_val ( bool  b)
inline

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

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

2916 { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.

◆ bv_const()

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

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

2910 { return constant(name, bv_sort(sz)); }
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:2731
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901

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

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

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

◆ bv_val() [1/6]

expr bv_val ( int  n,
unsigned  sz 
)
inline

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

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

◆ bv_val() [2/6]

expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

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

2932 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:2731

◆ bv_val() [3/6]

expr bv_val ( int64_t  n,
unsigned  sz 
)
inline

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

2933 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:2731

◆ bv_val() [4/6]

expr bv_val ( uint64_t  n,
unsigned  sz 
)
inline

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

2934 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:2731
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.

◆ bv_val() [5/6]

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

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

2935 { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:2731
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ bv_val() [6/6]

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

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

2936  {
2937  array<Z3_bool> _bits(n);
2938  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
2939  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
2940  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const *bits)
create a bit-vector numeral from a vector of Booleans.

◆ check_error()

Z3_error_code check_error ( ) const
inline

Auxiliary method used to check for API usage errors.

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

Referenced by context::array_sort(), context::bool_sort(), context::bv_sort(), context::bv_val(), object::check_error(), context::check_parser_error(), z3::concat(), context::constant(), context::enumeration_sort(), expr::extract(), context::fpa_sort(), context::fpa_val(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::num_val(), func_decl::operator()(), context::parse_file(), context::parse_string(), 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().

178  {
179  Z3_error_code e = Z3_get_error_code(m_ctx);
180  if (e != Z3_OK && enable_exceptions())
181  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
182  return e;
183  }
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
#define Z3_THROW(x)
Definition: z3++.h:96
Definition: z3_api.h:1323
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1321
bool enable_exceptions() const
Definition: z3++.h:198
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.

◆ check_parser_error()

void check_parser_error ( ) const
inline

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

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

185  {
186  check_error();
187  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178

◆ constant() [1/2]

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

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

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

2901  {
2902  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2903  check_error();
2904  return expr(*this, r);
2905  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.

◆ constant() [2/2]

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

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

2906 { return constant(str_symbol(name), s); }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901

◆ enable_exceptions()

bool enable_exceptions ( ) const
inline

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

Referenced by context::check_error().

198 { return m_enable_exceptions; }

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

2767  {
2768  array<Z3_symbol> _enum_names(n);
2769  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2770  array<Z3_func_decl> _cs(n);
2771  array<Z3_func_decl> _ts(n);
2772  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2773  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2774  check_error();
2775  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2776  return s;
2777  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1572

◆ fpa_const() [1/2]

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

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

2911 { return constant(name, fpa_sort(ebits, sbits)); }
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

◆ fpa_const() [2/2]

expr fpa_const ( char const *  name)
inline

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

2914 { return constant(name, fpa_sort<precision>()); }
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )
inline

Return a RoundingMode sort.

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

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

2749  {
2750  switch (m_rounding_mode) {
2751  case RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
2752  case RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
2753  case RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
2754  case RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
2755  case RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
2756  default: return sort(*this);
2757  }
2758  }
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Definition: z3++.h:137
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode...
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode...
Definition: z3++.h:134
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
Definition: z3++.h:138
Definition: z3++.h:136
Definition: z3++.h:135

◆ fpa_sort() [1/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 2735 of file z3++.h.

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

◆ fpa_sort() [2/6]

sort fpa_sort ( )

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

Referenced by context::fpa_const().

◆ fpa_sort() [3/6]

sort fpa_sort ( )
inline

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

Referenced by context::fpa_sort().

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

◆ fpa_sort() [4/6]

sort fpa_sort ( )
inline

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

Referenced by context::fpa_sort().

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

◆ fpa_sort() [5/6]

sort fpa_sort ( )
inline

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

Referenced by context::fpa_sort().

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

◆ fpa_sort() [6/6]

sort fpa_sort ( )
inline

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

Referenced by context::fpa_sort().

2747 { return fpa_sort(15, 113); }
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

◆ fpa_val() [1/2]

expr fpa_val ( double  n)
inline

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

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

◆ fpa_val() [2/2]

expr fpa_val ( float  n)
inline

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

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

◆ function() [1/9]

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

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

Referenced by z3::function().

2799  {
2800  array<Z3_sort> args(arity);
2801  for (unsigned i = 0; i < arity; i++) {
2802  check_context(domain[i], range);
2803  args[i] = domain[i];
2804  }
2805  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2806  check_error();
2807  return func_decl(*this, f);
2808  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ function() [2/9]

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

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

2810  {
2811  return function(range.ctx().str_symbol(name), arity, domain, range);
2812  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
context & ctx() const
Definition: z3++.h:404

◆ function() [3/9]

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

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

2814  {
2815  array<Z3_sort> args(domain.size());
2816  for (unsigned i = 0; i < domain.size(); i++) {
2817  check_context(domain[i], range);
2818  args[i] = domain[i];
2819  }
2820  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2821  check_error();
2822  return func_decl(*this, f);
2823  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ function() [4/9]

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

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

2825  {
2826  return function(range.ctx().str_symbol(name), domain, range);
2827  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
context & ctx() const
Definition: z3++.h:404

◆ function() [5/9]

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

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

2830  {
2831  check_context(domain, range);
2832  Z3_sort args[1] = { domain };
2833  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2834  check_error();
2835  return func_decl(*this, f);
2836  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ function() [6/9]

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

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

2838  {
2840  Z3_sort args[2] = { d1, d2 };
2841  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2842  check_error();
2843  return func_decl(*this, f);
2844  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ function() [7/9]

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

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

2846  {
2848  Z3_sort args[3] = { d1, d2, d3 };
2849  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2850  check_error();
2851  return func_decl(*this, f);
2852  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ function() [8/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 2854 of file z3++.h.

2854  {
2856  Z3_sort args[4] = { d1, d2, d3, d4 };
2857  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2858  check_error();
2859  return func_decl(*this, f);
2860  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ function() [9/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 2862 of file z3++.h.

2862  {
2864  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2865  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2866  check_error();
2867  return func_decl(*this, f);
2868  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ int_const()

expr int_const ( char const *  name)
inline

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

2908 { return constant(name, int_sort()); }
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901
sort int_sort()
Return the integer sort.
Definition: z3++.h:2729

◆ int_sort()

sort int_sort ( )
inline

Return the integer sort.

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

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

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

◆ int_symbol()

symbol int_symbol ( int  n)
inline

Create a Z3 symbol based on the given integer.

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

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

◆ int_val() [1/5]

expr int_val ( int  n)
inline

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

Referenced by z3::abs().

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

◆ int_val() [2/5]

expr int_val ( unsigned  n)
inline

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

2919 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
sort int_sort()
Return the integer sort.
Definition: z3++.h:2729

◆ int_val() [3/5]

expr int_val ( int64_t  n)
inline

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

2920 { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
sort int_sort()
Return the integer sort.
Definition: z3++.h:2729

◆ int_val() [4/5]

expr int_val ( uint64_t  n)
inline

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

2921 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
sort int_sort()
Return the integer sort.
Definition: z3++.h:2729

◆ int_val() [5/5]

expr int_val ( char const *  n)
inline

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

2922 { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
sort int_sort()
Return the integer sort.
Definition: z3++.h:2729

◆ 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); }
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...

◆ num_val()

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

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

Referenced by z3::ashr(), z3::lshr(), z3::mod(), z3::operator &(), z3::operator!=(), func_decl::operator()(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::pw(), z3::rem(), z3::select(), z3::shl(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

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

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

3261  {
3262  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3263  check_error();
3264  return expr_vector(*this, r);
3265  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71

◆ parse_file() [2/2]

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

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

3284  {
3285  array<Z3_symbol> sort_names(sorts.size());
3286  array<Z3_symbol> decl_names(decls.size());
3287  array<Z3_sort> sorts1(sorts);
3288  array<Z3_func_decl> decls1(decls);
3289  for (unsigned i = 0; i < sorts.size(); ++i) {
3290  sort_names[i] = sorts[i].name();
3291  }
3292  for (unsigned i = 0; i < decls.size(); ++i) {
3293  decl_names[i] = decls[i].name();
3294  }
3295  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3296  check_error();
3297  return expr_vector(*this, r);
3298  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71

◆ parse_string() [1/2]

expr_vector parse_string ( char const *  s)
inline

parsing

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

3255  {
3256  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3257  check_error();
3258  return expr_vector(*this, r);
3259 
3260  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71

◆ parse_string() [2/2]

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

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

3267  {
3268  array<Z3_symbol> sort_names(sorts.size());
3269  array<Z3_symbol> decl_names(decls.size());
3270  array<Z3_sort> sorts1(sorts);
3271  array<Z3_func_decl> decls1(decls);
3272  for (unsigned i = 0; i < sorts.size(); ++i) {
3273  sort_names[i] = sorts[i].name();
3274  }
3275  for (unsigned i = 0; i < decls.size(); ++i) {
3276  decl_names[i] = decls[i].name();
3277  }
3278 
3279  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3280  check_error();
3281  return expr_vector(*this, r);
3282  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71

◆ re_sort()

sort re_sort ( sort seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

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

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

◆ real_const()

expr real_const ( char const *  name)
inline

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

2909 { return constant(name, real_sort()); }
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901
sort real_sort()
Return the Real sort.
Definition: z3++.h:2730

◆ real_sort()

sort real_sort ( )
inline

Return the Real sort.

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

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

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

◆ real_val() [1/6]

expr real_val ( int  n,
int  d 
)
inline

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

Referenced by z3::abs().

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

◆ real_val() [2/6]

expr real_val ( int  n)
inline

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

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

◆ real_val() [3/6]

expr real_val ( unsigned  n)
inline

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

2926 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
sort real_sort()
Return the Real sort.
Definition: z3++.h:2730

◆ real_val() [4/6]

expr real_val ( int64_t  n)
inline

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

2927 { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
sort real_sort()
Return the Real sort.
Definition: z3++.h:2730

◆ real_val() [5/6]

expr real_val ( uint64_t  n)
inline

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

2928 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
sort real_sort()
Return the Real sort.
Definition: z3++.h:2730

◆ real_val() [6/6]

expr real_val ( char const *  n)
inline

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

2929 { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
sort real_sort()
Return the Real sort.
Definition: z3++.h:2730
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

◆ recdef()

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

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

2895  {
2896  check_context(f, args); check_context(f, body);
2897  array<Z3_ast> vars(args);
2898  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
2899  }
void check_context(object const &a, object const &b)
Definition: z3++.h:408
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.

◆ recfun() [1/4]

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

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

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

2870  {
2871  array<Z3_sort> args(arity);
2872  for (unsigned i = 0; i < arity; i++) {
2873  check_context(domain[i], range);
2874  args[i] = domain[i];
2875  }
2876  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
2877  check_error();
2878  return func_decl(*this, f);
2879 
2880  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
void check_context(object const &a, object const &b)
Definition: z3++.h:408
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.

◆ recfun() [2/4]

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

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

2882  {
2883  return recfun(str_symbol(name), arity, domain, range);
2884  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2870

◆ recfun() [3/4]

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

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

2886  {
2887  return recfun(str_symbol(name), 1, &d1, range);
2888  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2870

◆ recfun() [4/4]

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

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

2890  {
2891  sort dom[2] = { d1, d2 };
2892  return recfun(str_symbol(name), 2, dom, range);
2893  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2870

◆ seq_sort()

sort seq_sort ( sort s)
inline

Return a sequence sort over base sort s.

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

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

◆ set() [1/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); }
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.

◆ set() [2/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"); }
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.

◆ 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  }
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.

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

2760 { 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 2725 of file z3++.h.

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

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

◆ string_sort()

sort string_sort ( )
inline

Return the sort for ASCII strings.

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

2732 { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.

◆ string_val() [1/2]

expr string_val ( char const *  s)
inline

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

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

◆ string_val() [2/2]

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

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

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

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

2778  {
2779  array<Z3_symbol> _names(n);
2780  array<Z3_sort> _sorts(n);
2781  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
2782  array<Z3_func_decl> _projs(n);
2783  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2784  Z3_func_decl tuple;
2785  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
2786  check_error();
2787  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
2788  return func_decl(*this, tuple);
2789  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1572

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

2791  {
2792  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2793  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2794  }
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1572

◆ uninterpreted_sort() [2/2]

sort uninterpreted_sort ( symbol const &  name)
inline

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

2795  {
2796  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2797  }
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1572