From 9ede98a0291c215c485b2f6a87d1d7b9fcdba8a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Jan 2013 08:09:20 -0800 Subject: [PATCH] Fix bugs Signed-off-by: Leonardo de Moura --- src/math/realclosure/realclosure.cpp | 51 ++++++++++----- src/math/realclosure/realclosure.h | 93 ++++++++++++++++++++++++++++ 2 files changed, 129 insertions(+), 15 deletions(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index e2424b389..cdedaddff 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -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 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(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) { diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index a90951a5a..8870644b0 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -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