mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

working on api

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-07 18:44:03 -08:00
parent c011b05b61
commit 4e2a9e7caf
1 changed files with 145 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

202
src/api/api_algebraic.cpp
View file

@ -21,78 +21,165 @@ Notes:
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
#include"algebraic_numbers.h"
extern "C" {
bool Z3_algebraic_is_value_core(Z3_context c, Z3_ast a) {
api::context * _c = mk_c(c);
return
is_expr(a) &&
(_c->autil().is_numeral(to_expr(a)) ||
_c->autil().is_irrational_algebraic_numeral(to_expr(a)));
}
#define CHECK_IS_ALGEBRAIC(ARG, RET) { \
if (!Z3_algebraic_is_value_core(c, ARG)) { \
SET_ERROR_CODE(Z3_INVALID_ARG); \
return RET; \
} \
}
#define CHECK_IS_ALGEBRAIC_X(ARG, RET) { \
if (!Z3_algebraic_is_value_core(c, ARG)) { \
SET_ERROR_CODE(Z3_INVALID_ARG); \
RETURN_Z3(RET); \
} \
}
static arith_util & au(Z3_context c) {
return mk_c(c)->autil();
}
static algebraic_numbers::manager & am(Z3_context c) {
return au(c).am();
}
static bool is_rational(Z3_context c, Z3_ast a) {
return au(c).is_numeral(to_expr(a));
}
static bool is_irrational(Z3_context c, Z3_ast a) {
return au(c).is_irrational_algebraic_numeral(to_expr(a));
}
static rational get_rational(Z3_context c, Z3_ast a) {
SASSERT(is_rational(c, a));
rational r;
VERIFY(au(c).is_numeral(to_expr(a), r));
return r;
}
static algebraic_numbers::anum const & get_irrational(Z3_context c, Z3_ast a) {
SASSERT(is_irrational(c, a));
return au(c).to_irrational_algebraic_numeral(to_expr(a));
}
Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_algebraic_is_value(c, a);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
return Z3_algebraic_is_value_core(c, a) ? Z3_TRUE : Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_algebraic_is_pos(c, a);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
return Z3_algebraic_sign(c, a) > 0;
}
Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_algebraic_is_neg(c, a);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
return Z3_algebraic_sign(c, a) < 0;
}
Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_algebraic_is_zero(c, a);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
return Z3_algebraic_sign(c, a) == 0;
}
int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_algebraic_sign(c, a);
RESET_ERROR_CODE();
// TODO
return 0;
CHECK_IS_ALGEBRAIC(a, 0);
if (is_rational(c, a)) {
rational v = get_rational(c, a);
if (v.is_pos()) return 1;
else if (v.is_neg()) return -1;
else return 0;
}
else {
algebraic_numbers::anum const & v = get_irrational(c, a);
if (am(c).is_pos(v)) return 1;
else if (am(c).is_neg(v)) return -1;
else return 0;
}
Z3_CATCH_RETURN(0);
}
#define BIN_OP(RAT_OP, IRAT_OP) \
algebraic_numbers::manager & _am = am(c); \
ast * r = 0; \
if (is_rational(c, a)) { \
rational av = get_rational(c, a); \
if (is_rational(c, b)) { \
rational bv = get_rational(c, b); \
r = au(c).mk_numeral(av RAT_OP bv, false); \
} \
else { \
algebraic_numbers::anum const & bv = get_irrational(c, b); \
scoped_anum _av(_am); \
_am.set(_av, av.to_mpq()); \
scoped_anum _r(_am); \
_am.IRAT_OP(_av, bv, _r); \
r = au(c).mk_numeral(_r, false); \
} \
} \
else { \
algebraic_numbers::anum const & av = get_irrational(c, a); \
if (is_rational(c, b)) { \
rational bv = get_rational(c, b); \
scoped_anum _bv(_am); \
_am.set(_bv, bv.to_mpq()); \
scoped_anum _r(_am); \
_am.IRAT_OP(av, _bv, _r); \
r = au(c).mk_numeral(_r, false); \
} \
else { \
algebraic_numbers::anum const & bv = get_irrational(c, b); \
scoped_anum _r(_am); \
_am.IRAT_OP(av, bv, _r); \
r = au(c).mk_numeral(_r, false); \
} \
} \
RETURN_Z3(of_ast(r));
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_add(c, a, b);
RESET_ERROR_CODE();
// TODO
return 0;
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0);
BIN_OP(+,add);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_sub(c, a, b);
RESET_ERROR_CODE();
// TODO
return 0;
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0);
BIN_OP(-,sub);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_mul(c, a, b);
RESET_ERROR_CODE();
// TODO
return 0;
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0);
BIN_OP(*,mul);
Z3_CATCH_RETURN(0);
}
@ -100,8 +187,14 @@ extern "C" {
Z3_TRY;
LOG_Z3_algebraic_div(c, a, b);
RESET_ERROR_CODE();
// TODO
return 0;
CHECK_IS_ALGEBRAIC_X(a, 0);
CHECK_IS_ALGEBRAIC_X(b, 0);
if ((is_rational(c, b) && get_rational(c, b).is_zero()) ||
(!is_rational(c, b) && am(c).is_zero(get_irrational(c, b)))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
BIN_OP(/,div);
Z3_CATCH_RETURN(0);
}
@ -109,6 +202,14 @@ extern "C" {
Z3_TRY;
LOG_Z3_algebraic_root(c, a, k);
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0);
if (k % 2 == 0) {
if ((is_rational(c, a) && get_rational(c, a).is_neg()) ||
(!is_rational(c, a) && am(c).is_neg(get_irrational(c, a)))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
}
// TODO
return 0;
Z3_CATCH_RETURN(0);
@ -118,6 +219,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_algebraic_power(c, a, k);
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC_X(a, 0);
// TODO
return 0;
Z3_CATCH_RETURN(0);
@ -127,54 +229,40 @@ extern "C" {
Z3_TRY;
LOG_Z3_algebraic_lt(c, a, b);
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC(a, 0);
CHECK_IS_ALGEBRAIC(b, 0);
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_gt(c, a, b);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
return Z3_algebraic_lt(c, b, a);
}
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_le(c, a, b);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
return !Z3_algebraic_lt(c, b, a);
}
Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_ge(c, a, b);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(0);
return !Z3_algebraic_lt(c, a, b);
}
Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_eq(c, a, b);
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC(a, 0);
CHECK_IS_ALGEBRAIC(b, 0);
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) {
Z3_TRY;
LOG_Z3_algebraic_neq(c, a, b);
RESET_ERROR_CODE();
// TODO
return Z3_FALSE;
Z3_CATCH_RETURN(0);
return !Z3_algebraic_eq(c, a, b);
}
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {