From 39edf73e786c657645d41a6433a799a3fb685bf1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 5 Oct 2019 16:57:51 -0700 Subject: [PATCH] fix #2613 fix #2612 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 17 ++++++ src/ast/arith_decl_plugin.h | 3 + src/math/polynomial/algebraic_numbers.cpp | 67 +++++++++++----------- src/math/polynomial/algebraic_numbers.h | 4 +- src/math/polynomial/polynomial.cpp | 42 ++++++++++++-- src/math/polynomial/polynomial.h | 11 ++++ src/math/polynomial/polynomial_cache.cpp | 1 + src/math/polynomial/upolynomial.cpp | 40 ++++++------- src/math/polynomial/upolynomial.h | 22 ++++---- src/model/model_evaluator.cpp | 9 +-- src/nlsat/nlsat_evaluator.cpp | 45 ++++++++------- src/nlsat/nlsat_explain.cpp | 50 +++++++++-------- src/nlsat/nlsat_solver.cpp | 2 +- src/smt/asserted_formulas.cpp | 1 - src/smt/theory_seq.cpp | 68 ++++++++++++----------- src/smt/theory_seq.h | 2 +- 16 files changed, 222 insertions(+), 162 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 88fc59524..f372b9b6f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -779,3 +779,20 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { } return result; } + +bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args) { + rational r; + if (is_decl_of(f, m_afid, OP_DIV) && is_numeral(args[1], r) && r.is_zero()) { + return true; + } + if (is_decl_of(f, m_afid, OP_IDIV) && is_numeral(args[1], r) && r.is_zero()) { + return true; + } + if (is_decl_of(f, m_afid, OP_MOD) && is_numeral(args[1], r) && r.is_zero()) { + return true; + } + if (is_decl_of(f, m_afid, OP_REM) && is_numeral(args[1], r) && r.is_zero()) { + return true; + } + return plugin().is_considered_uninterpreted(f); +} diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 00c7e694f..aa650697d 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -442,6 +442,9 @@ public: expr_ref mk_add_simplify(expr_ref_vector const& args); expr_ref mk_add_simplify(unsigned sz, expr* const* args); + + bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args); + }; diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 31346acd9..e2cc249dd 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -257,7 +257,7 @@ namespace algebraic_numbers { SASSERT(bqm().ge(upper(c), candidate)); - if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == 0) { + if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == polynomial::sign_zero) { m_wrapper.set(a, candidate); return true; } @@ -320,7 +320,7 @@ namespace algebraic_numbers { SASSERT(bqm().ge(upper(c), candidate)); // Find if candidate is an actual root - if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == 0) { + if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == polynomial::sign_zero) { saved_a.restore_if_too_small(); set(a, candidate); return true; @@ -379,11 +379,11 @@ namespace algebraic_numbers { } void update_sign_lower(algebraic_cell * c) { - int sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c)); + polynomial::sign sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c)); // The isolating intervals are refinable. Thus, the polynomial has opposite signs at lower and upper. - SASSERT(sl != 0); + SASSERT(sl != polynomial::sign_zero); SASSERT(upm().eval_sign_at(c->m_p_sz, c->m_p, upper(c)) == -sl); - c->m_sign_lower = sl < 0; + c->m_sign_lower = sl == polynomial::sign_neg; } // Make sure the GCD of the coefficients is one and the leading coefficient is positive @@ -1594,8 +1594,8 @@ namespace algebraic_numbers { #define REFINE_LOOP(BOUND, TARGET_SIGN) \ while (true) { \ bqm().div2(BOUND); \ - int new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \ - if (new_sign == 0) { \ + polynomial::sign new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \ + if (new_sign == polynomial::sign_zero) { \ /* found actual root */ \ scoped_mpq r(qm()); \ to_mpq(qm(), BOUND, r); \ @@ -1695,8 +1695,8 @@ namespace algebraic_numbers { if (bqm().ge(l, b)) return 1; // b is in the isolating interval (l, u) - int sign_b = upm().eval_sign_at(c->m_p_sz, c->m_p, b); - if (sign_b == 0) + auto sign_b = upm().eval_sign_at(c->m_p_sz, c->m_p, b); + if (sign_b == polynomial::sign_zero) return 0; return sign_b == sign_lower(c) ? 1 : -1; } @@ -1979,7 +1979,7 @@ namespace algebraic_numbers { }; polynomial::var_vector m_eval_sign_vars; - int eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) { + polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) { polynomial::manager & ext_pm = p.m(); TRACE("anum_eval_sign", tout << "evaluating sign of: " << p << "\n";); while (true) { @@ -1990,7 +1990,7 @@ namespace algebraic_numbers { scoped_mpq r(qm()); ext_pm.eval(p, x2v_basic, r); TRACE("anum_eval_sign", tout << "all variables are assigned to rationals, value of p: " << r << "\n";); - return qm().sign(r); + return polynomial::to_sign(qm().sign(r)); } catch (const opt_var2basic::failed &) { // continue @@ -2004,13 +2004,13 @@ namespace algebraic_numbers { if (ext_pm.is_zero(p_prime)) { // polynomial vanished after substituting rational values. - return 0; + return polynomial::sign_zero; } if (is_const(p_prime)) { // polynomial became the constant polynomial after substitution. SASSERT(size(p_prime) == 1); - return ext_pm.m().sign(ext_pm.coeff(p_prime, 0)); + return polynomial::to_sign(ext_pm.m().sign(ext_pm.coeff(p_prime, 0))); } // Try to find sign using intervals @@ -2026,7 +2026,7 @@ namespace algebraic_numbers { ext_pm.eval(p_prime, x2v_interval, ri); TRACE("anum_eval_sign", tout << "evaluating using intervals: " << ri << "\n";); if (!bqim().contains_zero(ri)) { - return bqim().is_pos(ri) ? 1 : -1; + return bqim().is_pos(ri) ? polynomial::sign_pos : polynomial::sign_neg; } // refine intervals if magnitude > m_min_magnitude bool refined = false; @@ -2067,7 +2067,7 @@ namespace algebraic_numbers { // Remark: m_zero_accuracy == 0 means use precise computation. if (m_zero_accuracy > 0) { // assuming the value is 0, since the result is in (-1/2^k, 1/2^k), where m_zero_accuracy = k - return 0; + return polynomial::sign_zero; } #if 0 // Evaluating sign using algebraic arithmetic @@ -2143,7 +2143,7 @@ namespace algebraic_numbers { bqm().div2k(mL, k); bqm().div2k(L, k); if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L)) - return 0; + return polynomial::sign_zero; // keep refining ri until ri is inside (-L, L) or // ri does not contain zero. @@ -2166,14 +2166,13 @@ namespace algebraic_numbers { TRACE("anum_eval_sign", tout << "evaluating using intervals: " << ri << "\n"; tout << "zero lower bound is: " << L << "\n";); if (!bqim().contains_zero(ri)) { - return bqim().is_pos(ri) ? 1 : -1; + return bqim().is_pos(ri) ? polynomial::sign_pos : polynomial::sign_neg; } if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L)) - return 0; + return polynomial::sign_zero; - for (unsigned i = 0; i < xs.size(); i++) { - polynomial::var x = xs[i]; + for (auto x : xs) { SASSERT(x2v.contains(x)); anum const & v = x2v(x); SASSERT(!v.is_basic()); @@ -2242,18 +2241,14 @@ namespace algebraic_numbers { unsigned sz = roots.size(); unsigned j = 0; - // std::cout << "p: " << p << "\n"; - // std::cout << "sz: " << sz << "\n"; for (unsigned i = 0; i < sz; i++) { checkpoint(); - // display_root(std::cout, roots[i]); std::cout << std::endl; ext_var2num ext_x2v(m_wrapper, x2v, x, roots[i]); TRACE("isolate_roots", tout << "filter_roots i: " << i << ", ext_x2v: x" << x << " -> "; display_root(tout, roots[i]); tout << "\n";); - int sign = eval_sign_at(p, ext_x2v); + polynomial::sign sign = eval_sign_at(p, ext_x2v); TRACE("isolate_roots", tout << "filter_roots i: " << i << ", result sign: " << sign << "\n";); if (sign != 0) continue; - // display_decimal(std::cout, roots[i], 10); std::cout << " is root" << std::endl; if (i != j) set(roots[j], roots[i]); j++; @@ -2453,7 +2448,7 @@ namespace algebraic_numbers { } } - int eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) { + polynomial::sign eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) { scoped_mpq qv(qm()); to_mpq(qm(), v, qv); scoped_anum av(m_wrapper); @@ -2568,13 +2563,13 @@ namespace algebraic_numbers { #define DEFAULT_PRECISION 2 - void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector & signs) { + void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector & signs) { isolate_roots(p, x2v, roots); unsigned num_roots = roots.size(); if (num_roots == 0) { anum zero; ext2_var2num ext_x2v(m_wrapper, x2v, zero); - int s = eval_sign_at(p, ext_x2v); + polynomial::sign s = eval_sign_at(p, ext_x2v); signs.push_back(s); } else { @@ -2601,8 +2596,8 @@ namespace algebraic_numbers { TRACE("isolate_roots_bug", tout << "w: "; display_root(tout, w); tout << "\n";); { ext2_var2num ext_x2v(m_wrapper, x2v, w); - int s = eval_sign_at(p, ext_x2v); - SASSERT(s != 0); + auto s = eval_sign_at(p, ext_x2v); + SASSERT(s != polynomial::sign_zero); signs.push_back(s); } @@ -2611,16 +2606,16 @@ namespace algebraic_numbers { numeral & curr = roots[i]; select(prev, curr, w); ext2_var2num ext_x2v(m_wrapper, x2v, w); - int s = eval_sign_at(p, ext_x2v); - SASSERT(s != 0); + auto s = eval_sign_at(p, ext_x2v); + SASSERT(s != polynomial::sign_zero); signs.push_back(s); } int_gt(roots[num_roots - 1], w); { ext2_var2num ext_x2v(m_wrapper, x2v, w); - int s = eval_sign_at(p, ext_x2v); - SASSERT(s != 0); + auto s = eval_sign_at(p, ext_x2v); + SASSERT(s != polynomial::sign_zero); signs.push_back(s); } } @@ -2879,7 +2874,7 @@ namespace algebraic_numbers { m_imp->isolate_roots(p, x2v, roots); } - void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector & signs) { + void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector & signs) { m_imp->isolate_roots(p, x2v, roots, signs); } @@ -3037,7 +3032,7 @@ namespace algebraic_numbers { l = rational(_l); } - int manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) { + polynomial::sign manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) { SASSERT(&(x2v.m()) == this); return m_imp->eval_sign_at(p, x2v); } diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index fa9731b62..59e6401d7 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -173,7 +173,7 @@ namespace algebraic_numbers { /** \brief Isolate the roots of the given polynomial, and compute its sign between them. */ - void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector & signs); + void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector & signs); /** \brief Store in r the i-th root of p. @@ -304,7 +304,7 @@ namespace algebraic_numbers { Return 0 if p(alpha_1, ..., alpha_n) == 0 Return positive number if p(alpha_1, ..., alpha_n) > 0 */ - int eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v); + polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v); void get_polynomial(numeral const & a, svector & r); diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 8d4755e82..a368c9507 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -1068,12 +1068,12 @@ namespace polynomial { g.reserve(std::min(sz1, sz2)); r1.reserve(sz2); // r1 has at most num_args2 arguments r2.reserve(sz1); // r2 has at most num_args1 arguments - bool found = false; - unsigned i1 = 0; - unsigned i2 = 0; - unsigned j1 = 0; - unsigned j2 = 0; - unsigned j3 = 0; + bool found = false; + unsigned i1 = 0; + unsigned i2 = 0; + unsigned j1 = 0; + unsigned j2 = 0; + unsigned j3 = 0; while (true) { if (i1 == sz1) { if (found) { @@ -2501,6 +2501,32 @@ namespace polynomial { return p; } + void gcd_simplify(polynomial * p) { + if (m_manager.finite()) return; + auto& m = m_manager.m(); + unsigned sz = p->size(); + if (sz == 0) + return; + unsigned g = 0; + for (unsigned i = 0; i < sz; i++) { + if (!m.is_int(p->a(i))) { + return; + } + int j = m.get_int(p->a(i)); + if (j == INT_MIN || j == 1 || j == -1) + return; + g = u_gcd(abs(j), g); + if (g == 1) + return; + } + scoped_mpz r(m), gg(m); + m.set(gg, g); + for (unsigned i = 0; i < sz; ++i) { + m.div_gcd(p->a(i), gg, r); + m.set(p->a(i), r); + } + } + polynomial * mk_zero() { return m_zero; } @@ -7041,6 +7067,10 @@ namespace polynomial { return m_imp->hash(p); } + void manager::gcd_simplify(polynomial * p) { + m_imp->gcd_simplify(p); + } + polynomial * manager::coeff(polynomial const * p, var x, unsigned k) { return m_imp->coeff(p, x, k); } diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 0aa3f5db5..45d7c189d 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -44,6 +44,11 @@ namespace polynomial { typedef svector var_vector; class monomial; + typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign; + inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } }; + inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); } + inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); } + int lex_compare(monomial const * m1, monomial const * m2); int lex_compare2(monomial const * m1, monomial const * m2, var min_var); int graded_lex_compare(monomial const * m1, monomial const * m2); @@ -278,6 +283,12 @@ namespace polynomial { */ static unsigned id(polynomial const * p); + + /** + \brief Normalize coefficients by dividing by their gcd + */ + void gcd_simplify(polynomial* p); + /** \brief Return true if \c m is the unit monomial. */ diff --git a/src/math/polynomial/polynomial_cache.cpp b/src/math/polynomial/polynomial_cache.cpp index a617e9412..9f5f014e4 100644 --- a/src/math/polynomial/polynomial_cache.cpp +++ b/src/math/polynomial/polynomial_cache.cpp @@ -139,6 +139,7 @@ namespace polynomial { polynomial * mk_unique(polynomial * p) { if (m_in_cache.get(pid(p), false)) return p; + // m.gcd_simplify(p); polynomial * p_prime = m_poly_table.insert_if_not_there(p); if (p == p_prime) { m_cached_polys.push_back(p_prime); diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index cfc8339d7..9076a4d50 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -1327,25 +1327,25 @@ namespace upolynomial { div(sz, p, 2, two_x_1, buffer); } - int manager::sign_of(numeral const & c) { + polynomial::sign manager::sign_of(numeral const & c) { if (m().is_zero(c)) - return 0; + return polynomial::sign_zero; if (m().is_pos(c)) - return 1; + return polynomial::sign_pos; else - return -1; + return polynomial::sign_neg; } // Return the number of sign changes in the coefficients of p unsigned manager::sign_changes(unsigned sz, numeral const * p) { unsigned r = 0; - int prev_sign = 0; + auto prev_sign = polynomial::sign_zero; unsigned i = 0; for (; i < sz; i++) { - int sign = sign_of(p[i]); - if (sign == 0) + auto sign = sign_of(p[i]); + if (sign == polynomial::sign_zero) continue; - if (sign != prev_sign && prev_sign != 0) + if (sign != prev_sign && prev_sign != polynomial::sign_zero) r++; prev_sign = sign; } @@ -1729,14 +1729,14 @@ namespace upolynomial { } // Evaluate the sign of p(b) - int manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) { + polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) { // Actually, given b = c/2^k, we compute the sign of (2^k)^n*p(b) // Original Horner Sequence // ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ... // Variation of the Horner Sequence for (2^k)^n*p(b) // ((a_n * c + a_{n-1}*2_k)*c + a_{n-2}*(2_k)^2)*c + a_{n-3}*(2_k)^3 ... + a_0*(2_k)^n if (sz == 0) - return 0; + return polynomial::sign_zero; if (sz == 1) return sign_of(p[0]); numeral const & c = b.numerator(); @@ -1762,14 +1762,14 @@ namespace upolynomial { } // Evaluate the sign of p(b) - int manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) { + polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) { // Actually, given b = c/d, we compute the sign of (d^n)*p(b) // Original Horner Sequence // ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ... // Variation of the Horner Sequence for (d^n)*p(b) // ((a_n * c + a_{n-1}*d)*c + a_{n-2}*d^2)*c + a_{n-3}*d^3 ... + a_0*d^n if (sz == 0) - return 0; + return polynomial::sign_zero; if (sz == 1) return sign_of(p[0]); numeral const & c = b.numerator(); @@ -1796,11 +1796,11 @@ namespace upolynomial { } // Evaluate the sign of p(b) - int manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) { + polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) { // Using Horner Sequence // ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ... if (sz == 0) - return 0; + return polynomial::sign_zero; if (sz == 1) return sign_of(p[0]); scoped_numeral r(m()); @@ -1817,21 +1817,21 @@ namespace upolynomial { return sign_of(r); } - int manager::eval_sign_at_zero(unsigned sz, numeral const * p) { + polynomial::sign manager::eval_sign_at_zero(unsigned sz, numeral const * p) { if (sz == 0) - return 0; + return polynomial::sign_zero; return sign_of(p[0]); } - int manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) { + polynomial::sign manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) { if (sz == 0) - return 0; + return polynomial::sign_zero; return sign_of(p[sz-1]); } - int manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) { + polynomial::sign manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) { if (sz == 0) - return 0; + return polynomial::sign_zero; unsigned degree = sz - 1; if (degree % 2 == 0) return sign_of(p[sz-1]); diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index 52115ebc1..c8e868f4b 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -554,7 +554,7 @@ namespace upolynomial { numeral_vector m_tr_tmp; numeral_vector m_push_tmp; - int sign_of(numeral const & c); + polynomial::sign sign_of(numeral const & c); struct drs_frame; void pop_top_frame(numeral_vector & p_stack, svector & frame_stack); void push_child_frames(unsigned sz, numeral const * p, numeral_vector & p_stack, svector & frame_stack); @@ -735,32 +735,32 @@ namespace upolynomial { /** \brief Evaluate the sign of p(b) */ - int eval_sign_at(unsigned sz, numeral const * p, mpbq const & b); + polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpbq const & b); + + /** + \brief Evaluate the sign of p(b) + */ + polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpq const & b); /** \brief Evaluate the sign of p(b) */ - int eval_sign_at(unsigned sz, numeral const * p, mpq const & b); - - /** - \brief Evaluate the sign of p(b) - */ - int eval_sign_at(unsigned sz, numeral const * p, mpz const & b); + polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpz const & b); /** \brief Evaluate the sign of p(0) */ - int eval_sign_at_zero(unsigned sz, numeral const * p); + polynomial::sign eval_sign_at_zero(unsigned sz, numeral const * p); /** \brief Evaluate the sign of p(+oo) */ - int eval_sign_at_plus_inf(unsigned sz, numeral const * p); + polynomial::sign eval_sign_at_plus_inf(unsigned sz, numeral const * p); /** \brief Evaluate the sign of p(-oo) */ - int eval_sign_at_minus_inf(unsigned sz, numeral const * p); + polynomial::sign eval_sign_at_minus_inf(unsigned sz, numeral const * p); /** \brief Evaluate the sign variations in the polynomial sequence at -oo diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 35c637ade..d01541790 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -333,13 +333,8 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_REWRITE_FULL; } - rational r; - if (is_decl_of(f, m_au.get_family_id(), OP_DIV) && m_au.is_numeral(args[1], r) && r.is_zero()) { - result = m_au.mk_real(0); - return BR_DONE; - } - if (is_decl_of(f, m_au.get_family_id(), OP_IDIV) && m_au.is_numeral(args[1], r) && r.is_zero()) { - result = m_au.mk_int(0); + if (m_au.is_considered_uninterpreted(f, num, args)) { + result = m_au.mk_numeral(rational(0), f->get_range()); return BR_DONE; } return BR_FAILED; diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index ddce9fc09..81e8cf536 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -43,7 +43,7 @@ namespace nlsat { svector
m_sections; unsigned_vector m_sorted_sections; // refs to m_sections unsigned_vector m_poly_sections; // refs to m_sections - svector m_poly_signs; + svector m_poly_signs; struct poly_info { unsigned m_num_roots; unsigned m_first_section; // idx in m_poly_sections; @@ -149,18 +149,18 @@ namespace nlsat { \brief Add polynomial with the given roots and signs. */ unsigned_vector p_section_ids; - void add(anum_vector & roots, svector & signs) { + void add(anum_vector & roots, svector & signs) { p_section_ids.reset(); if (!roots.empty()) merge(roots, p_section_ids); unsigned first_sign = m_poly_signs.size(); unsigned first_section = m_poly_sections.size(); - unsigned num_signs = signs.size(); + unsigned num_poly_signs = signs.size(); // Must normalize signs since we use arithmetic operations such as * // during evaluation. // Without normalization, overflows may happen, and wrong results may be produced. - for (unsigned i = 0; i < num_signs; i++) - m_poly_signs.push_back(normalize_sign(signs[i])); + for (unsigned i = 0; i < num_poly_signs; i++) + m_poly_signs.push_back(signs[i]); m_poly_sections.append(p_section_ids); m_info.push_back(poly_info(roots.size(), first_section, first_sign)); SASSERT(check_invariant()); @@ -169,10 +169,10 @@ namespace nlsat { /** \brief Add constant polynomial */ - void add_const(int sign) { + void add_const(polynomial::sign sign) { unsigned first_sign = m_poly_signs.size(); unsigned first_section = m_poly_sections.size(); - m_poly_signs.push_back(normalize_sign(sign)); + m_poly_signs.push_back(sign); m_info.push_back(poly_info(0, first_section, first_sign)); } @@ -226,12 +226,12 @@ namespace nlsat { } // Return the sign idx of pinfo - int sign(poly_info const & pinfo, unsigned i) const { + polynomial::sign sign(poly_info const & pinfo, unsigned i) const { return m_poly_signs[pinfo.m_first_sign + i]; } #define LINEAR_SEARCH_THRESHOLD 8 - int sign_at(unsigned info_id, unsigned c) const { + polynomial::sign sign_at(unsigned info_id, unsigned c) const { poly_info const & pinfo = m_info[info_id]; unsigned num_roots = pinfo.m_num_roots; if (num_roots < LINEAR_SEARCH_THRESHOLD) { @@ -239,7 +239,7 @@ namespace nlsat { for (; i < num_roots; i++) { unsigned section_cell_id = cell_id(pinfo, i); if (section_cell_id == c) - return 0; + return polynomial::sign_zero; else if (section_cell_id > c) break; } @@ -253,7 +253,7 @@ namespace nlsat { if (c < root_1_cell_id) return sign(pinfo, 0); else if (c == root_1_cell_id || c == root_n_cell_id) - return 0; + return polynomial::sign_zero; else if (c > root_n_cell_id) return sign(pinfo, num_roots); int low = 0; @@ -272,7 +272,7 @@ namespace nlsat { SASSERT(low < mid && mid < high); unsigned mid_cell_id = cell_id(pinfo, mid); if (mid_cell_id == c) { - return 0; + return polynomial::sign_zero; } if (c < mid_cell_id) { high = mid; @@ -319,7 +319,7 @@ namespace nlsat { for (unsigned j = 0; j < num_cells(); j++) { if (j > 0) out << " "; - int s = sign_at(i, j); + auto s = sign_at(i, j); if (s < 0) out << "-"; else if (s == 0) out << "0"; else out << "+"; @@ -381,11 +381,10 @@ namespace nlsat { \pre All variables of p are assigned in the current interpretation. */ - int eval_sign(poly * p) { + polynomial::sign eval_sign(poly * p) { // TODO: check if it is useful to cache results SASSERT(m_assignment.is_assigned(max_var(p))); - int r = m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment); - return r > 0 ? +1 : (r < 0 ? -1 : 0); + return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment); } bool satisfied(int sign, atom::kind k) { @@ -450,7 +449,7 @@ namespace nlsat { return a->is_ineq_atom() ? eval_ineq(to_ineq_atom(a), neg) : eval_root(to_root_atom(a), neg); } - svector m_add_signs_tmp; + svector m_add_signs_tmp; void add(poly * p, var x, sign_table & t) { SASSERT(m_pm.max_var(p) <= x); if (m_pm.max_var(p) < x) { @@ -459,7 +458,7 @@ namespace nlsat { else { // isolate roots of p scoped_anum_vector & roots = m_add_roots_tmp; - svector & signs = m_add_signs_tmp; + svector & signs = m_add_signs_tmp; roots.reset(); signs.reset(); TRACE("nlsat_evaluator", tout << "x: " << x << " max_var(p): " << m_pm.max_var(p) << "\n";); @@ -471,18 +470,18 @@ namespace nlsat { } // Evaluate the sign of p1^e1*...*pn^en (of atom a) in cell c of table t. - int sign_at(ineq_atom * a, sign_table const & t, unsigned c) const { - int sign = 1; + polynomial::sign sign_at(ineq_atom * a, sign_table const & t, unsigned c) const { + auto sign = polynomial::sign_pos; unsigned num_ps = a->size(); for (unsigned i = 0; i < num_ps; i++) { - int curr_sign = t.sign_at(i, c); + polynomial::sign curr_sign = t.sign_at(i, c); TRACE("nlsat_evaluator_bug", tout << "sign of i: " << i << " at cell " << c << "\n"; m_pm.display(tout, a->p(i)); tout << "\nsign: " << curr_sign << "\n";); if (a->is_even(i) && curr_sign < 0) - curr_sign = 1; + curr_sign = polynomial::sign_pos; sign = sign * curr_sign; - if (sign == 0) + if (sign == polynomial::sign_zero) break; } return sign; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 3f02ec672..3c3120d5d 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -197,9 +197,10 @@ namespace nlsat { \brief Reset m_already_added vector using m_result */ void reset_already_added() { - SASSERT(m_result != 0); + SASSERT(m_result != nullptr); for (literal lit : *m_result) m_already_added_literal[lit.index()] = false; + SASSERT(check_already_added()); } @@ -207,9 +208,9 @@ namespace nlsat { \brief evaluate the given polynomial in the current interpretation. max_var(p) must be assigned in the current interpretation. */ - int sign(polynomial_ref const & p) { + polynomial::sign sign(polynomial_ref const & p) { SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p))); - int s = m_am.eval_sign_at(p, m_assignment); + auto s = m_am.eval_sign_at(p, m_assignment); TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";); return s; } @@ -270,7 +271,7 @@ namespace nlsat { polynomial_ref f(m_pm); for (unsigned i = 0; i < num_factors; i++) { f = m_factors.get(i); - if (sign(f) == 0) { + if (sign(f) == polynomial::sign_zero) { m_zero_fs.push_back(m_factors.get(i)); m_is_even.push_back(false); } @@ -323,7 +324,7 @@ namespace nlsat { return; // lc is a nonzero constant lc = m_pm.coeff(p, x, k, reduct); if (!is_zero(lc)) { - if (sign(lc) != 0) + if (sign(lc) != polynomial::sign_zero) return; // lc is not the zero polynomial, but it vanished in the current interpretation. // so we keep searching... @@ -959,8 +960,9 @@ namespace nlsat { if (ps.empty()) return; m_todo.reset(); - for (unsigned i = 0; i < ps.size(); i++) - m_todo.insert(ps.get(i)); + for (poly* p : ps) { + m_todo.insert(p); + } var x = m_todo.remove_max_polys(ps); // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore if (x < max_x) @@ -983,8 +985,8 @@ namespace nlsat { } bool check_already_added() const { - for (unsigned i = 0; i < m_already_added_literal.size(); i++) { - SASSERT(m_already_added_literal[i] == false); + for (bool b : m_already_added_literal) { + SASSERT(!b); } return true; } @@ -1062,7 +1064,7 @@ namespace nlsat { void simplify(literal l, eq_info & info, var max, scoped_literal & new_lit) { bool_var b = l.var(); atom * a = m_atoms[b]; - SASSERT(a != 0); + SASSERT(a); if (a->is_root_atom()) { new_lit = l; return; @@ -1091,19 +1093,24 @@ namespace nlsat { modified_lit = true; unsigned d; m_pm.pseudo_remainder(f, info.m_eq, info.m_x, d, new_factor); + polynomial_ref fact(f, m_pm), eq(const_cast(info.m_eq), m_pm); + + TRACE("nlsat_simplify_core", tout << "d: " << d << " factor " << fact << " eq " << eq << " new factor " << new_factor << "\n";); // adjust sign based on sign of lc of eq - if (d % 2 == 1 && // d is odd - !is_even && // degree of the factor is odd - info.m_lc_sign < 0 // lc of the eq is negative - ) { + if (d % 2 == 1 && // d is odd + !is_even && // degree of the factor is odd + info.m_lc_sign < 0) { // lc of the eq is negative atom_sign = -atom_sign; // flipped the sign of the current literal + TRACE("nlsat_simplify_core", tout << "odd degree\n";); } if (is_const(new_factor)) { - int s = sign(new_factor); - if (s == 0) { + TRACE("nlsat_simplify_core", tout << "new factor is const\n";); + polynomial::sign s = sign(new_factor); + if (s == polynomial::sign_zero) { bool atom_val = a->get_kind() == atom::EQ; bool lit_val = l.sign() ? !atom_val : atom_val; new_lit = lit_val ? true_literal : false_literal; + TRACE("nlsat_simplify_core", tout << "zero sign: " << info.m_lc_const << "\n";); if (!info.m_lc_const) { // We have essentially shown the current factor must be zero If the leading coefficient is not zero. // Note that, if the current factor is zero, then the whole polynomial is zero. @@ -1115,6 +1122,7 @@ namespace nlsat { return; } else { + TRACE("nlsat_simplify_core", tout << "non-zero sign: " << info.m_lc_const << "\n";); // We have shown the current factor is a constant MODULO the sign of the leading coefficient (of the equation used to rewrite the factor). if (!info.m_lc_const) { // If the leading coefficient is not a constant, we must store this information as an extra assumption. @@ -1266,11 +1274,9 @@ namespace nlsat { var_vector m_select_tmp; ineq_atom * select_lower_stage_eq(scoped_literal_vector & C, var max) { var_vector & xs = m_select_tmp; - unsigned sz = C.size(); - for (unsigned i = 0; i < sz; i++) { - literal l = C[i]; + for (literal l : C) { bool_var b = l.var(); - atom * a = m_atoms[b]; + atom * a = m_atoms[b]; if (a->is_root_atom()) continue; // we don't rewrite root atoms ineq_atom * _a = to_ineq_atom(a); @@ -1279,9 +1285,7 @@ namespace nlsat { poly * p = _a->p(j); xs.reset(); m_pm.vars(p, xs); - unsigned xs_sz = xs.size(); - for (unsigned k = 0; k < xs_sz; k++) { - var y = xs[k]; + for (var y : xs) { if (y >= max) continue; atom * eq = m_x2eq[y]; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 41c60c80d..d8beb0c63 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -766,7 +766,7 @@ namespace nlsat { TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n"; display(tout);); IF_VERBOSE(0, display(verbose_stream() << "check lemma: ", n, cls) << "\n"); - for (clause* c : m_learned) IF_VERBOSE(0, display(verbose_stream() << "lemma: ", *c) << "\n"); + for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n"); solver solver2(m_ctx); imp& checker = *(solver2.m_imp); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3125287bd..73f7ffe72 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -439,7 +439,6 @@ void asserted_formulas::commit() { } void asserted_formulas::commit(unsigned new_qhead) { - TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";); m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead); m_expr2depth.reset(); for (unsigned i = m_qhead; i < new_qhead; ++i) { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2eb0aa8c4..8597bd144 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -474,11 +474,11 @@ bool theory_seq::branch_binary_variable(eq const& e) { return true; } if (!get_length(x, lenX)) { - enforce_length(x); + add_length_to_eqc(x); return true; } if (!get_length(y, lenY)) { - enforce_length(y); + add_length_to_eqc(y); return true; } if (lenX + rational(xs.size()) != lenY + rational(ys.size())) { @@ -555,7 +555,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector rational lenX; if (!get_length(X, lenX)) { TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";); - enforce_length(X); + add_length_to_eqc(X); return; } if (lenX > rational(units.size())) { @@ -732,13 +732,13 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) { rational lenX, lenY1, lenY2; context& ctx = get_context(); if (!get_length(x, lenX)) { - enforce_length(x); + add_length_to_eqc(x); } if (!get_length(y1, lenY1)) { - enforce_length(y1); + add_length_to_eqc(y1); } if (!get_length(y2, lenY2)) { - enforce_length(y2); + add_length_to_eqc(y2); } SASSERT(!xs.empty() && !ys.empty()); @@ -848,13 +848,13 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) { rational lenX, lenY1, lenY2; context& ctx = get_context(); if (!get_length(x, lenX)) { - enforce_length(x); + add_length_to_eqc(x); } if (!get_length(y1, lenY1)) { - enforce_length(y1); + add_length_to_eqc(y1); } if (!get_length(y2, lenY2)) { - enforce_length(y2); + add_length_to_eqc(y2); } SASSERT(!xs.empty() && !ys.empty()); unsigned_vector indexes = overlap2(xs, ys); @@ -922,16 +922,16 @@ bool theory_seq::branch_quat_variable(eq const& e) { rational lenX1, lenX2, lenY1, lenY2; context& ctx = get_context(); if (!get_length(x1_l, lenX1)) { - enforce_length(x1_l); + add_length_to_eqc(x1_l); } if (!get_length(y1_l, lenY1)) { - enforce_length(y1_l); + add_length_to_eqc(y1_l); } if (!get_length(x2, lenX2)) { - enforce_length(x2); + add_length_to_eqc(x2); } if (!get_length(y2, lenY2)) { - enforce_length(y2); + add_length_to_eqc(y2); } SASSERT(!xs.empty() && !ys.empty()); @@ -1608,7 +1608,7 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector & le len.push_back(val); } else { - enforce_length(e); + add_length_to_eqc(e); all_have_length = false; } } @@ -1897,7 +1897,6 @@ bool theory_seq::check_length_coherence0(expr* e) { bool theory_seq::check_length_coherence() { -#if 1 for (expr* l : m_length) { expr* e = nullptr; VERIFY(m_util.str.is_length(l, e)); @@ -1905,15 +1904,18 @@ bool theory_seq::check_length_coherence() { return true; } } -#endif + bool change = false; for (expr* l : m_length) { expr* e = nullptr; VERIFY(m_util.str.is_length(l, e)); if (check_length_coherence(e)) { return true; } + if (add_length_to_eqc(e)) { + change = true; + } } - return false; + return change; } bool theory_seq::fixed_length(bool is_zero) { @@ -2270,16 +2272,16 @@ bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect } } if (!asserted) { - std::cout << "not asserted\n"; + IF_VERBOSE(0, verbose_stream() << "not asserted\n";); context& ctx = get_context(); for (assumption const& a : assumptions) { if (a.lit != null_literal) { - std::cout << a.lit << " " << ctx.get_assignment(a.lit) << " "; - ctx.display_literal_info(std::cout, a.lit); - ctx.display_detailed_literal(std::cout, a.lit) << "\n"; + IF_VERBOSE(0, + verbose_stream() << a.lit << " " << ctx.get_assignment(a.lit) << " "; + ctx.display_literal_info(verbose_stream(), a.lit); + ctx.display_detailed_literal(verbose_stream(), a.lit) << "\n";); } } - // ctx.display(std::cout); exit(0); } return asserted; @@ -2390,14 +2392,15 @@ bool theory_seq::propagate_eq(dependency* dep, literal lit, expr* e1, expr* e2, void theory_seq::enforce_length_coherence(enode* n1, enode* n2) { expr* o1 = n1->get_owner(); expr* o2 = n2->get_owner(); + // std::cout << mk_pp(o1, m) << " " << mk_pp(o2, m) << " " << has_length(o1) << " " << has_length(o2) << "\n"; if (m_util.str.is_concat(o1) && m_util.str.is_concat(o2)) { return; } if (has_length(o1) && !has_length(o2)) { - enforce_length(o2); + add_length_to_eqc(o2); } else if (has_length(o2) && !has_length(o1)) { - enforce_length(o1); + add_length_to_eqc(o1); } } @@ -3355,8 +3358,8 @@ bool theory_seq::solve_nc(unsigned idx) { if (ctx.get_assignment(len_gt) == l_true) { VERIFY(m_util.str.is_contains(n.contains(), a, b)); - enforce_length(a); - enforce_length(b); + add_length_to_eqc(a); + add_length_to_eqc(b); TRACE("seq", tout << len_gt << " is true\n";); return true; } @@ -3640,19 +3643,22 @@ void theory_seq::add_length(expr* e, expr* l) { /* ensure that all elements in equivalence class occur under an application of 'length' */ -void theory_seq::enforce_length(expr* e) { +bool theory_seq::add_length_to_eqc(expr* e) { enode* n = ensure_enode(e); enode* n1 = n; + bool change = false; do { expr* o = n->get_owner(); if (!has_length(o)) { expr_ref len(m_util.str.mk_length(o), m); enque_axiom(len); add_length(o, len); + change = true; } n = n->get_next(); } while (n1 != n); + return change; } @@ -3733,7 +3739,7 @@ bool theory_seq::add_itos_val_axiom(expr* e) { if (m_util.str.is_stoi(n)) { return false; } - enforce_length(e); + add_length_to_eqc(e); if (get_length(e, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val != val2)) { add_si_axiom(e, n, val.get_unsigned()); @@ -3756,7 +3762,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) { if (m_util.str.is_itos(n)) { return false; } - enforce_length(n); + add_length_to_eqc(n); if (get_length(n, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val2 != val)) { add_si_axiom(n, e, val.get_unsigned()); @@ -4564,7 +4570,7 @@ void theory_seq::deque_axiom(expr* n) { add_length_axiom(n); } else if (m_util.str.is_empty(n) && !has_length(n) && !m_has_length.empty()) { - enforce_length(n); + add_length_to_eqc(n); } else if (m_util.str.is_index(n)) { add_indexof_axiom(n); @@ -5906,7 +5912,7 @@ void theory_seq::relevant_eh(app* n) { expr* arg; if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) { - enforce_length(arg); + add_length_to_eqc(arg); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 6be5b3b2c..16503cd40 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -592,7 +592,7 @@ namespace smt { bool has_length(expr *e) const { return m_has_length.contains(e); } void add_length(expr* e, expr* l); - void enforce_length(expr* n); + bool add_length_to_eqc(expr* n); bool enforce_length(expr_ref_vector const& es, vector& len); void enforce_length_coherence(enode* n1, enode* n2);