From 77f58269edcdc4ebe0041483601bbd1e843ae38a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Jan 2013 10:19:54 -0800 Subject: [PATCH] Add html pretty printing mode for RCF package Signed-off-by: Leonardo de Moura --- src/api/api_rcf.cpp | 12 +- src/api/python/z3rcf.py | 9 +- src/api/z3_rcf.h | 8 +- src/math/interval/interval.h | 1 + src/math/interval/interval_def.h | 9 ++ src/math/realclosure/realclosure.cpp | 193 ++++++++++++++++----------- src/math/realclosure/realclosure.h | 6 +- src/util/ext_numeral.h | 12 ++ 8 files changed, 156 insertions(+), 94 deletions(-) diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index b325c4397..42558ba9e 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -98,13 +98,13 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c, Z3_string name) { + Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c) { Z3_TRY; - LOG_Z3_rcf_mk_infinitesimal(c, name); + LOG_Z3_rcf_mk_infinitesimal(c); RESET_ERROR_CODE(); reset_rcf_cancel(c); rcnumeral r; - rcfm(c).mk_infinitesimal(name, r); + rcfm(c).mk_infinitesimal(r); RETURN_Z3(from_rcnumeral(r)); Z3_CATCH_RETURN(0); } @@ -268,13 +268,13 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } - Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact) { + Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact, Z3_bool html) { Z3_TRY; - LOG_Z3_rcf_num_to_string(c, a, compact); + LOG_Z3_rcf_num_to_string(c, a, compact, html); RESET_ERROR_CODE(); reset_rcf_cancel(c); std::ostringstream buffer; - rcfm(c).display(buffer, to_rcnumeral(a), compact != 0); + rcfm(c).display(buffer, to_rcnumeral(a), compact != 0, html != 0); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/python/z3rcf.py b/src/api/python/z3rcf.py index b9c947b9f..66a6890c3 100644 --- a/src/api/python/z3rcf.py +++ b/src/api/python/z3rcf.py @@ -29,8 +29,10 @@ def E(ctx=None): return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx) def MkInfinitesimal(name="eps", ctx=None): + # Todo: remove parameter name. + # For now, we keep it for backward compatibility. ctx = z3._get_ctx(ctx) - return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref(), name), ctx) + return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref()), ctx) def MkRoots(p, ctx=None): ctx = z3._get_ctx(ctx) @@ -49,6 +51,7 @@ def MkRoots(p, ctx=None): return r class RCFNum: + html = False def __init__(self, num, ctx=None): # TODO: add support for converting AST numeral values into RCFNum if isinstance(num, RCFNumObj): @@ -65,10 +68,10 @@ class RCFNum: return self.ctx.ref() def __repr__(self): - return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False) + return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False, RCFNum.html) def compact_str(self): - return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True) + return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True, RCFNum.html) def __add__(self, other): v = _to_rcfnum(other, self.ctx) diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h index 305033690..e2b4b7e05 100644 --- a/src/api/z3_rcf.h +++ b/src/api/z3_rcf.h @@ -64,9 +64,9 @@ extern "C" { /** \brief Return a new infinitesimal that is smaller than all elements in the Z3 field. - def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT), _in(STRING))) + def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT),)) */ - Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c, __in Z3_string name); + Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c); /** \brief Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. @@ -173,9 +173,9 @@ extern "C" { /** \brief Convert the RCF numeral into a string. - def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL))) + def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL))) */ - Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact); + Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html); /** \brief Convert the RCF numeral into a string in decimal notation. diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h index 1fe797861..ed7654f01 100644 --- a/src/math/interval/interval.h +++ b/src/math/interval/interval.h @@ -231,6 +231,7 @@ public: bool contains(interval const & n, numeral const & v) const; void display(std::ostream & out, interval const & n) const; + void display_pp(std::ostream & out, interval const & n) const; bool check_invariant(interval const & n) const; diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h index 51c1652d7..89d699f1f 100644 --- a/src/math/interval/interval_def.h +++ b/src/math/interval/interval_def.h @@ -643,6 +643,15 @@ void interval_manager::display(std::ostream & out, interval const & n) const out << (upper_is_open(n) ? ")" : "]"); } +template +void interval_manager::display_pp(std::ostream & out, interval const & n) const { + out << (lower_is_open(n) ? "(" : "["); + ::display_pp(out, m(), lower(n), lower_kind(n)); + out << ", "; + ::display_pp(out, m(), upper(n), upper_kind(n)); + out << (upper_is_open(n) ? ")" : "]"); +} + template bool interval_manager::check_invariant(interval const & n) const { if (::eq(m(), lower(n), lower_kind(n), upper(n), upper_kind(n))) { diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index dac4c8e09..8c6a1d232 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -298,26 +298,41 @@ namespace realclosure { struct transcendental : public extension { symbol m_name; + symbol m_pp_name; unsigned m_k; mk_interval & m_proc; - transcendental(unsigned idx, symbol const & n, mk_interval & p):extension(TRANSCENDENTAL, idx), m_name(n), m_k(0), m_proc(p) {} + transcendental(unsigned idx, symbol const & n, symbol const & pp_n, mk_interval & p): + extension(TRANSCENDENTAL, idx), m_name(n), m_pp_name(pp_n), m_k(0), m_proc(p) {} - void display(std::ostream & out) const { - out << m_name; + void display(std::ostream & out, bool pp = false) const { + if (pp) + out << m_pp_name; + else + out << m_name; } }; struct infinitesimal : public extension { symbol m_name; + symbol m_pp_name; - infinitesimal(unsigned idx, symbol const & n):extension(INFINITESIMAL, idx), m_name(n) {} + infinitesimal(unsigned idx, symbol const & n, symbol const & pp_n):extension(INFINITESIMAL, idx), m_name(n), m_pp_name(pp_n) {} - void display(std::ostream & out) const { - if (m_name.is_numerical()) - out << "eps!" << m_name.get_num(); - else - out << m_name; + void display(std::ostream & out, bool pp = false) const { + if (pp) { + if (m_pp_name.is_numerical()) + out << "ε" << m_pp_name.get_num() << ""; + else + out << m_pp_name; + + } + else { + if (m_name.is_numerical()) + out << "eps!" << m_name.get_num(); + else + out << m_name; + } } }; @@ -1266,9 +1281,9 @@ namespace realclosure { /** \brief Create a new infinitesimal. */ - void mk_infinitesimal(symbol const & n, numeral & r) { + void mk_infinitesimal(symbol const & n, symbol const & pp_n, numeral & r) { unsigned idx = next_infinitesimal_idx(); - infinitesimal * eps = alloc(infinitesimal, idx, n); + infinitesimal * eps = alloc(infinitesimal, idx, n, pp_n); m_extensions[extension::INFINITESIMAL].push_back(eps); set_lower(eps->interval(), mpbq(0)); @@ -1280,12 +1295,12 @@ namespace realclosure { SASSERT(depends_on_infinitesimals(r)); } - void mk_infinitesimal(char const * n, numeral & r) { - mk_infinitesimal(symbol(n), r); + void mk_infinitesimal(char const * n, char const * pp_n, numeral & r) { + mk_infinitesimal(symbol(n), symbol(pp_n), r); } void mk_infinitesimal(numeral & r) { - mk_infinitesimal(symbol(next_infinitesimal_idx()), r); + mk_infinitesimal(symbol(next_infinitesimal_idx()), symbol(next_infinitesimal_idx()), r); } void refine_transcendental_interval(transcendental * t) { @@ -1318,9 +1333,9 @@ namespace realclosure { } } - void mk_transcendental(symbol const & n, mk_interval & proc, numeral & r) { + void mk_transcendental(symbol const & n, symbol const & pp_n, mk_interval & proc, numeral & r) { unsigned idx = next_transcendental_idx(); - transcendental * t = alloc(transcendental, idx, n, proc); + transcendental * t = alloc(transcendental, idx, n, pp_n, proc); m_extensions[extension::TRANSCENDENTAL].push_back(t); while (contains_zero(t->interval())) { @@ -1332,12 +1347,12 @@ namespace realclosure { SASSERT(!depends_on_infinitesimals(r)); } - void mk_transcendental(char const * p, mk_interval & proc, numeral & r) { - mk_transcendental(symbol(p), proc, r); + void mk_transcendental(char const * p, char const * pp_n, mk_interval & proc, numeral & r) { + mk_transcendental(symbol(p), symbol(pp_n), proc, r); } void mk_transcendental(mk_interval & proc, numeral & r) { - mk_transcendental(symbol(next_transcendental_idx()), proc, r); + mk_transcendental(symbol(next_transcendental_idx()), symbol(next_transcendental_idx()), proc, r); } void mk_pi(numeral & r) { @@ -1345,7 +1360,7 @@ namespace realclosure { set(r, m_pi); } else { - mk_transcendental(symbol("pi"), m_mk_pi_interval, r); + mk_transcendental(symbol("pi"), symbol("π"), m_mk_pi_interval, r); m_pi = r.m_value; inc_ref(m_pi); } @@ -1356,7 +1371,7 @@ namespace realclosure { set(r, m_e); } else { - mk_transcendental(symbol("e"), m_mk_e_interval, r); + mk_transcendental(symbol("e"), symbol("e"), m_mk_e_interval, r); m_e = r.m_value; inc_ref(m_e); } @@ -5762,7 +5777,7 @@ namespace realclosure { } template - void display_polynomial(std::ostream & out, unsigned sz, value * const * p, DisplayVar const & display_var, bool compact) const { + void display_polynomial(std::ostream & out, unsigned sz, value * const * p, DisplayVar const & display_var, bool compact, bool pp) const { if (sz == 0) { out << "0"; return; @@ -5778,33 +5793,44 @@ namespace realclosure { else out << " + "; if (i == 0) - display(out, p[i], compact); + display(out, p[i], compact, pp); else { if (!is_rational_one(p[i])) { if (use_parenthesis(p[i])) { out << "("; - display(out, p[i], compact); - out << ")*"; + display(out, p[i], compact, pp); + out << ")"; + if (pp) + out << " "; + else + out << "*"; } else { - display(out, p[i], compact); - out << "*"; + display(out, p[i], compact, pp); + if (pp) + out << " "; + else + out << "*"; } } - display_var(out, compact); - if (i > 1) - out << "^" << i; + display_var(out, compact, pp); + if (i > 1) { + if (pp) + out << "" << i << ""; + else + out << "^" << i; + } } } } template - void display_polynomial(std::ostream & out, polynomial const & p, DisplayVar const & display_var, bool compact) const { - display_polynomial(out, p.size(), p.c_ptr(), display_var, compact); + void display_polynomial(std::ostream & out, polynomial const & p, DisplayVar const & display_var, bool compact, bool pp) const { + display_polynomial(out, p.size(), p.c_ptr(), display_var, compact, pp); } struct display_free_var_proc { - void operator()(std::ostream & out, bool compact) const { + void operator()(std::ostream & out, bool compact, bool pp) const { out << "x"; } }; @@ -5813,13 +5839,13 @@ namespace realclosure { imp const & m; extension * m_ref; display_ext_proc(imp const & _m, extension * r):m(_m), m_ref(r) {} - void operator()(std::ostream & out, bool compact) const { - m.display_ext(out, m_ref, compact); + void operator()(std::ostream & out, bool compact, bool pp) const { + m.display_ext(out, m_ref, compact, pp); } }; - void display_polynomial_expr(std::ostream & out, polynomial const & p, extension * ext, bool compact) const { - display_polynomial(out, p, display_ext_proc(*this, ext), compact); + void display_polynomial_expr(std::ostream & out, polynomial const & p, extension * ext, bool compact, bool pp) const { + display_polynomial(out, p, display_ext_proc(*this, ext), compact, pp); } static void display_poly_sign(std::ostream & out, int s) { @@ -5846,7 +5872,7 @@ namespace realclosure { out << "}"; } - void display_sign_conditions(std::ostream & out, sign_condition * sc, array const & qs, bool compact) const { + void display_sign_conditions(std::ostream & out, sign_condition * sc, array const & qs, bool compact, bool pp) const { bool first = true; out << "{"; while (sc) { @@ -5854,21 +5880,28 @@ namespace realclosure { first = false; else out << ", "; - display_polynomial(out, qs[sc->qidx()], display_free_var_proc(), compact); + display_polynomial(out, qs[sc->qidx()], display_free_var_proc(), compact, pp); display_poly_sign(out, sc->sign()); sc = sc->prev(); } out << "}"; } - void display_algebraic_def(std::ostream & out, algebraic * a, bool compact) const { + void display_interval(std::ostream & out, mpbqi const & i, bool pp) const { + if (pp) + bqim().display_pp(out, i); + else + bqim().display(out, i); + } + + void display_algebraic_def(std::ostream & out, algebraic * a, bool compact, bool pp) const { out << "root("; - display_polynomial(out, a->p(), display_free_var_proc(), compact); + display_polynomial(out, a->p(), display_free_var_proc(), compact, pp); out << ", "; - bqim().display(out, a->iso_interval()); + display_interval(out, a->iso_interval(), pp); out << ", "; if (a->sdt() != 0) - display_sign_conditions(out, a->sdt()->sc(a->sc_idx()), a->sdt()->qs(), compact); + display_sign_conditions(out, a->sdt()->sc(a->sc_idx()), a->sdt()->qs(), compact, pp); else out << "{}"; out << ")"; @@ -5878,28 +5911,33 @@ namespace realclosure { collect_algebraic_refs c; for (unsigned i = 0; i < n; i++) c.mark(p[i]); - display_polynomial(out, n, p, display_free_var_proc(), true); + display_polynomial(out, n, p, display_free_var_proc(), true, false); std::sort(c.m_found.begin(), c.m_found.end(), rank_lt_proc()); for (unsigned i = 0; i < c.m_found.size(); i++) { algebraic * ext = c.m_found[i]; out << "\n r!" << ext->idx() << " := "; - display_algebraic_def(out, ext, true); + display_algebraic_def(out, ext, true, false); } } - void display_ext(std::ostream & out, extension * r, bool compact) const { + void display_ext(std::ostream & out, extension * r, bool compact, bool pp) const { switch (r->knd()) { - case extension::TRANSCENDENTAL: to_transcendental(r)->display(out); break; - case extension::INFINITESIMAL: to_infinitesimal(r)->display(out); break; + case extension::TRANSCENDENTAL: to_transcendental(r)->display(out, pp); break; + case extension::INFINITESIMAL: to_infinitesimal(r)->display(out, pp); break; case extension::ALGEBRAIC: - if (compact) - out << "r!" << r->idx(); - else - display_algebraic_def(out, to_algebraic(r), compact); + if (compact) { + if (pp) + out << "α" << r->idx() << ""; + else + out << "r!" << r->idx(); + } + else { + display_algebraic_def(out, to_algebraic(r), compact, pp); + } } } - void display(std::ostream & out, value * v, bool compact) const { + void display(std::ostream & out, value * v, bool compact, bool pp=false) const { if (v == 0) out << "0"; else if (is_nz_rational(v)) @@ -5907,51 +5945,50 @@ namespace realclosure { else { rational_function_value * rf = to_rational_function(v); if (is_denominator_one(rf)) { - display_polynomial_expr(out, rf->num(), rf->ext(), compact); + display_polynomial_expr(out, rf->num(), rf->ext(), compact, pp); } else if (is_rational_one(rf->num())) { out << "1/("; - display_polynomial_expr(out, rf->den(), rf->ext(), compact); + display_polynomial_expr(out, rf->den(), rf->ext(), compact, pp); out << ")"; } else { out << "("; - display_polynomial_expr(out, rf->num(), rf->ext(), compact); + display_polynomial_expr(out, rf->num(), rf->ext(), compact, pp); out << ")/("; - display_polynomial_expr(out, rf->den(), rf->ext(), compact); + display_polynomial_expr(out, rf->den(), rf->ext(), compact, pp); out << ")"; } } } - void display_compact(std::ostream & out, value * a) const { + void display_compact(std::ostream & out, value * a, bool pp=false) const { collect_algebraic_refs c; c.mark(a); if (c.m_found.empty()) { - display(out, a, true); + display(out, a, true, pp); } else { std::sort(c.m_found.begin(), c.m_found.end(), rank_lt_proc()); out << "["; - display(out, a, true); + display(out, a, true, pp); for (unsigned i = 0; i < c.m_found.size(); i++) { algebraic * ext = c.m_found[i]; - out << "; r!" << ext->idx() << " := "; - display_algebraic_def(out, ext, true); + if (pp) + out << "; α" << ext->idx() << " := "; + else + out << "; r!" << ext->idx() << " := "; + display_algebraic_def(out, ext, true, pp); } out << "]"; } } - void display_compact(std::ostream & out, numeral const & a) const { - display_compact(out, a.m_value); - } - - void display(std::ostream & out, numeral const & a, bool compact=false) const { + void display(std::ostream & out, numeral const & a, bool compact=false, bool pp=false) const { if (compact) - display_compact(out, a); + display_compact(out, a.m_value, pp); else - display(out, a.m_value, false); + display(out, a.m_value, false, pp); } void display_non_rational_in_decimal(std::ostream & out, numeral const & a, unsigned precision) { @@ -5989,7 +6026,7 @@ namespace realclosure { if (is_zero(a)) out << "[0, 0]"; else - bqim().display(out, interval(a.m_value)); + display_interval(out, interval(a.m_value), false); } }; @@ -6029,16 +6066,16 @@ namespace realclosure { m_imp->del(a); } - void manager::mk_infinitesimal(char const * n, numeral & r) { - m_imp->mk_infinitesimal(n, r); + void manager::mk_infinitesimal(char const * n, char const * pp_n, numeral & r) { + m_imp->mk_infinitesimal(n, pp_n, r); } void manager::mk_infinitesimal(numeral & r) { m_imp->mk_infinitesimal(r); } - void manager::mk_transcendental(char const * n, mk_interval & proc, numeral & r) { - m_imp->mk_transcendental(n, proc, r); + void manager::mk_transcendental(char const * n, char const * pp_n, mk_interval & proc, numeral & r) { + m_imp->mk_transcendental(n, pp_n, proc, r); } void manager::mk_transcendental(mk_interval & proc, numeral & r) { @@ -6212,9 +6249,9 @@ namespace realclosure { return gt(a, _b); } - void manager::display(std::ostream & out, numeral const & a, bool compact) const { + void manager::display(std::ostream & out, numeral const & a, bool compact, bool pp) const { save_interval_ctx ctx(this); - m_imp->display(out, a, compact); + m_imp->display(out, a, compact, pp); } void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const { @@ -6234,7 +6271,7 @@ namespace realclosure { }; void pp(realclosure::manager::imp * imp, realclosure::polynomial const & p, realclosure::extension * ext) { - imp->display_polynomial_expr(std::cout, p, ext, false); + imp->display_polynomial_expr(std::cout, p, ext, false, false); std::cout << std::endl; } @@ -6278,6 +6315,6 @@ void pp(realclosure::manager::imp * imp, mpq const & n) { } void pp(realclosure::manager::imp * imp, realclosure::extension * x) { - imp->display_ext(std::cout, x, false); + imp->display_ext(std::cout, x, false, false); std::cout << std::endl; } diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index 2b70d3be0..2a1b0dc20 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -70,7 +70,7 @@ namespace realclosure { /** \brief Add a new infinitesimal to the current field. The new infinitesimal is smaller than any positive element in the field. */ - void mk_infinitesimal(char const * name, numeral & r); + void mk_infinitesimal(char const * name, char const * pp_name, numeral & r); void mk_infinitesimal(numeral & r); /** @@ -83,7 +83,7 @@ namespace realclosure { Then, we extend the field F with 1 - Pi. 1 - Pi is transcendental with respect to algebraic real numbers, but it is NOT transcendental with respect to F, since F contains Pi. */ - void mk_transcendental(char const * name, mk_interval & proc, numeral & r); + void mk_transcendental(char const * name, char const * pp_name, mk_interval & proc, numeral & r); void mk_transcendental(mk_interval & proc, numeral & r); /** @@ -252,7 +252,7 @@ namespace realclosure { bool ge(numeral const & a, mpq const & b) { return !lt(a, b); } bool ge(numeral const & a, mpz const & b) { return !lt(a, b); } - void display(std::ostream & out, numeral const & a, bool compact=false) const; + void display(std::ostream & out, numeral const & a, bool compact=false, bool pp=false) const; /** \brief Display a real number in decimal notation. diff --git a/src/util/ext_numeral.h b/src/util/ext_numeral.h index af4b7ac10..83d326243 100644 --- a/src/util/ext_numeral.h +++ b/src/util/ext_numeral.h @@ -332,4 +332,16 @@ void display(std::ostream & out, } } +template +void display_pp(std::ostream & out, + numeral_manager & m, + typename numeral_manager::numeral const & a, + ext_numeral_kind ak) { + switch (ak) { + case EN_MINUS_INFINITY: out << "-∞"; break; + case EN_NUMERAL: m.display(out, a); break; + case EN_PLUS_INFINITY: out << "+∞"; break; + } +} + #endif