Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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.
 
bool is_bool () const
 Return true if this is a Boolean expression.
 
bool is_int () const
 Return true if this is an integer expression.
 
bool is_real () const
 Return true if this is a real expression.
 
bool is_arith () const
 Return true if this is an integer or real expression.
 
bool is_bv () const
 Return true if this is a Bit-vector expression.
 
bool is_array () const
 Return true if this is a Array expression.
 
bool is_datatype () const
 Return true if this is a Datatype expression.
 
bool is_relation () const
 Return true if this is a Relation expression.
 
bool is_finite_domain () const
 Return true if this is a Finite-domain expression.
 
bool is_numeral () const
 Return true if this expression is a numeral.
 
bool is_app () const
 Return true if this expression is an application.
 
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments).
 
bool is_quantifier () const
 Return true if this expression is a quantifier.
 
bool is_var () const
 Return true if this expression is a variable.
 
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct).
 
 operator Z3_app () const
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application.
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application.
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application.
 
expr body () const
 Return the 'body' of this quantifier.
 
expr simplify () const
 Return a simplified version of this expression.
 
expr simplify (params const &p) const
 Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.
 
- 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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

expr operator! (expr const &a)
 Return an expression representing not(a).
 
expr operator&& (expr const &a, expr const &b)
 Return an expression representing a and b.
 
expr operator&& (expr const &a, bool b)
 Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
 
expr operator&& (bool a, expr const &b)
 Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
 
expr operator|| (expr const &a, expr const &b)
 Return an expression representing a or b.
 
expr operator|| (expr const &a, bool b)
 Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
 
expr operator|| (bool a, expr const &b)
 Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
 
expr implies (expr const &a, expr const &b)
 
expr operator== (expr const &a, expr const &b)
 
expr operator== (expr const &a, int b)
 
expr operator== (int a, expr const &b)
 
expr operator!= (expr const &a, expr const &b)
 
expr operator!= (expr const &a, int b)
 
expr operator!= (int a, expr const &b)
 
expr operator+ (expr const &a, expr const &b)
 
expr operator+ (expr const &a, int b)
 
expr operator+ (int a, expr const &b)
 
expr operator* (expr const &a, expr const &b)
 
expr operator* (expr const &a, int b)
 
expr operator* (int a, expr const &b)
 
expr pw (expr const &a, expr const &b)
 Power operator.
 
expr pw (expr const &a, int b)
 
expr pw (int a, expr const &b)
 
expr operator/ (expr const &a, expr const &b)
 
expr operator/ (expr const &a, int b)
 
expr operator/ (int a, expr const &b)
 
expr operator- (expr const &a)
 
expr operator- (expr const &a, expr const &b)
 
expr operator- (expr const &a, int b)
 
expr operator- (int a, expr const &b)
 
expr operator<= (expr const &a, expr const &b)
 
expr operator<= (expr const &a, int b)
 
expr operator<= (int a, expr const &b)
 
expr operator>= (expr const &a, expr const &b)
 
expr operator>= (expr const &a, int b)
 
expr operator>= (int a, expr const &b)
 
expr operator< (expr const &a, expr const &b)
 
expr operator< (expr const &a, int b)
 
expr operator< (int a, expr const &b)
 
expr operator> (expr const &a, expr const &b)
 
expr operator> (expr const &a, int b)
 
expr operator> (int a, expr const &b)
 
expr operator& (expr const &a, expr const &b)
 
expr operator& (expr const &a, int b)
 
expr operator& (int a, expr const &b)
 
expr operator^ (expr const &a, expr const &b)
 
expr operator^ (expr const &a, int b)
 
expr operator^ (int a, expr const &b)
 
expr operator| (expr const &a, expr const &b)
 
expr operator| (expr const &a, int b)
 
expr operator| (int a, expr const &b)
 
expr operator~ (expr const &a)
 

Additional Inherited Members

- Protected Attributes inherited from ast
Z3_ast m_ast
 

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

Constructor & Destructor Documentation

expr ( context c)
inline

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

Referenced by expr::arg(), expr::body(), and expr::simplify().

:ast(c) {}
expr ( context c,
Z3_ast  n 
)
inline

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

:ast(c, reinterpret_cast<Z3_ast>(n)) {}
expr ( expr const &  n)
inline

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

:ast(n) {}

Member Function Documentation

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

Referenced by ExprRef::children().

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

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

Referenced by QuantifierRef::children().

{ assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
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 515 of file z3++.h.

{ Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
sort get_sort ( ) const
inline
bool is_app ( ) const
inline

Return true if this expression is an application.

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

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

{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

{ return get_sort().is_arith(); }
bool is_array ( ) const
inline

Return true if this is a Array expression.

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

{ return get_sort().is_array(); }
bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

Referenced by solver::add().

{ return get_sort().is_bool(); }
bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

{ return get_sort().is_bv(); }
bool is_const ( ) const
inline

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

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

Referenced by solver::add().

{ return is_app() && num_args() == 0; }
bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

{ return get_sort().is_datatype(); }
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 479 of file z3++.h.

{ return get_sort().is_finite_domain(); }
bool is_int ( ) const
inline

Return true if this is an integer expression.

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

{ return get_sort().is_int(); }
bool is_numeral ( ) const
inline

Return true if this expression is a numeral.

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

{ return kind() == Z3_NUMERAL_AST; }
bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

Referenced by expr::body().

{ return kind() == Z3_QUANTIFIER_AST; }
bool is_real ( ) const
inline

Return true if this is a real expression.

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

{ return get_sort().is_real(); }
bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

{ return get_sort().is_relation(); }
bool is_var ( ) const
inline

Return true if this expression is a variable.

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

{ return kind() == Z3_VAR_AST; }
bool is_well_sorted ( ) const
inline

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

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

{ bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
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 522 of file z3++.h.

Referenced by ExprRef::arg(), ExprRef::children(), and expr::is_const().

{ unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
operator Z3_app ( ) const
inline

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

{ assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
expr& operator= ( expr const &  n)
inline

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

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

Return a simplified version of this expression.

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

{ Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
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 842 of file z3++.h.

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

Friends And Related Function Documentation

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

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

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

Return an expression representing not(a).

Precondition
a.is_bool()

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

{
assert(a.is_bool());
Z3_ast r = Z3_mk_not(a.ctx(), a);
a.check_error();
return expr(a.ctx(), r);
}
expr operator!= ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast args[2] = { a, b };
Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
a.check_error();
return expr(a.ctx(), r);
}
expr operator!= ( expr const &  a,
int  b 
)
friend

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

{ assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }
expr operator!= ( int  a,
expr const &  b 
)
friend

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

{ assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }
expr operator& ( expr const &  a,
expr const &  b 
)
friend

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

{ check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
expr operator& ( expr const &  a,
int  b 
)
friend

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

{ return a & a.ctx().num_val(b, a.get_sort()); }
expr operator& ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) & b; }
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 557 of file z3++.h.

{
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);
}
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 572 of file z3++.h.

{ return a && a.ctx().bool_val(b); }
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 579 of file z3++.h.

{ return b.ctx().bool_val(a) && b; }
expr operator* ( expr const &  a,
expr const &  b 
)
friend

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

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

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

{ return a * a.ctx().num_val(b, a.get_sort()); }
expr operator* ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) * b; }
expr operator+ ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r;
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 {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator+ ( expr const &  a,
int  b 
)
friend

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

{ return a + a.ctx().num_val(b, a.get_sort()); }
expr operator+ ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) + b; }
expr operator- ( expr const &  a)
friend

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

{
Z3_ast r;
if (a.is_arith()) {
r = Z3_mk_unary_minus(a.ctx(), a);
}
else if (a.is_bv()) {
r = Z3_mk_bvneg(a.ctx(), a);
}
else {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator- ( expr const &  a,
expr const &  b 
)
friend

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

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

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

{ return a - a.ctx().num_val(b, a.get_sort()); }
expr operator- ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) - a; }
expr operator/ ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_div(a.ctx(), a, b);
}
else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvsdiv(a.ctx(), a, b);
}
else {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator/ ( expr const &  a,
int  b 
)
friend

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

{ return a / a.ctx().num_val(b, a.get_sort()); }
expr operator/ ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) / b; }
expr operator< ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_lt(a.ctx(), a, b);
}
else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvslt(a.ctx(), a, b);
}
else {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator< ( expr const &  a,
int  b 
)
friend

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

{ return a < a.ctx().num_val(b, a.get_sort()); }
expr operator< ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) < a; }
expr operator<= ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_le(a.ctx(), a, b);
}
else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvsle(a.ctx(), a, b);
}
else {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator<= ( expr const &  a,
int  b 
)
friend

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

{ return a <= a.ctx().num_val(b, a.get_sort()); }
expr operator<= ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) <= a; }
expr operator== ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
expr operator== ( expr const &  a,
int  b 
)
friend

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

{ assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }
expr operator== ( int  a,
expr const &  b 
)
friend

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

{ assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }
expr operator> ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_gt(a.ctx(), a, b);
}
else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvsgt(a.ctx(), a, b);
}
else {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator> ( expr const &  a,
int  b 
)
friend

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

{ return a > a.ctx().num_val(b, a.get_sort()); }
expr operator> ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) > a; }
expr operator>= ( expr const &  a,
expr const &  b 
)
friend

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

{
Z3_ast r;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_ge(a.ctx(), a, b);
}
else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvsge(a.ctx(), a, b);
}
else {
// operator is not supported by given arguments.
assert(false);
}
a.check_error();
return expr(a.ctx(), r);
}
expr operator>= ( expr const &  a,
int  b 
)
friend

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

{ return a >= a.ctx().num_val(b, a.get_sort()); }
expr operator>= ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) >= a; }
expr operator^ ( expr const &  a,
expr const &  b 
)
friend

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

{ check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr operator^ ( expr const &  a,
int  b 
)
friend

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

{ return a ^ a.ctx().num_val(b, a.get_sort()); }
expr operator^ ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) ^ b; }
expr operator| ( expr const &  a,
expr const &  b 
)
friend

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

{ check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr operator| ( expr const &  a,
int  b 
)
friend

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

{ return a | a.ctx().num_val(b, a.get_sort()); }
expr operator| ( int  a,
expr const &  b 
)
friend

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

{ return b.ctx().num_val(a, b.get_sort()) | b; }
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 587 of file z3++.h.

{
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);
}
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 601 of file z3++.h.

{ return a || a.ctx().bool_val(b); }
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 608 of file z3++.h.

{ return b.ctx().bool_val(a) || b; }
expr operator~ ( expr const &  a)
friend

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

{ Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr pw ( expr const &  a,
expr const &  b 
)
friend

Power operator.

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

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

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

{ return pw(a, a.ctx().num_val(b, a.get_sort())); }
expr pw ( int  a,
expr const &  b 
)
friend

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

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