Z3
Data Structures | Typedefs | Enumerations | Functions
z3 Namespace Reference
C++ API

Z3 C++ namespace. More...

Data Structures

class  exception
 Exception used to sign API usage errors. More...
class  config
 Z3 global configuration object. More...
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
class  array
class  object
class  symbol
class  params
class  ast
class  sort
 A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
class  func_decl
 Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
class  expr
 A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
class  cast_ast< ast >
class  cast_ast< expr >
class  cast_ast< sort >
class  cast_ast< func_decl >
class  ast_vector_tpl
class  func_entry
class  func_interp
class  model
class  stats
class  solver
class  goal
class  apply_result
class  tactic
class  probe

Typedefs

typedef ast_vector_tpl< ast > ast_vector
typedef ast_vector_tpl< expr > expr_vector
typedef ast_vector_tpl< sort > sort_vector
typedef ast_vector_tpl< func_decl > func_decl_vector

Enumerations

enum  check_result { unsat, sat, unknown }

Functions

void set_param (char const *param, char const *value)
void set_param (char const *param, bool value)
void set_param (char const *param, int value)
void reset_params ()
void check_context (object const &a, object const &b)
bool eq (ast const &a, ast const &b)
expr implies (expr const &a, bool b)
expr implies (bool a, expr const &b)
expr pw (expr const &a, expr const &b)
expr pw (expr const &a, int b)
expr pw (int a, expr const &b)
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e)
expr to_expr (context &c, Z3_ast a)
 Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.
sort to_sort (context &c, Z3_sort s)
func_decl to_func_decl (context &c, Z3_func_decl f)
expr ule (expr const &a, expr const &b)
 unsigned less than or equal to operator for bitvectors.
expr ule (expr const &a, int b)
expr ule (int a, expr const &b)
expr ult (expr const &a, expr const &b)
 unsigned less than operator for bitvectors.
expr ult (expr const &a, int b)
expr ult (int a, expr const &b)
expr uge (expr const &a, expr const &b)
 unsigned greater than or equal to operator for bitvectors.
expr uge (expr const &a, int b)
expr uge (int a, expr const &b)
expr ugt (expr const &a, expr const &b)
 unsigned greater than operator for bitvectors.
expr ugt (expr const &a, int b)
expr ugt (int a, expr const &b)
expr udiv (expr const &a, expr const &b)
 unsigned division operator for bitvectors.
expr udiv (expr const &a, int b)
expr udiv (int a, expr const &b)
expr forall (expr const &x, expr const &b)
expr forall (expr const &x1, expr const &x2, expr const &b)
expr forall (expr const &x1, expr const &x2, expr const &x3, expr const &b)
expr forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
expr forall (expr_vector const &xs, expr const &b)
expr exists (expr const &x, expr const &b)
expr exists (expr const &x1, expr const &x2, expr const &b)
expr exists (expr const &x1, expr const &x2, expr const &x3, expr const &b)
expr exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
expr exists (expr_vector const &xs, expr const &b)
expr distinct (expr_vector const &args)
std::ostream & operator<< (std::ostream &out, check_result r)
check_result to_check_result (Z3_lbool l)
tactic repeat (tactic const &t, unsigned max=UINT_MAX)
tactic with (tactic const &t, params const &p)
tactic try_for (tactic const &t, unsigned ms)
tactic fail_if (probe const &p)
tactic when (probe const &p, tactic const &t)
tactic cond (probe const &p, tactic const &t1, tactic const &t2)
expr to_real (expr const &a)
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 select (expr const &a, expr const &i)
expr select (expr const &a, int i)
expr store (expr const &a, expr const &i, expr const &v)
expr store (expr const &a, int i, expr const &v)
expr store (expr const &a, expr i, int v)
expr store (expr const &a, int i, int v)
expr const_array (sort const &d, expr const &v)

Detailed Description

Z3 C++ namespace.

Typedef Documentation

typedef ast_vector_tpl<ast> ast_vector

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

typedef ast_vector_tpl<expr> expr_vector

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

typedef ast_vector_tpl<func_decl> func_decl_vector

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

typedef ast_vector_tpl<sort> sort_vector

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

Enumeration Type Documentation

enum check_result
Enumerator:
unsat 
sat 
unknown 

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

                      {
        unsat, sat, unknown
    };

Function Documentation

void z3::check_context ( object const &  a,
object const &  b 
) [inline]

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

Referenced by cond(), const_array(), exists(), forall(), context::function(), ite(), pw(), select(), store(), and when().

{ assert(a.m_ctx == b.m_ctx); }
tactic z3::cond ( probe const &  p,
tactic const &  t1,
tactic const &  t2 
) [inline]

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

                                                                              {
        check_context(p, t1); check_context(p, t2);
        Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
        t1.check_error();
        return tactic(t1.ctx(), r);
    }
