mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
Fix bugs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
15ed819fbd
commit
9ede98a029
2 changed files with 129 additions and 15 deletions
|
|
@ -110,13 +110,14 @@ namespace realclosure {
|
|||
struct value {
|
||||
unsigned m_ref_count;
|
||||
bool m_rational;
|
||||
value():m_ref_count(0), m_rational(false) {}
|
||||
value(bool rat):m_ref_count(0), m_rational(rat) {}
|
||||
bool is_rational() const { return m_rational; }
|
||||
};
|
||||
|
||||
struct rational_value : public value {
|
||||
mpq m_value;
|
||||
mpbqi m_interval; // approximation as a binary rational
|
||||
rational_value():value(true) {}
|
||||
};
|
||||
|
||||
typedef ptr_array<value> polynomial;
|
||||
|
|
@ -147,7 +148,7 @@ namespace realclosure {
|
|||
polynomial_expr * num() const { return m_numerator; }
|
||||
polynomial_expr * den() const { return m_denominator; }
|
||||
|
||||
rational_function_value(polynomial_expr * num, polynomial_expr * den):m_numerator(num), m_denominator(den) {
|
||||
rational_function_value(polynomial_expr * num, polynomial_expr * den):value(false), m_numerator(num), m_denominator(den) {
|
||||
SASSERT(num != 0 || den != 0);
|
||||
}
|
||||
|
||||
|
|
@ -231,6 +232,7 @@ namespace realclosure {
|
|||
|
||||
polynomial const & p() const { return m_p; }
|
||||
signs const & s() const { return m_signs; }
|
||||
bool is_real() const { return m_real; }
|
||||
};
|
||||
|
||||
struct transcendental : public extension {
|
||||
|
|
@ -325,6 +327,7 @@ namespace realclosure {
|
|||
m_bqim(m_bqm) {
|
||||
mpq one(1);
|
||||
m_one = mk_rational(one);
|
||||
inc_ref(m_one);
|
||||
m_cancel = false;
|
||||
}
|
||||
|
||||
|
|
@ -484,7 +487,7 @@ namespace realclosure {
|
|||
return v->is_rational();
|
||||
}
|
||||
|
||||
bool is_one(value * v) {
|
||||
bool is_one(value * v) const {
|
||||
return !is_zero(v) && is_nz_rational(v) && qm().is_one(to_mpq(v));
|
||||
}
|
||||
|
||||
|
|
@ -586,6 +589,17 @@ namespace realclosure {
|
|||
return static_cast<algebraic*>(ext);
|
||||
}
|
||||
|
||||
bool is_real(extension * ext) {
|
||||
switch (ext->knd()) {
|
||||
case extension::TRANSCENDENTAL: return true;
|
||||
case extension::INFINITESIMAL: return false;
|
||||
case extension::ALGEBRAIC: return to_algebraic(ext)->is_real();
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
polynomial_expr * mk_polynomial_expr(unsigned sz, value * const * p, extension * ext, mpbqi & interval) {
|
||||
SASSERT(sz > 1);
|
||||
SASSERT(p[sz-1] != 0);
|
||||
|
|
@ -595,7 +609,7 @@ namespace realclosure {
|
|||
inc_ref_ext(ext);
|
||||
r->m_ext = ext;
|
||||
realclosure::swap(r->m_interval, interval);
|
||||
r->m_real = true;
|
||||
r->m_real = is_real(ext);
|
||||
for (unsigned i = 0; i < sz && r->m_real; i++) {
|
||||
if (!is_real(p[i]))
|
||||
r->m_real = false;
|
||||
|
|
@ -607,7 +621,7 @@ namespace realclosure {
|
|||
unsigned idx = next_infinitesimal_idx();
|
||||
infinitesimal * eps = alloc(infinitesimal, idx, n);
|
||||
m_extensions[extension::INFINITESIMAL].push_back(eps);
|
||||
value * p[2] = { one(), 0 };
|
||||
value * p[2] = { 0, one() };
|
||||
mpbq zero(0);
|
||||
mpbq tiny(1, m_eps_prec);
|
||||
mpbqi interval(zero, tiny);
|
||||
|
|
@ -711,9 +725,10 @@ namespace realclosure {
|
|||
return;
|
||||
}
|
||||
|
||||
if (!is_unique_nz_rational(a)) {
|
||||
if (is_zero(a) || !is_unique_nz_rational(a)) {
|
||||
del(a);
|
||||
a.m_value = mk_rational();
|
||||
inc_ref(a.m_value);
|
||||
}
|
||||
SASSERT(is_unique_nz_rational(a));
|
||||
qm().set(to_mpq(a), n);
|
||||
|
|
@ -725,9 +740,10 @@ namespace realclosure {
|
|||
return;
|
||||
}
|
||||
|
||||
if (!is_unique_nz_rational(a)) {
|
||||
if (is_zero(a) || !is_unique_nz_rational(a)) {
|
||||
del(a);
|
||||
a.m_value = mk_rational();
|
||||
inc_ref(a.m_value);
|
||||
}
|
||||
SASSERT(is_unique_nz_rational(a));
|
||||
qm().set(to_mpq(a), n);
|
||||
|
|
@ -739,9 +755,10 @@ namespace realclosure {
|
|||
return;
|
||||
}
|
||||
|
||||
if (!is_unique_nz_rational(a)) {
|
||||
if (is_zero(a) || !is_unique_nz_rational(a)) {
|
||||
del(a);
|
||||
a.m_value = mk_rational();
|
||||
inc_ref(a.m_value);
|
||||
}
|
||||
SASSERT(is_unique_nz_rational(a));
|
||||
qm().set(to_mpq(a), n);
|
||||
|
|
@ -1269,6 +1286,8 @@ namespace realclosure {
|
|||
SASSERT(i > 0);
|
||||
while (i > 0) {
|
||||
--i;
|
||||
if (p[i] == 0)
|
||||
continue;
|
||||
if (first)
|
||||
first = false;
|
||||
else
|
||||
|
|
@ -1276,9 +1295,11 @@ namespace realclosure {
|
|||
if (i == 0)
|
||||
display(out, p[i], compact);
|
||||
else {
|
||||
out << "(";
|
||||
display(out, p[i], compact);
|
||||
out << ")*";
|
||||
if (!is_one(p[i])) {
|
||||
out << "(";
|
||||
display(out, p[i], compact);
|
||||
out << ")*";
|
||||
}
|
||||
display_var(out, compact);
|
||||
if (i > 1)
|
||||
out << "^" << i;
|
||||
|
|
@ -1433,16 +1454,16 @@ namespace realclosure {
|
|||
m_imp->del(a);
|
||||
}
|
||||
|
||||
void manager::mk_infinitesimal(char const * p, numeral & r) {
|
||||
m_imp->mk_infinitesimal(r);
|
||||
void manager::mk_infinitesimal(char const * n, numeral & r) {
|
||||
m_imp->mk_infinitesimal(n, r);
|
||||
}
|
||||
|
||||
void manager::mk_infinitesimal(numeral & r) {
|
||||
m_imp->mk_infinitesimal(r);
|
||||
}
|
||||
|
||||
void manager::mk_transcendental(char const * p, mk_interval & proc, numeral & r) {
|
||||
m_imp->mk_transcendental(p, proc, r);
|
||||
void manager::mk_transcendental(char const * n, mk_interval & proc, numeral & r) {
|
||||
m_imp->mk_transcendental(n, proc, r);
|
||||
}
|
||||
|
||||
void manager::mk_transcendental(mk_interval & proc, numeral & r) {
|
||||
|
|
|
|||
|
|
@ -263,4 +263,97 @@ typedef rcmanager::numeral_vector rcnumeral_vector;
|
|||
typedef rcmanager::scoped_numeral scoped_rcnumeral;
|
||||
typedef rcmanager::scoped_numeral_vector scoped_rcnumeral_vector;
|
||||
|
||||
|
||||
#define RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, TYPE) \
|
||||
inline bool EXTERNAL(scoped_rcnumeral const & a, TYPE const & b) { \
|
||||
rcmanager & m = a.m(); \
|
||||
scoped_rcnumeral _b(m); \
|
||||
m.set(_b, b); \
|
||||
return m.INTERNAL(a, _b); \
|
||||
}
|
||||
|
||||
#define RCF_MK_COMPARISON(EXTERNAL, INTERNAL) \
|
||||
RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, int) \
|
||||
RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpz) \
|
||||
RCF_MK_COMPARISON_CORE(EXTERNAL, INTERNAL, mpq)
|
||||
|
||||
RCF_MK_COMPARISON(operator==, eq);
|
||||
RCF_MK_COMPARISON(operator!=, neq);
|
||||
RCF_MK_COMPARISON(operator<, lt);
|
||||
RCF_MK_COMPARISON(operator<=, le);
|
||||
RCF_MK_COMPARISON(operator>, gt);
|
||||
RCF_MK_COMPARISON(operator>=, ge);
|
||||
|
||||
#undef RCF_MK_COMPARISON
|
||||
#undef RCF_MK_COMPARISON_CORE
|
||||
|
||||
#define RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, TYPE) \
|
||||
inline scoped_rcnumeral EXTERNAL(scoped_rcnumeral const & a, TYPE const & b) { \
|
||||
rcmanager & m = a.m(); \
|
||||
scoped_rcnumeral _b(m); \
|
||||
m.set(_b, b); \
|
||||
scoped_rcnumeral r(m); \
|
||||
m.INTERNAL(a, _b, r); \
|
||||
return r; \
|
||||
}
|
||||
|
||||
#define RCF_MK_BINARY(EXTERNAL, INTERNAL) \
|
||||
RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, int) \
|
||||
RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, mpz) \
|
||||
RCF_MK_BINARY_CORE(EXTERNAL, INTERNAL, mpq)
|
||||
|
||||
RCF_MK_BINARY(operator+, add)
|
||||
RCF_MK_BINARY(operator-, sub)
|
||||
RCF_MK_BINARY(operator*, mul)
|
||||
RCF_MK_BINARY(operator/, div)
|
||||
|
||||
#undef RCF_MK_BINARY
|
||||
#undef RCF_MK_BINARY_CORE
|
||||
|
||||
inline scoped_rcnumeral root(scoped_rcnumeral const & a, unsigned k) {
|
||||
scoped_rcnumeral r(a.m());
|
||||
a.m().root(a, k, r);
|
||||
return r;
|
||||
}
|
||||
|
||||
inline scoped_rcnumeral power(scoped_rcnumeral const & a, unsigned k) {
|
||||
scoped_rcnumeral r(a.m());
|
||||
a.m().power(a, k, r);
|
||||
return r;
|
||||
}
|
||||
|
||||
inline scoped_rcnumeral operator^(scoped_rcnumeral const & a, unsigned k) {
|
||||
return power(a, k);
|
||||
}
|
||||
|
||||
inline bool is_int(scoped_rcnumeral const & a) {
|
||||
return a.m().is_int(a);
|
||||
}
|
||||
|
||||
struct sym_pp {
|
||||
rcmanager & m;
|
||||
rcnumeral const & n;
|
||||
sym_pp(rcmanager & _m, rcnumeral const & _n):m(_m), n(_n) {}
|
||||
sym_pp(scoped_rcnumeral const & _n):m(_n.m()), n(_n.get()) {}
|
||||
};
|
||||
|
||||
inline std::ostream & operator<<(std::ostream & out, sym_pp const & n) {
|
||||
n.m.display(out, n.n);
|
||||
return out;
|
||||
}
|
||||
|
||||
struct decimal_pp {
|
||||
rcmanager & m;
|
||||
rcnumeral const & n;
|
||||
unsigned prec;
|
||||
decimal_pp(rcmanager & _m, rcnumeral const & _n, unsigned p):m(_m), n(_n), prec(p) {}
|
||||
decimal_pp(scoped_rcnumeral const & _n, unsigned p):m(_n.m()), n(_n.get()), prec(p) {}
|
||||
};
|
||||
|
||||
inline std::ostream & operator<<(std::ostream & out, decimal_pp const & n) {
|
||||
n.m.display_decimal(out, n.n, n.prec);
|
||||
return out;
|
||||
}
|
||||
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue