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
 
void check_error () const
 Auxiliary method used to check for API usage errors. More...
 
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 actualy 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 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...
 
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 n)
 
expr int_val (__uint64 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 n)
 
expr real_val (__uint64 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 n, unsigned sz)
 
expr bv_val (__uint64 n, unsigned sz)
 
expr bv_val (char const *n, unsigned sz)
 
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 134 of file z3++.h.

Constructor & Destructor Documentation

§ context() [1/3]

context ( )
inline

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

153 { config c; init(c); }

§ context() [2/3]

context ( config c)
inline

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

154 { init(c); }

§ context() [3/3]

context ( config c,
interpolation   
)
inline

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

155 { init_interp(c); }

§ ~context()

~context ( )
inline

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

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

Member Function Documentation

§ array_sort()

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

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

§ bool_const()

expr bool_const ( char const *  name)
inline

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

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

§ bool_sort()

sort bool_sort ( )
inline

Return the Boolean sort.

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

2087 { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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 2197 of file z3++.h.

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

2197 { 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 2195 of file z3++.h.

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

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

2090 { 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.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ bv_val() [1/5]

expr bv_val ( int  n,
unsigned  sz 
)
inline

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

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

§ bv_val() [2/5]

expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

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

2213 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:2090

§ bv_val() [3/5]

expr bv_val ( __int64  n,
unsigned  sz 
)
inline

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

2214 { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:2090

§ bv_val() [4/5]

expr bv_val ( __uint64  n,
unsigned  sz 
)
inline

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

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

§ bv_val() [5/5]

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

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

2216 { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:2090

§ check_error()

void check_error ( ) const
inline

Auxiliary method used to check for API usage errors.

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

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

162  {
163  Z3_error_code e = Z3_get_error_code(m_ctx);
164  if (e != Z3_OK)
165  throw exception(Z3_get_error_msg(m_ctx, e));
166  }
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Definition: z3_api.h:1288
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1286
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.

§ compute_interpolant()

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

Interpolation support.

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

2514  {
2515  Z3_ast_vector interp = 0;
2516  Z3_model mdl = 0;
2517  Z3_lbool r = Z3_compute_interpolant(*this, pat, p, &interp, &mdl);
2518  switch (r) {
2519  case Z3_L_FALSE:
2520  i = expr_vector(*this, interp);
2521  break;
2522  case Z3_L_TRUE:
2523  m = model(*this, mdl);
2524  break;
2525  case Z3_L_UNDEF:
2526  break;
2527  }
2528  return to_check_result(r);
2529  }
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:105
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
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 2186 of file z3++.h.

2186  {
2187  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2188  check_error();
2189  return expr(*this, r);
2190  }
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ constant() [2/2]

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

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

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

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

2096  {
2097  array<Z3_symbol> _enum_names(n);
2098  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2099  array<Z3_func_decl> _cs(n);
2100  array<Z3_func_decl> _ts(n);
2101  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2102  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2103  check_error();
2104  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2105  return s;
2106  }
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:1259

§ function() [1/9]

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

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

Referenced by z3::function().

2115  {
2116  array<Z3_sort> args(arity);
2117  for (unsigned i = 0; i < arity; i++) {
2118  check_context(domain[i], range);
2119  args[i] = domain[i];
2120  }
2121  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2122  check_error();
2123  return func_decl(*this, f);
2124  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

§ function() [2/9]

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

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

2126  {
2127  return function(range.ctx().str_symbol(name), arity, domain, range);
2128  }

§ function() [3/9]

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

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

2130  {
2131  array<Z3_sort> args(domain.size());
2132  for (unsigned i = 0; i < domain.size(); i++) {
2133  check_context(domain[i], range);
2134  args[i] = domain[i];
2135  }
2136  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2137  check_error();
2138  return func_decl(*this, f);
2139  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

§ function() [4/9]

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

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

2141  {
2142  return function(range.ctx().str_symbol(name), domain, range);
2143  }

§ function() [5/9]

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

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

2146  {
2147  check_context(domain, range);
2148  Z3_sort args[1] = { domain };
2149  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2150  check_error();
2151  return func_decl(*this, f);
2152  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2084
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

§ function() [6/9]

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

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

2154  {
2155  check_context(d1, range); check_context(d2, range);
2156  Z3_sort args[2] = { d1, d2 };
2157  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2158  check_error();
2159  return func_decl(*this, f);
2160  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2084
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

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

2162  {
2163  check_context(d1, range); check_context(d2, range); check_context(d3, range);
2164  Z3_sort args[3] = { d1, d2, d3 };
2165  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2166  check_error();
2167  return func_decl(*this, f);
2168  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2084
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

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

2170  {
2171  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
2172  Z3_sort args[4] = { d1, d2, d3, d4 };
2173  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2174  check_error();
2175  return func_decl(*this, f);
2176  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2084
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

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

2178  {
2179  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
2180  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2181  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2182  check_error();
2183  return func_decl(*this, f);
2184  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2084
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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:336

§ get_interpolant()

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

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

2531  {
2532  return expr_vector(*this, Z3_get_interpolant(*this, proof, pat, p));
2533  }
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 2193 of file z3++.h.

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

§ int_sort()

sort int_sort ( )
inline

Return the integer sort.

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

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

§ int_symbol()

symbol int_symbol ( int  n)
inline

Create a Z3 symbol based on the given integer.

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

2085 { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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 2199 of file z3++.h.

2199 { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort int_sort()
Return the integer sort.
Definition: z3++.h:2088

§ int_val() [2/5]

expr int_val ( unsigned  n)
inline

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

2200 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort int_sort()
Return the integer sort.
Definition: z3++.h:2088

§ int_val() [3/5]

expr int_val ( __int64  n)
inline

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

2201 { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort int_sort()
Return the integer sort.
Definition: z3++.h:2088

§ int_val() [4/5]

expr int_val ( __uint64  n)
inline

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

2202 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort int_sort()
Return the integer sort.
Definition: z3++.h:2088

§ int_val() [5/5]

expr int_val ( char const *  n)
inline

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

2203 { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort int_sort()
Return the integer sort.
Definition: z3++.h:2088

§ 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 actualy stop.

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

189 { 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 2221 of file z3++.h.

Referenced by z3::ashr(), z3::lshr(), 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::select(), z3::shl(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

2221 { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ operator Z3_context()

operator Z3_context ( ) const
inline

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

157 { return m_ctx; }

§ parse_file() [1/2]

expr parse_file ( char const *  file)
inline

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

2475  {
2476  Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
2477  check_error();
2478  return expr(*this, r);
2479  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.

§ parse_file() [2/2]

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

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

2497  {
2498  array<Z3_symbol> sort_names(sorts.size());
2499  array<Z3_symbol> decl_names(decls.size());
2500  array<Z3_sort> sorts1(sorts);
2501  array<Z3_func_decl> decls1(decls);
2502  for (unsigned i = 0; i < sorts.size(); ++i) {
2503  sort_names[i] = sorts[i].name();
2504  }
2505  for (unsigned i = 0; i < decls.size(); ++i) {
2506  decl_names[i] = decls[i].name();
2507  }
2508  Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2509  check_error();
2510  return expr(*this, r);
2511  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.

§ parse_string() [1/2]

expr parse_string ( char const *  s)
inline

parsing

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

2469  {
2470  Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
2471  check_error();
2472  return expr(*this, r);
2473 
2474  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.

§ parse_string() [2/2]

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

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

2481  {
2482  array<Z3_symbol> sort_names(sorts.size());
2483  array<Z3_symbol> decl_names(decls.size());
2484  array<Z3_sort> sorts1(sorts);
2485  array<Z3_func_decl> decls1(decls);
2486  for (unsigned i = 0; i < sorts.size(); ++i) {
2487  sort_names[i] = sorts[i].name();
2488  }
2489  for (unsigned i = 0; i < decls.size(); ++i) {
2490  decl_names[i] = decls[i].name();
2491  }
2492  Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2493  check_error();
2494  return expr(*this, r);
2495  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.

§ re_sort()

sort re_sort ( sort seq_sort)
inline

Return a regular expression sort over sequences seq_sort.

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

2093 { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ real_const()

expr real_const ( char const *  name)
inline

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

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

§ real_sort()

sort real_sort ( )
inline

Return the Real sort.

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

2089 { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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 2205 of file z3++.h.

2205 { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ real_val() [2/6]

expr real_val ( int  n)
inline

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

2206 { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort real_sort()
Return the Real sort.
Definition: z3++.h:2089

§ real_val() [3/6]

expr real_val ( unsigned  n)
inline

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

2207 { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort real_sort()
Return the Real sort.
Definition: z3++.h:2089

§ real_val() [4/6]

expr real_val ( __int64  n)
inline

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

2208 { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort real_sort()
Return the Real sort.
Definition: z3++.h:2089

§ real_val() [5/6]

expr real_val ( __uint64  n)
inline

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

2209 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort real_sort()
Return the Real sort.
Definition: z3++.h:2089

§ real_val() [6/6]

expr real_val ( char const *  n)
inline

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

2210 { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
sort real_sort()
Return the Real sort.
Definition: z3++.h:2089

§ seq_sort()

sort seq_sort ( sort s)
inline

Return a sequence sort over base sort s.

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

2092 { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ set() [1/3]

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

Update global parameter param with string value.

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

171 { 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 175 of file z3++.h.

175 { 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 179 of file z3++.h.

179  {
180  std::ostringstream oss;
181  oss << value;
182  Z3_update_param_value(m_ctx, param, oss.str().c_str());
183  }
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.

§ str_symbol()

symbol str_symbol ( char const *  s)
inline

Create a Z3 symbol based on the given string.

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

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

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

§ string_sort()

sort string_sort ( )
inline

Return the sort for ASCII strings.

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

2091 { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ string_val() [1/2]

expr string_val ( char const *  s)
inline

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

2218 { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

§ string_val() [2/2]

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

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

2219 { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162

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

2107  {
2108  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2109  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2110  }
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:1259

§ uninterpreted_sort() [2/2]

sort uninterpreted_sort ( symbol const &  name)
inline

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

2111  {
2112  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2113  }
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:1259