Z3 |

Public Member Functions | Friends
context Class Reference

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

`#include <z3++.h>`

## 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_sort ()
| Return a RoundingMode sort. More...
void | set_rounding_mode (rounding_mode rm)
| Sets RoundingMode of FloatingPoints. More...
sort | enumeration_sort (char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts)
| Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. `cs` and `ts` are output parameters. The method stores in `cs` the constants corresponding to the enumerated elements, and in `ts` the predicates for testing if terms of the enumeration sort correspond to an enumeration. More...
func_decl | tuple_sort (char const *name, unsigned n, char const *const *names, sort const *sorts, func_decl_vector &projs)
| Return a tuple constructor. `name` is the name of the returned constructor, `n` are the number of arguments, `names` and `sorts` are their projected sorts. `projs` is an output parameter. It contains the set of projection functions. More...
sort | uninterpreted_sort (char const *name)
| create an uninterpreted sort with the name given by the string or symbol. More...
sort | uninterpreted_sort (symbol const &name)
func_decl | function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl | function (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl | function (symbol const &name, sort_vector const &domain, sort const &range)
func_decl | function (char const *name, sort_vector const &domain, sort const &range)
func_decl | function (char const *name, sort const &domain, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
func_decl | recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl | recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl | recfun (char const *name, sort const &domain, sort const &range)
func_decl | recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
void | recdef (func_decl, expr_vector const &args, expr const &body)
expr | constant (symbol const &name, sort const &s)
expr | constant (char const *name, sort const &s)
expr | bool_const (char const *name)
expr | int_const (char const *name)
expr | real_const (char const *name)
expr | string_const (char const *name)
expr | bv_const (char const *name, unsigned sz)
expr | fpa_const (char const *name, unsigned ebits, unsigned sbits)
template<size_t precision>
expr | fpa_const (char const *name)
expr | fpa_rounding_mode ()
expr | bool_val (bool b)
expr | int_val (int n)
expr | int_val (unsigned n)
expr | int_val (int64_t n)
expr | int_val (uint64_t n)
expr | int_val (char const *n)
expr | real_val (int n, int d)
expr | real_val (int n)
expr | real_val (unsigned n)
expr | real_val (int64_t n)
expr | real_val (uint64_t n)
expr | real_val (char const *n)
expr | bv_val (int n, unsigned sz)
expr | bv_val (unsigned n, unsigned sz)
expr | bv_val (int64_t n, unsigned sz)
expr | bv_val (uint64_t n, unsigned sz)
expr | bv_val (char const *n, unsigned sz)
expr | bv_val (unsigned n, bool const *bits)
expr | fpa_val (double n)
expr | fpa_val (float n)
expr | fpa_nan (sort const &s)
expr | fpa_inf (sort const &s, bool sgn)
expr | string_val (char const *s)
expr | string_val (char const *s, unsigned n)
expr | string_val (std::string const &s)
expr | num_val (int n, sort const &s)
expr_vector | parse_string (char const *s)
| parsing More...
expr_vector | parse_file (char const *file)
expr_vector | parse_string (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
expr_vector | parse_file (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
template<>
sort | fpa_sort ()
template<>
sort | fpa_sort ()
template<>
sort | fpa_sort ()
template<>
sort | fpa_sort ()

## Friends
class | scoped_context

## Detailed Description

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

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

## Constructor & Destructor Documentation

## ◆ context() [1/2]

context | ( |  | ) |
| inline

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

180{ config c; init(c); }

## ◆ context() [2/2]

context | ( | config & | c | ) |
| inline

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

181{ init(c); }

## ◆ ~context()

~context | ( |  | ) |
| inline

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

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

## Member Function Documentation

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

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

3221 {
3222 array<Z3_sort> dom(d);
3223 Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3224 }
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.

## ◆ bool_const()

expr bool_const | ( | char const * | name | ) |
| inline

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

3365{ return constant(name, bool_sort()); }
z3::context::bool_sort
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:3197
z3::context::constant
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3359

## ◆ bool_sort()

sort bool_sort | ( |  | ) |
| inline

Return the Boolean sort.

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

3197{ Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_mk_bool_sort
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.

Referenced by context::bool_const().

## ◆ bool_val()

expr bool_val | ( | bool | b | ) |
| inline

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

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

Referenced by goal::as_expr(), and solver::to_smt2().

## ◆ bv_const()

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

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

3369{ return constant(name, bv_sort(sz)); }
z3::context::bv_sort
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:3200

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

3200{ Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
Z3_mk_bv_sort
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.

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

3407{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
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.

## ◆ bv_val() [2/6]

expr bv_val | ( | int | n,
|  | unsigned | sz
| ) |  |
| inline

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

3403{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_int
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.

## ◆ bv_val() [3/6]

expr bv_val | ( | int64_t | n,
|  | unsigned | sz
| ) |  |
| inline

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

3405{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_int64
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.

## ◆ bv_val() [4/6]

expr bv_val | ( | uint64_t | n,
|  | unsigned | sz
| ) |  |
| inline

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

3406{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_unsigned_int64
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.

## ◆ bv_val() [5/6]

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

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

3408 {
3409 array<bool> _bits(n);
3410 for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3411 Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3412 }
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.

## ◆ bv_val() [6/6]

expr bv_val | ( | unsigned | n,
|  | unsigned | sz
| ) |  |
| inline

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

3404{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_unsigned_int
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.

## ◆ check_error()

Z3_error_code check_error | ( |  | ) | const
| inline

Auxiliary method used to check for API usage errors.

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

188 {
189 Z3_error_code e = Z3_get_error_code(m_ctx);
190 if (e != Z3_OK && enable_exceptions())
191 Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
192 return e;
193 }
z3::context::enable_exceptions
bool enable_exceptions() const
Definition: z3++.h:208
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:100
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_error_code
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1359
Z3_OK
@ Z3_OK
Definition: z3_api.h:1360
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.

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

## ◆ check_parser_error()

void check_parser_error | ( |  | ) | const
| inline

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

195 {
196 check_error();
197 }

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

## ◆ constant() [1/2]

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

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

3364{ return constant(str_symbol(name), s); }
z3::context::str_symbol
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3194

## ◆ constant() [2/2]

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

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

3359 {
3360 Z3_ast r = Z3_mk_const(m_ctx, name, s);
3361 check_error();
3362 return expr(*this, r);
3363 }
Z3_mk_const
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.

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

## ◆ enable_exceptions()

bool enable_exceptions | ( |  | ) | const
| inline

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

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

3225 {
3226 array<Z3_symbol> _enum_names(n);
3227 for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3228 array<Z3_func_decl> _cs(n);
3229 array<Z3_func_decl> _ts(n);
3230 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3231 sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3232 check_error();
3233 for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3234 return s;
3235 }
z3::to_sort
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1980
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_string_symbol
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.

## ◆ fpa_const() [1/2]

expr fpa_const | ( | char const * | name | ) |
| inline

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

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

## ◆ fpa_const() [2/2]

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

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

3370{ return constant(name, fpa_sort(ebits, sbits)); }
z3::context::fpa_sort
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

## ◆ fpa_inf()

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

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

3417{ Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
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.

## ◆ fpa_nan()

expr fpa_nan | ( | sort const & | s | ) |
| inline

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

3416{ Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
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.

## ◆ fpa_rounding_mode()

expr fpa_rounding_mode | ( |  | ) |
| inline

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

3377 {
3378 switch (m_rounding_mode) {
3379 case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3380 case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3381 case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3382 case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3383 case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3384 default: return expr(*this);
3385 }
3386 }
z3::RNE
@ RNE
Definition: z3++.h:138
z3::RNA
@ RNA
Definition: z3++.h:137
z3::RTZ
@ RTZ
Definition: z3++.h:141
z3::RTN
@ RTN
Definition: z3++.h:140
z3::RTP
@ RTP
Definition: z3++.h:139
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_fpa_rtn
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
Z3_mk_fpa_rtp
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
Z3_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_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.

## ◆ fpa_rounding_mode_sort()

sort fpa_rounding_mode_sort | ( |  | ) |
| inline

Return a RoundingMode sort.

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

3218{ Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }
Z3_mk_fpa_rounding_mode_sort
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.

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

3207{ return fpa_sort(5, 11); }

Referenced by context::fpa_sort().

## ◆ fpa_sort() [3/6]

sort fpa_sort | ( |  | ) |
| inline

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

3210{ return fpa_sort(8, 24); }

Referenced by context::fpa_sort().

## ◆ fpa_sort() [4/6]

sort fpa_sort | ( |  | ) |
| inline

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

3213{ return fpa_sort(11, 53); }

Referenced by context::fpa_sort().

## ◆ fpa_sort() [5/6]

sort fpa_sort | ( |  | ) |
| inline

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

3216{ 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 3204 of file z3++.h.

3204{ Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
Z3_mk_fpa_sort
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.

## ◆ fpa_val() [1/2]

expr fpa_val | ( | double | n | ) |
| inline

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

3414{ sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_fpa_numeral_double
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a double.

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

## ◆ fpa_val() [2/2]

expr fpa_val | ( | float | n | ) |
| inline

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

3415{ sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
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.

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

3320 {
3321 check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
3322 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3323 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3324 check_error();
3325 return func_decl(*this, f);
3326 }
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:426
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
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.

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

3312 {
3313 check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
3314 Z3_sort args[4] = { d1, d2, d3, d4 };
3315 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3316 check_error();
3317 return func_decl(*this, f);
3318 }

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

3304 {
3305 check_context(d1, range); check_context(d2, range); check_context(d3, range);
3306 Z3_sort args[3] = { d1, d2, d3 };
3307 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3308 check_error();
3309 return func_decl(*this, f);
3310 }

## ◆ function() [4/9]

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

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

3296 {
3297 check_context(d1, range); check_context(d2, range);
3298 Z3_sort args[2] = { d1, d2 };
3299 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3300 check_error();
3301 return func_decl(*this, f);
3302 }

## ◆ function() [5/9]

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

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

3288 {
3289 check_context(domain, range);
3290 Z3_sort args[1] = { domain };
3291 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3292 check_error();
3293 return func_decl(*this, f);
3294 }

## ◆ function() [6/9]

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

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

3283 {
3284 return function(range.ctx().str_symbol(name), domain, range);
3285 }
z3::context::function
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3257
z3::object::ctx
context & ctx() const
Definition: z3++.h:422

## ◆ function() [7/9]

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

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

3268 {
3269 return function(range.ctx().str_symbol(name), arity, domain, range);
3270 }

## ◆ function() [8/9]

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

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

3272 {
3273 array<Z3_sort> args(domain.size());
3274 for (unsigned i = 0; i < domain.size(); i++) {
3275 check_context(domain[i], range);
3276 args[i] = domain[i];
3277 }
3278 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3279 check_error();
3280 return func_decl(*this, f);
3281 }

## ◆ function() [9/9]

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

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

3257 {
3258 array<Z3_sort> args(arity);
3259 for (unsigned i = 0; i < arity; i++) {
3260 check_context(domain[i], range);
3261 args[i] = domain[i];
3262 }
3263 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3264 check_error();
3265 return func_decl(*this, f);
3266 }

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

## ◆ int_const()

expr int_const | ( | char const * | name | ) |
| inline

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

3366{ return constant(name, int_sort()); }
z3::context::int_sort
sort int_sort()
Return the integer sort.
Definition: z3++.h:3198

## ◆ int_sort()

sort int_sort | ( |  | ) |
| inline

Return the integer sort.

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

3198{ Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_mk_int_sort
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.

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

3195{ Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
Z3_mk_int_symbol
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.

## ◆ int_val() [1/5]

expr int_val | ( | char const * | n | ) |
| inline

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

3394{ 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 3390 of file z3++.h.

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

## ◆ int_val() [3/5]

expr int_val | ( | int64_t | n | ) |
| inline

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

3392{ 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 3393 of file z3++.h.

3393{ 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 3391 of file z3++.h.

3391{ 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 230 of file z3++.h.

230{ Z3_interrupt(m_ctx); }
Z3_interrupt
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...

## ◆ num_val()

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

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

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

Referenced by z3::ashr(), z3::lshr(), func_decl::operator()(), z3::select(), z3::sge(), z3::sgt(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

## ◆ operator Z3_context()

operator Z3_context | ( |  | ) | const
| inline

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

183{ return m_ctx; }

## ◆ parse_file() [1/2]

expr_vector parse_file | ( | char const * | file | ) |
| inline

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

3742 {
3743 Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3744 check_error();
3745 return expr_vector(*this, r);
3746 }
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
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.

## ◆ parse_file() [2/2]

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

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

3765 {
3766 array<Z3_symbol> sort_names(sorts.size());
3767 array<Z3_symbol> decl_names(decls.size());
3768 array<Z3_sort> sorts1(sorts);
3769 array<Z3_func_decl> decls1(decls);
3770 for (unsigned i = 0; i < sorts.size(); ++i) {
3771 sort_names[i] = sorts[i].name();
3772 }
3773 for (unsigned i = 0; i < decls.size(); ++i) {
3774 decl_names[i] = decls[i].name();
3775 }
3776 Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3777 check_error();
3778 return expr_vector(*this, r);
3779 }

## ◆ parse_string() [1/2]

expr_vector parse_string | ( | char const * | s | ) |
| inline

parsing

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

3736 {
3737 Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3738 check_error();
3739 return expr_vector(*this, r);
3740
3741 }
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.

## ◆ parse_string() [2/2]

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

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

3748 {
3749 array<Z3_symbol> sort_names(sorts.size());
3750 array<Z3_symbol> decl_names(decls.size());
3751 array<Z3_sort> sorts1(sorts);
3752 array<Z3_func_decl> decls1(decls);
3753 for (unsigned i = 0; i < sorts.size(); ++i) {
3754 sort_names[i] = sorts[i].name();
3755 }
3756 for (unsigned i = 0; i < decls.size(); ++i) {
3757 decl_names[i] = decls[i].name();
3758 }
3759
3760 Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3761 check_error();
3762 return expr_vector(*this, r);
3763 }

## ◆ re_sort()

sort re_sort | ( | sort & | seq_sort | ) |
| inline

Return a regular expression sort over sequences `seq_sort`.

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

3203{ Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
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.

## ◆ real_const()

expr real_const | ( | char const * | name | ) |
| inline

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

3367{ return constant(name, real_sort()); }
z3::context::real_sort
sort real_sort()
Return the Real sort.
Definition: z3++.h:3199

## ◆ real_sort()

sort real_sort | ( |  | ) |
| inline

Return the Real sort.

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

3199{ Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_mk_real_sort
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.

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

## ◆ real_val() [1/6]

expr real_val | ( | char const * | n | ) |
| inline

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

3401{ 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 3397 of file z3++.h.

3397{ 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 3396 of file z3++.h.

3396{ Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); }
Z3_mk_real
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.

## ◆ real_val() [4/6]

expr real_val | ( | int64_t | n | ) |
| inline

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

3399{ 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 3400 of file z3++.h.

3400{ 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 3398 of file z3++.h.

3398{ 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 3353 of file z3++.h.

3353 {
3354 check_context(f, args); check_context(f, body);
3355 array<Z3_ast> vars(args);
3356 Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3357 }
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.

## ◆ recfun() [1/4]

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

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

3348 {
3349 sort dom[2] = { d1, d2 };
3350 return recfun(str_symbol(name), 2, dom, range);
3351 }
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3328

## ◆ recfun() [2/4]

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

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

3344 {
3345 return recfun(str_symbol(name), 1, &d1, range);
3346 }

## ◆ recfun() [3/4]

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

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

3340 {
3341 return recfun(str_symbol(name), arity, domain, range);
3342 }

## ◆ recfun() [4/4]

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

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

3328 {
3329 array<Z3_sort> args(arity);
3330 for (unsigned i = 0; i < arity; i++) {
3331 check_context(domain[i], range);
3332 args[i] = domain[i];
3333 }
3334 Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3335 check_error();
3336 return func_decl(*this, f);
3337
3338 }
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.

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

3202{ Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
Z3_mk_seq_sort
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.

## ◆ set() [1/3]

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

Update global parameter `param` with Boolean `value`.

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

217{ Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
Z3_update_param_value
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.

## ◆ set() [2/3]

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

Update global parameter `param` with string `value`.

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

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

## ◆ set() [3/3]

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

Update global parameter `param` with Integer `value`.

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

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

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

206{ m_enable_exceptions = f; }

## ◆ set_rounding_mode()

void set_rounding_mode | ( | rounding_mode | rm | ) |
| inline

Sets RoundingMode of FloatingPoints.

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

3375{ 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 3194 of file z3++.h.

3194{ 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 3368 of file z3++.h.

3368{ return constant(name, string_sort()); }
z3::context::string_sort
sort string_sort()
Return the sort for ASCII strings.
Definition: z3++.h:3201

## ◆ string_sort()

sort string_sort | ( |  | ) |
| inline

Return the sort for ASCII strings.

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

3201{ Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_mk_string_sort
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.

Referenced by context::string_const().

## ◆ string_val() [1/3]

expr string_val | ( | char const * | s | ) |
| inline

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

3420{ Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
Z3_mk_string
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)
Create a string constant out of the string that is passed in.

## ◆ string_val() [2/3]

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

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

3419{ Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_mk_lstring
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...

## ◆ string_val() [3/3]

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

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

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

## ◆ tuple_sort()

func_decl tuple_sort | ( | char const * | name,
|  | unsigned | n,
|  | char const *const * | names,
|  | sort const * | sorts,
|  | func_decl_vector & | projs
| ) |  |
| inline

Return a tuple constructor. `name` is the name of the returned constructor, `n` are the number of arguments, `names` and `sorts` are their projected sorts. `projs` is an output parameter. It contains the set of projection functions.

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

3236 {
3237 array<Z3_symbol> _names(n);
3238 array<Z3_sort> _sorts(n);
3239 for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3240 array<Z3_func_decl> _projs(n);
3241 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3242 Z3_func_decl tuple;
3243 sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3244 check_error();
3245 for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3246 return func_decl(*this, tuple);
3247 }
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.

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

3249 {
3250 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3251 return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3252 }
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).

## ◆ uninterpreted_sort() [2/2]

sort uninterpreted_sort | ( | symbol const & | name | ) |
| inline

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

3253 {
3254 return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3255 }

## Friends And Related Function Documentation

## ◆ scoped_context

friend class scoped_context
| friend

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