Z3
Public Member Functions | Friends
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)
 
exproperator= (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 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...
 
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
 
 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
 
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 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 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
 
astoperator= (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)
 
contextctx () 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 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)
 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
contextm_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 643 of file z3++.h.

Constructor & Destructor Documentation

◆ expr() [1/3]

expr ( context c)
inline

◆ expr() [2/3]

expr ( context c,
Z3_ast  n 
)
inline

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

646 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:486

◆ expr() [3/3]

expr ( expr const &  n)
inline

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

647 :ast(n) {}
ast(context &c)
Definition: z3++.h:486

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

Referenced by AstRef::__bool__().

901 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
context & ctx() const
Definition: z3++.h:404

◆ at()

expr at ( expr const &  index) const
inline

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

1115  {
1116  check_context(*this, index);
1117  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1118  check_error();
1119  return expr(ctx(), r);
1120  }
Z3_error_code check_error() const
Definition: z3++.h:405
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index.
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

908 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:734

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

848  {
849  return Z3_get_bool_value(ctx(), m_ast);
850  }
context & ctx() const
Definition: z3++.h:404
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
Z3_ast m_ast
Definition: z3++.h:484

◆ contains()

expr contains ( expr const &  s)
inline

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

1109  {
1110  check_context(*this, s);
1111  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1112  check_error();
1113  return expr(ctx(), r);
1114  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.

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

Referenced by expr::hi(), expr::is_and(), 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().

886 { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
Z3_error_code check_error() const
Definition: z3++.h:405
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
context & ctx() const
Definition: z3++.h:404

◆ denominator()

expr denominator ( ) const
inline

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

860  {
861  assert(is_numeral());
862  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
863  check_error();
864  return expr(ctx(),r);
865  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.

◆ extract() [1/2]

expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

1080 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
unsigned lo() const
Definition: z3++.h:1081
unsigned hi() const
Definition: z3++.h:1082
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n...

◆ extract() [2/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 1094 of file z3++.h.

1094  {
1095  check_context(*this, offset); check_context(offset, length);
1096  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1097  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
expr length() const
Definition: z3++.h:1121
context & ctx() const
Definition: z3++.h:404
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )
inline

Return a RoundingMode sort.

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

872  {
873  assert(is_fpa());
874  Z3_sort s = ctx().fpa_rounding_mode();
875  check_error();
876  return sort(ctx(), s);
877  }
Z3_error_code check_error() const
Definition: z3++.h:405
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:2749
context & ctx() const
Definition: z3++.h:404
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:708

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

769  {
770  assert(is_numeral() || is_algebraic());
771  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
772  }
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:756
context & ctx() const
Definition: z3++.h:404
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
Z3_ast m_ast
Definition: z3++.h:484
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

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

784  {
785  int result = 0;
786  if (!is_numeral_i(result)) {
787  assert(ctx().enable_exceptions());
788  if (!ctx().enable_exceptions()) return 0;
789  Z3_THROW(exception("numeral does not fit in machine int"));
790  }
791  return result;
792  }
#define Z3_THROW(x)
Definition: z3++.h:96
context & ctx() const
Definition: z3++.h:404
bool is_numeral_i(int &i) const
Definition: z3++.h:718

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

820  {
821  assert(is_numeral());
822  int64_t result = 0;
823  if (!is_numeral_i64(result)) {
824  assert(ctx().enable_exceptions());
825  if (!ctx().enable_exceptions()) return 0;
826  Z3_THROW(exception("numeral does not fit in machine int64_t"));
827  }
828  return result;
829  }
#define Z3_THROW(x)
Definition: z3++.h:96
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:716
context & ctx() const
Definition: z3++.h:404
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

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

803  {
804  assert(is_numeral());
805  unsigned result = 0;
806  if (!is_numeral_u(result)) {
807  assert(ctx().enable_exceptions());
808  if (!ctx().enable_exceptions()) return 0;
809  Z3_THROW(exception("numeral does not fit in machine uint"));
810  }
811  return result;
812  }
#define Z3_THROW(x)
Definition: z3++.h:96
context & ctx() const
Definition: z3++.h:404
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:719
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

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

837  {
838  assert(is_numeral());
839  uint64_t result = 0;
840  if (!is_numeral_u64(result)) {
841  assert(ctx().enable_exceptions());
842  if (!ctx().enable_exceptions()) return 0;
843  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
844  }
845  return result;
846  }
#define Z3_THROW(x)
Definition: z3++.h:96
context & ctx() const
Definition: z3++.h:404
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:717
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

◆ get_sort()

sort get_sort ( ) const
inline

◆ hi()

unsigned hi ( ) const
inline

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

Referenced by expr::extract(), and expr::loop().

1082 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
context & ctx() const
Definition: z3++.h:404
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.

◆ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

Referenced by expr::get_decimal_string().

756 { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:404
Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
Z3_ast m_ast
Definition: z3++.h:484

◆ is_and()

bool is_and ( ) const
inline

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

976 { return is_app() && Z3_OP_AND == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

Referenced by expr::hi(), expr::is_and(), expr::is_const(), 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().

726 { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:493

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

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>=().

670 { return get_sort().is_arith(); }
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:548
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

678 { return get_sort().is_array(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:556

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

658 { return get_sort().is_bool(); }
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:536
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

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>=().

674 { return get_sort().is_bv(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:552

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

Referenced by solver::add().

730 { return is_app() && num_args() == 0; }
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:893

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

682 { return get_sort().is_datatype(); }
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:560
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_eq()

bool is_eq ( ) const
inline

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

980 { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

743 { return 0 != Z3_is_quantifier_exists(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:404
Z3_bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_ast m_ast
Definition: z3++.h:484

◆ is_false()

bool is_false ( ) const
inline

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

974 { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

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

704 { return get_sort().is_finite_domain(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:576

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

739 { return 0 != Z3_is_quantifier_forall(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:404
Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
Z3_ast m_ast
Definition: z3++.h:484

◆ is_fpa()

bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

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::rem(), and z3::sqrt().

708 { return get_sort().is_fpa(); }
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:580
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_implies()

bool is_implies ( ) const
inline

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

979 { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

Referenced by z3::abs().

662 { return get_sort().is_int(); }
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:540
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_ite()

bool is_ite ( ) const
inline

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

981 { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

747 { return 0 != Z3_is_lambda(ctx(), m_ast); }
Z3_bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484

◆ is_not()

bool is_not ( ) const
inline

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

975 { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

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

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

715 { return kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:493

◆ is_numeral() [2/4]

bool is_numeral ( std::string &  s) const
inline

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

Referenced by expr::is_numeral().

720 { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
Z3_ast m_ast
Definition: z3++.h:484
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

◆ is_numeral() [3/4]

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

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

Referenced by expr::is_numeral().

721 { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
Z3_ast m_ast
Definition: z3++.h:484
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

◆ is_numeral() [4/4]

bool is_numeral ( double &  d) const
inline

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

Referenced by expr::is_numeral().

722 { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_ast m_ast
Definition: z3++.h:484
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

◆ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

Referenced by expr::get_numeral_int().

718 { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int...
Z3_ast m_ast
Definition: z3++.h:484

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t &  i) const
inline

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

Referenced by expr::get_numeral_int64().

716 { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int...
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

Referenced by expr::get_numeral_uint().

719 { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int...
Z3_ast m_ast
Definition: z3++.h:484

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t &  i) const
inline

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

Referenced by expr::get_numeral_uint64().

717 { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:405
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int...
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484

◆ is_or()

bool is_or ( ) const
inline

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

977 { return is_app() && Z3_OP_OR == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

Referenced by expr::body().

734 { return kind() == Z3_QUANTIFIER_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:493

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

Referenced by z3::operator+().

694 { return get_sort().is_re(); }
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:572
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

Referenced by z3::abs().

666 { return get_sort().is_real(); }
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:544
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

686 { return get_sort().is_relation(); }
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:564
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

Referenced by z3::operator+().

690 { return get_sort().is_seq(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:568

◆ is_true()

bool is_true ( ) const
inline

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

973 { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

752 { return kind() == Z3_VAR_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:493

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

761 { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484
Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.

◆ is_xor()

bool is_xor ( ) const
inline

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

978 { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726

◆ itos()

expr itos ( ) const
inline

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

1131  {
1132  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1133  check_error();
1134  return expr(ctx(), r);
1135  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.

◆ length()

expr length ( ) const
inline

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

Referenced by expr::extract().

1121  {
1122  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1123  check_error();
1124  return expr(ctx(), r);
1125  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
context & ctx() const
Definition: z3++.h:404

◆ lo()

unsigned lo ( ) const
inline

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

Referenced by expr::extract(), and expr::loop().

1081 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
context & ctx() const
Definition: z3++.h:404
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.

◆ loop() [1/2]

expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1141  {
1142  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1143  check_error();
1144  return expr(ctx(), r);
1145  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
unsigned lo() const
Definition: z3++.h:1081
Z3_ast m_ast
Definition: z3++.h:484

◆ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1146  {
1147  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1148  check_error();
1149  return expr(ctx(), r);
1150  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
unsigned lo() const
Definition: z3++.h:1081
unsigned hi() const
Definition: z3++.h:1082
Z3_ast m_ast
Definition: z3++.h:484

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

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

893 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:405
context & ctx() const
Definition: z3++.h:404
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...

◆ numerator()

expr numerator ( ) const
inline

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

852  {
853  assert(is_numeral());
854  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
855  check_error();
856  return expr(ctx(),r);
857  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast m_ast
Definition: z3++.h:484
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

867 { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726
Z3_ast m_ast
Definition: z3++.h:484

◆ operator=()

expr& operator= ( expr const &  n)
inline

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

648 { return static_cast<expr&>(ast::operator=(n)); }
expr(context &c)
Definition: z3++.h:645
ast & operator=(ast const &s)
Definition: z3++.h:492

◆ repeat()

expr repeat ( unsigned  i)
inline

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

1074 { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.

◆ replace()

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

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

1098  {
1099  check_context(*this, src); check_context(src, dst);
1100  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1101  check_error();
1102  return expr(ctx(), r);
1103  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ rotate_left()

expr rotate_left ( unsigned  i)
inline

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

1072 { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.

◆ rotate_right()

expr rotate_right ( unsigned  i)
inline

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

1073 { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

1156 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:484

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

1160 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484

◆ stoi()

expr stoi ( ) const
inline

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

1126  {
1127  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1128  check_error();
1129  return expr(ctx(), r);
1130  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
context & ctx() const
Definition: z3++.h:404

◆ substitute() [1/2]

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

Apply substitution. Replace src expressions by dst.

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

3301  {
3302  assert(src.size() == dst.size());
3303  array<Z3_ast> _src(src.size());
3304  array<Z3_ast> _dst(dst.size());
3305  for (unsigned i = 0; i < src.size(); ++i) {
3306  _src[i] = src[i];
3307  _dst[i] = dst[i];
3308  }
3309  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3310  check_error();
3311  return expr(ctx(), r);
3312  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
context & ctx() const
Definition: z3++.h:404
Z3_ast m_ast
Definition: z3++.h:484

◆ substitute() [2/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

3314  {
3315  array<Z3_ast> _dst(dst.size());
3316  for (unsigned i = 0; i < dst.size(); ++i) {
3317  _dst[i] = dst[i];
3318  }
3319  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3320  check_error();
3321  return expr(ctx(), r);
3322  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_ast m_ast
Definition: z3++.h:484

◆ unit()

expr unit ( ) const
inline

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

1104  {
1105  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1106  check_error();
1107  return expr(ctx(), r);
1108  }
Z3_error_code check_error() const
Definition: z3++.h:405
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

Friends And Related Function Documentation

◆ abs

expr abs ( expr const &  a)
friend

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

1514  {
1515  Z3_ast r;
1516  if (a.is_int()) {
1517  expr zero = a.ctx().int_val(0);
1518  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1519  }
1520  else if (a.is_real()) {
1521  expr zero = a.ctx().real_val(0);
1522  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1523  }
1524  else {
1525  r = Z3_mk_fpa_abs(a.ctx(), a);
1526  }
1527  return expr(a.ctx(), r);
1528  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).

◆ atleast

expr atleast ( expr_vector const &  es,
unsigned  bound 
)
friend

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

1876  {
1877  assert(es.size() > 0);
1878  context& ctx = es[0].ctx();
1879  array<Z3_ast> _es(es);
1880  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1881  ctx.check_error();
1882  return expr(ctx, r);
1883  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ atmost

expr atmost ( expr_vector const &  es,
unsigned  bound 
)
friend

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

1868  {
1869  assert(es.size() > 0);
1870  context& ctx = es[0].ctx();
1871  array<Z3_ast> _es(es);
1872  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1873  ctx.check_error();
1874  return expr(ctx, r);
1875  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ concat [1/2]

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

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

1902  {
1903  check_context(a, b);
1904  Z3_ast r;
1905  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1906  Z3_ast _args[2] = { a, b };
1907  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1908  }
1909  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1910  Z3_ast _args[2] = { a, b };
1911  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1912  }
1913  else {
1914  r = Z3_mk_concat(a.ctx(), a, b);
1915  }
1916  a.ctx().check_error();
1917  return expr(a.ctx(), r);
1918  }
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.

◆ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

1920  {
1921  Z3_ast r;
1922  assert(args.size() > 0);
1923  if (args.size() == 1) {
1924  return args[0];
1925  }
1926  context& ctx = args[0].ctx();
1927  array<Z3_ast> _args(args);
1928  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1929  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1930  }
1931  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1932  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1933  }
1934  else {
1935  r = _args[args.size()-1];
1936  for (unsigned i = args.size()-1; i > 0; ) {
1937  --i;
1938  r = Z3_mk_concat(ctx, _args[i], r);
1939  ctx.check_error();
1940  }
1941  }
1942  ctx.check_error();
1943  return expr(ctx, r);
1944  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
context & ctx() const
Definition: z3++.h:404
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

1893  {
1894  assert(args.size() > 0);
1895  context& ctx = args[0].ctx();
1896  array<Z3_ast> _args(args);
1897  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1898  ctx.check_error();
1899  return expr(ctx, r);
1900  }
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404

◆ fma

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

FloatingPoint fused multiply-add.

◆ implies [1/3]

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

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

1181  {
1182  assert(a.is_bool() && b.is_bool());
1183  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1184  }
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1174

◆ implies [2/3]

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

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

1185 { return implies(a, a.ctx().bool_val(b)); }
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1181

◆ implies [3/3]

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

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

1186 { return implies(b.ctx().bool_val(a), b); }
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1181

◆ is_int

expr is_int ( expr const &  e)
friend

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

1217 { _Z3_MK_UN_(e, Z3_mk_is_int); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1209
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.

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

1550  {
1551  check_context(c, t); check_context(c, e);
1552  assert(c.is_bool());
1553  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1554  c.check_error();
1555  return expr(c.ctx(), r);
1556  }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).

◆ max

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

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

1499  {
1500  check_context(a, b);
1501  Z3_ast r;
1502  if (a.is_arith()) {
1503  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1504  }
1505  else if (a.is_bv()) {
1506  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1507  }
1508  else {
1509  assert(a.is_fpa());
1510  r = Z3_mk_fpa_max(a.ctx(), a, b);
1511  }
1512  return expr(a.ctx(), r);
1513  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).

◆ min

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

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

1484  {
1485  check_context(a, b);
1486  Z3_ast r;
1487  if (a.is_arith()) {
1488  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1489  }
1490  else if (a.is_bv()) {
1491  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1492  }
1493  else {
1494  assert(a.is_fpa());
1495  r = Z3_mk_fpa_min(a.ctx(), a, b);
1496  }
1497  return expr(a.ctx(), r);
1498  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

1952  {
1953  array<Z3_ast> _args(args);
1954  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1955  args.check_error();
1956  return expr(args.ctx(), r);
1957  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

◆ mk_or

expr mk_or ( expr_vector const &  args)
friend

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

1946  {
1947  array<Z3_ast> _args(args);
1948  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1949  args.check_error();
1950  return expr(args.ctx(), r);
1951  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].

◆ mod [1/3]

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

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

1193 { _Z3_MK_BIN_(a, b, Z3_mk_mod); }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1174

◆ mod [2/3]

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

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

1194 { return mod(a, a.ctx().num_val(b, a.get_sort())); }
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1193

◆ mod [3/3]

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

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

1195 { return mod(b.ctx().num_val(a, b.get_sort()), b); }
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1193

◆ nand

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

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

1481 { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ nor

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

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

1482 { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator & [1/3]

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

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

1469 { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.

◆ operator & [2/3]

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

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

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

1221  {
1222  check_context(a, b);
1223  assert(a.is_bool() && b.is_bool());
1224  Z3_ast args[2] = { a, b };
1225  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1226  a.check_error();
1227  return expr(a.ctx(), r);
1228  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

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

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

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

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

1215 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1209
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).

◆ operator!= [1/3]

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

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

1255  {
1256  check_context(a, b);
1257  Z3_ast args[2] = { a, b };
1258  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1259  a.check_error();
1260  return expr(a.ctx(), r);
1261  }
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator!= [2/3]

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

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

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

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

1295  {
1296  check_context(a, b);
1297  Z3_ast r = 0;
1298  if (a.is_arith() && b.is_arith()) {
1299  Z3_ast args[2] = { a, b };
1300  r = Z3_mk_mul(a.ctx(), 2, args);
1301  }
1302  else if (a.is_bv() && b.is_bv()) {
1303  r = Z3_mk_bvmul(a.ctx(), a, b);
1304  }
1305  else if (a.is_fpa() && b.is_fpa()) {
1306  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1307  }
1308  else {
1309  // operator is not supported by given arguments.
1310  assert(false);
1311  }
1312  a.check_error();
1313  return expr(a.ctx(), r);
1314  }
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

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

1265  {
1266  check_context(a, b);
1267  Z3_ast r = 0;
1268  if (a.is_arith() && b.is_arith()) {
1269  Z3_ast args[2] = { a, b };
1270  r = Z3_mk_add(a.ctx(), 2, args);
1271  }
1272  else if (a.is_bv() && b.is_bv()) {
1273  r = Z3_mk_bvadd(a.ctx(), a, b);
1274  }
1275  else if (a.is_seq() && b.is_seq()) {
1276  return concat(a, b);
1277  }
1278  else if (a.is_re() && b.is_re()) {
1279  Z3_ast _args[2] = { a, b };
1280  r = Z3_mk_re_union(a.ctx(), 2, _args);
1281  }
1282  else if (a.is_fpa() && b.is_fpa()) {
1283  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1284  }
1285  else {
1286  // operator is not supported by given arguments.
1287  assert(false);
1288  }
1289  a.check_error();
1290  return expr(a.ctx(), r);
1291  }
expr(context &c)
Definition: z3++.h:645
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:1902
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1358  {
1359  Z3_ast r = 0;
1360  if (a.is_arith()) {
1361  r = Z3_mk_unary_minus(a.ctx(), a);
1362  }
1363  else if (a.is_bv()) {
1364  r = Z3_mk_bvneg(a.ctx(), a);
1365  }
1366  else if (a.is_fpa()) {
1367  r = Z3_mk_fpa_neg(a.ctx(), a);
1368  }
1369  else {
1370  // operator is not supported by given arguments.
1371  assert(false);
1372  }
1373  a.check_error();
1374  return expr(a.ctx(), r);
1375  }
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;s complement unary minus.

◆ operator- [2/4]

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

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

1377  {
1378  check_context(a, b);
1379  Z3_ast r = 0;
1380  if (a.is_arith() && b.is_arith()) {
1381  Z3_ast args[2] = { a, b };
1382  r = Z3_mk_sub(a.ctx(), 2, args);
1383  }
1384  else if (a.is_bv() && b.is_bv()) {
1385  r = Z3_mk_bvsub(a.ctx(), a, b);
1386  }
1387  else if (a.is_fpa() && b.is_fpa()) {
1388  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1389  }
1390  else {
1391  // operator is not supported by given arguments.
1392  assert(false);
1393  }
1394  a.check_error();
1395  return expr(a.ctx(), r);
1396  }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

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

1336  {
1337  check_context(a, b);
1338  Z3_ast r = 0;
1339  if (a.is_arith() && b.is_arith()) {
1340  r = Z3_mk_div(a.ctx(), a, b);
1341  }
1342  else if (a.is_bv() && b.is_bv()) {
1343  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1344  }
1345  else if (a.is_fpa() && b.is_fpa()) {
1346  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1347  }
1348  else {
1349  // operator is not supported by given arguments.
1350  assert(false);
1351  }
1352  a.check_error();
1353  return expr(a.ctx(), r);
1354  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed division.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

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

1425  {
1426  check_context(a, b);
1427  Z3_ast r = 0;
1428  if (a.is_arith() && b.is_arith()) {
1429  r = Z3_mk_lt(a.ctx(), a, b);
1430  }
1431  else if (a.is_bv() && b.is_bv()) {
1432  r = Z3_mk_bvslt(a.ctx(), a, b);
1433  }
1434  else if (a.is_fpa() && b.is_fpa()) {
1435  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1436  }
1437  else {
1438  // operator is not supported by given arguments.
1439  assert(false);
1440  }
1441  a.check_error();
1442  return expr(a.ctx(), r);
1443  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

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

1400  {
1401  check_context(a, b);
1402  Z3_ast r = 0;
1403  if (a.is_arith() && b.is_arith()) {
1404  r = Z3_mk_le(a.ctx(), a, b);
1405  }
1406  else if (a.is_bv() && b.is_bv()) {
1407  r = Z3_mk_bvsle(a.ctx(), a, b);
1408  }
1409  else if (a.is_fpa() && b.is_fpa()) {
1410  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1411  }
1412  else {
1413  // operator is not supported by given arguments.
1414  assert(false);
1415  }
1416  a.check_error();
1417  return expr(a.ctx(), r);
1418  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

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

1246  {
1247  check_context(a, b);
1248  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1249  a.check_error();
1250  return expr(a.ctx(), r);
1251  }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

◆ operator== [2/3]

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

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

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

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

1447  {
1448  check_context(a, b);
1449  Z3_ast r = 0;
1450  if (a.is_arith() && b.is_arith()) {
1451  r = Z3_mk_gt(a.ctx(), a, b);
1452  }
1453  else if (a.is_bv() && b.is_bv()) {
1454  r = Z3_mk_bvsgt(a.ctx(), a, b);
1455  }
1456  else if (a.is_fpa() && b.is_fpa()) {
1457  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1458  }
1459  else {
1460  // operator is not supported by given arguments.
1461  assert(false);
1462  }
1463  a.check_error();
1464  return expr(a.ctx(), r);
1465  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

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

1319  {
1320  check_context(a, b);
1321  Z3_ast r = 0;
1322  if (a.is_arith() && b.is_arith()) {
1323  r = Z3_mk_ge(a.ctx(), a, b);
1324  }
1325  else if (a.is_bv() && b.is_bv()) {
1326  r = Z3_mk_bvsge(a.ctx(), a, b);
1327  }
1328  else {
1329  // operator is not supported by given arguments.
1330  assert(false);
1331  }
1332  a.check_error();
1333  return expr(a.ctx(), r);
1334  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

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

1473 { check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

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

1477 { check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.

◆ operator| [2/3]

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

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

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

◆ operator| [3/3]

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

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

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

1233  {
1234  check_context(a, b);
1235  assert(a.is_bool() && b.is_bool());
1236  Z3_ast args[2] = { a, b };
1237  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1238  a.check_error();
1239  return expr(a.ctx(), r);
1240  }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408

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

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

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

◆ operator~

expr operator~ ( expr const &  a)
friend

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

1535 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.

◆ pbeq

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

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

1860  {
1861  assert(es.size() > 0);
1862  context& ctx = es[0].ctx();
1863  array<Z3_ast> _es(es);
1864  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1865  ctx.check_error();
1866  return expr(ctx, r);
1867  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
context & ctx() const
Definition: z3++.h:404

◆ pbge

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

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

1852  {
1853  assert(es.size() > 0);
1854  context& ctx = es[0].ctx();
1855  array<Z3_ast> _es(es);
1856  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1857  ctx.check_error();
1858  return expr(ctx, r);
1859  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pble

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

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

1844  {
1845  assert(es.size() > 0);
1846  context& ctx = es[0].ctx();
1847  array<Z3_ast> _es(es);
1848  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1849  ctx.check_error();
1850  return expr(ctx, r);
1851  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
context & ctx() const
Definition: z3++.h:404
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pw [1/3]

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

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

1189 { _Z3_MK_BIN_(a, b, Z3_mk_power); }
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1174

◆ pw [2/3]

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

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

1190 { return pw(a, a.ctx().num_val(b, a.get_sort())); }
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1189

◆ pw [3/3]

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

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

1191 { return pw(b.ctx().num_val(a, b.get_sort()), b); }
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1189

◆ range

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

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

3244  {
3245  check_context(lo, hi);
3246  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3247  lo.check_error();
3248  return expr(lo.ctx(), r);
3249  }
expr(context &c)
Definition: z3++.h:645
unsigned lo() const
Definition: z3++.h:1081
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
unsigned hi() const
Definition: z3++.h:1082

◆ rem [1/3]

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

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

1197  {
1198  if (a.is_fpa() && b.is_fpa()) {
1199  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1200  } else {
1201  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1202  }
1203  }
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1174

◆ rem [2/3]

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

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

1204 { return rem(a, a.ctx().num_val(b, a.get_sort())); }
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1197

◆ rem [3/3]

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

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

1205 { return rem(b.ctx().num_val(a, b.get_sort()), b); }
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1197

◆ sqrt

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

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

1529  {
1530  check_context(a, rm);
1531  assert(a.is_fpa());
1532  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1533  return expr(a.ctx(), r);
1534  }
expr(context &c)
Definition: z3++.h:645
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.

◆ sum

expr sum ( expr_vector const &  args)
friend

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

1884  {
1885  assert(args.size() > 0);
1886  context& ctx = args[0].ctx();
1887  array<Z3_ast> _args(args);
1888  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
1889  ctx.check_error();
1890  return expr(ctx, r);
1891  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
context & ctx() const
Definition: z3++.h:404

◆ xnor

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

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

1483 { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:645
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408