z3 Namespace Reference

Z3 C++ namespace. More...

Data Structures
class	apply_result
class	array
class	ast
class	ast_vector_tpl
class	cast_ast
class	cast_ast< ast >
class	cast_ast< expr >
class	cast_ast< func_decl >
class	cast_ast< sort >
class	config
	Z3 global configuration object. More...
class	context
	A Context manages all other Z3 objects, global configuration options, etc. More...
class	exception
	Exception used to sign API usage errors. 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	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	func_entry
class	func_interp
class	goal
class	model
class	object
class	optimize
class	param_descrs
class	params
class	probe
class	solver
class	sort
	A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
class	stats
class	symbol
class	tactic

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 ()
std::ostream &	operator<< (std::ostream &out, exception const &e)
check_result	to_check_result (Z3_lbool l)
void	check_context (object const &a, object const &b)
std::ostream &	operator<< (std::ostream &out, symbol const &s)
std::ostream &	operator<< (std::ostream &out, param_descrs const &d)
std::ostream &	operator<< (std::ostream &out, params const &p)
std::ostream &	operator<< (std::ostream &out, ast const &n)
bool	eq (ast const &a, ast const &b)
expr	implies (expr const &a, expr 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	operator! (expr const &a)
expr	operator && (expr const &a, expr const &b)
expr	operator && (expr const &a, bool b)
expr	operator && (bool a, expr const &b)
expr	operator|| (expr const &a, expr const &b)
expr	operator|| (expr const &a, bool b)
expr	operator|| (bool a, expr const &b)
expr	operator== (expr const &a, expr const &b)
expr	operator== (expr const &a, int b)
expr	operator== (int a, expr const &b)
expr	operator!= (expr const &a, expr const &b)
expr	operator!= (expr const &a, int b)
expr	operator!= (int a, expr const &b)
expr	operator+ (expr const &a, expr const &b)
expr	operator+ (expr const &a, int b)
expr	operator+ (int a, expr const &b)
expr	operator* (expr const &a, expr const &b)
expr	operator* (expr const &a, int b)
expr	operator* (int a, expr const &b)
expr	operator>= (expr const &a, expr const &b)
expr	operator/ (expr const &a, expr const &b)
expr	operator/ (expr const &a, int b)
expr	operator/ (int a, expr const &b)
expr	operator- (expr const &a)
expr	operator- (expr const &a, expr const &b)
expr	operator- (expr const &a, int b)
expr	operator- (int a, expr const &b)
expr	operator<= (expr const &a, expr const &b)
expr	operator<= (expr const &a, int b)
expr	operator<= (int a, expr const &b)
expr	operator>= (expr const &a, int b)
expr	operator>= (int a, expr const &b)
expr	operator< (expr const &a, expr const &b)
expr	operator< (expr const &a, int b)
expr	operator< (int a, expr const &b)
expr	operator> (expr const &a, expr const &b)
expr	operator> (expr const &a, int b)
expr	operator> (int a, expr const &b)
expr	operator & (expr const &a, expr const &b)
expr	operator & (expr const &a, int b)
expr	operator & (int a, expr const &b)
expr	operator^ (expr const &a, expr const &b)
expr	operator^ (expr const &a, int b)
expr	operator^ (int a, expr const &b)
expr	operator| (expr const &a, expr const &b)
expr	operator| (expr const &a, int b)
expr	operator| (int a, expr const &b)
expr	operator~ (expr const &a)
expr	ite (expr const &c, expr const &t, expr const &e)
	Create the if-then-else expression ite(c, t, e) More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
expr	udiv (expr const &a, int b)
expr	udiv (int a, expr const &b)
expr	srem (expr const &a, expr const &b)
	signed reminder operator for bitvectors More...
expr	srem (expr const &a, int b)
expr	srem (int a, expr const &b)
expr	urem (expr const &a, expr const &b)
	unsigned reminder operator for bitvectors More...
expr	urem (expr const &a, int b)
expr	urem (int a, expr const &b)
expr	shl (expr const &a, expr const &b)
	shift left operator for bitvectors More...
expr	shl (expr const &a, int b)
expr	shl (int a, expr const &b)
expr	lshr (expr const &a, expr const &b)
	logic shift right operator for bitvectors More...
expr	lshr (expr const &a, int b)
expr	lshr (int a, expr const &b)
expr	ashr (expr const &a, expr const &b)
	arithmetic shift right operator for bitvectors More...
expr	ashr (expr const &a, int b)
expr	ashr (int a, expr const &b)
expr	zext (expr const &a, unsigned i)
	Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More...
expr	sext (expr const &a, unsigned i)
	Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More...
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)
expr	concat (expr const &a, expr const &b)
expr	concat (expr_vector const &args)
expr	mk_or (expr_vector const &args)
expr	mk_and (expr_vector const &args)
std::ostream &	operator<< (std::ostream &out, model const &m)
std::ostream &	operator<< (std::ostream &out, stats const &s)
std::ostream &	operator<< (std::ostream &out, check_result r)
std::ostream &	operator<< (std::ostream &out, solver const &s)
std::ostream &	operator<< (std::ostream &out, goal const &g)
std::ostream &	operator<< (std::ostream &out, apply_result const &r)
tactic	operator & (tactic const &t1, tactic const &t2)
tactic	operator| (tactic const &t1, tactic const &t2)
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)
probe	operator<= (probe const &p1, probe const &p2)
probe	operator<= (probe const &p1, double p2)
probe	operator<= (double p1, probe const &p2)
probe	operator>= (probe const &p1, probe const &p2)
probe	operator>= (probe const &p1, double p2)
probe	operator>= (double p1, probe const &p2)
probe	operator< (probe const &p1, probe const &p2)
probe	operator< (probe const &p1, double p2)
probe	operator< (double p1, probe const &p2)
probe	operator> (probe const &p1, probe const &p2)
probe	operator> (probe const &p1, double p2)
probe	operator> (double p1, probe const &p2)
probe	operator== (probe const &p1, probe const &p2)
probe	operator== (probe const &p1, double p2)
probe	operator== (double p1, probe const &p2)
probe	operator && (probe const &p1, probe const &p2)
probe	operator|| (probe const &p1, probe const &p2)
probe	operator! (probe const &p)
std::ostream &	operator<< (std::ostream &out, optimize const &s)
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)
expr	empty_set (sort const &s)
expr	full_set (sort const &s)
expr	set_add (expr const &s, expr const &e)
expr	set_del (expr const &s, expr const &e)
expr	set_union (expr const &a, expr const &b)
expr	set_intersect (expr const &a, expr const &b)
expr	set_difference (expr const &a, expr const &b)
expr	set_complement (expr const &a)
expr	set_member (expr const &s, expr const &e)
expr	set_subset (expr const &a, expr const &b)
expr	empty (sort const &s)
expr	suffixof (expr const &a, expr const &b)
expr	prefixof (expr const &a, expr const &b)
expr	indexof (expr const &s, expr const &substr, expr const &offset)
expr	to_re (expr const &s)
expr	in_re (expr const &s, expr const &re)
expr	plus (expr const &re)
expr	option (expr const &re)
expr	star (expr const &re)
expr	interpolant (expr const &a)