expr z3::const_array ( sort const &  d,
expr const &  v 
) [inline]

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

                                                            {
        check_context(d, v);
        Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
        d.check_error();
        return expr(d.ctx(), r);
    }
expr z3::distinct ( expr_vector const &  args) [inline]

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

                                                  {
        assert(args.size() > 0);
        context& ctx = args[0].ctx();
        array<Z3_ast> _args(args);
        Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
        ctx.check_error();
        return expr(ctx, r);
    }
bool z3::eq ( ast const &  a,
ast const &  b 
) [inline]

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

{ return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
expr z3::exists ( expr const &  x,
expr const &  b 
) [inline]

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

                                                       {
        check_context(x, b);
        Z3_app vars[] = {(Z3_app) x}; 
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  b 
) [inline]

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

                                                                         {
        check_context(x1, b); check_context(x2, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; 
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
) [inline]

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

                                                                                          {
        check_context(x1, b); check_context(x2, b); check_context(x3, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; 
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
) [inline]

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

                                                                                                           {
        check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; 
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::exists ( expr_vector const &  xs,
expr const &  b 
) [inline]

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

                                                               {
        array<Z3_app> vars(xs);  
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
tactic z3::fail_if ( probe const &  p) [inline]

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

                                           {
        Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
        p.check_error();
        return tactic(p.ctx(), r);
    }
expr z3::forall ( expr const &  x,
expr const &  b 
) [inline]

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

                                                       {
        check_context(x, b);
        Z3_app vars[] = {(Z3_app) x}; 
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  b 
) [inline]

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

                                                                         {
        check_context(x1, b); check_context(x2, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; 
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
) [inline]

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

                                                                                          {
        check_context(x1, b); check_context(x2, b); check_context(x3, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; 
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
) [inline]

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

                                                                                                           {
        check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; 
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
expr z3::forall ( expr_vector const &  xs,
expr const &  b 
) [inline]

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

                                                               {
        array<Z3_app> vars(xs);  
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }
func_decl z3::function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
) [inline]

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

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

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

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

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

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

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

                                                                                                       {
        return range.ctx().function(name, d1, d2, range);
    }
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
) [inline]

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

                                                                                                                        {
        return range.ctx().function(name, d1, d2, d3, range);
    }
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  d4,
sort const &  range 
) [inline]

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

                                                                                                                                         {
        return range.ctx().function(name, d1, d2, d3, d4, range);
    }
func_decl z3::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 1761 of file z3++.h.

                                                                                                                                                          {
        return range.ctx().function(name, d1, d2, d3, d4, d5, range);
    }
expr z3::implies ( expr const &  a,
bool  b 
) [inline]

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

Referenced by implies().

{ return implies(a, a.ctx().bool_val(b)); }
expr z3::implies ( bool  a,
expr const &  b 
) [inline]

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

{ return implies(b.ctx().bool_val(a), b); }
expr z3::ite ( expr const &  c,
expr const &  t,
expr const &  e 
) [inline]

Create the if-then-else expression ite(c, t, e)

Precondition:
c.is_bool()

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

                                                                    {
        check_context(c, t); check_context(c, e);
        assert(c.is_bool());
        Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
        c.check_error();
        return expr(c.ctx(), r);
    }
std::ostream& z3::operator<< ( std::ostream &  out,
check_result  r 
) [inline]

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

                                                                     { 
        if (r == unsat) out << "unsat";
        else if (r == sat) out << "sat";
        else out << "unknown";
        return out;
    }
expr z3::pw ( expr const &  a,
expr const &  b 
) [inline]

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

Referenced by pw().

                                                   {
        assert(a.is_arith() && b.is_arith());
        check_context(a, b);
        Z3_ast r = Z3_mk_power(a.ctx(), a, b);
        a.check_error();
        return expr(a.ctx(), r);
    }
expr z3::pw ( expr const &  a,
int  b 
) [inline]

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

{ return pw(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::pw ( int  a,
expr const &  b 
) [inline]

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

{ return pw(b.ctx().num_val(a, b.get_sort()), b); }
tactic z3::repeat ( tactic const &  t,
unsigned  max = UINT_MAX 
) [inline]

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

                                                                  {
        Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
        t.check_error();
        return tactic(t.ctx(), r);
    }
void z3::reset_params ( ) [inline]

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

{ Z3_global_param_reset_all(); }
expr z3::select ( expr const &  a,
expr const &  i 
) [inline]

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

Referenced by select().

                                                       {
        check_context(a, i);
        Z3_ast r = Z3_mk_select(a.ctx(), a, i);
        a.check_error();
        return expr(a.ctx(), r);
    }
expr z3::select ( expr const &  a,
int  i 
) [inline]

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

{ return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
void z3::set_param ( char const *  param,
char const *  value 
) [inline]

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

{ Z3_global_param_set(param, value); }
void z3::set_param ( char const *  param,
bool  value 
) [inline]

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

{ Z3_global_param_set(param, value ? "true" : "false"); }
void z3::set_param ( char const *  param,
int  value 
) [inline]

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

{ std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
expr z3::store ( expr const &  a,
expr const &  i,
expr const &  v 
) [inline]

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

Referenced by store().

                                                                      {
        check_context(a, i); check_context(a, v);
        Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
        a.check_error();
        return expr(a.ctx(), r);
    }
expr z3::store ( expr const &  a,
int  i,
expr const &  v 
) [inline]

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

{ return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
expr z3::store ( expr const &  a,
expr  i,
int  v 
) [inline]

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

{ return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
expr z3::store ( expr const &  a,
int  i,
int  v 
) [inline]

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

                                                    { 
        return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range())); 
    }
check_result z3::to_check_result ( Z3_lbool  l) [inline]

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

Referenced by solver::check().

                                                    {
        if (l == Z3_L_TRUE) return sat;
        else if (l == Z3_L_FALSE) return unsat;
        return unknown;
    }
expr z3::to_expr ( context &  c,
Z3_ast  a 
) [inline]

Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.

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

Referenced by udiv(), uge(), ugt(), ule(), and ult().

                                               {
        c.check_error();
        assert(Z3_get_ast_kind(c, a) == Z3_APP_AST || 
               Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || 
               Z3_get_ast_kind(c, a) == Z3_VAR_AST || 
               Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST);
        return expr(c, a);
    }
func_decl z3::to_func_decl ( context &  c,
Z3_func_decl  f 
) [inline]

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

                                                               {
        c.check_error();
        return func_decl(c, f);
    }
expr z3::to_real ( expr const &  a) [inline]

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

{ Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
sort z3::to_sort ( context &  c,
Z3_sort  s 
) [inline]

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

Referenced by context::enumeration_sort().

                                                {
        c.check_error();
        return sort(c, s);
    }
tactic z3::try_for ( tactic const &  t,
unsigned  ms 
) [inline]

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

                                                         {
        Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
        t.check_error();
        return tactic(t.ctx(), r);
    }
expr z3::udiv ( expr const &  a,
expr const &  b 
) [inline]

unsigned division operator for bitvectors.

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

Referenced by udiv().

{ return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
expr z3::udiv ( expr const &  a,
int  b 
) [inline]

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

{ return udiv(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::udiv ( int  a,
expr const &  b 
) [inline]

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

{ return udiv(b.ctx().num_val(a, b.get_sort()), b); }
expr z3::uge ( expr const &  a,
expr const &  b 
) [inline]

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

{ return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
expr z3::uge ( expr const &  a,
int  b 
) [inline]

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

{ return uge(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::uge ( int  a,
expr const &  b 
) [inline]

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

{ return uge(b.ctx().num_val(a, b.get_sort()), b); }
expr z3::ugt ( expr const &  a,
expr const &  b 
) [inline]

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

{ return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
expr z3::ugt ( expr const &  a,
int  b 
) [inline]

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

{ return ugt(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::ugt ( int  a,
expr const &  b 
) [inline]

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

{ return ugt(b.ctx().num_val(a, b.get_sort()), b); }
expr z3::ule ( expr const &  a,
expr const &  b 
) [inline]

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

{ return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
expr z3::ule ( expr const &  a,
int  b 
) [inline]

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

{ return ule(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::ule ( int  a,
expr const &  b 
) [inline]

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

{ return ule(b.ctx().num_val(a, b.get_sort()), b); }
expr z3::ult ( expr const &  a,
expr const &  b 
) [inline]

unsigned less than operator for bitvectors.

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

Referenced by ult().

{ return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
expr z3::ult ( expr const &  a,
int  b 
) [inline]

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

{ return ult(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::ult ( int  a,
expr const &  b 
) [inline]

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

{ return ult(b.ctx().num_val(a, b.get_sort()), b); }
tactic z3::when ( probe const &  p,
tactic const &  t 
) [inline]

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

                                                          {
        check_context(p, t);
        Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
        t.check_error();
        return tactic(t.ctx(), r);
    }
tactic z3::with ( tactic const &  t,
params const &  p 
) [inline]

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

                                                           {
        Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
        t.check_error();
        return tactic(t.ctx(), r);
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Generated on Sat Apr 2 2016 19:31:12 for Z3 by   doxygen 1.7.6.1