Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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.
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.
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.

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

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

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

Definition at line 135 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 1541 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 1631 of file z3++.h.

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

Return the Boolean sort.

Definition at line 1537 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 1636 of file z3++.h.

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

{ 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 1634 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 1540 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 1651 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 1652 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 1653 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 1654 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 1655 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 1625 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 1630 of file z3++.h.

{ return constant(str_symbol(name), s); }
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.

                                                                                                                                                      {
        array<Z3_symbol> _enum_names(n);
        for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
        array<Z3_func_decl> _cs(n);
        array<Z3_func_decl> _ts(n);
        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
        sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
        check_error();
        for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
        return s;
    }
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().

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

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

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

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

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

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

Definition at line 1585 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 1593 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 1601 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 1609 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 1617 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 1632 of file z3++.h.

{ return constant(name, int_sort()); }
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().

{ 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 1535 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 1638 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 1639 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 1640 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 1641 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 1642 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 168 of file z3++.h.

{ Z3_interrupt(m_ctx); }
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().

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

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

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

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

{ return constant(name, real_sort()); }
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().

{ 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 1644 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 1645 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 1646 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 1647 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 1648 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 1649 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 150 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 154 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 158 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 1534 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); }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines