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

Inheritance diagram for expr:

Public Member Functions
	expr (context &c)
	expr (context &c, Z3_ast n)
	expr (expr const &n)
expr &	operator= (expr const &n)
sort	get_sort () const
	Return the sort of this expression. More...
bool	is_bool () const
	Return true if this is a Boolean expression. More...
bool	is_int () const
	Return true if this is an integer expression. More...
bool	is_real () const
	Return true if this is a real expression. More...
bool	is_arith () const
	Return true if this is an integer or real expression. More...
bool	is_bv () const
	Return true if this is a Bit-vector expression. More...
bool	is_array () const
	Return true if this is a Array expression. More...
bool	is_datatype () const
	Return true if this is a Datatype expression. More...
bool	is_relation () const
	Return true if this is a Relation expression. More...
bool	is_seq () const
	Return true if this is a sequence expression. More...
bool	is_re () const
	Return true if this is a regular expression. More...
bool	is_finite_domain () const
	Return true if this is a Finite-domain expression. More...
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. More...
bool	is_numeral_i64 (__int64 &i) const
bool	is_numeral_u64 (__uint64 &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_app () const
	Return true if this expression is an application. More...
bool	is_const () const
	Return true if this expression is a constant (i.e., an application with 0 arguments). More...
bool	is_quantifier () const
	Return true if this expression is a quantifier. More...
bool	is_var () const
	Return true if this expression is a variable. More...
bool	is_algebraic () const
	Return true if expression is an algebraic number. More...
bool	is_well_sorted () const
	Return true if this expression is well sorted (aka type correct). More...
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. More...
int	get_numeral_int () const
	Return int value of numeral, throw if result cannot fit in machine int. More...
unsigned	get_numeral_uint () const
	Return uint value of numeral, throw if result cannot fit in machine uint. More...
__int64	get_numeral_int64 () const
	Return __int64 value of numeral, throw if result cannot fit in __int64. More...
__uint64	get_numeral_uint64 () const
	Return __uint64 value of numeral, throw if result cannot fit in __uint64. More...
	operator Z3_app () const
func_decl	decl () const
	Return the declaration associated with this application. This method assumes the expression is an application. More...
unsigned	num_args () const
	Return the number of arguments in this application. This method assumes the expression is an application. More...
expr	arg (unsigned i) const
	Return the i-th argument of this application. This method assumes the expression is an application. More...
expr	body () const
	Return the 'body' of this quantifier. More...
expr	extract (unsigned hi, unsigned lo) const
unsigned	lo () const
unsigned	hi () const
expr	extract (expr const &offset, expr const &length) const
	sequence and regular expression operations. More...
expr	replace (expr const &src, expr const &dst) const
expr	unit () const
expr	contains (expr const &s)
expr	at (expr const &index) const
expr	length () const
expr	simplify () const
	Return a simplified version of this expression. More...
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. More...
expr	substitute (expr_vector const &src, expr_vector const &dst)
	Apply substitution. Replace src expressions by dst. More...
expr	substitute (expr_vector const &dst)
	Apply substitution. Replace bound variables by expressions. More...
Public Member Functions inherited from ast
	ast (context &c)
	ast (context &c, Z3_ast n)
	ast (ast const &s)
	~ast ()
	operator Z3_ast () const
	operator bool () const
ast &	operator= (ast const &s)
Z3_ast_kind	kind () const
unsigned	hash () const
Public Member Functions inherited from object
	object (context &c)
	object (object const &s)
context &	ctx () const
void	check_error () const

Friends
expr	operator! (expr const &a)
	Return an expression representing not(a). More...
expr	operator && (expr const &a, expr const &b)
	Return an expression representing a and b. More...
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. More...
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. More...
expr	operator|| (expr const &a, expr const &b)
	Return an expression representing a or b. More...
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. More...
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. More...
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_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) More...
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	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)
	Power operator. More...
expr	pw (expr const &a, int b)
expr	pw (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	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	wasoperator (expr const &a, expr const &b)
expr	operator>= (expr const &a, int b)
expr	operator>= (int a, expr const &b)
expr	operator< (expr const &a, expr const &b)
expr	operator< (expr const &a, int b)
expr	operator< (int a, expr const &b)
expr	operator> (expr const &a, expr const &b)
expr	operator> (expr const &a, int b)
expr	operator> (int a, expr const &b)
expr	operator & (expr const &a, expr const &b)
expr	operator & (expr const &a, int b)
expr	operator & (int a, expr const &b)
expr	operator^ (expr const &a, expr const &b)
expr	operator^ (expr const &a, int b)
expr	operator^ (int a, expr const &b)
expr	operator| (expr const &a, expr const &b)
expr	operator| (expr const &a, int b)
expr	operator| (int a, expr const &b)
expr	operator~ (expr const &a)

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

Constructor & Destructor Documentation

expr() [1/3]

expr ( context &  c )

inline

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

:ast(c) {}

Referenced by expr::arg(), expr::at(), expr::body(), expr::contains(), expr::extract(), expr::length(), expr::replace(), expr::simplify(), expr::substitute(), and expr::unit().

expr() [2/3]

expr ( context &  c, Z3_ast  n  )

inline

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

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

expr() [3/3]

expr ( expr const &  n )

inline

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

:ast(n) {}

Member Function Documentation

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

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

Referenced by AstRef::__bool__(), and ExprRef::children().

at()

expr at ( expr const &  index ) const

inline

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

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

body()

expr body ( ) const

inline

Return the 'body' of this quantifier.

Precondition

is_quantifier()

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

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

Referenced by QuantifierRef::children().

contains()

expr contains ( expr const &  s )

inline

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

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

Referenced by expr::hi(), FPNumRef::isInf(), FPNumRef::isNaN(), FPNumRef::isNegative(), FPNumRef::isZero(), and expr::lo().

extract() [1/2]

expr extract ( unsigned  hi, unsigned  lo  ) const

inline

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

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

extract() [2/2]

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

inline

sequence and regular expression operations.

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

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

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

Precondition

is_numeral()

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

                                    {             
            int result;
            if (!is_numeral_i(result)) {
                throw exception("numeral does not fit in machine int");
            }
            return result;
        }

get_numeral_int64()

__int64 get_numeral_int64 ( ) const

inline

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

Precondition

is_numeral()

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

                                          {
            assert(is_numeral());
            __int64 result;
            if (!is_numeral_i64(result)) {
                throw exception("numeral does not fit in machine __int64");
            }
            return result;
        }

get_numeral_uint()

unsigned get_numeral_uint ( ) const

inline

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

Precondition

is_numeral()

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

                                          {
            assert(is_numeral());
            unsigned result;
            if (!is_numeral_u(result)) {
                throw exception("numeral does not fit in machine uint");
            }
            return result;
        }

get_numeral_uint64()

__uint64 get_numeral_uint64 ( ) const

inline

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

Precondition

is_numeral()

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

                                            {
            assert(is_numeral());
            __uint64 result;
            if (!is_numeral_u64(result)) {
                throw exception("numeral does not fit in machine __uint64");
            }
            return result;
        }

get_sort()

sort get_sort ( ) const

inline

Return the sort of this expression.

Definition at line 570 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::concat(), expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), z3::lshr(), z3::operator &(), z3::operator *(), z3::operator!=(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::pw(), z3::select(), z3::shl(), ModelRef::sorts(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

hi()

unsigned hi ( ) const

inline

Definition at line 898 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 expr::extract().

is_algebraic()

bool is_algebraic ( ) const

inline

Return true if expression is an algebraic number.

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

{ return 0 != Z3_is_algebraic_number(ctx(), m_ast); }

Referenced by expr::get_decimal_string().

is_app()

bool is_app ( ) const

inline

Return true if this expression is an application.

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

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

Referenced by expr::hi(), expr::is_const(), expr::lo(), and expr::operator Z3_app().

is_arith()

bool is_arith ( ) const

inline

Return true if this is an integer or real expression.

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

{ return get_sort().is_arith(); }

Referenced by z3::operator *(), z3::operator!=(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), and z3::pw().

is_array()

bool is_array ( ) const

inline

Return true if this is a Array expression.

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

{ return get_sort().is_array(); }

is_bool()

bool is_bool ( ) const

inline

Return true if this is a Boolean expression.

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

{ return get_sort().is_bool(); }

Referenced by solver::add(), optimize::add(), z3::implies(), z3::ite(), z3::operator &&(), z3::operator!(), and z3::operator||().

is_bv()

bool is_bv ( ) const

inline

Return true if this is a Bit-vector expression.

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

{ return get_sort().is_bv(); }

Referenced by z3::operator *(), z3::operator!=(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), and z3::operator>=().

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

{ return get_sort().is_datatype(); }

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

{ return get_sort().is_finite_domain(); }

is_int()

bool is_int ( ) const

inline

Return true if this is an integer expression.

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

{ return get_sort().is_int(); }

Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().

is_numeral() [1/3]

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

{ return kind() == Z3_NUMERAL_AST; }

Referenced by expr::get_decimal_string(), expr::get_numeral_int64(), expr::get_numeral_uint(), and expr::get_numeral_uint64().

is_numeral() [2/3]

bool is_numeral ( std::string &  s ) const

inline

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

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

Referenced by expr::is_numeral().

is_numeral() [3/3]

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

inline

Definition at line 634 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 expr::is_numeral().

is_numeral_i()

bool is_numeral_i ( int &  i ) const

inline

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

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

Referenced by expr::get_numeral_int().

is_numeral_i64()

bool is_numeral_i64 ( __int64 &  i ) const

inline

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

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

Referenced by expr::get_numeral_int64().

is_numeral_u()

bool is_numeral_u ( unsigned &  i ) const

inline

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

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

Referenced by expr::get_numeral_uint().

is_numeral_u64()

bool is_numeral_u64 ( __uint64 &  i ) const

inline

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

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

Referenced by expr::get_numeral_uint64().

is_quantifier()

bool is_quantifier ( ) const

inline

Return true if this expression is a quantifier.

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

{ return kind() == Z3_QUANTIFIER_AST; }

Referenced by expr::body().

is_re()

bool is_re ( ) const

inline

Return true if this is a regular expression.

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

{ return get_sort().is_re(); }

Referenced by z3::operator+().

is_real()

bool is_real ( ) const

inline

Return true if this is a real expression.

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

{ return get_sort().is_real(); }

is_relation()

bool is_relation ( ) const

inline

Return true if this is a Relation expression.

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

{ return get_sort().is_seq(); }

Referenced by z3::operator+().

is_var()

bool is_var ( ) const

inline

Return true if this expression is a variable.

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

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

length()

expr length ( ) const

inline

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

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

Referenced by expr::extract().

lo()

unsigned lo ( ) const

inline

Definition at line 897 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 expr::extract().

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

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

Referenced by AstRef::__bool__(), ExprRef::arg(), FuncEntry::arg_value(), FuncEntry::as_list(), ExprRef::children(), expr::is_const(), and FPNumRef::isNegative().

operator Z3_app()

operator Z3_app ( ) const

inline

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

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

operator=()

expr& operator= ( expr const &  n )

inline

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

{ return static_cast<expr&>(ast::operator=(n)); }

replace()

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

inline

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

simplify() [1/2]

expr simplify ( ) const

inline

Return a simplified version of this expression.

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

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

substitute() [1/2]

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

inline

Apply substitution. Replace src expressions by dst.

Definition at line 2535 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() [2/2]

expr substitute ( expr_vector const &  dst )

inline

Apply substitution. Replace bound variables by expressions.

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

unit()

expr unit ( ) const

inline

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

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

Friends And Related Function Documentation

concat [1/2]

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

friend

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

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

distinct

expr distinct ( expr_vector const &  args )

friend

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

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

implies [1/3]

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

friend

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

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

implies [2/3]

expr implies ( expr const &  a, bool  b  )

friend

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

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

implies [3/3]

expr implies ( bool  a, expr const &  b  )

friend

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

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

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

mk_and

expr mk_and ( expr_vector const &  args )

friend

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

operator & [1/3]

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

friend

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

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

operator & [2/3]

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

friend

Definition at line 1215 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 1216 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

Return an expression representing a and b.

Precondition

a.is_bool()

b.is_bool()

Definition at line 990 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 && [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 999 of file z3++.h.

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

operator && [3/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 1000 of file z3++.h.

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

operator * [1/3]

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

friend

Definition at line 1061 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 {
            // 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 1078 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 1079 of file z3++.h.

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

operator!

expr operator! ( expr const &  a )

friend

Return an expression representing not(a).

Precondition

a.is_bool()

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

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

operator!= [1/3]

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

friend

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

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

operator!= [3/3]

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

friend

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

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

operator+ [1/3]

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

friend

Definition at line 1034 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 {
            // 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 1058 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 1059 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 1118 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 {
            // 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 1134 of file z3++.h.

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

operator- [3/4]

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

friend

Definition at line 1151 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 1152 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 1099 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 {
            // 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 1115 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 1116 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 1176 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 {
            // 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 1192 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 1193 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 1154 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 {
            // 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 1170 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 1171 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 1015 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 1021 of file z3++.h.

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

operator== [3/3]

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

friend

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

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

operator> [1/3]

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

friend

Definition at line 1195 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 {
            // 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 1211 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 1212 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 1082 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 {
            // 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 1173 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 1174 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 1218 of file z3++.h.

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

operator^ [2/3]

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

friend

Definition at line 1219 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 1220 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 1222 of file z3++.h.

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

operator| [2/3]

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

friend

Definition at line 1223 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 1224 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

Return an expression representing a or b.

Precondition

a.is_bool()

b.is_bool()

Definition at line 1002 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|| [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 1011 of file z3++.h.

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

operator|| [3/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 1013 of file z3++.h.

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

operator~

expr operator~ ( expr const &  a )

friend

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

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

pw [1/3]

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

friend

Power operator.

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

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

pw [2/3]

expr pw ( expr const &  a, int  b  )

friend

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

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

wasoperator

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

friend