Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions
context Class Reference

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

Public Member Functions

 context ()
 
 context (config &c)
 
 ~context ()
 
 operator Z3_context () const
 
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 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...
 
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 num_val (int n, sort const &s)
 

Detailed Description

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

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

Constructor & Destructor Documentation

context ( )
inline

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

133 { config c; init(c); }
context ( config c)
inline

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

134 { init(c); }
~context ( )
inline

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

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

Member Function Documentation

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

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

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

1631 { return constant(name, bool_sort()); }
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:1537
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1625
sort bool_sort ( )
inline

Return the Boolean sort.

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

Referenced by context::bool_const().

1537 { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_bool_sort(__in Z3_context c)
Create the Boolean type.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr bool_val ( bool  b)
inline

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

Referenced by goal::as_expr(), and z3::implies().

1636 { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
Z3_ast Z3_API Z3_mk_true(__in Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false(__in Z3_context c)
Create an AST node representing false.
expr bv_const ( char const *  name,
unsigned  sz 
)
inline

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

1634 { 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:1540
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1625
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 1540 of file z3++.h.

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

1540 { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_bv_sort(__in Z3_context c, __in 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:141
expr bv_val ( int  n,
unsigned  sz 
)
inline

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

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

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

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

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

1653 { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
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:1540
Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr bv_val ( __uint64  n,
unsigned  sz 
)
inline

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

1654 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
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:1540
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
expr bv_val ( char const *  n,
unsigned  sz 
)
inline

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

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

Auxiliary method used to check for API usage errors.

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

Referenced by context::array_sort(), context::bool_sort(), context::bv_sort(), context::bv_val(), object::check_error(), context::constant(), context::enumeration_sort(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::num_val(), func_decl::operator()(), context::real_sort(), context::real_val(), context::str_symbol(), z3::to_expr(), z3::to_func_decl(), and z3::to_sort().

141  {
142  Z3_error_code e = Z3_get_error_code(m_ctx);
143  if (e != Z3_OK)
144  throw exception(Z3_get_error_msg_ex(m_ctx, e));
145  }
Definition: z3_api.h:1150
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_error_msg_ex(__in Z3_context c, __in Z3_error_code err)
Return a string describing the given error code.
Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c)
Return the error code for the last API call.
expr constant ( symbol const &  name,
sort const &  s 
)
inline

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

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

1625  {
1626  Z3_ast r = Z3_mk_const(m_ctx, name, s);
1627  check_error();
1628  return expr(*this, r);
1629  }
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr constant ( char const *  name,
sort const &  s 
)
inline

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

1630 { return constant(str_symbol(name), s); }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1625
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 1542 of file z3++.h.

1542  {
1543  array<Z3_symbol> _enum_names(n);
1544  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
1545  array<Z3_func_decl> _cs(n);
1546  array<Z3_func_decl> _ts(n);
1547  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
1548  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
1549  check_error();
1550  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
1551  return s;
1552  }
Z3_sort Z3_API Z3_mk_enumeration_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned n, __in_ecount(n) Z3_symbol const enum_names[], __out_ecount(n) Z3_func_decl enum_consts[], __out_ecount(n) Z3_func_decl enum_testers[])
Create a enumeration sort.
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in 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:141
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:936
func_decl function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

Referenced by z3::function().

1554  {
1555  array<Z3_sort> args(arity);
1556  for (unsigned i = 0; i < arity; i++) {
1557  check_context(domain[i], range);
1558  args[i] = domain[i];
1559  }
1560  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
1561  check_error();
1562  return func_decl(*this, f);
1563  }
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
func_decl function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

1565  {
1566  return function(range.ctx().str_symbol(name), arity, domain, range);
1567  }
func_decl function ( symbol const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

1569  {
1570  array<Z3_sort> args(domain.size());
1571  for (unsigned i = 0; i < domain.size(); i++) {
1572  check_context(domain[i], range);
1573  args[i] = domain[i];
1574  }
1575  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
1576  check_error();
1577  return func_decl(*this, f);
1578  }
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
func_decl function ( char const *  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

1580  {
1581  return function(range.ctx().str_symbol(name), domain, range);
1582  }
func_decl function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

1585  {
1586  check_context(domain, range);
1587  Z3_sort args[1] = { domain };
1588  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
1589  check_error();
1590  return func_decl(*this, f);
1591  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

1593  {
1594  check_context(d1, range); check_context(d2, range);
1595  Z3_sort args[2] = { d1, d2 };
1596  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
1597  check_error();
1598  return func_decl(*this, f);
1599  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

1601  {
1602  check_context(d1, range); check_context(d2, range); check_context(d3, range);
1603  Z3_sort args[3] = { d1, d2, d3 };
1604  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
1605  check_error();
1606  return func_decl(*this, f);
1607  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
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 1609 of file z3++.h.

1609  {
1610  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
1611  Z3_sort args[4] = { d1, d2, d3, d4 };
1612  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
1613  check_error();
1614  return func_decl(*this, f);
1615  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
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 1617 of file z3++.h.

1617  {
1618  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
1619  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
1620  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
1621  check_error();
1622  return func_decl(*this, f);
1623  }
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
void check_context(object const &a, object const &b)
Definition: z3++.h:276
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
expr int_const ( char const *  name)
inline

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

1632 { return constant(name, int_sort()); }
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1625
sort int_sort()
Return the integer sort.
Definition: z3++.h:1538
sort int_sort ( )
inline

Return the integer sort.

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

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

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

Create a Z3 symbol based on the given integer.

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

1535 { 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:141
Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i)
Create a Z3 symbol using an integer.
expr int_val ( int  n)
inline

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

1638 { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort int_sort()
Return the integer sort.
Definition: z3++.h:1538
expr int_val ( unsigned  n)
inline

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

1639 { 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(__in Z3_context c, __in unsigned v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort int_sort()
Return the integer sort.
Definition: z3++.h:1538
expr int_val ( __int64  n)
inline

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

1640 { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort int_sort()
Return the integer sort.
Definition: z3++.h:1538
expr int_val ( __uint64  n)
inline

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

1641 { 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:141
Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in 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:1538
expr int_val ( char const *  n)
inline

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

1642 { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
sort int_sort()
Return the integer sort.
Definition: z3++.h:1538
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 168 of file z3++.h.

168 { Z3_interrupt(m_ctx); }
void Z3_API Z3_interrupt(__in Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
expr num_val ( int  n,
sort const &  s 
)
inline

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

Referenced by func_decl::operator()(), z3::pw(), z3::select(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), and z3::ult().

1657 { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
operator Z3_context ( ) const
inline

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

136 { return m_ctx; }
expr real_const ( char const *  name)
inline

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

1633 { return constant(name, real_sort()); }
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1625
sort real_sort()
Return the Real sort.
Definition: z3++.h:1539
sort real_sort ( )
inline

Return the Real sort.

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

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

1539 { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
Z3_sort Z3_API Z3_mk_real_sort(__in Z3_context c)
Create the real type.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr real_val ( int  n,
int  d 
)
inline

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

1644 { 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:141
Z3_ast Z3_API Z3_mk_real(__in Z3_context c, __in int num, __in int den)
Create a real from a fraction.
expr real_val ( int  n)
inline

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

1645 { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
sort real_sort()
Return the Real sort.
Definition: z3++.h:1539
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr real_val ( unsigned  n)
inline

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

1646 { 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(__in Z3_context c, __in unsigned v, __in 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:1539
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr real_val ( __int64  n)
inline

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

1647 { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
sort real_sort()
Return the Real sort.
Definition: z3++.h:1539
Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
expr real_val ( __uint64  n)
inline

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

1648 { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
sort real_sort()
Return the Real sort.
Definition: z3++.h:1539
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
expr real_val ( char const *  n)
inline

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

1649 { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
sort real_sort()
Return the Real sort.
Definition: z3++.h:1539
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
void set ( char const *  param,
char const *  value 
)
inline

Update global parameter param with string value.

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

150 { Z3_update_param_value(m_ctx, param, value); }
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value)
Set a value of a context parameter.
void set ( char const *  param,
bool  value 
)
inline

Update global parameter param with Boolean value.

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

154 { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value)
Set a value of a context parameter.
void set ( char const *  param,
int  value 
)
inline

Update global parameter param with Integer value.

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

158  {
159  std::ostringstream oss;
160  oss << value;
161  Z3_update_param_value(m_ctx, param, oss.str().c_str());
162  }
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value)
Set a value of a context parameter.
symbol str_symbol ( char const *  s)
inline

Create a Z3 symbol based on the given string.

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

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

1534 { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in 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:141