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_fpa () const
	Return true if this is a FloatingPoint 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_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

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_forall () const
	Return true if this expression is a universal quantifier. More...

bool	is_exists () const
	Return true if this expression is an existential quantifier. More...

bool	is_lambda () const
	Return true if this expression is a lambda expression. 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...

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

unsigned	algebraic_i () const
	Return i of an algebraic number (root-obj p i) More...

unsigned	id () const
	retrieve unique identifier for expression. 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_t	get_numeral_int64 () const
	Return `int64_t` value of numeral, throw if result cannot fit in `int64_t`. More...

uint64_t	get_numeral_uint64 () const
	Return `uint64_t` value of numeral, throw if result cannot fit in `uint64_t`. More...

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()` More...

std::string	get_escaped_string () const
	for a string value expression return an escaped or unescaped string value. More...

std::string	get_string () const

	operator Z3_app () const

sort	fpa_rounding_mode ()
	Return a RoundingMode sort. More...

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

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)

expr	rotate_right (unsigned i)

expr	repeat (unsigned i)

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	nth (expr const &index) const

expr	length () const

expr	stoi () const

expr	itos () const

expr	loop (unsigned lo)
	create a looping regular expression. More...

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

std::string	to_string () const

Public Member Functions inherited from object
	object (context &c)

	object (object const &s)

context &	ctx () const

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

expr	int2bv (unsigned n, expr const &a)

expr	bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
	bit-vector overflow/underflow checks More...

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

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

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

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

expr	bvneg_no_overflow (expr const &a)

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

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

expr	abs (expr const &a)

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

expr	operator~ (expr const &a)

expr	fma (expr const &a, expr const &b, expr const &c, expr const &rm)
	FloatingPoint fused multiply-add. More...

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

Constructor & Destructor Documentation

◆ expr() [1/3]

expr ( context & c )

inline

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

748 :ast(c) {}

Referenced by expr::algebraic_lower(), expr::algebraic_upper(), expr::arg(), expr::at(), expr::body(), expr::contains(), expr::denominator(), expr::extract(), expr::itos(), expr::length(), expr::loop(), expr::nth(), expr::numerator(), expr::repeat(), expr::replace(), expr::rotate_left(), expr::rotate_right(), expr::simplify(), expr::stoi(), expr::substitute(), and expr::unit().

◆ expr() [2/3]

expr	(	context &	c,
		Z3_ast	n
	)

inline

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

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

◆ expr() [3/3]

expr ( expr const & n )

inline

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

750 :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 909 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 882 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 899 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 889 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 1075 of file z3++.h.

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

Referenced by AstRef::__bool__().

◆ as_binary()

bool as_binary ( std::string & s ) const

inline

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

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

◆ at()

expr at ( expr const & index ) const

inline

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

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

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

◆ contains()

expr contains ( expr const & s )

inline

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

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

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

◆ denominator()

expr denominator ( ) const

inline

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

                                  {
             assert(is_numeral());
             Z3_ast r = Z3_get_denominator(ctx(), m_ast);
             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 1280 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 1266 of file z3++.h.

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

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )

inline

Return a RoundingMode sort.

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

                                  {
             assert(is_fpa());
             Z3_sort s = ctx().fpa_rounding_mode();
             check_error();
             return sort(ctx(), s);
         }

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

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

◆ get_escaped_string()

std::string get_escaped_string ( ) const

inline

for a string value expression return an escaped or unescaped string value.

Precondition: expression is for a string value.

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

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

◆ 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 931 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 967 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 950 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 984 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 756 of file z3++.h.

756 { 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_fpa(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), z3::lshr(), z3::mod(), 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::rem(), z3::select(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

◆ get_string()

std::string get_string ( ) const

inline

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

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

◆ hi()

unsigned hi ( ) const

inline

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

1268 { 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(), and expr::loop().

◆ id()

unsigned id ( ) const

inline

retrieve unique identifier for expression.

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

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

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

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

◆ is_and()

bool is_and ( ) const

inline

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

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

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

Referenced by expr::hi(), expr::is_and(), expr::is_const(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), expr::is_xor(), 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 773 of file z3++.h.

773 { return get_sort().is_arith(); }

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

◆ is_array()

bool is_array ( ) const

inline

Return true if this is a Array expression.

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

781 { return get_sort().is_array(); }

Referenced by expr::operator[]().

◆ is_bool()

bool is_bool ( ) const

inline

Return true if this is a Boolean expression.

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

761 { return get_sort().is_bool(); }

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

◆ is_bv()

bool is_bv ( ) const

inline

Return true if this is a Bit-vector expression.

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

777 { return get_sort().is_bv(); }

Referenced by z3::max(), z3::min(), z3::mod(), 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 835 of file z3++.h.

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

785 { return get_sort().is_datatype(); }

◆ is_distinct()

bool is_distinct ( ) const

inline

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

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

◆ is_eq()

bool is_eq ( ) const

inline

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

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

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

◆ is_false()

bool is_false ( ) const

inline

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

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

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

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

811 { return get_sort().is_fpa(); }

Referenced by z3::fma(), expr::fpa_rounding_mode(), z3::max(), z3::min(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::rem(), and z3::sqrt().

◆ is_implies()

bool is_implies ( ) const

inline

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

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

765 { return get_sort().is_int(); }

Referenced by z3::abs().

◆ is_ite()

bool is_ite ( ) const

inline

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

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

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

◆ is_not()

bool is_not ( ) const

inline

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

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

818 { return kind() == Z3_NUMERAL_AST; }

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

◆ is_numeral() [2/4]

bool is_numeral ( double & d ) const

inline

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

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

Referenced by expr::is_numeral().

◆ is_numeral() [3/4]

bool is_numeral ( std::string & s ) const

inline

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

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

Referenced by expr::is_numeral().

◆ is_numeral() [4/4]

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

inline

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

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

821 { bool r = 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_t & i ) const

inline

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

819 { bool r = 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 822 of file z3++.h.

822 { bool r = 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_t & i ) const

inline

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

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

Referenced by expr::get_numeral_uint64().

◆ is_or()

bool is_or ( ) const

inline

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

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

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

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

769 { return get_sort().is_real(); }

Referenced by z3::abs().

◆ is_relation()

bool is_relation ( ) const

inline

Return true if this is a Relation expression.

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

789 { return get_sort().is_relation(); }

◆ is_seq()

bool is_seq ( ) const

inline

Return true if this is a sequence expression.

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

793 { return get_sort().is_seq(); }

Referenced by z3::operator+(), and expr::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 1019 of file z3++.h.

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

Referenced by expr::get_escaped_string(), and expr::get_string().

◆ is_true()

bool is_true ( ) const

inline

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

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

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

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

◆ is_xor()

bool is_xor ( ) const

inline

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

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

◆ itos()

expr itos ( ) const

inline

Definition at line 1323 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 1313 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 1267 of file z3++.h.

1267 { 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(), and expr::loop().

◆ loop() [1/2]

expr loop ( unsigned lo )

inline

create a looping regular expression.

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

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

◆ nth()

expr nth ( expr const & index ) const

inline

Definition at line 1307 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 expr::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 1067 of file z3++.h.

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

Referenced by AstRef::__bool__(), and expr::is_const().

◆ numerator()

expr numerator ( ) const

inline

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

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

◆ operator=()

expr& operator= ( expr const & n )

inline

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

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

◆ operator[]() [1/2]

expr operator[] ( expr const & index ) const

inline

index operator defined on arrays and sequences.

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

                                                         {
             return select(*this, index);
         }

◆ repeat()

expr repeat ( unsigned i )

inline

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

1260 { 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 1284 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 )

inline

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

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

◆ rotate_right()

expr rotate_right ( unsigned i )

inline

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

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

◆ simplify() [1/2]

expr simplify ( ) const

inline

Return a simplified version of this expression.

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

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

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

◆ stoi()

expr stoi ( ) const

inline

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

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

◆ substitute() [1/2]

expr substitute ( expr_vector const & dst )

inline

Apply substitution. Replace bound variables by expressions.

Definition at line 3585 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/2]

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

inline

Apply substitution. Replace src expressions by dst.

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

◆ unit()

expr unit ( ) const

inline

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

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

Friends And Related Function Documentation

◆ abs

expr abs ( expr const & a )

friend

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

                                     { 
         Z3_ast r;
         if (a.is_int()) {
             expr zero = a.ctx().int_val(0);
             r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
         }
         else if (a.is_real()) {
             expr zero = a.ctx().real_val(0);
             r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
         }
         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 2104 of file z3++.h.

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

◆ atmost

expr atmost	(	expr_vector const &	es,
		unsigned	bound
	)

friend

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

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

◆ bv2int

expr bv2int	(	expr const &	a,
		bool	is_signed
	)

friend

bit-vector and integer conversions.

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

1905 { 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 1911 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 1914 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 1929 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 1932 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 1926 of file z3++.h.

                                                  {
         Z3_ast r = Z3_mk_bvneg_no_overflow(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 1923 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 1917 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 1920 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 2130 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 2148 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 2121 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);
     }

◆ fma

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

friend

FloatingPoint fused multiply-add.

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

◆ implies [1/3]

expr implies	(	bool	a,
		expr const &	b
	)

friend

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

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

◆ implies [2/3]

expr implies	(	expr const &	a,
		bool	b
	)

friend

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

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

◆ implies [3/3]

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

friend

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

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

1435 { _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 1778 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 1724 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); 
         }
         return expr(a.ctx(), r); 
     }

◆ min

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

friend

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

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

◆ mk_and

expr mk_and ( expr_vector const & args )

friend

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

◆ mod [1/3]

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

friend

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

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

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

◆ nand

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

friend

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

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

◆ nor

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

friend

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

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

◆ operator!

expr operator! ( expr const & a )

friend

Return an expression representing not(a).

Precondition: a.is_bool()

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

1433 { 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 1475 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 1482 of file z3++.h.

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

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

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

◆ operator& [2/3]

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

friend

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

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

◆ operator& [3/3]

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

friend

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

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

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

1448 { 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 1439 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 1517 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 1537 of file z3++.h.

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

◆ operator* [3/3]

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

friend

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

1538 { 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 1487 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 1514 of file z3++.h.

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

◆ operator+ [3/3]

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

friend

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

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

◆ operator- [1/4]

expr operator- ( expr const & a )

friend

Definition at line 1583 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 1602 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 1622 of file z3++.h.

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

◆ operator- [4/4]

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

friend

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

1623 { 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 1561 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 1580 of file z3++.h.

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

◆ operator/ [3/3]

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

friend

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

1581 { 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 1650 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 1669 of file z3++.h.

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

◆ operator< [3/3]

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

friend

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

1670 { 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 1625 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 1644 of file z3++.h.

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

◆ operator<= [3/3]

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

friend

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

1645 { 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 1464 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 1470 of file z3++.h.

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

1471 { 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 1672 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 1691 of file z3++.h.

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

◆ operator> [3/3]

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

friend

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

1692 { 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 1541 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 1647 of file z3++.h.

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

◆ operator>= [3/3]

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

friend

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

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

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

◆ operator^ [2/3]

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

friend

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

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

◆ operator^ [3/3]

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

friend

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

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

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

◆ operator| [2/3]

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

friend

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

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

◆ operator| [3/3]

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

friend

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

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

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

1460 { 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 1451 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 1762 of file z3++.h.

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

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

◆ pbge

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

friend

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

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

◆ pble

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

friend

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

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

◆ pw [1/3]

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

friend

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

1395 { _Z3_MK_BIN_(a, b, Z3_mk_power); }

◆ pw [2/3]

expr pw	(	expr const &	a,
		int	b
	)

friend

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

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

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

◆ range

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

friend

Definition at line 3515 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 1415 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 1422 of file z3++.h.

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

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

◆ sqrt

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

friend

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

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

◆ xnor

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

friend

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

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

Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ expr() [1/3]

◆ expr() [2/3]

◆ expr() [3/3]

Member Function Documentation

◆ algebraic_i()

◆ algebraic_lower()

◆ algebraic_poly()

◆ algebraic_upper()

◆ arg()

◆ as_binary()

◆ at()

◆ body()

◆ bool_value()

◆ contains()

◆ decl()

◆ denominator()

◆ extract() [1/2]

◆ extract() [2/2]

◆ fpa_rounding_mode()

◆ get_decimal_string()

◆ get_escaped_string()

◆ get_numeral_int()

◆ get_numeral_int64()

◆ get_numeral_uint()

◆ get_numeral_uint64()

◆ get_sort()

◆ get_string()

◆ hi()

◆ id()

◆ is_algebraic()

◆ is_and()

◆ is_app()

◆ is_arith()

◆ is_array()

◆ is_bool()

◆ is_bv()

◆ is_const()

◆ is_datatype()

◆ is_distinct()

◆ is_eq()

◆ is_exists()

◆ is_false()

◆ is_finite_domain()

◆ is_forall()

◆ is_fpa()

◆ is_implies()

◆ is_int()

◆ is_ite()

◆ is_lambda()

◆ is_not()

◆ is_numeral() [1/4]

◆ is_numeral() [2/4]

◆ is_numeral() [3/4]

◆ is_numeral() [4/4]

◆ is_numeral_i()

◆ is_numeral_i64()

◆ is_numeral_u()

◆ is_numeral_u64()

◆ is_or()

◆ is_quantifier()

◆ is_re()

◆ is_real()

◆ is_relation()

◆ is_seq()

◆ is_string_value()

◆ is_true()

◆ is_var()

◆ is_well_sorted()

◆ is_xor()

◆ itos()

◆ length()

◆ lo()

◆ loop() [1/2]

◆ loop() [2/2]

◆ nth()