Detailed Description

Z3 C++ namespace.

Typedef Documentation

ast_vector

typedef ast_vector_tpl<ast> ast_vector

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

expr_vector

typedef ast_vector_tpl<expr> expr_vector

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

func_decl_vector

typedef ast_vector_tpl<func_decl> func_decl_vector

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

sort_vector

typedef ast_vector_tpl<sort> sort_vector

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

Enumeration Type Documentation

check_result

enum check_result

Enumerator
unsat
sat
unknown

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

                      {
        unsat, sat, unknown
    };

Function Documentation

ashr() [1/3]

expr z3::ashr ( expr const &  a, expr const &  b  )

inline

arithmetic shift right operator for bitvectors

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

Referenced by ashr().

{ return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }

ashr() [2/3]

expr z3::ashr ( expr const &  a, int  b  )

inline

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

{ return ashr(a, a.ctx().num_val(b, a.get_sort())); }

ashr() [3/3]

expr z3::ashr ( int  a, expr const &  b  )

inline

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

{ return ashr(b.ctx().num_val(a, b.get_sort()), b); }

check_context()

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

inline

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

Referenced by goal::add(), tactic::apply(), expr::at(), solver::check(), object::check_error(), concat(), cond(), expr::contains(), apply_result::convert_model(), model::eval(), exists(), expr::extract(), forall(), context::function(), model::get_const_interp(), model::get_func_interp(), model::has_interp(), implies(), in_re(), indexof(), ite(), operator &(), operator &&(), operator!=(), func_decl::operator()(), operator*(), operator+(), operator-(), operator/(), operator<(), operator<=(), operator==(), operator>(), operator>=(), operator^(), operator|(), operator||(), prefixof(), pw(), expr::replace(), select(), set_intersect(), set_union(), store(), suffixof(), and when().

{ assert(a.m_ctx == b.m_ctx); }

concat() [1/2]

expr z3::concat ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and operator+().

                                                     {
        check_context(a, b);
        Z3_ast r;
        if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
            Z3_ast _args[2] = { a, b };
            r = Z3_mk_seq_concat(a.ctx(), 2, _args);
        }
        else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
            Z3_ast _args[2] = { a, b };
            r = Z3_mk_re_concat(a.ctx(), 2, _args);
        }
        else {
            r = Z3_mk_concat(a.ctx(), a, b);
        }
        a.ctx().check_error();
        return expr(a.ctx(), r);
    }

concat() [2/2]

expr z3::concat ( expr_vector const &  args )

inline

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

                                                {
        Z3_ast r;
        assert(args.size() > 0);
        if (args.size() == 1) {
            return args[0];
        }
        context& ctx = args[0].ctx();
        array<Z3_ast> _args(args);
        if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
            r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
        }
        else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
            r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
        }
        else {
            r = _args[args.size()-1];
            for (unsigned i = args.size()-1; i > 0; ) {
                --i;
                r = Z3_mk_concat(ctx, _args[i], r);
                ctx.check_error();
            }
        }
        ctx.check_error();
        return expr(ctx, r);
    }

cond()

tactic z3::cond ( probe const &  p, tactic const &  t1, tactic const &  t2  )

inline

Definition at line 2077 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);
    }

const_array()

expr z3::const_array ( sort const &  d, expr const &  v  )

inline

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

                                                            {
        MK_EXPR2(Z3_mk_const_array, d, v);
    }

distinct()

expr z3::distinct ( expr_vector const &  args )

inline

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

Referenced by expr::body().

                                                  {
        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);
    }

empty()

expr z3::empty ( sort const &  s )

inline

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

                                     {
        Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
        s.check_error();
        return expr(s.ctx(), r);
    }

empty_set()

expr z3::empty_set ( sort const &  s )

inline

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

                                         {
        MK_EXPR1(Z3_mk_empty_set, s);
    }

eq()

bool z3::eq ( ast const &  a, ast const &  b  )

inline

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

Referenced by ast::hash().

{ return Z3_is_eq_ast(a.ctx(), a, b) != 0; }

exists() [1/5]

expr z3::exists ( expr const &  x, expr const &  b  )

inline

Definition at line 1443 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);
    }

exists() [2/5]

expr z3::exists ( expr const &  x1, expr const &  x2, expr const &  b  )

inline

Definition at line 1448 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);
    }

exists() [3/5]

expr z3::exists ( expr const &  x1, expr const &  x2, expr const &  x3, expr const &  b  )

inline

Definition at line 1453 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);
    }

exists() [4/5]

expr z3::exists ( expr const &  x1, expr const &  x2, expr const &  x3, expr const &  x4, expr const &  b  )

inline

Definition at line 1458 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);
    }

exists() [5/5]

expr z3::exists ( expr_vector const &  xs, expr const &  b  )

inline

Definition at line 1463 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);
    }

fail_if()

tactic z3::fail_if ( probe const &  p )

inline

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

                                           {
        Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
        p.check_error();
        return tactic(p.ctx(), r);
    }

forall() [1/5]

expr z3::forall ( expr const &  x, expr const &  b  )

inline

Definition at line 1419 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);
    }

forall() [2/5]

expr z3::forall ( expr const &  x1, expr const &  x2, expr const &  b  )

inline

Definition at line 1424 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);
    }

forall() [3/5]

expr z3::forall ( expr const &  x1, expr const &  x2, expr const &  x3, expr const &  b  )

inline

Definition at line 1429 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);
    }

forall() [4/5]

expr z3::forall ( expr const &  x1, expr const &  x2, expr const &  x3, expr const &  x4, expr const &  b  )

inline

Definition at line 1434 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);
    }

forall() [5/5]

expr z3::forall ( expr_vector const &  xs, expr const &  b  )

inline

Definition at line 1439 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);
    }

full_set()

expr z3::full_set ( sort const &  s )

inline

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

                                        {
        MK_EXPR1(Z3_mk_full_set, s);
    }

function() [1/7]

func_decl z3::function ( symbol const &  name, unsigned  arity, sort const *  domain, sort const &  range  )

inline

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

                                                                                                            {
        return range.ctx().function(name, arity, domain, range);
    }

function() [2/7]

func_decl z3::function ( char const *  name, unsigned  arity, sort const *  domain, sort const &  range  )

inline

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

                                                                                                          {
        return range.ctx().function(name, arity, domain, range);
    }

function() [3/7]

func_decl z3::function ( char const *  name, sort const &  domain, sort const &  range  )

inline

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

                                                                                          {
        return range.ctx().function(name, domain, range);
    }

function() [4/7]

func_decl z3::function ( char const *  name, sort const &  d1, sort const &  d2, sort const &  range  )

inline

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

                                                                                                       {
        return range.ctx().function(name, d1, d2, range);
    }

function() [5/7]

func_decl z3::function ( char const *  name, sort const &  d1, sort const &  d2, sort const &  d3, sort const &  range  )

inline

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

                                                                                                                        {
        return range.ctx().function(name, d1, d2, d3, range);
    }

function() [6/7]

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

                                                                                                                                         {
        return range.ctx().function(name, d1, d2, d3, d4, range);
    }

function() [7/7]

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

                                                                                                                                                          {
        return range.ctx().function(name, d1, d2, d3, d4, d5, range);
    }

implies() [1/3]

expr z3::implies ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and implies().

                                                        {
        check_context(a, b);
        assert(a.is_bool() && b.is_bool());
        Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
        a.check_error();
        return expr(a.ctx(), r);
    }

implies() [2/3]

expr z3::implies ( expr const &  a, bool  b  )

inline

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

{ return implies(a, a.ctx().bool_val(b)); }

implies() [3/3]

expr z3::implies ( bool  a, expr const &  b  )

