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	fixedpoint
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	scoped_context
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
class	user_propagator_base

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 }
enum	rounding_mode {   RNA, RNE, RTP, RTN,   RTZ }

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	select (expr const &a, expr const &i)
	forward declarations More...
expr	select (expr const &a, expr_vector const &i)
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	mod (expr const &a, expr const &b)
expr	mod (expr const &a, int b)
expr	mod (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	rem (expr const &a, expr const &b)
expr	rem (expr const &a, int b)
expr	rem (int a, expr const &b)
expr	operator! (expr const &a)
expr	is_int (expr const &e)
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, double b)
expr	operator== (double 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, double b)
expr	operator!= (double 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	nand (expr const &a, expr const &b)
expr	nor (expr const &a, expr const &b)
expr	xnor (expr const &a, expr const &b)
expr	min (expr const &a, expr const &b)
expr	max (expr const &a, expr const &b)
expr	bvredor (expr const &a)
expr	bvredand (expr const &a)
expr	abs (expr const &a)
expr	sqrt (expr const &a, expr const &rm)
expr	fp_eq (expr const &a, expr const &b)
expr	operator~ (expr const &a)
expr	fma (expr const &a, expr const &b, expr const &c, expr const &rm)
expr	fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
expr	fpa_to_sbv (expr const &t, unsigned sz)
expr	fpa_to_ubv (expr const &t, unsigned sz)
expr	sbv_to_fpa (expr const &t, sort s)
expr	ubv_to_fpa (expr const &t, sort s)
expr	fpa_to_fpa (expr const &t, sort s)
expr	round_fpa_to_closest_integer (expr const &t)
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	sle (expr const &a, expr const &b)
	signed less than or equal to operator for bitvectors. More...
expr	sle (expr const &a, int b)
expr	sle (int a, expr const &b)
expr	slt (expr const &a, expr const &b)
	signed less than operator for bitvectors. More...
expr	slt (expr const &a, int b)
expr	slt (int a, expr const &b)
expr	sge (expr const &a, expr const &b)
	signed greater than or equal to operator for bitvectors. More...
expr	sge (expr const &a, int b)
expr	sge (int a, expr const &b)
expr	sgt (expr const &a, expr const &b)
	signed greater than operator for bitvectors. More...
expr	sgt (expr const &a, int b)
expr	sgt (int a, expr const &b)
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 remainder operator for bitvectors More...
expr	srem (expr const &a, int b)
expr	srem (int a, expr const &b)
expr	smod (expr const &a, expr const &b)
	signed modulus operator for bitvectors More...
expr	smod (expr const &a, int b)
expr	smod (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	bv2int (expr const &a, bool is_signed)
	bit-vector and integer conversions. More...
expr	int2bv (unsigned n, expr const &a)
expr	bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
	bit-vector overflow/underflow checks More...
expr	bvadd_no_underflow (expr const &a, expr const &b)
expr	bvsub_no_overflow (expr const &a, expr const &b)
expr	bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
expr	bvsdiv_no_overflow (expr const &a, expr const &b)
expr	bvneg_no_overflow (expr const &a)
expr	bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
expr	bvmul_no_underflow (expr const &a, expr const &b)
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...
func_decl	linear_order (sort const &a, unsigned index)
func_decl	partial_order (sort const &a, unsigned index)
func_decl	piecewise_linear_order (sort const &a, unsigned index)
func_decl	tree_order (sort const &a, unsigned index)
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	lambda (expr const &x, expr const &b)
expr	lambda (expr const &x1, expr const &x2, expr const &b)
expr	lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b)
expr	lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
expr	lambda (expr_vector const &xs, expr const &b)
expr	pble (expr_vector const &es, int const *coeffs, int bound)
expr	pbge (expr_vector const &es, int const *coeffs, int bound)
expr	pbeq (expr_vector const &es, int const *coeffs, int bound)
expr	atmost (expr_vector const &es, unsigned bound)
expr	atleast (expr_vector const &es, unsigned bound)
expr	sum (expr_vector const &args)
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)
expr	mk_xor (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)
tactic	par_or (unsigned n, tactic const *tactics)
tactic	par_and_then (tactic const &t1, tactic const &t2)
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)
std::ostream &	operator<< (std::ostream &out, fixedpoint const &f)
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)
func_decl	function (char const *name, sort_vector const &domain, sort const &range)
func_decl	function (std::string const &name, sort_vector const &domain, sort const &range)
func_decl	recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl	recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl	recfun (char const *name, sort const &d1, sort const &range)
func_decl	recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
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	store (expr const &a, expr_vector const &i, expr const &v)
expr	as_array (func_decl &f)
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	last_indexof (expr const &s, expr const &substr)
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	re_empty (sort const &s)
expr	re_full (sort const &s)
expr	re_intersect (expr_vector const &args)
expr	re_complement (expr const &a)
expr	range (expr const &lo, expr const &hi)

Detailed Description

Z3 C++ namespace.

Typedef Documentation

typedef ast_vector_tpl<ast> ast_vector

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

typedef ast_vector_tpl<expr> expr_vector

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

typedef ast_vector_tpl<func_decl> func_decl_vector

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

typedef ast_vector_tpl<sort> sort_vector

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

Enumeration Type Documentation

enum check_result

Enumerator
unsat
sat
unknown

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

                      {
        unsat, sat, unknown
    };

enum rounding_mode

Enumerator
RNA
RNE
RTP
RTN
RTZ

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

                       {
        RNA,
        RNE,
        RTP,
        RTN,
        RTZ
    };

Function Documentation

expr z3::abs ( expr const &  a )

inline

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

                                    { 
        Z3_ast r;
        if (a.is_int()) {
            expr zero = a.ctx().int_val(0);
        expr ge = a >= zero;
        expr na = -a;
            r = Z3_mk_ite(a.ctx(), ge, a, na);      
        }
        else if (a.is_real()) {
            expr zero = a.ctx().real_val(0);
        expr ge = a >= zero;
        expr na = -a;
            r = Z3_mk_ite(a.ctx(), ge, a, na);
        }
        else {
            r = Z3_mk_fpa_abs(a.ctx(), a); 
        }
        a.check_error();
        return expr(a.ctx(), r); 
    }

expr z3::as_array ( func_decl &  f )

inline

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

                                        {
        Z3_ast r = Z3_mk_as_array(f.ctx(), f);
        f.check_error();
        return expr(f.ctx(), r);
    }

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

inline

arithmetic shift right operator for bitvectors

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

Referenced by ashr().

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

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

inline

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

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

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

inline

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

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

expr z3::atleast ( expr_vector const &  es, unsigned  bound  )

inline

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

                                                               {
        assert(es.size() > 0);
        context& ctx = es[0].ctx();
        array<Z3_ast> _es(es);
        Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
        ctx.check_error();
        return expr(ctx, r);
    }

expr z3::atmost ( expr_vector const &  es, unsigned  bound  )

inline

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

                                                              {
        assert(es.size() > 0);
        context& ctx = es[0].ctx();
        array<Z3_ast> _es(es);
        Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
        ctx.check_error();
        return expr(ctx, r);
    }

expr z3::bv2int ( expr const &  a, bool  is_signed  )

inline

bit-vector and integer conversions.

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

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

expr z3::bvadd_no_overflow ( expr const &  a, expr const &  b, bool  is_signed  )

inline

bit-vector overflow/underflow checks

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

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

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

inline

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

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

expr z3::bvmul_no_overflow ( expr const &  a, expr const &  b, bool  is_signed  )

inline

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

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

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

inline

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

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

expr z3::bvneg_no_overflow ( expr const &  a )

inline

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

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

expr z3::bvredand ( expr const &  a )

inline

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

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

expr z3::bvredor ( expr const &  a )

inline

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

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

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

inline

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

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

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

inline

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

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

