Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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.
 
void set (char const *param, char const *value)
 Update global parameter param with string value.
 
void set (char const *param, bool value)
 Update global parameter param with Boolean value.
 
void set (char const *param, int value)
 Update global parameter param with Integer value.
 
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.
 
symbol str_symbol (char const *s)
 Create a Z3 symbol based on the given string.
 
symbol int_symbol (int n)
 Create a Z3 symbol based on the given integer.
 
sort bool_sort ()
 Return the Boolean sort.
 
sort int_sort ()
 Return the integer sort.
 
sort real_sort ()
 Return the Real sort.
 
sort bv_sort (unsigned sz)
 Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
 
sort array_sort (sort d, sort r)
 Return an array sort for arrays from d to r.
 
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 (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 110 of file z3++.h.

Constructor & Destructor Documentation

context ( )
inline

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

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

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

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

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

{ Z3_del_context(m_ctx); }

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

{ Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
expr bool_const ( char const *  name)
inline

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

{ return constant(name, bool_sort()); }
sort bool_sort ( )
inline

Return the Boolean sort.

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

Referenced by context::bool_const().

{ Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
expr bool_val ( bool  b)
inline

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

{ return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
expr bv_const ( char const *  name,
unsigned  sz 
)
inline

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

{ return constant(name, bv_sort(sz)); }
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 1418 of file z3++.h.

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

{ Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
expr bv_val ( int  n,
unsigned  sz 
)
inline

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

{ Z3_ast r = Z3_mk_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
expr bv_val ( unsigned  n,
unsigned  sz 
)
inline

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

{ Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
expr bv_val ( __int64  n,
unsigned  sz 
)
inline

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

{ Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
expr bv_val ( __uint64  n,
unsigned  sz 
)
inline

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

{ Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
expr bv_val ( char const *  n,
unsigned  sz 
)
inline

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

{ Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
void check_error ( ) const
inline
expr constant ( symbol const &  name,
sort const &  s 
)
inline

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

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

{
Z3_ast r = Z3_mk_const(m_ctx, name, s);
return expr(*this, r);
}
expr constant ( char const *  name,
sort const &  s 
)
inline

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

{ return constant(str_symbol(name), s); }
func_decl function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

Referenced by z3::function().

{
array<Z3_sort> args(arity);
for (unsigned i = 0; i < arity; i++) {
check_context(domain[i], range);
args[i] = domain[i];
}
Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
return func_decl(*this, f);
}
func_decl function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

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

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

{
check_context(domain, range);
Z3_sort args[1] = { domain };
Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
return func_decl(*this, f);
}
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

{
check_context(d1, range); check_context(d2, range);
Z3_sort args[2] = { d1, d2 };
Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
return func_decl(*this, f);
}
func_decl function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

{
check_context(d1, range); check_context(d2, range); check_context(d3, range);
Z3_sort args[3] = { d1, d2, d3 };
Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
return func_decl(*this, f);
}
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 1460 of file z3++.h.

{
check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
Z3_sort args[4] = { d1, d2, d3, d4 };
Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
return func_decl(*this, f);
}
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 1468 of file z3++.h.

{
check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
Z3_sort args[5] = { d1, d2, d3, d4, d5 };
Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
return func_decl(*this, f);
}
expr int_const ( char const *  name)
inline

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

{ return constant(name, int_sort()); }
sort int_sort ( )
inline

Return the integer sort.

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

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

{ Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
symbol int_symbol ( int  n)
inline

Create a Z3 symbol based on the given integer.

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

{ Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
expr int_val ( int  n)
inline

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

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

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

{ Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
expr int_val ( __int64  n)
inline

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

{ Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
expr int_val ( __uint64  n)
inline

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

{ Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
expr int_val ( char const *  n)
inline

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

{ Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
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 156 of file z3++.h.

{ Z3_interrupt(m_ctx); }
expr num_val ( int  n,
sort const &  s 
)
inline

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

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

{ Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
operator Z3_context ( ) const
inline

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

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

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

{ return constant(name, real_sort()); }
sort real_sort ( )
inline

Return the Real sort.

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

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

{ Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
expr real_val ( int  n,
int  d 
)
inline

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

{ Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); }
expr real_val ( int  n)
inline

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

{ Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
expr real_val ( unsigned  n)
inline

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

{ Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
expr real_val ( __int64  n)
inline

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

{ Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
expr real_val ( __uint64  n)
inline

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

{ Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
expr real_val ( char const *  n)
inline

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

{ Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
void set ( char const *  param,
char const *  value 
)
inline

Update global parameter param with string value.

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

{ Z3_update_param_value(m_ctx, param, value); }
void set ( char const *  param,
bool  value 
)
inline

Update global parameter param with Boolean value.

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

{ Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
void set ( char const *  param,
int  value 
)
inline

Update global parameter param with Integer value.

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

{
std::ostringstream oss;
oss << value;
Z3_update_param_value(m_ctx, param, oss.str().c_str());
}
symbol str_symbol ( char const *  s)
inline

Create a Z3 symbol based on the given string.

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

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

{ Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }