mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

Fixing VS warning

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-10 06:52:56 -08:00
parent 1fb0fec7d1
commit 4981134fd7
1 changed files with 32 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

63
src/api/api_algebraic.cpp
View file

@ -27,15 +27,6 @@ Notes:
#include"cancel_eh.h" #include"cancel_eh.h"
#include"scoped_timer.h" #include"scoped_timer.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) { \ #define CHECK_IS_ALGEBRAIC(ARG, RET) { \
if (!Z3_algebraic_is_value_core(c, ARG)) { \ if (!Z3_algebraic_is_value_core(c, ARG)) { \
@ -51,32 +42,42 @@ extern "C" {
} \ } \
} }
static arith_util & au(Z3_context c) { static arith_util & au(Z3_context c) {
return mk_c(c)->autil(); return mk_c(c)->autil();
} }
static algebraic_numbers::manager & am(Z3_context c) { static algebraic_numbers::manager & am(Z3_context c) {
return au(c).am(); return au(c).am();
} }
static bool is_rational(Z3_context c, Z3_ast a) { static bool is_rational(Z3_context c, Z3_ast a) {
return au(c).is_numeral(to_expr(a)); return au(c).is_numeral(to_expr(a));
} }
static bool is_irrational(Z3_context c, Z3_ast a) { static bool is_irrational(Z3_context c, Z3_ast a) {
return au(c).is_irrational_algebraic_numeral(to_expr(a)); return au(c).is_irrational_algebraic_numeral(to_expr(a));
} }
static rational get_rational(Z3_context c, Z3_ast a) { static rational get_rational(Z3_context c, Z3_ast a) {
SASSERT(is_rational(c, a)); SASSERT(is_rational(c, a));
rational r; rational r;
VERIFY(au(c).is_numeral(to_expr(a), r)); VERIFY(au(c).is_numeral(to_expr(a), r));
return r; return r;
} }
static algebraic_numbers::anum const & get_irrational(Z3_context c, Z3_ast a) { static algebraic_numbers::anum const & get_irrational(Z3_context c, Z3_ast a) {
SASSERT(is_irrational(c, a)); SASSERT(is_irrational(c, a));
return au(c).to_irrational_algebraic_numeral(to_expr(a)); return au(c).to_irrational_algebraic_numeral(to_expr(a));
}
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)));
} }
Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) { Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {