add abs function to API

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · May 10, 2024 · efc8932 · efc8932
1 parent b120745
commit efc8932
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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.