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

Auxiliary method used to check for API usage errors.

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

Referenced by context::array_sort(), context::bool_sort(), context::bv_sort(), context::bv_val(), object::check_error(), context::constant(), 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().

                                 {
            Z3_error_code e = Z3_get_error_code(m_ctx);
            if (e != Z3_OK)
                throw exception(Z3_get_error_msg_ex(m_ctx, e));
        }

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); 
        check_error(); 
        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);
        check_error();
        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);
        check_error();
        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);
        check_error();
        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);
        check_error();
        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);
        check_error();
        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);
        check_error();
        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); }