mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add abs function to API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-09 20:54:39 -07:00
parent b120745078
commit efc893263a
3 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_arith.cpp
View file

@ -123,6 +123,7 @@ extern "C" {
Z3_CATCH_RETURN(nullptr); 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_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_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); MK_UNARY(Z3_mk_is_int, mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP);

1
src/api/api_ast.cpp
View file

@ -1152,6 +1152,7 @@ extern "C" {
case OP_REM: return Z3_OP_REM; case OP_REM: return Z3_OP_REM;
case OP_MOD: return Z3_OP_MOD; case OP_MOD: return Z3_OP_MOD;
case OP_POWER: return Z3_OP_POWER; 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_REAL: return Z3_OP_TO_REAL;
case OP_TO_INT: return Z3_OP_TO_INT; case OP_TO_INT: return Z3_OP_TO_INT;
case OP_IS_INT: return Z3_OP_IS_INT; case OP_IS_INT: return Z3_OP_IS_INT;

8
src/api/z3_api.h
View file

@ -1023,6 +1023,7 @@ typedef enum {
Z3_OP_TO_INT, Z3_OP_TO_INT,
Z3_OP_IS_INT, Z3_OP_IS_INT,
Z3_OP_POWER, Z3_OP_POWER,
Z3_OP_ABS,
// Arrays & Sets // Arrays & Sets
Z3_OP_STORE = 0x300, 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); 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. \brief Create less than.