expr Class Reference

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...

#include <z3++.h>

Inheritance diagram for expr:

Data Structures
class	iterator

Public Member Functions
	expr (context &c)
	expr (context &c, Z3_ast n)
sort	get_sort () const
	Return the sort of this expression.
bool	is_bool () const
	Return true if this is a Boolean expression.
bool	is_int () const
	Return true if this is an integer expression.
bool	is_real () const
	Return true if this is a real expression.
bool	is_arith () const
	Return true if this is an integer or real expression.
bool	is_bv () const
	Return true if this is a Bit-vector expression.
bool	is_array () const
	Return true if this is a Array expression.
bool	is_datatype () const
	Return true if this is a Datatype expression.
bool	is_relation () const
	Return true if this is a Relation expression.
bool	is_seq () const
	Return true if this is a sequence expression.
bool	is_re () const
	Return true if this is a regular expression.
bool	is_finite_domain () const
	Return true if this is a Finite-domain expression.
bool	is_fpa () const
	Return true if this is a FloatingPoint expression. .
bool	is_numeral () const
	Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings.
bool	is_numeral_i64 (int64_t &i) const
bool	is_numeral_u64 (uint64_t &i) const
bool	is_numeral_i (int &i) const
bool	is_numeral_u (unsigned &i) const
bool	is_numeral (std::string &s) const
bool	is_numeral (std::string &s, unsigned precision) const
bool	is_numeral (double &d) const
bool	as_binary (std::string &s) const
double	as_double () const
uint64_t	as_uint64 () const
int64_t	as_int64 () const
bool	is_app () const
	Return true if this expression is an application.
bool	is_const () const
	Return true if this expression is a constant (i.e., an application with 0 arguments).
bool	is_quantifier () const
	Return true if this expression is a quantifier.
bool	is_forall () const
	Return true if this expression is a universal quantifier.
bool	is_exists () const
	Return true if this expression is an existential quantifier.
bool	is_lambda () const
	Return true if this expression is a lambda expression.
bool	is_var () const
	Return true if this expression is a variable.
bool	is_algebraic () const
	Return true if expression is an algebraic number.
bool	is_well_sorted () const
	Return true if this expression is well sorted (aka type correct).
expr	mk_is_inf () const
	Return Boolean expression to test for whether an FP expression is inf.
expr	mk_is_nan () const
	Return Boolean expression to test for whether an FP expression is a NaN.
expr	mk_is_normal () const
	Return Boolean expression to test for whether an FP expression is a normal.
expr	mk_is_subnormal () const
	Return Boolean expression to test for whether an FP expression is a subnormal.
expr	mk_is_zero () const
	Return Boolean expression to test for whether an FP expression is a zero.
expr	mk_to_ieee_bv () const
	Convert this fpa into an IEEE BV.
expr	mk_from_ieee_bv (sort const &s) const
	Convert this IEEE BV into a fpa.
std::string	get_decimal_string (int precision) const
	Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.
expr	algebraic_lower (unsigned precision) const
expr	algebraic_upper (unsigned precision) const
expr_vector	algebraic_poly () const
	Return coefficients for p of an algebraic number (root-obj p i).
unsigned	algebraic_i () const
	Return i of an algebraic number (root-obj p i).
unsigned	id () const
	retrieve unique identifier for expression.
int	get_numeral_int () const
	Return int value of numeral, throw if result cannot fit in machine int.
unsigned	get_numeral_uint () const
	Return uint value of numeral, throw if result cannot fit in machine uint.
int64_t	get_numeral_int64 () const
	Return int64_t value of numeral, throw if result cannot fit in int64_t.
uint64_t	get_numeral_uint64 () const
	Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Z3_lbool	bool_value () const
expr	numerator () const
expr	denominator () const
bool	is_string_value () const
	Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string().
std::string	get_string () const
	for a string value expression return an escaped string value.
std::u32string	get_u32string () const
	for a string value expression return an unespaced string value.
	operator Z3_app () const
func_decl	decl () const
	Return the declaration associated with this application. This method assumes the expression is an application.
unsigned	num_args () const
	Return the number of arguments in this application. This method assumes the expression is an application.
expr	arg (unsigned i) const
	Return the i-th argument of this application. This method assumes the expression is an application.
expr_vector	args () const
	Return a vector of all the arguments of this application. This method assumes the expression is an application.
expr	update (expr_vector const &args) const
	Update the arguments of this application. Return a new expression with the same function declaration and updated arguments. The number of new arguments must match the current number of arguments.
expr	update_field (func_decl const &field_access, expr const &new_value) const
	Update a datatype field. Return a new datatype expression with the specified field updated to the new value. The remaining fields are unchanged.
expr	body () const
	Return the 'body' of this quantifier.
bool	is_true () const
bool	is_false () const
bool	is_not () const
bool	is_and () const
bool	is_or () const
bool	is_xor () const
bool	is_implies () const
bool	is_eq () const
bool	is_ite () const
bool	is_distinct () const
expr	rotate_left (unsigned i) const
expr	rotate_right (unsigned i) const
expr	ext_rotate_left (expr const &n) const
expr	ext_rotate_right (expr const &n) const
expr	repeat (unsigned i) const
expr	extract (unsigned hi, unsigned lo) const
expr	bit2bool (unsigned i) const
unsigned	lo () const
unsigned	hi () const
expr	extract (expr const &offset, expr const &length) const
	sequence and regular expression operations.
expr	replace (expr const &src, expr const &dst) const
expr	unit () const
expr	contains (expr const &s) const
expr	at (expr const &index) const
expr	nth (expr const &index) const
expr	length () const
expr	stoi () const
expr	itos () const
expr	ubvtos () const
expr	sbvtos () const
expr	char_to_int () const
expr	char_to_bv () const
expr	char_from_bv () const
expr	is_digit () const
expr	loop (unsigned lo)
	create a looping regular expression.
expr	loop (unsigned lo, unsigned hi)
expr	operator[] (expr const &index) const
expr	operator[] (expr_vector const &index) const
expr	simplify () const
	Return a simplified version of this expression.
expr	simplify (params const &p) const
	Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.
expr	substitute (expr_vector const &src, expr_vector const &dst)
	Apply substitution. Replace src expressions by dst.
expr	substitute (expr_vector const &dst)
	Apply substitution. Replace bound variables by expressions.
expr	substitute (func_decl_vector const &funs, expr_vector const &bodies)
	Apply function substitution by macro definitions.
iterator	begin ()
iterator	end ()
Public Member Functions inherited from ast
	ast (context &c)
	ast (context &c, Z3_ast n)
	ast (ast const &s)
	~ast () override
	operator Z3_ast () const
	operator bool () const
ast &	operator= (ast const &s)
Z3_ast_kind	kind () const
unsigned	hash () const
std::string	to_string () const
Public Member Functions inherited from object
	object (context &c)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

Friends
expr	operator! (expr const &a)
	Return an expression representing not(a).
expr	operator&& (expr const &a, expr const &b)
	Return an expression representing a and b.
expr	operator&& (expr const &a, bool b)
	Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr	operator&& (bool a, expr const &b)
	Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr	operator|| (expr const &a, expr const &b)
	Return an expression representing a or b.
expr	operator|| (expr const &a, bool b)
	Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr	operator|| (bool a, expr const &b)
	Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr	implies (expr const &a, expr const &b)
expr	implies (expr const &a, bool b)
expr	implies (bool a, expr const &b)
expr	mk_or (expr_vector const &args)
expr	mk_xor (expr_vector const &args)
expr	mk_and (expr_vector const &args)
expr	ite (expr const &c, expr const &t, expr const &e)
	Create the if-then-else expression ite(c, t, e).
expr	distinct (expr_vector const &args)
expr	concat (expr const &a, expr const &b)
expr	concat (expr_vector const &args)
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	sum (expr_vector const &args)
expr	operator* (expr const &a, expr const &b)
expr	operator* (expr const &a, int b)
expr	operator* (int 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	rem (expr const &a, expr const &b)
expr	rem (expr const &a, int b)
expr	rem (int a, expr const &b)
expr	is_int (expr const &e)
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, 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	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	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	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	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)
	FloatingPoint fused multiply-add.
expr	fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
	Create an expression of FloatingPoint sort from three bit-vector expressions.
expr	fpa_to_sbv (expr const &t, unsigned sz)
	Conversion of a floating-point term into a signed bit-vector.
expr	fpa_to_ubv (expr const &t, unsigned sz)
	Conversion of a floating-point term into an unsigned bit-vector.
expr	sbv_to_fpa (expr const &t, sort s)
	Conversion of a signed bit-vector term into a floating-point.
expr	ubv_to_fpa (expr const &t, sort s)
	Conversion of an unsigned bit-vector term into a floating-point.
expr	fpa_to_fpa (expr const &t, sort s)
	Conversion of a floating-point term into another floating-point.
expr	round_fpa_to_closest_integer (expr const &t)
	Round a floating-point term into its closest integer.
expr	range (expr const &lo, expr const &hi)

Additional Inherited Members
Protected Attributes inherited from ast
Z3_ast	m_ast
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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.

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

Constructor & Destructor Documentation

expr() [1/2]

expr ( context & c )

inline

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

:ast(c) {}

Referenced by abs, algebraic_lower(), algebraic_upper(), arg(), at(), atleast, atmost, bit2bool(), body(), bv2int, bvadd_no_overflow, bvadd_no_underflow, bvmul_no_overflow, bvmul_no_underflow, bvneg_no_overflow, bvredand, bvredor, bvsdiv_no_overflow, bvsub_no_overflow, bvsub_no_underflow, char_from_bv(), char_to_bv(), char_to_int(), concat, concat, contains(), denominator(), distinct, ext_rotate_left(), ext_rotate_right(), extract(), extract(), fma, fp_eq, fpa_fp, fpa_to_fpa, fpa_to_sbv, fpa_to_ubv, implies, implies, implies, int2bv, is_digit(), is_int, ite, expr::iterator::iterator(), itos(), length(), loop(), loop(), max, min, mk_and, mk_from_ieee_bv(), mk_is_inf(), mk_is_nan(), mk_is_normal(), mk_is_subnormal(), mk_is_zero(), mk_or, mk_to_ieee_bv(), mk_xor, mod, mod, mod, nand, nor, nth(), numerator(), operator!, operator!=, operator!=, operator!=, operator&, operator&, operator&, operator&&, operator&&, operator&&, expr::iterator::operator*(), operator*, operator*, operator*, operator+, operator+, operator+, operator-, operator-, operator-, operator-, operator/, operator/, operator/, operator<, operator<, operator<, operator<=, operator<=, operator<=, operator==, operator==, operator==, operator>, operator>, operator>, operator>=, operator>=, operator>=, operator[](), operator[](), operator^, operator^, operator^, operator|, operator|, operator|, operator||, operator||, operator||, operator~, pbeq, pbge, pble, pw, pw, pw, range, rem, rem, rem, repeat(), replace(), rotate_left(), rotate_right(), round_fpa_to_closest_integer, sbv_to_fpa, sbvtos(), simplify(), simplify(), sqrt, stoi(), substitute(), substitute(), substitute(), sum, ubv_to_fpa, ubvtos(), unit(), update(), update_field(), and xnor.

expr() [2/2]

expr ( context & c, Z3_ast n )

inline

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

:ast(c, reinterpret_cast<Z3_ast>(n)) {}

Member Function Documentation

algebraic_i()

unsigned algebraic_i ( ) const

inline

Return i of an algebraic number (root-obj p i).

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

                                     {
            assert(is_algebraic());
            unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
            check_error();
            return i;
        }

algebraic_lower()

expr algebraic_lower ( unsigned precision ) const

inline

Retrieve lower and upper bounds for algebraic numerals based on a decimal precision

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

                                                       { 
            assert(is_algebraic());      
            Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
            check_error();
            return expr(ctx(), r);
        }

algebraic_poly()

expr_vector algebraic_poly ( ) const

inline

Return coefficients for p of an algebraic number (root-obj p i).

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

                                           {
            assert(is_algebraic());
            Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
            check_error();
            return expr_vector(ctx(), r);
        }

algebraic_upper()

expr algebraic_upper ( unsigned precision ) const

inline

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

                                                       { 
            assert(is_algebraic());      
            Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
            check_error();
            return expr(ctx(), r);
        }

arg()

expr arg ( unsigned i ) const

inline

Return the i-th argument of this application. This method assumes the expression is an application.

Precondition

is_app()

i < num_args()

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

{ Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }

Referenced by AstRef::__bool__(), args(), and expr::iterator::operator*().

args()

expr_vector args ( ) const

inline

Return a vector of all the arguments of this application. This method assumes the expression is an application.

Precondition

is_app()

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

                                 {
          expr_vector vec(ctx());
          unsigned argCnt = num_args();
          for (unsigned i = 0; i < argCnt; ++i)
            vec.push_back(arg(i));
          return vec;
        }

Referenced by concat, distinct, mk_and, mk_or, mk_xor, operator!=, operator&&, operator*, operator+, operator-, operator||, sum, and update().

as_binary()

bool as_binary ( std::string & s ) const

inline

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

{ if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }

as_double()

double as_double ( ) const

inline

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

{ double d = 0; is_numeral(d); return d; }

as_int64()

int64_t as_int64 ( ) const

inline

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

{ int64_t r = 0; is_numeral_i64(r); return r; }

as_uint64()

uint64_t as_uint64 ( ) const

inline

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

{ uint64_t r = 0; is_numeral_u64(r); return r; }

at()

expr at ( expr const & index ) const

inline

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

                                         {
            check_context(*this, index);
            Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
            check_error();
            return expr(ctx(), r);
        }

begin()

iterator begin ( )

inline

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

{ return iterator(*this, 0); }

bit2bool()

expr bit2bool ( unsigned i ) const

inline

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

{ Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

body()

expr body ( ) const

inline

Return the 'body' of this quantifier.

Precondition

is_quantifier()

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

{ assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }

bool_value()

Z3_lbool bool_value ( ) const

inline

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

                                    {
            return Z3_get_bool_value(ctx(), m_ast);
        }

char_from_bv()

expr char_from_bv ( ) const

inline

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

                                  {
            Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

char_to_bv()

expr char_to_bv ( ) const

inline

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

                                {
            Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

char_to_int()

expr char_to_int ( ) const

inline

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

                                 {
            Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

contains()

expr contains ( expr const & s ) const

inline

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

                                           {
            check_context(*this, s);
            Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
            check_error();
            return expr(ctx(), r);
        }

decl()

func_decl decl ( ) const

inline

Return the declaration associated with this application. This method assumes the expression is an application.

Precondition

is_app()

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

{ Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }

Referenced by hi(), is_and(), is_distinct(), is_eq(), is_false(), is_implies(), is_ite(), is_not(), is_or(), is_true(), is_xor(), and lo().

denominator()

expr denominator ( ) const

inline

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

                                 {
            assert(is_numeral());
            Z3_ast r = Z3_get_denominator(ctx(), m_ast);
            check_error();
            return expr(ctx(),r);
        }

end()

iterator end ( )

inline

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

{ return iterator(*this, is_app() ? num_args() : 0); }

ext_rotate_left()

expr ext_rotate_left ( expr const & n ) const

inline

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

{ Z3_ast r = Z3_mk_ext_rotate_left(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }

ext_rotate_right()

expr ext_rotate_right ( expr const & n ) const

inline

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

{ Z3_ast r = Z3_mk_ext_rotate_right(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }

extract() [1/2]

expr extract ( expr const & offset, expr const & length ) const

inline

sequence and regular expression operations.

• is overloaded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions

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

                                                                   {
            check_context(*this, offset); check_context(offset, length);
            Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
        }

extract() [2/2]

expr extract ( unsigned hi, unsigned lo ) const

inline

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

{ Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }

get_decimal_string()

std::string get_decimal_string ( int precision ) const

inline

Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.

Precondition

is_numeral() || is_algebraic()

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

                                                          {
            assert(is_numeral() || is_algebraic());
            return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
        }

get_numeral_int()

int get_numeral_int ( ) const

inline

Return int value of numeral, throw if result cannot fit in machine int.

It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_i function.

Precondition

is_numeral()

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

                                    {
            int result = 0;
            if (!is_numeral_i(result)) {
                assert(ctx().enable_exceptions());
                if (!ctx().enable_exceptions()) return 0;
                Z3_THROW(exception("numeral does not fit in machine int"));
            }
            return result;
        }

get_numeral_int64()

int64_t get_numeral_int64 ( ) const

inline

Return int64_t value of numeral, throw if result cannot fit in int64_t.

Precondition

is_numeral()

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

                                          {
            assert(is_numeral());
            int64_t result = 0;
            if (!is_numeral_i64(result)) {
                assert(ctx().enable_exceptions());
                if (!ctx().enable_exceptions()) return 0;
                Z3_THROW(exception("numeral does not fit in machine int64_t"));
            }
            return result;
        }

get_numeral_uint()

unsigned get_numeral_uint ( ) const

inline

Return uint value of numeral, throw if result cannot fit in machine uint.

It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_u function.

Precondition

is_numeral()

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

                                          {
            assert(is_numeral());
            unsigned result = 0;
            if (!is_numeral_u(result)) {
                assert(ctx().enable_exceptions());
                if (!ctx().enable_exceptions()) return 0;
                Z3_THROW(exception("numeral does not fit in machine uint"));
            }
            return result;
        }

get_numeral_uint64()

uint64_t get_numeral_uint64 ( ) const

inline

Return uint64_t value of numeral, throw if result cannot fit in uint64_t.

Precondition

is_numeral()

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

                                            {
            assert(is_numeral());
            uint64_t result = 0;
            if (!is_numeral_u64(result)) {
                assert(ctx().enable_exceptions());
                if (!ctx().enable_exceptions()) return 0;
                Z3_THROW(exception("numeral does not fit in machine uint64_t"));
            }
            return result;
        }

get_sort()

sort get_sort ( ) const

inline

Return the sort of this expression.

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

{ Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }

Referenced by z3::ashr(), z3::ashr(), concat, concat, is_arith(), is_array(), is_bool(), is_bv(), is_datatype(), is_finite_domain(), is_fpa(), is_int(), is_re(), is_real(), is_relation(), is_seq(), z3::lshr(), z3::lshr(), mod, mod, operator!=, operator!=, operator&, operator&, operator*, operator*, operator+, operator+, operator-, operator-, operator/, operator/, operator<, operator<, operator<=, operator<=, operator==, operator==, operator>, operator>, operator>=, operator>=, operator^, operator^, operator|, operator|, pw, pw, rem, rem, z3::sdiv(), z3::sdiv(), z3::select(), optimize::set_initial_value(), solver::set_initial_value(), z3::sge(), z3::sge(), z3::sgt(), z3::sgt(), z3::shl(), z3::shl(), z3::sle(), z3::sle(), z3::slt(), z3::slt(), z3::smod(), z3::smod(), z3::srem(), z3::srem(), z3::store(), z3::store(), z3::store(), z3::udiv(), z3::udiv(), z3::uge(), z3::uge(), z3::ugt(), z3::ugt(), z3::ule(), z3::ule(), z3::ult(), z3::ult(), z3::urem(), and z3::urem().

get_string()

std::string get_string ( ) const

inline

for a string value expression return an escaped string value.

Precondition

expression is for a string value.

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

                                     {            
            assert(is_string_value());
            char const* s = Z3_get_string(ctx(), m_ast);
            check_error();
            return std::string(s);
        }

get_u32string()

std::u32string get_u32string ( ) const

inline

for a string value expression return an unespaced string value.

Precondition

expression is for a string value.

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

                                           {
            assert(is_string_value());
            unsigned n = Z3_get_string_length(ctx(), m_ast);
            std::u32string s;
            s.resize(n);
            Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
            return s;
        }

hi()

unsigned hi ( ) const

inline

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

{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }

Referenced by extract(), loop(), and range.

id()

unsigned id ( ) const

inline

retrieve unique identifier for expression.

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

{ unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }

is_algebraic()

bool is_algebraic ( ) const

inline

Return true if expression is an algebraic number.

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

{ return Z3_is_algebraic_number(ctx(), m_ast); }

Referenced by algebraic_i(), algebraic_lower(), algebraic_poly(), algebraic_upper(), and get_decimal_string().

is_and()

bool is_and ( ) const

inline

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

{ return is_app() && Z3_OP_AND == decl().decl_kind(); }

is_app()

bool is_app ( ) const

inline

Return true if this expression is an application.

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

{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }

Referenced by end(), hi(), is_and(), is_const(), is_distinct(), is_eq(), is_false(), is_implies(), is_ite(), is_not(), is_or(), is_true(), is_xor(), lo(), and operator Z3_app().

is_arith()

bool is_arith ( ) const

inline

Return true if this is an integer or real expression.

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

{ return get_sort().is_arith(); }

Referenced by max, min, operator!=, operator!=, operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, operator>, and operator>=.

is_array()

bool is_array ( ) const

inline

Return true if this is a Array expression.

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

{ return get_sort().is_array(); }

Referenced by operator[]().

is_bool()

bool is_bool ( ) const

inline

Return true if this is a Boolean expression.

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

{ return get_sort().is_bool(); }

Referenced by optimize::add(), optimize::add(), optimize::add(), solver::add(), solver::add(), optimize::add_soft(), optimize::add_soft(), implies, ite, nand, nor, operator!, operator&, operator&&, operator^, operator|, operator||, and xnor.

is_bv()

bool is_bv ( ) const

inline

Return true if this is a Bit-vector expression.

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

{ return get_sort().is_bv(); }

Referenced by bvredand, bvredor, fpa_fp, max, min, mk_from_ieee_bv(), mod, operator!=, operator!=, operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, operator>, operator>=, sbv_to_fpa, and ubv_to_fpa.

is_const()

bool is_const ( ) const

inline

Return true if this expression is a constant (i.e., an application with 0 arguments).

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

{ return is_app() && num_args() == 0; }

Referenced by solver::add().

is_datatype()

bool is_datatype ( ) const

inline

Return true if this is a Datatype expression.

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

{ return get_sort().is_datatype(); }

Referenced by update_field().

is_digit()

expr is_digit ( ) const

inline

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

                              {
            Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

is_distinct()

bool is_distinct ( ) const

inline

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

{ return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }

is_eq()

bool is_eq ( ) const

inline

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

{ return is_app() && Z3_OP_EQ == decl().decl_kind(); }

is_exists()

bool is_exists ( ) const

inline

Return true if this expression is an existential quantifier.

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

{ return Z3_is_quantifier_exists(ctx(), m_ast); }

is_false()

bool is_false ( ) const

inline

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

{ return is_app() && Z3_OP_FALSE == decl().decl_kind(); }

is_finite_domain()

bool is_finite_domain ( ) const

inline

Return true if this is a Finite-domain expression.

Remarks

Finite-domain is special kind of interpreted sort: is_bool(), is_bv() and is_finite_domain() are mutually exclusive.

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

{ return get_sort().is_finite_domain(); }

is_forall()

bool is_forall ( ) const

inline

Return true if this expression is a universal quantifier.

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

{ return Z3_is_quantifier_forall(ctx(), m_ast); }

is_fpa()

bool is_fpa ( ) const

inline

Return true if this is a FloatingPoint expression. .

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

{ return get_sort().is_fpa(); }

Referenced by fma, fp_eq, fpa_to_fpa, fpa_to_sbv, fpa_to_ubv, max, min, mk_is_inf(), mk_is_nan(), mk_is_normal(), mk_is_subnormal(), mk_is_zero(), mk_to_ieee_bv(), operator!=, operator!=, z3::operator!=(), z3::operator!=(), operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, z3::operator==(), z3::operator==(), operator>, operator>=, rem, round_fpa_to_closest_integer, and sqrt.

is_implies()

bool is_implies ( ) const

inline

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

{ return is_app() && Z3_OP_IMPLIES  == decl().decl_kind(); }

is_int()

bool is_int ( ) const

inline

Return true if this is an integer expression.

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

{ return get_sort().is_int(); }

Referenced by abs.

is_ite()

bool is_ite ( ) const

inline

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

{ return is_app() && Z3_OP_ITE == decl().decl_kind(); }

is_lambda()

bool is_lambda ( ) const

inline

Return true if this expression is a lambda expression.

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

{ return Z3_is_lambda(ctx(), m_ast); }

is_not()

bool is_not ( ) const

inline

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

{ return is_app() && Z3_OP_NOT == decl().decl_kind(); }

is_numeral() [1/4]

bool is_numeral ( ) const

inline

Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings.

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

{ return kind() == Z3_NUMERAL_AST; }

Referenced by as_binary(), as_double(), denominator(), get_decimal_string(), get_numeral_int64(), get_numeral_uint(), get_numeral_uint64(), and numerator().

is_numeral() [2/4]

bool is_numeral ( double & d ) const

inline

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

{ if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }

Referenced by is_numeral().

is_numeral() [3/4]

bool is_numeral ( std::string & s ) const

inline

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

{ if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }

Referenced by is_numeral().

is_numeral() [4/4]

bool is_numeral ( std::string & s, unsigned precision ) const

inline

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

{ if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }

Referenced by is_numeral().

is_numeral_i()

bool is_numeral_i ( int & i ) const

inline

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

{ bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}

Referenced by get_numeral_int().

is_numeral_i64()

bool is_numeral_i64 ( int64_t & i ) const

inline

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

{ bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}

Referenced by as_int64(), and get_numeral_int64().

is_numeral_u()

bool is_numeral_u ( unsigned & i ) const

inline

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

{ bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}

Referenced by get_numeral_uint().

is_numeral_u64()

bool is_numeral_u64 ( uint64_t & i ) const

inline

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

{ bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}

Referenced by as_uint64(), and get_numeral_uint64().

is_or()

bool is_or ( ) const

inline

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

{ return is_app() && Z3_OP_OR  == decl().decl_kind(); }

is_quantifier()

bool is_quantifier ( ) const

inline

Return true if this expression is a quantifier.

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

{ return kind() == Z3_QUANTIFIER_AST; }

Referenced by body().

is_re()

bool is_re ( ) const

inline

Return true if this is a regular expression.

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

{ return get_sort().is_re(); }

Referenced by operator+.

is_real()

bool is_real ( ) const

inline

Return true if this is a real expression.

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

{ return get_sort().is_real(); }

Referenced by abs.

is_relation()

bool is_relation ( ) const

inline

Return true if this is a Relation expression.

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

{ return get_sort().is_relation(); }

is_seq()

bool is_seq ( ) const

inline

Return true if this is a sequence expression.

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

{ return get_sort().is_seq(); }

Referenced by operator+, and operator[]().

is_string_value()

bool is_string_value ( ) const

inline

Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string().

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

{ return Z3_is_string(ctx(), m_ast); }

Referenced by get_string(), and get_u32string().

is_true()

bool is_true ( ) const

inline

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

{ return is_app() && Z3_OP_TRUE == decl().decl_kind(); }

is_var()

bool is_var ( ) const

inline

Return true if this expression is a variable.

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

{ return kind() == Z3_VAR_AST; }

is_well_sorted()

bool is_well_sorted ( ) const

inline

Return true if this expression is well sorted (aka type correct).

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

{ bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }

is_xor()

bool is_xor ( ) const

inline

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

{ return is_app() && Z3_OP_XOR  == decl().decl_kind(); }

itos()

expr itos ( ) const

inline

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

                          {
            Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

length()

expr length ( ) const

inline

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

                            {
            Z3_ast r = Z3_mk_seq_length(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

Referenced by extract().

lo()

unsigned lo ( ) const

inline

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

{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }

Referenced by extract(), loop(), loop(), and range.

loop() [1/2]

expr loop ( unsigned lo )

inline

create a looping regular expression.

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

                               {
            Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
            check_error();
            return expr(ctx(), r);
        }

loop() [2/2]

expr loop ( unsigned lo, unsigned hi )

inline

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

                                            {
            Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
            check_error();
            return expr(ctx(), r);
        }

mk_from_ieee_bv()

expr mk_from_ieee_bv ( sort const & s ) const

inline

Convert this IEEE BV into a fpa.

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

                                                  {
            assert(is_bv());
            Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
            check_error();
            return expr(ctx(), r);
        }

mk_is_inf()

expr mk_is_inf ( ) const

inline

Return Boolean expression to test for whether an FP expression is inf.

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

                               {
            assert(is_fpa());
            Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
            check_error();
            return expr(ctx(), r);
        }

mk_is_nan()

expr mk_is_nan ( ) const

inline

Return Boolean expression to test for whether an FP expression is a NaN.

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

                               {
            assert(is_fpa());
            Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
            check_error();
            return expr(ctx(), r);
        }

mk_is_normal()

expr mk_is_normal ( ) const

inline

Return Boolean expression to test for whether an FP expression is a normal.

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

                                  {
            assert(is_fpa());
            Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
            check_error();
            return expr(ctx(), r);
        }

mk_is_subnormal()

expr mk_is_subnormal ( ) const

inline

Return Boolean expression to test for whether an FP expression is a subnormal.

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

                                     {
            assert(is_fpa());
            Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
            check_error();
            return expr(ctx(), r);
        }

mk_is_zero()

expr mk_is_zero ( ) const

inline

Return Boolean expression to test for whether an FP expression is a zero.

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

                                {
            assert(is_fpa());
            Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
            check_error();
            return expr(ctx(), r);
        }

mk_to_ieee_bv()

expr mk_to_ieee_bv ( ) const

inline

Convert this fpa into an IEEE BV.

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

                                   {
            assert(is_fpa());
            Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
            check_error();
            return expr(ctx(), r);
        }

nth()

expr nth ( expr const & index ) const

inline

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

                                          {
            check_context(*this, index);
            Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
            check_error();
            return expr(ctx(), r);
        }

Referenced by operator[]().

num_args()

unsigned num_args ( ) const

inline

Return the number of arguments in this application. This method assumes the expression is an application.

Precondition

is_app()

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

{ unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }

Referenced by AstRef::__bool__(), args(), end(), and is_const().

numerator()

expr numerator ( ) const

inline

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

                               {
            assert(is_numeral());
            Z3_ast r = Z3_get_numerator(ctx(), m_ast);
            check_error();
            return expr(ctx(),r);
        }

operator Z3_app()

operator Z3_app ( ) const

inline

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

{ assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }

operator[]() [1/2]

expr operator[] ( expr const & index ) const

inline

index operator defined on arrays and sequences.

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

                                                 {
            assert(is_array() || is_seq());
            if (is_array()) {
                return select(*this, index);
            }
            return nth(index);            
        }

operator[]() [2/2]

expr operator[] ( expr_vector const & index ) const

inline

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

                                                        {
            return select(*this, index);
        }

repeat()

expr repeat ( unsigned i ) const

inline

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

{ Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

replace()

expr replace ( expr const & src, expr const & dst ) const

inline

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

                                                             {
            check_context(*this, src); check_context(src, dst);
            Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
            check_error();
            return expr(ctx(), r);
        }

rotate_left()

expr rotate_left ( unsigned i ) const

inline

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

{ Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

rotate_right()

expr rotate_right ( unsigned i ) const

inline

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

{ Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

sbvtos()

expr sbvtos ( ) const

inline

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

                            {
            Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

simplify() [1/2]

expr simplify ( ) const

inline

Return a simplified version of this expression.

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

{ Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }

simplify() [2/2]

expr simplify ( params const & p ) const

inline

Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.

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

{ Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }

stoi()

expr stoi ( ) const

inline

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

                          {
            Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

substitute() [1/3]

expr substitute ( expr_vector const & dst )

inline

Apply substitution. Replace bound variables by expressions.

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

                                                       {
        array<Z3_ast> _dst(dst.size());
        for (unsigned i = 0; i < dst.size(); ++i) {
            _dst[i] = dst[i];
        }
        Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
        check_error();
        return expr(ctx(), r);
    }

substitute() [2/3]

expr substitute ( expr_vector const & src, expr_vector const & dst )

inline

Apply substitution. Replace src expressions by dst.

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

                                                                               {
        assert(src.size() == dst.size());
        array<Z3_ast> _src(src.size());
        array<Z3_ast> _dst(dst.size());
        for (unsigned i = 0; i < src.size(); ++i) {
            _src[i] = src[i];
            _dst[i] = dst[i];
        }
        Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
        check_error();
        return expr(ctx(), r);
    }

substitute() [3/3]

expr substitute ( func_decl_vector const & funs, expr_vector const & bodies )

inline

Apply function substitution by macro definitions.

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

                                                                                     {
        array<Z3_ast> _dst(dst.size());
        array<Z3_func_decl> _funs(funs.size());
        if (dst.size() != funs.size()) {
            Z3_THROW(exception("length of argument lists don't align"));
            return expr(ctx(), nullptr);
        }
        for (unsigned i = 0; i < dst.size(); ++i) {
            _dst[i] = dst[i];
            _funs[i] = funs[i];
        }
        Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
        check_error();
        return expr(ctx(), r);
    }

ubvtos()

expr ubvtos ( ) const

inline

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

                            {
            Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

unit()

expr unit ( ) const

inline

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

                          {
            Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
            check_error();
            return expr(ctx(), r);
        }

update()

expr update ( expr_vector const & args ) const

inline

Update the arguments of this application. Return a new expression with the same function declaration and updated arguments. The number of new arguments must match the current number of arguments.

Precondition

is_app()

args.size() == num_args()

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

                                                          {
        array<Z3_ast> _args(args.size());
        for (unsigned i = 0; i < args.size(); ++i) {
            _args[i] = args[i];
        }
        Z3_ast r = Z3_update_term(ctx(), m_ast, args.size(), _args.ptr());
        check_error();
        return expr(ctx(), r);
    }

update_field()

expr update_field ( func_decl const & field_access, expr const & new_value ) const

inline

Update a datatype field. Return a new datatype expression with the specified field updated to the new value. The remaining fields are unchanged.

Precondition

is_datatype()

Parameters

field_access	The accessor function declaration for the field to update
new_value	The new value for the field

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

                                                                                             {
        assert(is_datatype());
        Z3_ast r = Z3_datatype_update_field(ctx(), field_access, m_ast, new_value);
        check_error();
        return expr(ctx(), r);
    }

Friends And Related Symbol Documentation

abs

expr abs ( expr const & a )

friend

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

atleast

expr atleast ( expr_vector const & es, unsigned bound )

friend

Definition at line 2656 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 )

friend

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

friend

bit-vector and integer conversions.

Definition at line 2446 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 )

friend

bit-vector overflow/underflow checks

Definition at line 2452 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 )

friend

Definition at line 2455 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 )

friend

Definition at line 2470 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 )

friend

Definition at line 2473 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 )

friend

Definition at line 2467 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 )

friend

Definition at line 2194 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 )

friend

Definition at line 2188 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 )

friend

Definition at line 2464 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 )

friend

Definition at line 2458 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 )

friend

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

concat [1/2]

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

friend

Definition at line 2682 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 )

friend

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

distinct

expr distinct ( expr_vector const & args )

friend

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

fma

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

friend

FloatingPoint fused multiply-add.

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

fp_eq

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

friend

Definition at line 2227 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 )

friend

Create an expression of FloatingPoint sort from three bit-vector expressions.

Definition at line 2244 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 )

friend

Conversion of a floating-point term into another floating-point.

Definition at line 2280 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 )

friend

Conversion of a floating-point term into a signed bit-vector.

Definition at line 2252 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 )

friend

Conversion of a floating-point term into an unsigned bit-vector.

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

implies [1/3]

expr implies ( bool a, expr const & b )

friend

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

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

implies [2/3]

expr implies ( expr const & a, bool b )

friend

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

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

implies [3/3]

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

friend

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

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

int2bv

expr int2bv ( unsigned n, expr const & a )

friend

Definition at line 2447 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 )

friend

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

{ _Z3_MK_UN_(e, Z3_mk_is_int); }

ite

expr ite ( expr const & c, expr const & t, expr const & e )

friend

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

Precondition

c.is_bool()

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

max

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

friend

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

min

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

friend

Definition at line 2156 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 )

friend

Definition at line 2760 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 )

friend

Definition at line 2754 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 )

friend

Definition at line 2766 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 )

friend

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

mod [2/3]

expr mod ( expr const & a, int b )

friend

Definition at line 1854 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 )

friend

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

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

nand

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

friend

Definition at line 2153 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 )

friend

Definition at line 2154 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!

expr operator! ( expr const & a )

friend

Return an expression representing not(a).

Precondition

a.is_bool()

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

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

operator!= [1/3]

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

friend

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

operator!= [2/3]

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

friend

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

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

operator!= [3/3]

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

friend

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

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

operator& [1/3]

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

friend

