Z3
Data Structures | Public Member Functions
context Class Reference

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

Data Structures

struct  interpolation
 

Public Member Functions

 context ()
 
 context (config &c)
 
 context (config &c, interpolation)
 
 ~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 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 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 paramter. 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)
 
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 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 string_val (char const *s)
 
expr string_val (std::string const &s)
 
expr num_val (int n, sort const &s)
 
expr parse_string (char const *s)
 parsing More...
 
expr parse_file (char const *file)
 
expr parse_string (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
 
expr parse_file (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
 
check_result compute_interpolant (expr const &pat, params const &p, expr_vector &interp, model &m)
 Interpolation support. More...
 
expr_vector get_interpolant (expr const &proof, expr const &pat, params const &p)
 

Detailed Description

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

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

Constructor & Destructor Documentation

§ context() [1/3]

context ( )
inline

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

161 { config c; init(c); }

§ context() [2/3]

context ( config c)
inline

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

162 { init(c); }

§ context() [3/3]

context ( config c,
interpolation   
)
inline

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

163 { init_interp(c); }

§ ~context()

~context ( )
inline

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

164 { 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 2439 of file z3++.h.

2439 { 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:170
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 2440 of file z3++.h.

2440  {
2441  array<Z3_sort> dom(d);
2442  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2443  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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 2554 of file z3++.h.

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

§ bool_sort()

sort bool_sort ( )
inline

Return the Boolean sort.

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

2431 { 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:170
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 2559 of file z3++.h.

Referenced by z3::implies(), z3::operator &&(), and z3::operator||().

2559 { 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 2557 of file z3++.h.

2557 { 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:2434
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2548

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

2434 { 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:170

§ bv_val() [1/6]

expr bv_val ( int  n,
unsigned  sz 
)
inline

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

2574 { 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:170
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:2434
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 2575 of file z3++.h.

2575 { 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:170
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:2434

§ bv_val() [3/6]

expr bv_val ( int64_t  n,
unsigned  sz 
)
inline

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

2576 { 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:170
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:2434

§ bv_val() [4/6]

expr bv_val ( uint64_t  n,
unsigned  sz 
)
inline

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

2577 { 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:170
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:2434
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 2578 of file z3++.h.

2578 { 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:170
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:2434
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 2579 of file z3++.h.

2579  {
2580  array<Z3_bool> _bits(n);
2581  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
2582  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
2583  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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 170 of file z3++.h.

Referenced by object::check_error(), z3::concat(), z3::to_expr(), z3::to_func_decl(), and z3::to_sort().

170  {
171  Z3_error_code e = Z3_get_error_code(m_ctx);
172  if (e != Z3_OK && enable_exceptions())
173  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
174  return e;
175  }
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:93
Definition: z3_api.h:1321
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1319
bool enable_exceptions() const
Definition: z3++.h:195
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 177 of file z3++.h.

177  {
178  Z3_error_code e = Z3_get_error_code(*this);
179  if (e != Z3_OK && enable_exceptions()) {
180  Z3_string s = Z3_get_parser_error(*this);
181  if (s && *s) Z3_THROW(exception(s));
182  }
183  check_error();
184  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
#define Z3_THROW(x)
Definition: z3++.h:93
Definition: z3_api.h:1321
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1319
bool enable_exceptions() const
Definition: z3++.h:195
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
Z3_string Z3_API Z3_get_parser_error(Z3_context c)
Retrieve that last error message information generated from parsing.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:82

§ compute_interpolant()

check_result compute_interpolant ( expr const &  pat,
params const &  p,
expr_vector interp,
model m 
)
inline

Interpolation support.

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

2927  {
2928  Z3_ast_vector interp = 0;
2929  Z3_model mdl = 0;
2930  Z3_lbool r = Z3_compute_interpolant(*this, pat, p, &interp, &mdl);
2931  switch (r) {
2932  case Z3_L_FALSE:
2933  i = expr_vector(*this, interp);
2934  break;
2935  case Z3_L_TRUE:
2936  m = model(*this, mdl);
2937  break;
2938  case Z3_L_UNDEF:
2939  break;
2940  }
2941  return to_check_result(r);
2942  }
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:98
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:130
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68

§ constant() [1/2]

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

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

2548  {
2549  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2550  check_error();
2551  return expr(*this, r);
2552  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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 2553 of file z3++.h.

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

§ enable_exceptions()

bool enable_exceptions ( ) const
inline

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

195 { 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 2445 of file z3++.h.

2445  {
2446  array<Z3_symbol> _enum_names(n);
2447  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2448  array<Z3_func_decl> _cs(n);
2449  array<Z3_func_decl> _ts(n);
2450  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2451  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2452  check_error();
2453  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2454  return s;
2455  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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:1397

§ function() [1/9]

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

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

Referenced by z3::function().

2477  {
2478  array<Z3_sort> args(arity);
2479  for (unsigned i = 0; i < arity; i++) {
2480  check_context(domain[i], range);
2481  args[i] = domain[i];
2482  }
2483  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2484  check_error();
2485  return func_decl(*this, f);
2486  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

§ function() [2/9]

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

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

2488  {
2489  return function(range.ctx().str_symbol(name), arity, domain, range);
2490  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
context & ctx() const
Definition: z3++.h:373

§ function() [3/9]

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

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

2492  {
2493  array<Z3_sort> args(domain.size());
2494  for (unsigned i = 0; i < domain.size(); i++) {
2495  check_context(domain[i], range);
2496  args[i] = domain[i];
2497  }
2498  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2499  check_error();
2500  return func_decl(*this, f);
2501  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

§ function() [4/9]

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

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

2503  {
2504  return function(range.ctx().str_symbol(name), domain, range);
2505  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
context & ctx() const
Definition: z3++.h:373

§ function() [5/9]

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

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

2508  {
2509  check_context(domain, range);
2510  Z3_sort args[1] = { domain };
2511  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2512  check_error();
2513  return func_decl(*this, f);
2514  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

§ function() [6/9]

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

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

2516  {
2518  Z3_sort args[2] = { d1, d2 };
2519  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2520  check_error();
2521  return func_decl(*this, f);
2522  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

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

2524  {
2526  Z3_sort args[3] = { d1, d2, d3 };
2527  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2528  check_error();
2529  return func_decl(*this, f);
2530  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

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

2532  {
2534  Z3_sort args[4] = { d1, d2, d3, d4 };
2535  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2536  check_error();
2537  return func_decl(*this, f);
2538  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

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

2540  {
2542  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2543  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2544  check_error();
2545  return func_decl(*this, f);
2546  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:377

§ get_interpolant()

expr_vector get_interpolant ( expr const &  proof,
expr const &  pat,
params const &  p 
)
inline

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

2944  {
2945  return expr_vector(*this, Z3_get_interpolant(*this, proof, pat, p));
2946  }
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p)

§ int_const()

expr int_const ( char const *  name)
inline

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

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

§ int_sort()

sort int_sort ( )
inline

Return the integer sort.

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

2432 { 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:170
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 2429 of file z3++.h.

2429 { 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:170
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 2561 of file z3++.h.

2561 { 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:170
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:2432

§ int_val() [2/5]

expr int_val ( unsigned  n)
inline

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

2562 { 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:170
sort int_sort()
Return the integer sort.
Definition: z3++.h:2432

§ int_val() [3/5]

expr int_val ( int64_t  n)
inline

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

2563 { 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:170
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:2432

§ int_val() [4/5]

expr int_val ( uint64_t  n)
inline

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

2564 { 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:170
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:2432

§ int_val() [5/5]

expr int_val ( char const *  n)
inline

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

2565 { 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:170
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:2432

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

218 { 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 2588 of file z3++.h.

Referenced by z3::ashr(), z3::lshr(), z3::mod(), z3::operator &(), z3::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().

2588 { 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:170
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 165 of file z3++.h.

165 { return m_ctx; }

§ parse_file() [1/2]

expr parse_file ( char const *  file)
inline

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

2888  {
2889  Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
2891  return expr(*this, r);
2892  }
Z3_ast 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.
void check_parser_error() const
Definition: z3++.h:177

§ parse_file() [2/2]

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

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

2910  {
2911  array<Z3_symbol> sort_names(sorts.size());
2912  array<Z3_symbol> decl_names(decls.size());
2913  array<Z3_sort> sorts1(sorts);
2914  array<Z3_func_decl> decls1(decls);
2915  for (unsigned i = 0; i < sorts.size(); ++i) {
2916  sort_names[i] = sorts[i].name();
2917  }
2918  for (unsigned i = 0; i < decls.size(); ++i) {
2919  decl_names[i] = decls[i].name();
2920  }
2921  Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2923  return expr(*this, r);
2924  }
Z3_ast 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.
void check_parser_error() const
Definition: z3++.h:177

§ parse_string() [1/2]

expr parse_string ( char const *  s)
inline

parsing

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

2883  {
2884  Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
2886  return expr(*this, r);
2887  }
Z3_ast 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.
void check_parser_error() const
Definition: z3++.h:177

§ parse_string() [2/2]

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

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

2894  {
2895  array<Z3_symbol> sort_names(sorts.size());
2896  array<Z3_symbol> decl_names(decls.size());
2897  array<Z3_sort> sorts1(sorts);
2898  array<Z3_func_decl> decls1(decls);
2899  for (unsigned i = 0; i < sorts.size(); ++i) {
2900  sort_names[i] = sorts[i].name();
2901  }
2902  for (unsigned i = 0; i < decls.size(); ++i) {
2903  decl_names[i] = decls[i].name();
2904  }
2905  Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2907  return expr(*this, r);
2908  }
Z3_ast 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.
void check_parser_error() const
Definition: z3++.h:177

§ re_sort()

sort re_sort ( sort seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

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

2437 { 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:170
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 2556 of file z3++.h.

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

§ real_sort()

sort real_sort ( )
inline

Return the Real sort.

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

2433 { 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:170
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 2567 of file z3++.h.

2567 { 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:170
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 2568 of file z3++.h.

2568 { 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:170
sort real_sort()
Return the Real sort.
Definition: z3++.h:2433
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 2569 of file z3++.h.

2569 { 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:170
sort real_sort()
Return the Real sort.
Definition: z3++.h:2433

§ real_val() [4/6]

expr real_val ( int64_t  n)
inline

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

2570 { 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:170
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:2433

§ real_val() [5/6]

expr real_val ( uint64_t  n)
inline

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

2571 { 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:170
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:2433

§ real_val() [6/6]

expr real_val ( char const *  n)
inline

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

2572 { 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:170
sort real_sort()
Return the Real sort.
Definition: z3++.h:2433
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.

§ seq_sort()

sort seq_sort ( sort s)
inline

Return a sequence sort over base sort s.

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

2436 { 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:170
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 200 of file z3++.h.

200 { 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 204 of file z3++.h.

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

208  {
209  std::ostringstream oss;
210  oss << value;
211  Z3_update_param_value(m_ctx, param, oss.str().c_str());
212  }
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 very careful about using check_error() after calls that may result in an erroneous state.

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

193 { m_enable_exceptions = f; }

§ str_symbol()

symbol str_symbol ( char const *  s)
inline

Create a Z3 symbol based on the given string.

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

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

2428 { 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:170
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 2435 of file z3++.h.

2435 { 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:170
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 2585 of file z3++.h.

2585 { 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:170
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 2586 of file z3++.h.

2586 { 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:170
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 paramter. It contains the set of projection functions.

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

2456  {
2457  array<Z3_symbol> _names(n);
2458  array<Z3_sort> _sorts(n);
2459  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
2460  array<Z3_func_decl> _projs(n);
2461  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2462  Z3_func_decl tuple;
2463  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
2464  check_error();
2465  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
2466  return func_decl(*this, tuple);
2467  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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:1397

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

2469  {
2470  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2471  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2472  }
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:1397

§ uninterpreted_sort() [2/2]

sort uninterpreted_sort ( symbol const &  name)
inline

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

2473  {
2474  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2475  }
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:1397