inline

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

{ return implies(b.ctx().bool_val(a), b); }

in_re()

expr z3::in_re ( expr const &  s, expr const &  re  )

inline

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

                                                     {
        check_context(s, re);
        Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
        s.check_error();
        return expr(s.ctx(), r);
    }

indexof()

expr z3::indexof ( expr const &  s, expr const &  substr, expr const &  offset  )

inline

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

                                                                               {
        check_context(s, substr); check_context(s, offset);
        Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
        s.check_error();
        return expr(s.ctx(), r);
    }

interpolant()

expr z3::interpolant ( expr const &  a )

inline

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

                                           {
        return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
    }

ite()

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

Referenced by expr::body().

                                                                    {
        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);
    }

lshr() [1/3]

expr z3::lshr ( expr const &  a, expr const &  b  )

inline

logic shift right operator for bitvectors

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

Referenced by lshr().

{ return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }

lshr() [2/3]

expr z3::lshr ( expr const &  a, int  b  )

inline

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

{ return lshr(a, a.ctx().num_val(b, a.get_sort())); }

lshr() [3/3]

expr z3::lshr ( int  a, expr const &  b  )

inline

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

{ return lshr(b.ctx().num_val(a, b.get_sort()), b); }

mk_and()

expr z3::mk_and ( expr_vector const &  args )

inline

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

Referenced by expr::body().

                                                {
        array<Z3_ast> _args(args);
        Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
        args.check_error();
        return expr(args.ctx(), r);
    }

mk_or()

expr z3::mk_or ( expr_vector const &  args )

inline

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

Referenced by expr::body().

                                               { 
        array<Z3_ast> _args(args);
        Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
        args.check_error();
        return expr(args.ctx(), r);
    }

operator &() [1/4]

expr z3::operator& ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and tactic::help().

{ check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }

operator &() [2/4]

expr z3::operator& ( expr const &  a, int  b  )

inline

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

{ return a & a.ctx().num_val(b, a.get_sort()); }

operator &() [3/4]

expr z3::operator& ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) & b; }

operator &() [4/4]

tactic z3::operator& ( tactic const &  t1, tactic const &  t2  )

inline

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

                                                                  {
        check_context(t1, t2);
        Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
        t1.check_error();
        return tactic(t1.ctx(), r);
    }

operator &&() [1/4]

expr z3::operator&& ( expr const &  a, expr const &  b  )

inline

Precondition

a.is_bool()

b.is_bool()

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

Referenced by expr::body(), and probe::operator()().

                                                           {
        check_context(a, b);
        assert(a.is_bool() && b.is_bool());
        Z3_ast args[2] = { a, b };
        Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
        a.check_error();
        return expr(a.ctx(), r);
    }

operator &&() [2/4]

expr z3::operator&& ( expr const &  a, bool  b  )

inline

Precondition

a.is_bool()

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

{ return a && a.ctx().bool_val(b); }

operator &&() [3/4]

expr z3::operator&& ( bool  a, expr const &  b  )

inline

Precondition

b.is_bool()

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

{ return b.ctx().bool_val(a) && b; }

operator &&() [4/4]

probe z3::operator&& ( probe const &  p1, probe const &  p2  )

inline

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

                                                                {
        check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator!() [1/2]

expr z3::operator! ( expr const &  a )

inline

Precondition

a.is_bool()

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

Referenced by expr::body(), and probe::operator()().

                                          {
        assert(a.is_bool());
        Z3_ast r = Z3_mk_not(a.ctx(), a);
        a.check_error();
        return expr(a.ctx(), r);
    }

operator!() [2/2]

probe z3::operator! ( probe const &  p )

inline

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

                                            {
        Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
    }

operator!=() [1/3]

expr z3::operator!= ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body().

                                                           {
        check_context(a, b);
        Z3_ast args[2] = { a, b };
        Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
        a.check_error();
        return expr(a.ctx(), r);
    }

operator!=() [2/3]

expr z3::operator!= ( expr const &  a, int  b  )

inline

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

{ assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }

operator!=() [3/3]

expr z3::operator!= ( int  a, expr const &  b  )

inline

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

{ assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }

operator*() [1/3]

expr z3::operator* ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body().

                                                          {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            Z3_ast args[2] = { a, b };
            r = Z3_mk_mul(a.ctx(), 2, args);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvmul(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator*() [2/3]

expr z3::operator* ( expr const &  a, int  b  )

inline

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

{ return a * a.ctx().num_val(b, a.get_sort()); }

operator*() [3/3]

expr z3::operator* ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) * b; }

operator+() [1/3]

expr z3::operator+ ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body().

                                                          {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            Z3_ast args[2] = { a, b };
            r = Z3_mk_add(a.ctx(), 2, args);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvadd(a.ctx(), a, b);
        }
        else if (a.is_seq() && b.is_seq()) {
            return concat(a, b);
        }
        else if (a.is_re() && b.is_re()) {
            Z3_ast _args[2] = { a, b };
            r = Z3_mk_re_union(a.ctx(), 2, _args);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator+() [2/3]

expr z3::operator+ ( expr const &  a, int  b  )

inline

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

{ return a + a.ctx().num_val(b, a.get_sort()); }

operator+() [3/3]

expr z3::operator+ ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) + b; }

operator-() [1/4]

expr z3::operator- ( expr const &  a )

inline

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

Referenced by expr::body().

                                          {
        Z3_ast r = 0;
        if (a.is_arith()) {
            r = Z3_mk_unary_minus(a.ctx(), a);
        }
        else if (a.is_bv()) {
            r = Z3_mk_bvneg(a.ctx(), a);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator-() [2/4]

expr z3::operator- ( expr const &  a, expr const &  b  )

inline

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

                                                          {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            Z3_ast args[2] = { a, b };
            r = Z3_mk_sub(a.ctx(), 2, args);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvsub(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator-() [3/4]

expr z3::operator- ( expr const &  a, int  b  )

inline

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

{ return a - a.ctx().num_val(b, a.get_sort()); }

operator-() [4/4]

expr z3::operator- ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) - b; }

operator/() [1/3]

expr z3::operator/ ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body().

                                                          {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_div(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvsdiv(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator/() [2/3]

expr z3::operator/ ( expr const &  a, int  b  )

inline

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

{ return a / a.ctx().num_val(b, a.get_sort()); }

operator/() [3/3]

expr z3::operator/ ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) / b; }

operator<() [1/6]

expr z3::operator< ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and probe::operator()().

                                                          {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_lt(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvslt(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator<() [2/6]

expr z3::operator< ( expr const &  a, int  b  )

inline

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

{ return a < a.ctx().num_val(b, a.get_sort()); }

operator<() [3/6]

expr z3::operator< ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) < b; }

operator<() [4/6]

probe z3::operator< ( probe const &  p1, probe const &  p2  )

inline

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

                                                               {
        check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator<() [5/6]

probe z3::operator< ( probe const &  p1, double  p2  )

inline

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

{ return p1 < probe(p1.ctx(), p2); }

operator<() [6/6]

probe z3::operator< ( double  p1, probe const &  p2  )

inline

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

{ return probe(p2.ctx(), p1) < p2; }

operator<<() [1/12]

std::ostream& z3::operator<< ( std::ostream &  out, exception const &  e  )

inline

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

{ out << e.msg(); return out; }

operator<<() [2/12]

std::ostream& z3::operator<< ( std::ostream &  out, symbol const &  s  )

inline

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

                                                                       {
        if (s.kind() == Z3_INT_SYMBOL)
            out << "k!" << s.to_int();
        else
            out << s.str().c_str();
        return out;
    }

operator<<() [3/12]

std::ostream& z3::operator<< ( std::ostream &  out, param_descrs const &  d  )

inline

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

{ return out << d.to_string(); }

operator<<() [4/12]

std::ostream& z3::operator<< ( std::ostream &  out, params const &  p  )

inline

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

                                                                       {
        out << Z3_params_to_string(p.ctx(), p); return out;
    }

operator<<() [5/12]

std::ostream& z3::operator<< ( std::ostream &  out, ast const &  n  )

inline

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

                                                                    {
        out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
    }

operator<<() [6/12]

std::ostream& z3::operator<< ( std::ostream &  out, model const &  m  )

inline

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

{ out << Z3_model_to_string(m.ctx(), m); return out; }

operator<<() [7/12]

std::ostream& z3::operator<< ( std::ostream &  out, stats const &  s  )

inline

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

{ out << Z3_stats_to_string(s.ctx(), s); return out; }

operator<<() [8/12]

std::ostream& z3::operator<< ( std::ostream &  out, check_result  r  )

inline

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

                                                                     {
        if (r == unsat) out << "unsat";
        else if (r == sat) out << "sat";
        else out << "unknown";
        return out;
    }

operator<<() [9/12]

std::ostream& z3::operator<< ( std::ostream &  out, solver const &  s  )

inline

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

{ out << Z3_solver_to_string(s.ctx(), s); return out; }

operator<<() [10/12]

std::ostream& z3::operator<< ( std::ostream &  out, goal const &  g  )

inline

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

{ out << Z3_goal_to_string(g.ctx(), g); return out; }

operator<<() [11/12]

std::ostream& z3::operator<< ( std::ostream &  out, apply_result const &  r  )

inline

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

{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }

operator<<() [12/12]

std::ostream& z3::operator<< ( std::ostream &  out, optimize const &  s  )

inline

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

{ out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }

operator<=() [1/6]

expr z3::operator<= ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and probe::operator()().

                                                           {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_le(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvsle(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator<=() [2/6]

expr z3::operator<= ( expr const &  a, int  b  )

inline

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

{ return a <= a.ctx().num_val(b, a.get_sort()); }

operator<=() [3/6]

expr z3::operator<= ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) <= b; }

operator<=() [4/6]

probe z3::operator<= ( probe const &  p1, probe const &  p2  )

inline

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

                                                                {
        check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator<=() [5/6]

probe z3::operator<= ( probe const &  p1, double  p2  )

inline

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

{ return p1 <= probe(p1.ctx(), p2); }

operator<=() [6/6]

probe z3::operator<= ( double  p1, probe const &  p2  )

inline

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

{ return probe(p2.ctx(), p1) <= p2; }

operator==() [1/6]

expr z3::operator== ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and probe::operator()().

                                                           {
        check_context(a, b);
        Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
        a.check_error();
        return expr(a.ctx(), r);
    }

operator==() [2/6]

expr z3::operator== ( expr const &  a, int  b  )

inline

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

{ assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }

operator==() [3/6]

expr z3::operator== ( int  a, expr const &  b  )

inline

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

{ assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }

operator==() [4/6]

probe z3::operator== ( probe const &  p1, probe const &  p2  )

inline

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

                                                                {
        check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator==() [5/6]

probe z3::operator== ( probe const &  p1, double  p2  )

inline

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

{ return p1 == probe(p1.ctx(), p2); }

operator==() [6/6]

probe z3::operator== ( double  p1, probe const &  p2  )

inline

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

{ return probe(p2.ctx(), p1) == p2; }

operator>() [1/6]

expr z3::operator> ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and probe::operator()().

                                                          {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_gt(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvsgt(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator>() [2/6]

expr z3::operator> ( expr const &  a, int  b  )

inline

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

{ return a > a.ctx().num_val(b, a.get_sort()); }

operator>() [3/6]

expr z3::operator> ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) > b; }

operator>() [4/6]

probe z3::operator> ( probe const &  p1, probe const &  p2  )

inline

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

                                                               {
        check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator>() [5/6]

probe z3::operator> ( probe const &  p1, double  p2  )

inline

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

{ return p1 > probe(p1.ctx(), p2); }

operator>() [6/6]

probe z3::operator> ( double  p1, probe const &  p2  )

inline

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

{ return probe(p2.ctx(), p1) > p2; }

operator>=() [1/6]

expr z3::operator>= ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and probe::operator()().

                                                           {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_ge(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvsge(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

operator>=() [2/6]

expr z3::operator>= ( expr const &  a, int  b  )

inline

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

{ return a >= a.ctx().num_val(b, a.get_sort()); }

operator>=() [3/6]

expr z3::operator>= ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) >= b; }

operator>=() [4/6]

probe z3::operator>= ( probe const &  p1, probe const &  p2  )

inline

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

                                                                {
        check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator>=() [5/6]

probe z3::operator>= ( probe const &  p1, double  p2  )

inline

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

{ return p1 >= probe(p1.ctx(), p2); }

operator>=() [6/6]

probe z3::operator>= ( double  p1, probe const &  p2  )

inline

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

{ return probe(p2.ctx(), p1) >= p2; }

operator^() [1/3]

expr z3::operator^ ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body().

{ check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }

operator^() [2/3]

expr z3::operator^ ( expr const &  a, int  b  )

inline

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

{ return a ^ a.ctx().num_val(b, a.get_sort()); }

operator^() [3/3]

expr z3::operator^ ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) ^ b; }

operator|() [1/4]

expr z3::operator| ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and tactic::help().

{ check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }

operator|() [2/4]

expr z3::operator| ( expr const &  a, int  b  )

inline

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

{ return a | a.ctx().num_val(b, a.get_sort()); }

operator|() [3/4]

expr z3::operator| ( int  a, expr const &  b  )

inline

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

{ return b.ctx().num_val(a, b.get_sort()) | b; }

operator|() [4/4]

tactic z3::operator| ( tactic const &  t1, tactic const &  t2  )

inline

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

                                                                  {
        check_context(t1, t2);
        Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
        t1.check_error();
        return tactic(t1.ctx(), r);
    }

operator||() [1/4]

expr z3::operator|| ( expr const &  a, expr const &  b  )

inline

Precondition

a.is_bool()

b.is_bool()

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

Referenced by expr::body(), and probe::operator()().

                                                           {
        check_context(a, b);
        assert(a.is_bool() && b.is_bool());
        Z3_ast args[2] = { a, b };
        Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
        a.check_error();
        return expr(a.ctx(), r);
    }

operator||() [2/4]

expr z3::operator|| ( expr const &  a, bool  b  )

inline

Precondition

a.is_bool()

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

{ return a || a.ctx().bool_val(b); }

operator||() [3/4]

expr z3::operator|| ( bool  a, expr const &  b  )

inline

Precondition

b.is_bool()

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

{ return b.ctx().bool_val(a) || b; }

operator||() [4/4]

probe z3::operator|| ( probe const &  p1, probe const &  p2  )

inline

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

                                                                {
        check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
    }

operator~()

expr z3::operator~ ( expr const &  a )

inline

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

Referenced by expr::body().

{ Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }

option()

expr z3::option ( expr const &  re )

inline

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

                                       {
        Z3_ast r = Z3_mk_re_option(re.ctx(), re);
        re.check_error();
        return expr(re.ctx(), r);
    }

plus()

expr z3::plus ( expr const &  re )

inline

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

                                     {
        Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
        re.check_error();
        return expr(re.ctx(), r);
    }

prefixof()

expr z3::prefixof ( expr const &  a, expr const &  b  )

inline

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

                                                       {
        check_context(a, b);
        Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
        a.check_error();
        return expr(a.ctx(), r);
    }

pw() [1/3]

expr z3::pw ( expr const &  a, expr const &  b  )

inline

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

Referenced by expr::body(), and 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);
    }

pw() [2/3]

expr z3::pw ( expr const &  a, int  b  )

inline

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

{ return pw(a, a.ctx().num_val(b, a.get_sort())); }

pw() [3/3]

expr z3::pw ( int  a, expr const &  b  )

inline

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

{ return pw(b.ctx().num_val(a, b.get_sort()), b); }

repeat()

tactic z3::repeat ( tactic const &  t, unsigned  max = UINT_MAX  )

inline

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

Referenced by tactic::help().

                                                                  {
        Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
        t.check_error();
        return tactic(t.ctx(), r);
    }

reset_params()

void z3::reset_params ( )

inline

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

{ Z3_global_param_reset_all(); }

select() [1/2]

expr z3::select ( expr const &  a, expr const &  i  )

inline

Definition at line 2329 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);
    }

select() [2/2]

expr z3::select ( expr const &  a, int  i  )

inline

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

{ return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }

set_add()

expr z3::set_add ( expr const &  s, expr const &  e  )

inline

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

                                                      {
        MK_EXPR2(Z3_mk_set_add, s, e);
    }

set_complement()

expr z3::set_complement ( expr const &  a )

inline

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

                                              {
        MK_EXPR1(Z3_mk_set_complement, a);
    }

set_del()

expr z3::set_del ( expr const &  s, expr const &  e  )

inline

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

                                                      {
        MK_EXPR2(Z3_mk_set_del, s, e);
    }    

set_difference()

expr z3::set_difference ( expr const &  a, expr const &  b  )

inline

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

                                                             {
        MK_EXPR2(Z3_mk_set_difference, a, b);
    }

set_intersect()

expr z3::set_intersect ( expr const &  a, expr const &  b  )

inline

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

                                                            {
        check_context(a, b); 
        Z3_ast es[2] = { a, b };
        Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
        a.check_error();                    
        return expr(a.ctx(), r);
    }

set_member()

expr z3::set_member ( expr const &  s, expr const &  e  )

inline

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

                                                         {
        MK_EXPR2(Z3_mk_set_member, s, e);
    }

set_param() [1/3]

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

set_param() [2/3]

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"); }

set_param() [3/3]

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

set_subset()

expr z3::set_subset ( expr const &  a, expr const &  b  )

inline

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

                                                         {
        MK_EXPR2(Z3_mk_set_subset, a, b);
    }

set_union()

expr z3::set_union ( expr const &  a, expr const &  b  )

inline

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

                                                        {
        check_context(a, b); 
        Z3_ast es[2] = { a, b };
        Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
        a.check_error();                    
        return expr(a.ctx(), r);
    }

sext()

expr z3::sext ( expr const &  a, unsigned  i  )

inline

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

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

{ return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }

shl() [1/3]

expr z3::shl ( expr const &  a, expr const &  b  )

inline

shift left operator for bitvectors

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

Referenced by shl().

{ return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }

shl() [2/3]

expr z3::shl ( expr const &  a, int  b  )

inline

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

{ return shl(a, a.ctx().num_val(b, a.get_sort())); }

shl() [3/3]

expr z3::shl ( int  a, expr const &  b  )

inline

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

{ return shl(b.ctx().num_val(a, b.get_sort()), b); }

srem() [1/3]

expr z3::srem ( expr const &  a, expr const &  b  )

inline

signed reminder operator for bitvectors

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

Referenced by srem().

{ return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }

srem() [2/3]

expr z3::srem ( expr const &  a, int  b  )

inline

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

{ return srem(a, a.ctx().num_val(b, a.get_sort())); }

srem() [3/3]

expr z3::srem ( int  a, expr const &  b  )

inline

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

{ return srem(b.ctx().num_val(a, b.get_sort()), b); }

star()

expr z3::star ( expr const &  re )

inline

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

                                     {
        Z3_ast r = Z3_mk_re_star(re.ctx(), re);
        re.check_error();
        return expr(re.ctx(), r);
    }

store() [1/4]

expr z3::store ( expr const &  a, expr const &  i, expr const &  v  )

inline

Definition at line 2336 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);
    }

store() [2/4]

expr z3::store ( expr const &  a, int  i, expr const &  v  )

inline

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

{ return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }

store() [3/4]

expr z3::store ( expr const &  a, expr  i, int  v  )

inline

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

{ return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }

store() [4/4]

expr z3::store ( expr const &  a, int  i, int  v  )

inline

Definition at line 2344 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()));
    }

suffixof()

expr z3::suffixof ( expr const &  a, expr const &  b  )

inline

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

                                                       {
        check_context(a, b);
        Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
        a.check_error();
        return expr(a.ctx(), r);
    }

to_check_result()

check_result z3::to_check_result ( Z3_lbool  l )

inline

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

Referenced by solver::check(), optimize::check(), context::compute_interpolant(), and solver::consequences().

                                                    {
        if (l == Z3_L_TRUE) return sat;
        else if (l == Z3_L_FALSE) return unsat;
        return unknown;
    }

to_expr()

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

Referenced by ashr(), lshr(), sext(), shl(), srem(), udiv(), uge(), ugt(), ule(), ult(), urem(), and zext().

                                               {
        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);
    }

to_func_decl()

func_decl z3::to_func_decl ( context &  c, Z3_func_decl  f  )

inline

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

                                                               {
        c.check_error();
        return func_decl(c, f);
    }

to_re()

expr z3::to_re ( expr const &  s )

inline

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

                                     {
        Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
        s.check_error();
        return expr(s.ctx(), r);
    }

to_real()

expr z3::to_real ( expr const &  a )

inline

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

{ Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }

to_sort()

sort z3::to_sort ( context &  c, Z3_sort  s  )

inline

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

Referenced by context::enumeration_sort(), and context::uninterpreted_sort().

                                                {
        c.check_error();
        return sort(c, s);
    }

try_for()

tactic z3::try_for ( tactic const &  t, unsigned  ms  )

inline

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

Referenced by tactic::help().

                                                         {
        Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
        t.check_error();
        return tactic(t.ctx(), r);
    }

udiv() [1/3]

expr z3::udiv ( expr const &  a, expr const &  b  )

inline

unsigned division operator for bitvectors.

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

Referenced by udiv().

{ return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }

udiv() [2/3]

expr z3::udiv ( expr const &  a, int  b  )

inline

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

{ return udiv(a, a.ctx().num_val(b, a.get_sort())); }

udiv() [3/3]

expr z3::udiv ( int  a, expr const &  b  )

inline

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

{ return udiv(b.ctx().num_val(a, b.get_sort()), b); }

uge() [1/3]

expr z3::uge ( expr const &  a, expr const &  b  )

inline

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

{ return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }

uge() [2/3]

expr z3::uge ( expr const &  a, int  b  )

inline

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

{ return uge(a, a.ctx().num_val(b, a.get_sort())); }

uge() [3/3]

expr z3::uge ( int  a, expr const &  b  )

inline

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

{ return uge(b.ctx().num_val(a, b.get_sort()), b); }

ugt() [1/3]

expr z3::ugt ( expr const &  a, expr const &  b  )

inline

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

{ return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }

ugt() [2/3]

expr z3::ugt ( expr const &  a, int  b  )

inline

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

{ return ugt(a, a.ctx().num_val(b, a.get_sort())); }

ugt() [3/3]

expr z3::ugt ( int  a, expr const &  b  )

inline

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

{ return ugt(b.ctx().num_val(a, b.get_sort()), b); }

ule() [1/3]

expr z3::ule ( expr const &  a, expr const &  b  )

inline

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

{ return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }

ule() [2/3]

expr z3::ule ( expr const &  a, int  b  )

inline

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

{ return ule(a, a.ctx().num_val(b, a.get_sort())); }

ule() [3/3]

