mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

add unit test for #2867

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-24 11:52:41 -07:00
parent 33b644adad
commit a4f668eef0
5 changed files with 98 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
src/math/polynomial/algebraic_numbers.cpp
View file

@ -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() {

12
src/math/polynomial/algebraic_numbers.h
View file

@ -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();

1
src/sat/sat_probing.cpp
View file

@ -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())

2
src/smt/theory_seq.cpp
View file

@ -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;
}

63
src/test/algebraic.cpp
View file

@ -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");