mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix #6326

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-06 23:48:05 -07:00
parent adf6e98cdf
commit 5322d4f241
2 changed files with 44 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

23
examples/c/test_capi.c
View file

@ -2946,6 +2946,28 @@ void mk_model_example() {
Z3_del_context(ctx); Z3_del_context(ctx);
} }
void divides_example()
{
Z3_context ctx;
Z3_solver s;
Z3_ast x, number;
Z3_ast c;
ctx = mk_context();
s = mk_solver(ctx);
x = mk_int_var(ctx, "x");
number = mk_int(ctx, 2);
c = Z3_mk_divides(ctx, number, x);
Z3_solver_assert(ctx, s, c);
check2(ctx, s, Z3_L_TRUE);
del_solver(ctx, s);
Z3_del_context(ctx);
}
/**@}*/ /**@}*/
/**@}*/ /**@}*/
@ -2955,6 +2977,7 @@ int main() {
#ifdef LOG_Z3_CALLS #ifdef LOG_Z3_CALLS
Z3_open_log("z3.log"); Z3_open_log("z3.log");
#endif #endif
divides_example();
display_version(); display_version();
simple_example(); simple_example();
demorgan(); demorgan();

22
src/api/api_arith.cpp
View file

@ -22,6 +22,8 @@ Revision History:
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/algebraic_numbers.h"
#include <iostream>
#define MK_ARITH_OP(NAME, OP) MK_NARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP) #define MK_ARITH_OP(NAME, OP) MK_NARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
#define MK_BINARY_ARITH_OP(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP) #define MK_BINARY_ARITH_OP(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
#define MK_ARITH_PRED(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP) #define MK_ARITH_PRED(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP)
@ -88,7 +90,25 @@ extern "C" {
MK_ARITH_PRED(Z3_mk_gt, OP_GT); MK_ARITH_PRED(Z3_mk_gt, OP_GT);
MK_ARITH_PRED(Z3_mk_le, OP_LE); MK_ARITH_PRED(Z3_mk_le, OP_LE);
MK_ARITH_PRED(Z3_mk_ge, OP_GE); MK_ARITH_PRED(Z3_mk_ge, OP_GE);
MK_ARITH_PRED(Z3_mk_divides, OP_IDIVIDES);
Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast n1, Z3_ast n2) {
Z3_TRY;
LOG_Z3_mk_divides(c, n1, n2);
RESET_ERROR_CODE();
rational val;
if (!is_expr(n1) || !mk_c(c)->autil().is_numeral(to_expr(n1), val) || !val.is_unsigned()) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);
}
parameter p(val.get_unsigned());
expr* arg = to_expr(n2);
expr* a = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_IDIVIDES, 1, &p, 1, &arg);
mk_c(c)->save_ast_trail(a);
check_sorts(c, a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(nullptr);
}
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);