diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 7cfd5a345..bba2cf0c3 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -123,6 +123,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + MK_UNARY(Z3_mk_abs, mk_c(c)->get_arith_fid(), OP_ABS, SKIP); MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP); MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP); MK_UNARY(Z3_mk_is_int, mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 931167110..ecbf86b37 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1152,6 +1152,7 @@ extern "C" { case OP_REM: return Z3_OP_REM; case OP_MOD: return Z3_OP_MOD; case OP_POWER: return Z3_OP_POWER; + case OP_ABS: return Z3_OP_ABS; case OP_TO_REAL: return Z3_OP_TO_REAL; case OP_TO_INT: return Z3_OP_TO_INT; case OP_IS_INT: return Z3_OP_IS_INT; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 312acc268..fce5f15d1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1023,6 +1023,7 @@ typedef enum { Z3_OP_TO_INT, Z3_OP_IS_INT, Z3_OP_POWER, + Z3_OP_ABS, // Arrays & Sets Z3_OP_STORE = 0x300, @@ -2548,6 +2549,13 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2); + /** + \brief Take the absolute value of an integer + + def_API('Z3_mk_abs', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast arg); + /** \brief Create less than.