Definition at line 2141 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/3]

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

friend

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

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

operator& [3/3]

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

friend

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

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

operator&& [1/3]

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

friend

Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition

b.is_bool()

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

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

operator&& [2/3]

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

friend

Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition

a.is_bool()

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

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

operator&& [3/3]

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

friend

Return an expression representing a and b.

Precondition

a.is_bool()

b.is_bool()

Definition at line 1886 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* [1/3]

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

friend

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

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

operator* [2/3]

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

friend

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

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

operator* [3/3]

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

friend

Definition at line 1985 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 )

friend

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

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

operator+ [2/3]

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

friend

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

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

operator+ [3/3]

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

friend

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

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

operator- [1/4]

expr operator- ( expr const & a )

friend

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

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

operator- [2/4]

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

friend

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

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

operator- [3/4]

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

friend

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

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

operator- [4/4]

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

friend

Definition at line 2070 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 )

friend

Definition at line 2008 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 )

friend

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

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

operator/ [3/3]

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

friend

Definition at line 2028 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 )

friend

Definition at line 2097 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< [2/3]

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

friend

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

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

operator< [3/3]

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

friend

Definition at line 2117 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 )

friend

Definition at line 2072 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<= [2/3]

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

friend

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

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

operator<= [3/3]

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

friend

Definition at line 2092 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 )

friend

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

operator== [2/3]

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

friend

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

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

operator== [3/3]

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

friend

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

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

operator> [1/3]

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

friend

Definition at line 2119 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> [2/3]

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

friend

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

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

operator> [3/3]

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

friend

Definition at line 2139 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 )

friend

Definition at line 1988 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>= [2/3]

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

friend

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

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

operator>= [3/3]

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

friend

Definition at line 2095 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 )

friend

Definition at line 2145 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 )

friend

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

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

operator^ [3/3]

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

friend

Definition at line 2147 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 )

friend

Definition at line 2149 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/3]

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

friend

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

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

operator| [3/3]

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

friend

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

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

operator|| [1/3]

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

friend

Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition

b.is_bool()

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

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

operator|| [2/3]

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

friend

Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition

a.is_bool()

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

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

operator|| [3/3]

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

friend

Return an expression representing a or b.

Precondition

a.is_bool()

b.is_bool()

Definition at line 1898 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~

expr operator~ ( expr const & a )

friend

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

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

pbeq

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

friend

Definition at line 2640 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 )

friend

Definition at line 2632 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 )

friend

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

pw [1/3]

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

friend

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

{ _Z3_MK_BIN_(a, b, Z3_mk_power);   }

pw [2/3]

expr pw ( expr const & a, int b )

friend

Definition at line 1843 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 )

friend

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

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

range

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

friend

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

rem [1/3]

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

friend

Definition at line 1862 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 )

friend

Definition at line 1869 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 )

friend

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

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

round_fpa_to_closest_integer

expr round_fpa_to_closest_integer ( expr const & t )

friend

Round a floating-point term into its closest integer.

Definition at line 2287 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 )

friend

Conversion of a signed bit-vector term into a floating-point.

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

sqrt

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

friend

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

sum

expr sum ( expr_vector const & args )

friend

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

ubv_to_fpa

expr ubv_to_fpa ( expr const & t, sort s )

friend

Conversion of an unsigned bit-vector term into a floating-point.

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

xnor

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

friend

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