z3 Namespace Reference

Z3 C++ namespace. More...

Data Structures
class	cast_ast
class	ast_vector_tpl
class	exception
	Exception used to sign API usage errors. More...
class	config
	Z3 global configuration object. More...
class	context
	A Context manages all other Z3 objects, global configuration options, etc. More...
class	array
class	object
class	symbol
class	param_descrs
class	params
class	ast
class	ast_map
	A map from ASTs to ASTs. More...
class	sort
	A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
class	func_decl
	Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
class	parser_context
class	expr
	A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
class	cast_ast< ast >
class	cast_ast< expr >
class	cast_ast< sort >
class	cast_ast< func_decl >
class	func_entry
class	func_interp
class	model
class	stats
class	parameter
	class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc). More...
class	solver
class	goal
class	apply_result
class	tactic
class	simplifier
class	probe
class	optimize
class	fixedpoint
class	constructor_list
class	constructors
class	on_clause
class	user_propagator_base
class	rcf_num
	Wrapper for Z3 Real Closed Field (RCF) numerals. More...

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
typedef std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)>	on_clause_eh_t

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 ()
void	get_version (unsigned &major, unsigned &minor, unsigned &build_number, unsigned &revision_number)
	Return Z3 version number information.
std::string	get_full_version ()
	Return a string that fully describes the version of Z3 in use.
void	enable_trace (char const *tag)
	Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
void	disable_trace (char const *tag)
	Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
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
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	complex (expr const &re, expr const &im)
	Construct a Complex expression from Int or Real components.
expr	real_part (expr const &z)
expr	imag_part (expr const &z)
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).
expr	to_expr (context &c, Z3_ast a)
	Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.
sort	to_sort (context &c, Z3_sort s)
func_decl	to_func_decl (context &c, Z3_func_decl f)
expr	sle (expr const &a, expr const &b)
	signed less than or equal to operator for bitvectors.
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.
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.
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.
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.
expr	ule (expr const &a, int b)
expr	ule (int a, expr const &b)
expr	ult (expr const &a, expr const &b)
	unsigned less than operator for bitvectors.
expr	ult (expr const &a, int b)
expr	ult (int a, expr const &b)
expr	uge (expr const &a, expr const &b)
	unsigned greater than or equal to operator for bitvectors.
expr	uge (expr const &a, int b)
expr	uge (int a, expr const &b)
expr	ugt (expr const &a, expr const &b)
	unsigned greater than operator for bitvectors.
expr	ugt (expr const &a, int b)
expr	ugt (int a, expr const &b)
expr	sdiv (expr const &a, expr const &b)
	signed division operator for bitvectors.
expr	sdiv (expr const &a, int b)
expr	sdiv (int a, expr const &b)
expr	udiv (expr const &a, expr const &b)
	unsigned division operator for bitvectors.
expr	udiv (expr const &a, int b)
expr	udiv (int a, expr const &b)
expr	srem (expr const &a, expr const &b)
	signed remainder operator for bitvectors
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
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
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
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
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
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.
expr	bv2int (expr const &a, bool is_signed)
	bit-vector and integer conversions.
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
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.
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_vector	polynomial_subresultants (expr const &p, expr const &q, expr const &x)
	Return the nonzero subresultants of p and q with respect to the "variable" x.
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	map (expr const &f, expr const &list)
expr	mapi (expr const &f, expr const &i, expr const &list)
expr	foldl (expr const &f, expr const &a, expr const &list)
expr	foldli (expr const &f, expr const &i, expr const &a, expr const &list)
expr	mk_or (expr_vector const &args)
expr	mk_and (expr_vector const &args)
expr	mk_xor (expr_vector const &args)
expr	qe_lite (expr_vector const &vars, expr const &body)
std::vector< Z3_app >	to_apps (expr_vector const &bounds)
expr	qe_model_project (model const &m, expr_vector const &bounds, expr const &body)
expr	qe_model_project_skolem (model const &m, expr_vector const &bounds, expr const &body, ast_map &map)
	Project variables and write the introduced Skolem terms to map.
expr	qe_model_project_with_witness (model const &m, expr_vector const &bounds, expr const &body, ast_map &map)
	Project variables and write the introduced witnesses to map.
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)
simplifier	operator& (simplifier const &t1, simplifier const &t2)
simplifier	with (simplifier const &t, params const &p)
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	array_default (expr const &a)
expr	array_ext (expr const &a, expr const &b)
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	finite_set_empty (sort const &s)
expr	finite_set_singleton (expr const &e)
expr	finite_set_union (expr const &a, expr const &b)
expr	finite_set_intersect (expr const &a, expr const &b)
expr	finite_set_difference (expr const &a, expr const &b)
expr	finite_set_member (expr const &e, expr const &s)
expr	finite_set_size (expr const &s)
expr	finite_set_subset (expr const &a, expr const &b)
expr	finite_set_map (expr const &f, expr const &s)
expr	finite_set_filter (expr const &f, expr const &s)
expr	finite_set_range (expr const &low, expr const &high)
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_diff (expr const &a, expr const &b)
expr	re_complement (expr const &a)
expr	range (expr const &lo, expr const &hi)
rcf_num	rcf_pi (context &c)
	Create an RCF numeral representing pi.
rcf_num	rcf_e (context &c)
	Create an RCF numeral representing e (Euler's constant).
rcf_num	rcf_infinitesimal (context &c)
	Create an RCF numeral representing an infinitesimal.
std::vector< rcf_num >	rcf_roots (context &c, std::vector< rcf_num > const &coeffs)
	Find roots of a polynomial with given coefficients.

Detailed Description

Z3 C++ namespace.

Typedef Documentation

ast_vector

typedef ast_vector_tpl<ast> ast_vector

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

expr_vector

typedef ast_vector_tpl<expr> expr_vector

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

func_decl_vector

typedef ast_vector_tpl<func_decl> func_decl_vector

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

on_clause_eh_t

typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t

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

sort_vector

typedef ast_vector_tpl<sort> sort_vector

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

Enumeration Type Documentation

check_result

enum check_result

Enumerator
unsat
sat
unknown

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

                      {
        unsat, sat, unknown
    };

rounding_mode

enum rounding_mode

Enumerator
RNA
RNE
RTP
RTN
RTZ

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

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

Function Documentation

abs()

expr abs ( expr const & a )

inline

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

array_default()

expr array_default ( expr const & a )

inline

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

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

Referenced by array_default().

array_ext()

expr array_ext ( expr const & a, expr const & b )

inline

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

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

Referenced by array_ext().

as_array()

expr as_array ( func_decl & f )

inline

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

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

Referenced by as_array().

ashr() [1/3]

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

inline

arithmetic shift right operator for bitvectors

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

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

Referenced by ashr(), ashr(), and ashr().

ashr() [2/3]

expr ashr ( expr const & a, int b )

inline

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

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

ashr() [3/3]

expr ashr ( int a, expr const & b )

inline

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

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

atleast()

expr atleast ( expr_vector const & es, unsigned bound )

inline

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

                                                               {
        assert(es.size() > 0);
        context& ctx = es[0u].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);
    }

atmost()

expr atmost ( expr_vector const & es, unsigned bound )

inline

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

                                                              {
        assert(es.size() > 0);
        context& ctx = es[0u].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);
    }

bv2int()

expr bv2int ( expr const & a, bool is_signed )

inline

bit-vector and integer conversions.

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

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

bvadd_no_overflow()

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

inline

bit-vector overflow/underflow checks

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

bvadd_no_underflow()

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

inline

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

bvmul_no_overflow()

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

inline

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

bvmul_no_underflow()

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

inline

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

bvneg_no_overflow()

expr bvneg_no_overflow ( expr const & a )

inline

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

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

bvredand()

expr bvredand ( expr const & a )

inline

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

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

bvredor()

expr bvredor ( expr const & a )

inline

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

bvsdiv_no_overflow()

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

inline

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

bvsub_no_overflow()

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

inline

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

bvsub_no_underflow()

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

inline

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

check_context()

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

inline

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

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

Referenced by array_ext(), complex(), cond(), exists(), exists(), exists(), exists(), forall(), forall(), forall(), forall(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), indexof(), lambda(), lambda(), lambda(), lambda(), last_indexof(), polynomial_subresultants(), prefixof(), qe_lite(), qe_model_project(), qe_model_project_skolem(), qe_model_project_with_witness(), re_diff(), context::recdef(), context::recfun(), context::recfun(), select(), select(), set_intersect(), set_union(), store(), store(), suffixof(), context::user_propagate_function(), and when().

complex()

expr complex ( expr const & re, expr const & im )

inline

Construct a Complex expression from Int or Real components.

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

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

Referenced by complex(), context::complex_val(), and context::complex_val().

concat() [1/2]

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

inline

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

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

concat() [2/2]

expr concat ( expr_vector const & args )

inline

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

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

cond()

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

inline

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

Referenced by cond().

const_array()

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

inline

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

                                                            {
        MK_EXPR2(Z3_mk_const_array, d, v);
    }

Referenced by const_array().

disable_trace()

void disable_trace ( char const * tag )

inline

Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.

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

                                                {
        Z3_disable_trace(tag);
    }

Referenced by disable_trace().

distinct()

expr distinct ( expr_vector const & args )

inline

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

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

empty()

expr empty ( sort const & s )

inline

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

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

Referenced by empty().

empty_set()

expr empty_set ( sort const & s )

inline

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

                                         {
        MK_EXPR1(Z3_mk_empty_set, s);
    }

Referenced by empty_set().

enable_trace()

void enable_trace ( char const * tag )

inline

Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.

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

                                               {
        Z3_enable_trace(tag);
    }

Referenced by enable_trace().

eq()

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

inline

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

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

exists() [1/5]

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

inline

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

Referenced by exists(), exists(), exists(), exists(), and exists().

exists() [2/5]

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

inline

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

                                                                         {
        check_context(x1, b); check_context(x2, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }

exists() [3/5]

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

inline

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

                                                                                          {
        check_context(x1, b); check_context(x2, b); check_context(x3, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }

exists() [4/5]

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

inline

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

                                                                                                           {
        check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
        Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }

exists() [5/5]

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

inline

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

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

fail_if()

tactic fail_if ( probe const & p )

inline

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

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

Referenced by fail_if().

finite_set_difference()

expr finite_set_difference ( expr const & a, expr const & b )

inline

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

                                                                    {
        MK_EXPR2(Z3_mk_finite_set_difference, a, b);
    }

Referenced by finite_set_difference().

finite_set_empty()

expr finite_set_empty ( sort const & s )

inline

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

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

Referenced by finite_set_empty().

finite_set_filter()

expr finite_set_filter ( expr const & f, expr const & s )

inline

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

                                                                {
        MK_EXPR2(Z3_mk_finite_set_filter, f, s);
    }

Referenced by finite_set_filter().

finite_set_intersect()

expr finite_set_intersect ( expr const & a, expr const & b )

inline

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

                                                                   {
        MK_EXPR2(Z3_mk_finite_set_intersect, a, b);
    }

Referenced by finite_set_intersect().

finite_set_map()

expr finite_set_map ( expr const & f, expr const & s )

inline

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

                                                             {
        MK_EXPR2(Z3_mk_finite_set_map, f, s);
    }

Referenced by finite_set_map().

finite_set_member()

expr finite_set_member ( expr const & e, expr const & s )

inline

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

                                                                {
        MK_EXPR2(Z3_mk_finite_set_member, e, s);
    }

Referenced by finite_set_member().

finite_set_range()

expr finite_set_range ( expr const & low, expr const & high )

inline

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

                                                                    {
        MK_EXPR2(Z3_mk_finite_set_range, low, high);
    }

Referenced by finite_set_range().

finite_set_singleton()

expr finite_set_singleton ( expr const & e )

inline

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

                                                    {
        MK_EXPR1(Z3_mk_finite_set_singleton, e);
    }

Referenced by finite_set_singleton().

finite_set_size()

expr finite_set_size ( expr const & s )

inline

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

                                               {
        MK_EXPR1(Z3_mk_finite_set_size, s);
    }

Referenced by finite_set_size().

finite_set_subset()

expr finite_set_subset ( expr const & a, expr const & b )

inline

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

                                                                {
        MK_EXPR2(Z3_mk_finite_set_subset, a, b);
    }

Referenced by finite_set_subset().

finite_set_union()

expr finite_set_union ( expr const & a, expr const & b )

inline

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

                                                               {
        MK_EXPR2(Z3_mk_finite_set_union, a, b);
    }

Referenced by finite_set_union().

fma()

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

inline

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

foldl()

expr foldl ( expr const & f, expr const & a, expr const & list )

inline

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

                                                                      {
        context& ctx = f.ctx();
        Z3_ast r = Z3_mk_seq_foldl(ctx, f, a, list);
        ctx.check_error();
        return expr(ctx, r);
    }

Referenced by foldl().

foldli()

expr foldli ( expr const & f, expr const & i, expr const & a, expr const & list )

inline

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

                                                                                      {
        context& ctx = f.ctx();
        Z3_ast r = Z3_mk_seq_foldli(ctx, f, i, a, list);
        ctx.check_error();
        return expr(ctx, r);
    }

Referenced by foldli().

forall() [1/5]

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

inline

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

Referenced by forall(), forall(), forall(), forall(), and forall().

forall() [2/5]

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

inline

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

                                                                         {
        check_context(x1, b); check_context(x2, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }

forall() [3/5]

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

inline

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

                                                                                          {
        check_context(x1, b); check_context(x2, b); check_context(x3, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }

forall() [4/5]

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

inline

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

                                                                                                           {
        check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
        Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
        Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
    }

forall() [5/5]

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

inline

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

fp_eq()

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

inline

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

fpa_fp()

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

inline

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

fpa_to_fpa()

expr fpa_to_fpa ( expr const & t, sort s )

inline

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

fpa_to_sbv()

expr fpa_to_sbv ( expr const & t, unsigned sz )

inline

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

fpa_to_ubv()

expr fpa_to_ubv ( expr const & t, unsigned sz )

inline

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

full_set()

expr full_set ( sort const & s )

inline

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

                                        {
        MK_EXPR1(Z3_mk_full_set, s);
    }

Referenced by full_set().

function() [1/9]

func_decl function ( char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range )

inline

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

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

function() [2/9]

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

inline

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

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

function() [3/9]

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

inline

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

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

function() [4/9]

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

inline

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

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

function() [5/9]

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

inline

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

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

function() [6/9]

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

inline

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

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

function() [7/9]

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

inline

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

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

function() [8/9]

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

inline

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

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

function() [9/9]

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

inline

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

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

Referenced by function(), function(), function(), function(), function(), function(), function(), function(), and function().

get_full_version()

std::string get_full_version ( )

inline

Return a string that fully describes the version of Z3 in use.

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

                                        {
        return std::string(Z3_get_full_version());
    }

Referenced by get_full_version().

get_version()

void get_version ( unsigned & major, unsigned & minor, unsigned & build_number, unsigned & revision_number )

inline

Return Z3 version number information.

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

                                                                                                                 {
        Z3_get_version(&major, &minor, &build_number, &revision_number);
    }

Referenced by get_version().

imag_part()

expr imag_part ( expr const & z )

inline

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

                                         {
        Z3_ast r = Z3_mk_imag_part(z.ctx(), z);
        z.check_error();
        return expr(z.ctx(), r);
    }

Referenced by imag_part().

implies() [1/3]

expr implies ( bool a, expr const & b )

inline

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

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

implies() [2/3]

expr implies ( expr const & a, bool b )

inline

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

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

implies() [3/3]

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

inline

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

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

in_re()

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

inline

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

                                                     {
        MK_EXPR2(Z3_mk_seq_in_re, s, re);
    }

Referenced by in_re().

indexof()

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

inline

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

Referenced by indexof().

int2bv()

expr int2bv ( unsigned n, expr const & a )

inline

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

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

is_int()

expr is_int ( expr const & e )

inline

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

{ _Z3_MK_UN_(e, Z3_mk_is_int); }

ite()

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

lambda() [1/5]

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

inline

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

Referenced by lambda(), lambda(), lambda(), lambda(), and lambda().

lambda() [2/5]

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

inline

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

lambda() [3/5]

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

inline

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

lambda() [4/5]

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

inline

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

lambda() [5/5]

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

inline

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

last_indexof()

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

inline

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

Referenced by last_indexof().

linear_order()

func_decl linear_order ( sort const & a, unsigned index )

inline

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

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

Referenced by linear_order().

lshr() [1/3]

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

inline

logic shift right operator for bitvectors

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

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

Referenced by lshr(), lshr(), and lshr().

lshr() [2/3]

expr lshr ( expr const & a, int b )

inline

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

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

lshr() [3/3]

expr lshr ( int a, expr const & b )

inline

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

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

map()

expr map ( expr const & f, expr const & list )

inline

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

                                                     {
        context& ctx = f.ctx();
        Z3_ast r = Z3_mk_seq_map(ctx, f, list);
        ctx.check_error();
        return expr(ctx, r);
    }

Referenced by map(), qe_model_project_skolem(), and qe_model_project_with_witness().

mapi()

expr mapi ( expr const & f, expr const & i, expr const & list )

inline

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

                                                                     {
        context& ctx = f.ctx();
        Z3_ast r = Z3_mk_seq_mapi(ctx, f, i, list);
        ctx.check_error();
        return expr(ctx, r);
    }

Referenced by mapi().

max()

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

inline

Definition at line 2221 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), 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); 
        }
        a.check_error();
        return expr(a.ctx(), r); 
    }

Referenced by tactic::repeat.

min()

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

inline

Definition at line 2205 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); 
        }
        a.check_error();
        return expr(a.ctx(), r); 
    }

mk_and()

expr mk_and ( expr_vector const & args )

inline

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

mk_or()

expr mk_or ( expr_vector const & args )

inline

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

mk_xor()

expr mk_xor ( expr_vector const & args )

inline

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

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

mod() [1/3]

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

inline

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

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

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

mod() [2/3]

expr mod ( expr const & a, int b )

inline

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

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

mod() [3/3]

expr mod ( int a, expr const & b )

inline

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

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

nand()

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

inline

Definition at line 2202 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); a.check_error(); return expr(a.ctx(), r); }

nor()

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

inline

Definition at line 2203 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); a.check_error(); return expr(a.ctx(), r); }

operator!() [1/2]

expr operator! ( expr const & a )

inline

Precondition

a.is_bool()

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

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

operator!() [2/2]

probe operator! ( probe const & p )

inline

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

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

operator!=() [1/5]

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

inline

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

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

operator!=() [2/5]

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

inline

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

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

operator!=() [3/5]

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

inline

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

Referenced by operator!=(), and operator!=().

operator!=() [4/5]

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

inline

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

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

operator!=() [5/5]

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

inline

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

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

operator%() [1/3]

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

inline

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

{ return mod(a, b); }

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

operator%() [2/3]

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

inline

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

{ return mod(a, b); }

operator%() [3/3]

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

inline

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

{ return mod(a, b); }

operator&() [1/5]

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

inline

Definition at line 2190 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); a.check_error(); return expr(a.ctx(), r); }

operator&() [2/5]

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

inline

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

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

operator&() [3/5]

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

inline

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

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

operator&() [4/5]

simplifier operator& ( simplifier const & t1, simplifier const & t2 )

inline

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

                                                                              {
        check_context(t1, t2);
        Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
        t1.check_error();
        return simplifier(t1.ctx(), r);
    }

operator&() [5/5]

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

inline

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

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

operator&&() [1/4]

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

inline

Precondition

b.is_bool()

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

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

operator&&() [2/4]

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

inline

Precondition

a.is_bool()

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

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

operator&&() [3/4]

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

inline

Precondition

a.is_bool()

b.is_bool()

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

operator&&() [4/4]

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

inline

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

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

operator*() [1/3]

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

inline

Definition at line 2007 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_finite_field() && b.is_finite_field()) {
            Z3_ast args[2] = { a, b };
            r = Z3_mk_ff_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);
    }

operator*() [2/3]

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

inline

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

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

operator*() [3/3]

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

inline

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

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

operator+() [1/3]

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

inline

Definition at line 1973 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_finite_field() && b.is_finite_field()) {
            Z3_ast args[2] = { a, b };
            r = Z3_mk_ff_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);
    }

operator+() [2/3]

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

inline

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

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

operator+() [3/3]

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

inline

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

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

operator-() [1/4]

expr operator- ( expr const & a )

inline

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

                                          {
        Z3_ast r = 0;
        if (a.is_arith()) {
            r = Z3_mk_unary_minus(a.ctx(), a);
        }
        else if (a.is_finite_field()) { r = Z3_mk_ff_neg(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);
    }

operator-() [2/4]

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

inline

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

                                                          {
        check_context(a, b);
        if (a.is_finite_field() && b.is_finite_field()) return 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);
    }

operator-() [3/4]

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

inline

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

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

operator-() [4/4]

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

inline

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

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

operator/() [1/3]

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

inline

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

operator/() [2/3]

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

inline

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

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

operator/() [3/3]

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

inline

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

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

operator<() [1/6]

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

inline

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

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

operator<() [2/6]

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

inline

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

operator<() [3/6]

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

inline

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

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

operator<() [4/6]

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

inline

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

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

operator<() [5/6]

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

inline

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

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

operator<() [6/6]

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

inline

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

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

operator<<() [1/13]

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

inline

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

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

operator<<() [2/13]

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

inline

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

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

operator<<() [3/13]

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

inline

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

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

operator<<() [4/13]

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

inline

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

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

Referenced by operator<<(), operator<<(), and operator<<().

operator<<() [5/13]

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

inline

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

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

operator<<() [6/13]

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

inline

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

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

operator<<() [7/13]

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

inline

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

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

operator<<() [8/13]

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

inline

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

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

operator<<() [9/13]

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

inline

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

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

operator<<() [10/13]

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

inline

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

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

operator<<() [11/13]

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

inline

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

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

operator<<() [12/13]

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

inline

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

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

operator<<() [13/13]

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

inline

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

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

operator<=() [1/6]

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

inline

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

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

operator<=() [2/6]

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

inline

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

operator<=() [3/6]

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

inline

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

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

operator<=() [4/6]

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

inline

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

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

operator<=() [5/6]

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

inline

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

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

operator<=() [6/6]

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

inline

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

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

operator==() [1/8]

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

inline

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

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

operator==() [2/8]

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

inline

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

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

operator==() [3/8]

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

inline

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

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

operator==() [4/8]

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

inline

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

Referenced by operator==(), and operator==().

operator==() [5/8]

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

inline

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

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

operator==() [6/8]

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

inline

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

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

operator==() [7/8]

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

inline

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

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

operator==() [8/8]

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

inline

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

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

operator>() [1/6]

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

inline

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

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

operator>() [2/6]

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

inline

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

operator>() [3/6]

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

inline

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

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

operator>() [4/6]

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

inline

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

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

operator>() [5/6]

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

inline

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

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

operator>() [6/6]

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

inline

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

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

operator>=() [1/6]

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

inline

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

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

operator>=() [2/6]

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

inline

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

operator>=() [3/6]

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

inline

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

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

operator>=() [4/6]

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

inline

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

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

operator>=() [5/6]

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

inline

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

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

operator>=() [6/6]

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

inline

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

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

operator^() [1/3]

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

inline

Definition at line 2194 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); a.check_error(); return expr(a.ctx(), r); }

operator^() [2/3]

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

inline

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

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

operator^() [3/3]

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

inline

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

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

operator|() [1/4]

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

inline

Definition at line 2198 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); a.check_error(); return expr(a.ctx(), r); }

operator|() [2/4]

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

inline

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

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

operator|() [3/4]

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

inline

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

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

operator|() [4/4]

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

inline

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

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

operator||() [1/4]

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

inline

Precondition

b.is_bool()

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

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

operator||() [2/4]

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

inline

Precondition

a.is_bool()

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

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

operator||() [3/4]

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

inline

Precondition

a.is_bool()

b.is_bool()

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

operator||() [4/4]

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

inline

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

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

operator~()

expr operator~ ( expr const & a )

inline

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

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

option()

expr option ( expr const & re )

inline

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

                                       {
        MK_EXPR1(Z3_mk_re_option, re);
    }

Referenced by option().

par_and_then()

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

inline

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

par_or()

tactic par_or ( unsigned n, tactic const * tactics )

inline

Definition at line 3538 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[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
    }

partial_order()

func_decl partial_order ( sort const & a, unsigned index )

inline

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

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

Referenced by partial_order().

pbeq()

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

inline

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

                                                                          {
        assert(es.size() > 0);
        context& ctx = es[0u].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);
    }

pbge()

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

inline

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

                                                                          {
        assert(es.size() > 0);
        context& ctx = es[0u].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);
    }

pble()

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

inline

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

                                                                          {
        assert(es.size() > 0);
        context& ctx = es[0u].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);
    }

piecewise_linear_order()

func_decl piecewise_linear_order ( sort const & a, unsigned index )

inline

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

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

Referenced by piecewise_linear_order().

plus()

expr plus ( expr const & re )

inline

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

                                     {
        MK_EXPR1(Z3_mk_re_plus, re);
    }

Referenced by plus().

polynomial_subresultants()

expr_vector polynomial_subresultants ( expr const & p, expr const & q, expr const & x )

inline

Return the nonzero subresultants of p and q with respect to the "variable" x.

Precondition

p, q and x are Z3 expressions where p and q are arithmetic terms. Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.

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

                                                                                             {
        check_context(p, q); check_context(p, x);
        Z3_ast_vector r = Z3_polynomial_subresultants(p.ctx(), p, q, x);
        p.check_error();
        return expr_vector(p.ctx(), r);
    }

Referenced by polynomial_subresultants().

prefixof()

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

inline

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

Referenced by prefixof().

pw() [1/3]

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

inline

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

{ _Z3_MK_BIN_(a, b, Z3_mk_power);   }

pw() [2/3]

expr pw ( expr const & a, int b )

inline

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

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

pw() [3/3]

expr pw ( int a, expr const & b )

inline

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

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

qe_lite()

expr qe_lite ( expr_vector const & vars, expr const & body )

inline

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

                                                                   {
        check_context(vars, body);
        Z3_ast r = Z3_qe_lite(body.ctx(), vars, body);
        body.check_error();
        return expr(body.ctx(), r);
    }

Referenced by qe_lite().

qe_model_project()

expr qe_model_project ( model const & m, expr_vector const & bounds, expr const & body )

inline

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

                                                                                              {
        check_context(m, bounds); check_context(m, body);
        std::vector<Z3_app> apps = to_apps(bounds);
        Z3_ast r = Z3_qe_model_project(m.ctx(), m, bounds.size(), apps.data(), body);
        m.check_error();
        return expr(m.ctx(), r);
    }

Referenced by qe_model_project().

qe_model_project_skolem()

expr qe_model_project_skolem ( model const & m, expr_vector const & bounds, expr const & body, ast_map & map )

inline

Project variables and write the introduced Skolem terms to map.

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

                                                                                                                   {
        check_context(m, bounds); check_context(m, body); check_context(m, map);
        std::vector<Z3_app> apps = to_apps(bounds);
        Z3_ast r = Z3_qe_model_project_skolem(m.ctx(), m, bounds.size(), apps.data(), body, map);
        m.check_error();
        return expr(m.ctx(), r);
    }

Referenced by qe_model_project_skolem().

qe_model_project_with_witness()

expr qe_model_project_with_witness ( model const & m, expr_vector const & bounds, expr const & body, ast_map & map )

inline

Project variables and write the introduced witnesses to map.

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

                                                                                                                         {
        check_context(m, bounds); check_context(m, body); check_context(m, map);
        std::vector<Z3_app> apps = to_apps(bounds);
        Z3_ast r = Z3_qe_model_project_with_witness(m.ctx(), m, bounds.size(), apps.data(), body, map);
        m.check_error();
        return expr(m.ctx(), r);
    }

Referenced by qe_model_project_with_witness().

range()

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

inline

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

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

Referenced by context::fpa_sort(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), function(), function(), function(), function(), function(), function(), function(), function(), function(), context::recfun(), context::recfun(), context::recfun(), context::recfun(), context::recfun(), context::recfun(), recfun(), recfun(), recfun(), recfun(), and context::user_propagate_function().

rcf_e()

rcf_num rcf_e ( context & c )

inline

Create an RCF numeral representing e (Euler's constant).

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

                                     {
        return rcf_num(c, Z3_rcf_mk_e(c));
    }

Referenced by rcf_e().

rcf_infinitesimal()

rcf_num rcf_infinitesimal ( context & c )

inline

Create an RCF numeral representing an infinitesimal.

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

                                                 {
        return rcf_num(c, Z3_rcf_mk_infinitesimal(c));
    }

Referenced by rcf_infinitesimal().

rcf_pi()

rcf_num rcf_pi ( context & c )

inline

Create an RCF numeral representing pi.

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

                                      {
        return rcf_num(c, Z3_rcf_mk_pi(c));
    }

Referenced by rcf_pi().

rcf_roots()

std::vector< rcf_num > rcf_roots ( context & c, std::vector< rcf_num > const & coeffs )

inline

Find roots of a polynomial with given coefficients.

The polynomial is a[n-1]*x^(n-1) + ... + a[1]*x + a[0]. Returns a vector of RCF numerals representing the roots.

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

                                                                                      {
        if (coeffs.empty()) {
            Z3_THROW(exception("polynomial coefficients cannot be empty"));
        }
 
        unsigned n = static_cast<unsigned>(coeffs.size());
        std::vector<Z3_rcf_num> a(n);
        std::vector<Z3_rcf_num> roots(n);
        
        for (unsigned i = 0; i < n; ++i) {
            a[i] = coeffs[i];
        }
        
        unsigned num_roots = Z3_rcf_mk_roots(c, n, a.data(), roots.data());
        
        std::vector<rcf_num> result;
        result.reserve(num_roots);
        for (unsigned i = 0; i < num_roots; ++i) {
            result.push_back(rcf_num(c, roots[i]));
        }
        
        return result;
    }

Referenced by rcf_roots().

re_complement()

expr re_complement ( expr const & a )

inline

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

                                             {
        MK_EXPR1(Z3_mk_re_complement, a);
    }

Referenced by re_complement().

re_diff()

expr re_diff ( expr const & a, expr const & b )

inline

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

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

Referenced by re_diff().

re_empty()

expr re_empty ( sort const & s )

inline

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

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

Referenced by re_empty().

re_full()

expr re_full ( sort const & s )

inline

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

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

Referenced by re_full().

re_intersect()

expr re_intersect ( expr_vector const & args )

inline

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

                                                      {
        assert(args.size() > 0);
        context& ctx = args[0u].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);
    }

Referenced by re_intersect().

real_part()

expr real_part ( expr const & z )

inline

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

                                         {
        Z3_ast r = Z3_mk_real_part(z.ctx(), z);
        z.check_error();
        return expr(z.ctx(), r);
    }

Referenced by real_part().

recfun() [1/4]

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

inline

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

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

recfun() [2/4]

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

inline

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

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

recfun() [3/4]

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

inline

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

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

recfun() [4/4]

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

inline

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

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

Referenced by recfun(), recfun(), recfun(), and recfun().

rem() [1/3]

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

inline

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

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

rem() [2/3]

expr rem ( expr const & a, int b )

inline

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

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

rem() [3/3]

expr rem ( int a, expr const & b )

inline

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

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

repeat()

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

inline

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

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

reset_params()

void reset_params ( )

inline

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

{ Z3_global_param_reset_all(); }

Referenced by reset_params().

round_fpa_to_closest_integer()

expr round_fpa_to_closest_integer ( expr const & t )

inline

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

sbv_to_fpa()

expr sbv_to_fpa ( expr const & t, sort s )

inline

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

sdiv() [1/3]

expr sdiv ( expr const & a, expr const & b )

inline

signed division operator for bitvectors.

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

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

Referenced by sdiv(), sdiv(), and sdiv().

sdiv() [2/3]

expr sdiv ( expr const & a, int b )

inline

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

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

sdiv() [3/3]

expr sdiv ( int a, expr const & b )

inline

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

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

select() [1/3]

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

inline

forward declarations

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

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

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

select() [2/3]

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

inline

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

select() [3/3]

expr select ( expr const & a, int i )

inline

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

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

set_add()

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

inline

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

                                                      {
        MK_EXPR2(Z3_mk_set_add, s, e);
    }

Referenced by set_add().

set_complement()

expr set_complement ( expr const & a )

inline

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

                                              {
        MK_EXPR1(Z3_mk_set_complement, a);
    }

Referenced by set_complement().

set_del()

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

inline

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

                                                      {
        MK_EXPR2(Z3_mk_set_del, s, e);
    }

Referenced by set_del().

set_difference()

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

inline

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

                                                             {
        MK_EXPR2(Z3_mk_set_difference, a, b);
    }

Referenced by set_difference().

set_intersect()

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

inline

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

Referenced by set_intersect().

set_member()

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

inline

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

                                                         {
        MK_EXPR2(Z3_mk_set_member, s, e);
    }

Referenced by set_member().

set_param() [1/3]

void set_param ( char const * param, bool value )

inline

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

{ Z3_global_param_set(param, value ? "true" : "false"); }

set_param() [2/3]

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

inline

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

{ Z3_global_param_set(param, value); }

Referenced by set_param(), set_param(), and set_param().

set_param() [3/3]

void set_param ( char const * param, int value )

inline

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

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

set_subset()

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

inline

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

                                                         {
        MK_EXPR2(Z3_mk_set_subset, a, b);
    }

Referenced by set_subset().

set_union()

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

inline

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

Referenced by set_union().

sext()

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

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

Referenced by sext().

sge() [1/3]

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

inline

signed greater than or equal to operator for bitvectors.

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

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

Referenced by sge(), sge(), and sge().

sge() [2/3]

expr sge ( expr const & a, int b )

inline

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

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

sge() [3/3]

expr sge ( int a, expr const & b )

inline

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

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

sgt() [1/3]

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

inline

signed greater than operator for bitvectors.

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

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

Referenced by sgt(), sgt(), and sgt().

sgt() [2/3]

expr sgt ( expr const & a, int b )

inline

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

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

sgt() [3/3]

expr sgt ( int a, expr const & b )

inline

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

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

shl() [1/3]

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

inline

shift left operator for bitvectors

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

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

Referenced by shl(), shl(), and shl().

shl() [2/3]

expr shl ( expr const & a, int b )

inline

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

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

shl() [3/3]

expr shl ( int a, expr const & b )

inline

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

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

sle() [1/3]

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

inline

signed less than or equal to operator for bitvectors.

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

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

Referenced by sle(), sle(), and sle().

sle() [2/3]

expr sle ( expr const & a, int b )

inline

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

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

sle() [3/3]

expr sle ( int a, expr const & b )

inline

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

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

slt() [1/3]

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

inline

signed less than operator for bitvectors.

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

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

Referenced by slt(), slt(), and slt().

slt() [2/3]

expr slt ( expr const & a, int b )

inline

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

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

slt() [3/3]

expr slt ( int a, expr const & b )

inline

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

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

smod() [1/3]

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

inline

signed modulus operator for bitvectors

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

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

Referenced by smod(), smod(), and smod().

smod() [2/3]

expr smod ( expr const & a, int b )

inline

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

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

smod() [3/3]

expr smod ( int a, expr const & b )

inline

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

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

sqrt()

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

inline

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

srem() [1/3]

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

inline

signed remainder operator for bitvectors

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

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

Referenced by srem(), srem(), and srem().

srem() [2/3]

expr srem ( expr const & a, int b )

inline

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

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

srem() [3/3]

expr srem ( int a, expr const & b )

inline

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

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

star()

expr star ( expr const & re )

inline

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

                                     {
        MK_EXPR1(Z3_mk_re_star, re);
    }

Referenced by star().

store() [1/5]

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

inline

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

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

Referenced by store(), store(), store(), store(), and store().

store() [2/5]

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

inline

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

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

store() [3/5]

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

inline

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

store() [4/5]

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

inline

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

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

store() [5/5]

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

inline

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

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

suffixof()

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

inline

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

Referenced by suffixof().

sum()

expr sum ( expr_vector const & args )

inline

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

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

to_apps()

std::vector< Z3_app > to_apps ( expr_vector const & bounds )

inline

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

                                                                {
        std::vector<Z3_app> apps;
        for (unsigned i = 0; i < bounds.size(); ++i) {
            if (!Z3_is_app(bounds.ctx(), bounds[i]))
                Z3_THROW(exception("model projection bounds must be applications"));
            apps.push_back(Z3_to_app(bounds.ctx(), bounds[i]));
        }
        return apps;
    }

Referenced by qe_model_project(), qe_model_project_skolem(), qe_model_project_with_witness(), and to_apps().

to_check_result()

check_result to_check_result ( Z3_lbool l )

inline

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

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

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

to_expr()

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

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

Referenced by ashr(), lshr(), sdiv(), sext(), sge(), sgt(), shl(), sle(), slt(), smod(), srem(), to_expr(), udiv(), uge(), ugt(), ule(), ult(), urem(), and zext().

to_func_decl()

func_decl to_func_decl ( context & c, Z3_func_decl f )

inline

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

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

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

to_re()

expr to_re ( expr const & s )

inline

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

                                     {
        MK_EXPR1(Z3_mk_seq_to_re, s);
    }

Referenced by to_re().

to_real()

expr to_real ( expr const & a )

inline

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

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

Referenced by to_real().

to_sort()

sort to_sort ( context & c, Z3_sort s )

inline

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

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

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

tree_order()

func_decl tree_order ( sort const & a, unsigned index )

inline

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

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

Referenced by tree_order().

try_for()

tactic try_for ( tactic const & t, unsigned ms )

inline

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

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

ubv_to_fpa()

expr ubv_to_fpa ( expr const & t, sort s )

inline

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

udiv() [1/3]

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

inline

unsigned division operator for bitvectors.

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

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

Referenced by udiv(), udiv(), and udiv().

udiv() [2/3]

expr udiv ( expr const & a, int b )

inline

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

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

udiv() [3/3]

expr udiv ( int a, expr const & b )

inline

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

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

uge() [1/3]

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

inline

unsigned greater than or equal to operator for bitvectors.

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

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

Referenced by uge(), uge(), and uge().

uge() [2/3]

expr uge ( expr const & a, int b )

inline

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

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

uge() [3/3]

expr uge ( int a, expr const & b )

inline

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

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

ugt() [1/3]

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

inline

unsigned greater than operator for bitvectors.

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

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

Referenced by ugt(), ugt(), and ugt().

ugt() [2/3]

expr ugt ( expr const & a, int b )

inline

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

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

ugt() [3/3]

expr ugt ( int a, expr const & b )

inline

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

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

ule() [1/3]

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

inline

unsigned less than or equal to operator for bitvectors.

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

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

Referenced by ule(), ule(), and ule().

ule() [2/3]

expr ule ( expr const & a, int b )

inline

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

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

ule() [3/3]

expr ule ( int a, expr const & b )

inline

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

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

ult() [1/3]

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

inline

unsigned less than operator for bitvectors.

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

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

Referenced by ult(), ult(), and ult().

ult() [2/3]

expr ult ( expr const & a, int b )

inline

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

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

ult() [3/3]

expr ult ( int a, expr const & b )

inline

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

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

urem() [1/3]

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

inline

unsigned reminder operator for bitvectors

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

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

Referenced by urem(), urem(), and urem().

urem() [2/3]

expr urem ( expr const & a, int b )

inline

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

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

urem() [3/3]

expr urem ( int a, expr const & b )

inline

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

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

when()

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

inline

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

Referenced by when().

with() [1/2]

simplifier with ( simplifier const & t, params const & p )

inline

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

                                                                   {
        Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
        t.check_error();
        return simplifier(t.ctx(), r);
    }

with() [2/2]

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

inline

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

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

xnor()

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

inline

Definition at line 2204 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); a.check_error(); return expr(a.ctx(), r); }

zext()

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

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

Referenced by zext().