1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_arith.cpp 7 8 Abstract: 9 API for arith theory 10 11 Author: 12 13 Leonardo de Moura (leonardo) 2012-02-29. 14 15 Revision History: 16 17 --*/ 18 #include "api/z3.h" 19 #include "api/api_log_macros.h" 20 #include "api/api_context.h" 21 #include "api/api_util.h" 22 #include "ast/arith_decl_plugin.h" 23 #include "math/polynomial/algebraic_numbers.h" 24 25 #define MK_ARITH_OP(NAME, OP) MK_NARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP) 26 #define MK_BINARY_ARITH_OP(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP) 27 #define MK_ARITH_PRED(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_arith_fid(), OP, SKIP) 28 29 extern "C" { 30 Z3_mk_int_sort(Z3_context c)31 Z3_sort Z3_API Z3_mk_int_sort(Z3_context c) { 32 Z3_TRY; 33 LOG_Z3_mk_int_sort(c); 34 RESET_ERROR_CODE(); 35 Z3_sort r = of_sort(mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), INT_SORT)); 36 RETURN_Z3(r); 37 Z3_CATCH_RETURN(nullptr); 38 } 39 Z3_mk_real_sort(Z3_context c)40 Z3_sort Z3_API Z3_mk_real_sort(Z3_context c) { 41 Z3_TRY; 42 LOG_Z3_mk_real_sort(c); 43 RESET_ERROR_CODE(); 44 Z3_sort r = of_sort(mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT)); 45 RETURN_Z3(r); 46 Z3_CATCH_RETURN(nullptr); 47 } 48 Z3_mk_real(Z3_context c,int num,int den)49 Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) { 50 Z3_TRY; 51 LOG_Z3_mk_real(c, num, den); 52 RESET_ERROR_CODE(); 53 if (den == 0) { 54 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 55 RETURN_Z3(nullptr); 56 } 57 sort* s = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); 58 ast* a = mk_c(c)->mk_numeral_core(rational(num, den), s); 59 RETURN_Z3(of_ast(a)); 60 Z3_CATCH_RETURN(nullptr); 61 } 62 63 MK_ARITH_OP(Z3_mk_add, OP_ADD); 64 MK_ARITH_OP(Z3_mk_mul, OP_MUL); 65 MK_BINARY_ARITH_OP(Z3_mk_power, OP_POWER); 66 MK_BINARY_ARITH_OP(Z3_mk_mod, OP_MOD); 67 MK_BINARY_ARITH_OP(Z3_mk_rem, OP_REM); 68 Z3_mk_div(Z3_context c,Z3_ast n1,Z3_ast n2)69 Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast n1, Z3_ast n2) { 70 Z3_TRY; 71 LOG_Z3_mk_div(c, n1, n2); 72 RESET_ERROR_CODE(); 73 decl_kind k = OP_IDIV; 74 sort* ty = mk_c(c)->m().get_sort(to_expr(n1)); 75 sort* real_ty = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); 76 if (ty == real_ty) { 77 k = OP_DIV; 78 } 79 expr * args[2] = { to_expr(n1), to_expr(n2) }; 80 ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), k, 0, nullptr, 2, args); 81 mk_c(c)->save_ast_trail(a); 82 check_sorts(c, a); 83 RETURN_Z3(of_ast(a)); 84 Z3_CATCH_RETURN(nullptr); 85 } 86 87 MK_ARITH_PRED(Z3_mk_lt, OP_LT); 88 MK_ARITH_PRED(Z3_mk_gt, OP_GT); 89 MK_ARITH_PRED(Z3_mk_le, OP_LE); 90 MK_ARITH_PRED(Z3_mk_ge, OP_GE); 91 MK_ARITH_PRED(Z3_mk_divides, OP_IDIVIDES); 92 MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP); 93 MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP); 94 MK_UNARY(Z3_mk_is_int, mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP); 95 Z3_mk_sub(Z3_context c,unsigned num_args,Z3_ast const args[])96 Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]) { 97 Z3_TRY; 98 LOG_Z3_mk_sub(c, num_args, args); 99 RESET_ERROR_CODE(); 100 if (num_args == 0) { 101 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 102 RETURN_Z3(nullptr); 103 } 104 expr* r = to_expr(args[0]); 105 for (unsigned i = 1; i < num_args; ++i) { 106 expr* args1[2] = { r, to_expr(args[i]) }; 107 r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, nullptr, 2, args1); 108 check_sorts(c, r); 109 } 110 mk_c(c)->save_ast_trail(r); 111 RETURN_Z3(of_expr(r)); 112 Z3_CATCH_RETURN(nullptr); 113 } 114 Z3_mk_unary_minus(Z3_context c,Z3_ast n)115 Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast n) { 116 Z3_TRY; 117 LOG_Z3_mk_unary_minus(c, n); 118 RESET_ERROR_CODE(); 119 MK_UNARY_BODY(Z3_mk_unary_minus, mk_c(c)->get_arith_fid(), OP_UMINUS, SKIP); 120 Z3_CATCH_RETURN(nullptr); 121 } 122 Z3_is_algebraic_number(Z3_context c,Z3_ast a)123 bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { 124 LOG_Z3_is_algebraic_number(c, a); 125 return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)); 126 } 127 Z3_get_algebraic_number_lower(Z3_context c,Z3_ast a,unsigned precision)128 Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { 129 Z3_TRY; 130 LOG_Z3_get_algebraic_number_lower(c, a, precision); 131 RESET_ERROR_CODE(); 132 if (!Z3_is_algebraic_number(c, a)) { 133 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 134 RETURN_Z3(nullptr); 135 } 136 expr * e = to_expr(a); 137 algebraic_numbers::anum const & val = mk_c(c)->autil().to_irrational_algebraic_numeral(e); 138 rational l; 139 mk_c(c)->autil().am().get_lower(val, l, precision); 140 expr * r = mk_c(c)->autil().mk_numeral(l, false); 141 mk_c(c)->save_ast_trail(r); 142 RETURN_Z3(of_expr(r)); 143 Z3_CATCH_RETURN(nullptr); 144 } 145 Z3_get_algebraic_number_upper(Z3_context c,Z3_ast a,unsigned precision)146 Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision) { 147 Z3_TRY; 148 LOG_Z3_get_algebraic_number_upper(c, a, precision); 149 RESET_ERROR_CODE(); 150 if (!Z3_is_algebraic_number(c, a)) { 151 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 152 RETURN_Z3(nullptr); 153 } 154 expr * e = to_expr(a); 155 algebraic_numbers::anum const & val = mk_c(c)->autil().to_irrational_algebraic_numeral(e); 156 rational l; 157 mk_c(c)->autil().am().get_upper(val, l, precision); 158 expr * r = mk_c(c)->autil().mk_numeral(l, false); 159 mk_c(c)->save_ast_trail(r); 160 RETURN_Z3(of_expr(r)); 161 Z3_CATCH_RETURN(nullptr); 162 } 163 Z3_get_numerator(Z3_context c,Z3_ast a)164 Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a) { 165 Z3_TRY; 166 LOG_Z3_get_numerator(c, a); 167 RESET_ERROR_CODE(); 168 rational val; 169 ast * _a = to_ast(a); 170 if (!is_expr(_a) || !mk_c(c)->autil().is_numeral(to_expr(_a), val)) { 171 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 172 RETURN_Z3(nullptr); 173 } 174 expr * r = mk_c(c)->autil().mk_numeral(numerator(val), true); 175 mk_c(c)->save_ast_trail(r); 176 RETURN_Z3(of_expr(r)); 177 Z3_CATCH_RETURN(nullptr); 178 } 179 Z3_get_denominator(Z3_context c,Z3_ast a)180 Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a) { 181 Z3_TRY; 182 LOG_Z3_get_denominator(c, a); 183 RESET_ERROR_CODE(); 184 rational val; 185 ast * _a = to_ast(a); 186 if (!is_expr(_a) || !mk_c(c)->autil().is_numeral(to_expr(_a), val)) { 187 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 188 RETURN_Z3(nullptr); 189 } 190 expr * r = mk_c(c)->autil().mk_numeral(denominator(val), true); 191 mk_c(c)->save_ast_trail(r); 192 RETURN_Z3(of_expr(r)); 193 Z3_CATCH_RETURN(nullptr); 194 } 195 196 }; 197