expr z3::ule ( int  a, expr const &  b  )

inline

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

{ return ule(b.ctx().num_val(a, b.get_sort()), b); }

ult() [1/3]

expr z3::ult ( expr const &  a, expr const &  b  )

inline

unsigned less than operator for bitvectors.

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

Referenced by ult().

{ return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }

ult() [2/3]

expr z3::ult ( expr const &  a, int  b  )

inline

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

{ return ult(a, a.ctx().num_val(b, a.get_sort())); }

ult() [3/3]

expr z3::ult ( int  a, expr const &  b  )

inline

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

{ return ult(b.ctx().num_val(a, b.get_sort()), b); }

urem() [1/3]

expr z3::urem ( expr const &  a, expr const &  b  )

inline

unsigned reminder operator for bitvectors

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

Referenced by urem().

{ return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }

urem() [2/3]

expr z3::urem ( expr const &  a, int  b  )

inline

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

{ return urem(a, a.ctx().num_val(b, a.get_sort())); }

urem() [3/3]

expr z3::urem ( int  a, expr const &  b  )

inline

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

{ return urem(b.ctx().num_val(a, b.get_sort()), b); }

when()

tactic z3::when ( probe const &  p, tactic const &  t  )

inline

Definition at line 2071 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);
    }

with()

tactic z3::with ( tactic const &  t, params const &  p  )

inline

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

Referenced by tactic::help().

                                                           {
        Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
        t.check_error();
        return tactic(t.ctx(), r);
    }

zext()

expr z3::zext ( expr const &  a, unsigned  i  )

inline

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

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

{ return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }