From a4f668eef07b357dd13bfe22bd7cdf9b7d86e079 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Mar 2020 11:52:41 -0700 Subject: [PATCH] add unit test for #2867 Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/algebraic_numbers.cpp | 51 +++++++++--------- src/math/polynomial/algebraic_numbers.h | 12 ++--- src/sat/sat_probing.cpp | 1 - src/smt/theory_seq.cpp | 2 +- src/test/algebraic.cpp | 63 +++++++++++++++++++++++ 5 files changed, 98 insertions(+), 31 deletions(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index e32846ddd..1c5f03aa1 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -569,22 +569,26 @@ namespace algebraic_numbers { } }; - void check_triangle_inequality(numeral_vector& r) { + void check_transitivity(numeral_vector& r) { lt_proc lt(m_wrapper); for (unsigned i = 0; i < r.size(); ++i) { auto& a = r[i]; - for (unsigned j = i + 1; j < r.size(); ++j) { + for (unsigned j = 0; j < r.size(); ++j) { auto& b = r[j]; bool ltab = lt(a, b); - for (unsigned k = j + 1; k < r.size(); ++k) { + for (unsigned k = 0; k < r.size(); ++k) { auto& c = r[k]; - CTRACE("algebraic", (lt(b, a) && lt(a, c) && !lt(b, c)), - display_root(tout << "b ", b) << "\n"; - display_root(tout << "a ", a) << "\n"; - display_root(tout << "c ", c) << "\n";); - SASSERT(!lt(a, b) || !lt(b, c) || lt(a, c)); - SASSERT(!lt(a, b) || !lt(c, a) || lt(c, b)); - SASSERT(!lt(b, a) || !lt(a, c) || lt(b, c)); + bool b_lt_a = lt(b, a); + bool c_lt_b = lt(c, b); + bool c_lt_a = lt(c, a); + // (a <= b & b <= c) => a <= c + // b < a or c < b or !(c < a) + CTRACE("algebraic_bug", + (!b_lt_a && !c_lt_b && c_lt_a), + display_root(tout << "a ", a) << "\n"; + display_root(tout << "b ", b) << "\n"; + display_root(tout << "c ", c) << "\n";); + SASSERT(b_lt_a || c_lt_b || !c_lt_a); } } } @@ -592,7 +596,7 @@ namespace algebraic_numbers { void sort_roots(numeral_vector & r) { if (m_limit.inc()) { - //DEBUG_CODE(check_triangle_inequality(r);); + // DEBUG_CODE(check_transitivity(r);); std::sort(r.begin(), r.end(), lt_proc(m_wrapper)); } } @@ -2782,8 +2786,8 @@ namespace algebraic_numbers { // the precision on refine is base 2 return upm().refine(c->m_p_sz, c->m_p, bqm(), l, u, precision * 4); } - - void display_decimal(std::ostream & out, numeral const & a, unsigned precision) { + + std::ostream& display_decimal(std::ostream & out, numeral const & a, unsigned precision) { if (a.is_basic()) { qm().display_decimal(out, basic_value(a), precision); } @@ -2798,6 +2802,7 @@ namespace algebraic_numbers { bqm().display_decimal(out, l, precision); } } + return out; } void get_lower(numeral const & a, mpq & l, unsigned precision) { @@ -3102,24 +3107,24 @@ namespace algebraic_numbers { return m_imp->eval_sign_at(p, x2v); } - void manager::display_interval(std::ostream & out, numeral const & a) const { - m_imp->display_interval(out, a); + std::ostream& manager::display_interval(std::ostream & out, numeral const & a) const { + return m_imp->display_interval(out, a); } - void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const { - m_imp->display_decimal(out, a, precision); + std::ostream& manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const { + return m_imp->display_decimal(out, a, precision); } - void manager::display_root(std::ostream & out, numeral const & a) const { - m_imp->display_root(out, a); + std::ostream& manager::display_root(std::ostream & out, numeral const & a) const { + return m_imp->display_root(out, a); } - void manager::display_mathematica(std::ostream & out, numeral const & a) const { - m_imp->display_mathematica(out, a); + std::ostream& manager::display_mathematica(std::ostream & out, numeral const & a) const { + return m_imp->display_mathematica(out, a); } - void manager::display_root_smt2(std::ostream & out, numeral const & a) const { - m_imp->display_root_smt2(out, a); + std::ostream& manager::display_root_smt2(std::ostream & out, numeral const & a) const { + return m_imp->display_root_smt2(out, a); } void manager::reset_statistics() { diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index e1f37b718..d6fafbd74 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -326,32 +326,32 @@ namespace algebraic_numbers { \brief Display algebraic number as a rational if is_rational(n) Otherwise, display it as an interval. */ - void display_interval(std::ostream & out, numeral const & a) const; + std::ostream& display_interval(std::ostream & out, numeral const & a) const; /** \brief Display algebraic number in decimal notation. A question mark is added based on the precision requested. */ - void display_decimal(std::ostream & out, numeral const & a, unsigned precision = 10) const; + std::ostream& display_decimal(std::ostream & out, numeral const & a, unsigned precision = 10) const; /** \brief Display algebraic number as a root object: (p, i) That is, 'a' is the i-th root of p. */ - void display_root(std::ostream & out, numeral const & a) const; + std::ostream& display_root(std::ostream & out, numeral const & a) const; /** \brief Display algebraic number as a root object in SMT 2.0 style: (root-obj p i) That is, 'a' is the i-th root of p. */ - void display_root_smt2(std::ostream & out, numeral const & a) const; + std::ostream& display_root_smt2(std::ostream & out, numeral const & a) const; /** \brief Display algebraic number in Mathematica format. */ - void display_mathematica(std::ostream & out, numeral const & a) const; + std::ostream& display_mathematica(std::ostream & out, numeral const & a) const; - void display(std::ostream & out, numeral const & a) { return display_decimal(out, a); } + std::ostream& display(std::ostream & out, numeral const & a) { return display_decimal(out, a); } void reset_statistics(); diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index bfb33551f..ed790a856 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -161,7 +161,6 @@ namespace sat { if (m_probing_binary) { watch_list & wlist = s.get_wlist(~l); - unsigned sz0 = wlist.size(); for (unsigned i = 0; i < wlist.size(); ++i) { watched & w = wlist[i]; if (!w.is_binary_clause()) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index aca35b04b..883bda173 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3474,7 +3474,6 @@ bool theory_seq::solve_ne(unsigned idx) { bool theory_seq::solve_nc(unsigned idx) { nc const& n = m_ncs[idx]; - dependency* deps = n.deps(); literal len_gt = n.len_gt(); context& ctx = get_context(); expr_ref c(m); @@ -3509,6 +3508,7 @@ bool theory_seq::solve_nc(unsigned idx) { } #else + dependency* deps = n.deps(); if (!canonize(n.contains(), deps, c)) { return false; } diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index 508bc7a2f..a22ca8c80 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -562,7 +562,70 @@ static void tst_root() { } +static void tst_sturm() { + reslimit rl; + unsynch_mpq_manager nm; + polynomial::manager m(rl, nm); + polynomial_ref x(m); + x = m.mk_polynomial(m.mk_var()); + polynomial_ref p(m); + polynomial_ref q(m); + +#define N(s) (rational(#s).to_mpq()) + + p = N(507962865083498496)*(x^10) + + N(102100535881783197696)*(x^9) - + N(14783112447185507561472)*(x^8) - + N(2001324733200883839555072)*(x^7) + + N(195168383210843217999079936)*(x^6) + + N(38119811955608999164032)*(x^5) + + N(9215524544769908136049956)*(x^4) - + N(733241058456905205563830332)*(x^3) - + N(15888459782104331950227)*(x^2) - + N(10235992917286431461226534)*x + + N(688689757310708660505387921); + + q = N(1286741608255488)*(x^6) + + N(129317531629676544)*(x^5) - + N(25384908626459170944)*(x^4) + + N(16014650289587907456)*(x^3) + + N(2042137943326838560)*(x^2) + + N(44729821875714513846)*x - + N(29154410578758924855); + + algebraic_numbers::manager am(rl, nm); + scoped_anum_vector rs1(am), rs2(am); + std::cout << "p: " << p << "\n"; + am.isolate_roots(p, rs1); + scoped_anum a(am), b(am), c(am); + a = rs1[2]; + b = rs1[3]; + am.isolate_roots(q, rs2); + c = rs2[3]; + am.display_decimal(std::cout << "a:", a) << "\n"; + am.display_interval(std::cout << "a:", a) << "\n"; + am.display_root(std::cout << "a:", a) << "\n"; + + am.display_decimal(std::cout << "b:", b) << "\n"; + am.display_interval(std::cout << "b:", b) << "\n"; + am.display_root(std::cout << "b:", b) << "\n"; + + am.display_decimal(std::cout << "c:", c) << "\n"; + am.display_interval(std::cout << "c:", c) << "\n"; + am.display_root(std::cout << "c:", c) << "\n"; + + std::cout << "b < a " << am.lt(b, a) << "\n"; + std::cout << "c < b " << am.lt(c, b) << "\n"; + std::cout << "c < a " << am.lt(c, a) << "\n"; + // it should not be the case that b < a == 0, c < b == 0 and c < a == 1. +} + + + + void tst_algebraic() { + tst_sturm(); + // enable_trace("resultant_bug"); // enable_trace("poly_sign"); disable_trace("algebraic");