expr z3::bvsub_no_underflow ( expr const &  a, expr const &  b, bool  is_signed  )

inline

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

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

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

inline

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

Referenced by bvadd_no_overflow(), bvadd_no_underflow(), bvmul_no_overflow(), bvmul_no_underflow(), bvsdiv_no_overflow(), bvsub_no_overflow(), bvsub_no_underflow(), concat(), cond(), exists(), fma(), forall(), fp_eq(), fpa_fp(), context::function(), indexof(), ite(), lambda(), last_indexof(), max(), min(), nand(), nor(), operator!=(), operator&(), operator&&(), operator*(), operator+(), operator-(), operator/(), operator<(), operator<=(), operator==(), operator>(), operator>=(), operator^(), operator|(), operator||(), par_and_then(), prefixof(), range(), context::recdef(), context::recfun(), select(), set_intersect(), set_union(), sqrt(), store(), suffixof(), when(), and xnor().

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

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

inline

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

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

expr z3::concat ( expr_vector const &  args )

inline

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

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

inline

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

                                                            {
        MK_EXPR2(Z3_mk_const_array, d, v);
    }

expr z3::distinct ( expr_vector const &  args )

inline

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

expr z3::empty ( sort const &  s )

inline

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

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

expr z3::empty_set ( sort const &  s )

inline

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

                                         {
        MK_EXPR1(Z3_mk_empty_set, s);
    }

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

inline

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

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

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

inline

Definition at line 2272 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 2277 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 2282 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 2287 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 2292 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 3243 of file z3++.h.

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

expr z3::fma ( expr const &  a, expr const &  b, expr const &  c, expr const &  rm  )

inline

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

                                                                                 {
        check_context(a, b); check_context(a, c); check_context(a, rm);
        assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
        Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

Definition at line 2248 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 2253 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 2258 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 2263 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 2268 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);
    }

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

inline

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

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

expr z3::fpa_fp ( expr const &  sgn, expr const &  exp, expr const &  sig  )

inline

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

                                                                          {
        check_context(sgn, exp); check_context(exp, sig);
        assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
        Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
        sgn.check_error();
        return expr(sgn.ctx(), r);
    }

expr z3::fpa_to_fpa ( expr const &  t, sort  s  )

inline

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

                                                  {
        assert(t.is_fpa());
        Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
        t.check_error();
        return expr(t.ctx(), r);
    }

expr z3::fpa_to_sbv ( expr const &  t, unsigned  sz  )

inline

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

                                                       {
        assert(t.is_fpa());
        Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
        t.check_error();
        return expr(t.ctx(), r);
    }

expr z3::fpa_to_ubv ( expr const &  t, unsigned  sz  )

inline

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

                                                       {
        assert(t.is_fpa());
        Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
        t.check_error();
        return expr(t.ctx(), r);
    }

expr z3::full_set ( sort const &  s )

inline

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

                                        {
        MK_EXPR1(Z3_mk_full_set, s);
    }

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

inline

Definition at line 3578 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 3581 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 3584 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 3587 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 3590 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 3593 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 3596 of file z3++.h.

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

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

inline

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

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

func_decl z3::function ( std::string const &  name, sort_vector const &  domain, sort const &  range  )

inline

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

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

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

inline

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

Referenced by implies().

                                                        {
        assert(a.is_bool() && b.is_bool());
        _Z3_MK_BIN_(a, b, Z3_mk_implies);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

                                                     {
        MK_EXPR2(Z3_mk_seq_in_re, s, re);
    }

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

inline

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

expr z3::int2bv ( unsigned  n, expr const &  a  )

inline

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

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

expr z3::is_int ( expr const &  e )

inline

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

{ _Z3_MK_UN_(e, Z3_mk_is_int); }

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

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

inline

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

                                                       {
        check_context(x, b);
        Z3_app vars[] = {(Z3_app) x};
        Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
    }

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

inline

Definition at line 2301 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_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
    }

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

inline

Definition at line 2306 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_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
    }

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

inline

Definition at line 2311 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_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
    }

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

inline

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

                                                               {
        array<Z3_app> vars(xs);
        Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
    }

expr z3::last_indexof ( expr const &  s, expr const &  substr  )

inline

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

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

func_decl z3::linear_order ( sort const &  a, unsigned  index  )

inline

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

                                                                 {
        return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
    }

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

inline

logic shift right operator for bitvectors

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

Referenced by lshr().

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

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

inline

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

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

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

inline

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

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

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

inline

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

Referenced by repeat().

                                                  { 
        check_context(a, b); 
        Z3_ast r;
        if (a.is_arith()) {
            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
        }
        else if (a.is_bv()) {
            r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
        }
        else {
            assert(a.is_fpa());
            r = Z3_mk_fpa_max(a.ctx(), a, b); 
        }
        return expr(a.ctx(), r); 
    }

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

inline

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

                                                  { 
        check_context(a, b); 
        Z3_ast r;
        if (a.is_arith()) {
            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
        }
        else if (a.is_bv()) {
            r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
        }
        else {
            assert(a.is_fpa());
            r = Z3_mk_fpa_min(a.ctx(), a, b); 
        }
        return expr(a.ctx(), r); 
    }

expr z3::mk_and ( expr_vector const &  args )

inline

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

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

expr z3::mk_or ( expr_vector const &  args )

inline

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

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

expr z3::mk_xor ( expr_vector const &  args )

inline

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

                                                {
        if (args.empty())
            return args.ctx().bool_val(false);
        expr r = args[0];
        for (unsigned i = 1; i < args.size(); ++i)
            r = r ^ args[i];
        return r;
    }

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

inline

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

Referenced by mod(), and operator%().

                                                  { 
        if (a.is_bv()) {
            _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);   
        }
        else {
            _Z3_MK_BIN_(a, b, Z3_mk_mod);   
        }
    }

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

inline

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

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

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

inline

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

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

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

inline

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

{ if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }

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

inline

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

{ if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }

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

inline

Precondition

a.is_bool()

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

{ assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

{ assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }

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

inline

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

{ assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }

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

inline

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

{ return mod(a, b); }

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

inline

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

{ return mod(a, b); }

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

inline

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

{ return mod(a, b); }

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

inline

Precondition

a.is_bool()

b.is_bool()

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

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

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

inline

Precondition

a.is_bool()

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

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

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

inline

Precondition

b.is_bool()

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

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

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

inline

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

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

inline

Definition at line 1684 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_mul(a.ctx(), 2, args);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvmul(a.ctx(), a, b);
        }
        else if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

Definition at line 1654 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_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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

                                          {
        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 if (a.is_fpa()) {
            r = Z3_mk_fpa_neg(a.ctx(), a);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

Definition at line 1769 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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

                                                          {
        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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

                                                          {
        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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_lt(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

std::ostream& z3::operator<< ( std::ostream &  out, fixedpoint const &  f  )

inline

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

{ return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }

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

inline

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

                                                           {
        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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_leq(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

{ assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }

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

inline

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

{ assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }

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

inline

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

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

inline

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

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

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

inline

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

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

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

inline

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

                                                          {
        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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_gt(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

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

inline

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

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

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

inline

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

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

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

inline

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

                                                           {
        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 if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_geq(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

inline

Precondition

a.is_bool()

b.is_bool()

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

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

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

inline

Precondition

a.is_bool()

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

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

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

inline

Precondition

b.is_bool()

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

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

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

inline

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

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

inline

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

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

expr z3::option ( expr const &  re )

inline

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

                                       {
        MK_EXPR1(Z3_mk_re_option, re);
    }

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

inline

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

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

tactic z3::par_or ( unsigned  n, tactic const *  tactics  )

inline

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

                                                            {
        if (n == 0) {
            Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
        }
        array<Z3_tactic> buffer(n);
        for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
        return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
    }

func_decl z3::partial_order ( sort const &  a, unsigned  index  )

inline

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

                                                                  {
        return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
    }

expr z3::pbeq ( expr_vector const &  es, int const *  coeffs, int  bound  )

inline

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

                                                                          {
        assert(es.size() > 0);
        context& ctx = es[0].ctx();
        array<Z3_ast> _es(es);
        Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
        ctx.check_error();
        return expr(ctx, r);
    }

expr z3::pbge ( expr_vector const &  es, int const *  coeffs, int  bound  )

inline

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

                                                                          {
        assert(es.size() > 0);
        context& ctx = es[0].ctx();
        array<Z3_ast> _es(es);
        Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
        ctx.check_error();
        return expr(ctx, r);
    }

expr z3::pble ( expr_vector const &  es, int const *  coeffs, int  bound  )

inline

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

                                                                          {
        assert(es.size() > 0);
        context& ctx = es[0].ctx();
        array<Z3_ast> _es(es);
        Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
        ctx.check_error();
        return expr(ctx, r);
    }

func_decl z3::piecewise_linear_order ( sort const &  a, unsigned  index  )

inline

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

                                                                           {
        return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
    }

expr z3::plus ( expr const &  re )

inline

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

                                     {
        MK_EXPR1(Z3_mk_re_plus, re);
    }

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

inline

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

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

inline

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

Referenced by pw().

{ _Z3_MK_BIN_(a, b, Z3_mk_power);   }

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

inline

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

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

expr z3::range ( expr const &  lo, expr const &  hi  )

inline

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

Referenced by z3py::AndThen(), ApplyResult::as_expr(), z3py::AtLeast(), Optimize::check(), ExprRef::children(), z3py::describe_probes(), z3py::eq(), z3py::FreshFunction(), context::function(), z3py::Function(), function(), z3py::OrElse(), z3py::ParOr(), z3py::probes(), z3py::RealVarVector(), z3py::RecAddDefinition(), context::recfun(), z3py::RecFunction(), AstVector::resize(), Fixedpoint::set_predicate_representation(), z3py::substitute(), z3py::substitute_vars(), z3py::tactics(), and Solver::to_smt2().

                                                      {
        check_context(lo, hi);
        Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
        lo.check_error();
        return expr(lo.ctx(), r);
    }

expr z3::re_complement ( expr const &  a )

inline

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

                                             {
        MK_EXPR1(Z3_mk_re_complement, a);
    }

expr z3::re_empty ( sort const &  s )

inline

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

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

expr z3::re_full ( sort const &  s )

inline

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

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

expr z3::re_intersect ( expr_vector const &  args )

inline

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

                                                      {
        assert(args.size() > 0);
        context& ctx = args[0].ctx();
        array<Z3_ast> _args(args);
        Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
        ctx.check_error();
        return expr(ctx, r);
    }

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

Referenced by rem().

                                                  {
        if (a.is_fpa() && b.is_fpa()) {
            _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
        } else {
            _Z3_MK_BIN_(a, b, Z3_mk_rem);
        }
    }

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

inline

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

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

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

inline

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

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

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

inline

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

{ Z3_global_param_reset_all(); }

expr z3::round_fpa_to_closest_integer ( expr const &  t )

inline

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

                                                            {
        assert(t.is_fpa());
        Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
        t.check_error();
        return expr(t.ctx(), r);
    }

expr z3::sbv_to_fpa ( expr const &  t, sort  s  )

inline

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

                                                  {
        assert(t.is_bv());
        Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
        t.check_error();
        return expr(t.ctx(), r);
    }

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

inline

forward declarations

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

Referenced by expr::operator[](), and select().

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

expr select ( expr const &  a, expr_vector const &  i  )

inline

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

                                                              {
        check_context(a, i);
        array<Z3_ast> idxs(i);
        Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

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

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

inline

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

                                                      {
        MK_EXPR2(Z3_mk_set_add, s, e);
    }

expr z3::set_complement ( expr const &  a )

inline

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

                                              {
        MK_EXPR1(Z3_mk_set_complement, a);
    }

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

inline

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

                                                      {
        MK_EXPR2(Z3_mk_set_del, s, e);
    }

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

inline

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

                                                             {
        MK_EXPR2(Z3_mk_set_difference, a, b);
    }

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

inline

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

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

inline

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

                                                         {
        MK_EXPR2(Z3_mk_set_member, s, e);
    }

void z3::set_param ( char const *  param, char const *  value  )

inline

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

{ Z3_global_param_set(param, value); }

void z3::set_param ( char const *  param, bool  value  )

inline

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

{ auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); }

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

inline

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

                                                         {
        MK_EXPR2(Z3_mk_set_subset, a, b);
    }

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

inline

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

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

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

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

inline

signed greater than or equal to operator for bitvectors.

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

Referenced by sge().

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

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

inline

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

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

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

inline

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

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

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

inline

signed greater than operator for bitvectors.

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

Referenced by sgt().

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

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

inline

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

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

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

inline

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

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

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

inline

shift left operator for bitvectors

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

Referenced by shl().

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

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

inline

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

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

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

inline

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

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

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

inline

signed less than or equal to operator for bitvectors.

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

Referenced by sle().

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

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

inline

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

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

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

inline

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

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

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

inline

signed less than operator for bitvectors.

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

Referenced by slt().

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

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

inline

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

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

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

inline

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

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

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

inline

signed modulus operator for bitvectors

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

Referenced by smod().

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

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

inline

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

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

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

inline

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

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

expr z3::sqrt ( expr const &  a, expr const &  rm  )

inline

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

                                                     {
        check_context(a, rm);
        assert(a.is_fpa());
        Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

signed remainder operator for bitvectors

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

Referenced by srem().

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

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

inline

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

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

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

inline

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

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

expr z3::star ( expr const &  re )

inline

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

                                     {
        MK_EXPR1(Z3_mk_re_star, re);
    }

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

inline

Definition at line 3636 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 3643 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 3644 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 3645 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()));
    }

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

inline

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

                                                                             {
        check_context(a, i); check_context(a, v);
        array<Z3_ast> idxs(i);
        Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
        a.check_error();
        return expr(a.ctx(), r);
    }

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

inline

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

expr z3::sum ( expr_vector const &  args )

inline

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

                                             {
        assert(args.size() > 0);
        context& ctx = args[0].ctx();
        array<Z3_ast> _args(args);
        Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
        ctx.check_error();
        return expr(ctx, r);
    }

check_result z3::to_check_result ( Z3_lbool  l )

inline

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

Referenced by solver::check(), optimize::check(), solver::consequences(), and fixedpoint::query().

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

Referenced by ashr(), lshr(), sext(), sge(), sgt(), shl(), sle(), slt(), smod(), 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);
    }

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

inline

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

Referenced by linear_order(), partial_order(), piecewise_linear_order(), and tree_order().

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

expr z3::to_re ( expr const &  s )

inline

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

                                     {
        MK_EXPR1(Z3_mk_seq_to_re, s);
    }

expr z3::to_real ( expr const &  a )

inline

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

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

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

func_decl z3::tree_order ( sort const &  a, unsigned  index  )

inline

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

                                                               {
        return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
    }

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

inline

Definition at line 2983 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::ubv_to_fpa ( expr const &  t, sort  s  )

inline

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

                                                  {
        assert(t.is_bv());
        Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
        t.check_error();
        return expr(t.ctx(), r);
    }

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

inline

unsigned division operator for bitvectors.

Definition at line 2102 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 2103 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 2104 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 2090 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 2091 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 2092 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 2096 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 2097 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 2098 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 2078 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 2079 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 2080 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 2084 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 2085 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 2086 of file z3++.h.

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

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

inline

unsigned reminder operator for bitvectors

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

Referenced by urem().

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

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

inline

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

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

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

inline

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

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

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

inline

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

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

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

inline

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

{ if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }

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

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