diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index f3e2aafa7..abe49cc15 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -126,8 +126,8 @@ public: else { get_interval(p.lo(), lo_interval); m_dep_intervals.sub(bound, lo_interval, hi_bound); - m_dep_intervals.div(hi_bound, p.hi().val(), hi_bound); - vectro as; + m_dep_intervals.div(hi_bound, p.hi().val().to_mpq(), hi_bound); + vector as; m_var2intervals(p.var(), true, as); // use hi_bound to adjust for variable bound. } diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp index 4a8140681..d778b8554 100644 --- a/src/math/grobner/pdd_simplifier.cpp +++ b/src/math/grobner/pdd_simplifier.cpp @@ -75,7 +75,7 @@ namespace dd { } } catch (pdd_manager::mem_out) { - IF_VERBOSE(2, verbose_stream() << "simplifier memout\n"); + IF_VERBOSE(3, verbose_stream() << "simplifier memout\n"); // done reduce DEBUG_CODE(s.invariant();); } @@ -89,7 +89,7 @@ namespace dd { bool simplifier::simplify_linear_step(bool binary) { TRACE("dd.solver", tout << "binary " << binary << "\n";); - IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n"); + IF_VERBOSE(3, verbose_stream() << "binary " << binary << "\n"); equation_vector linear; for (equation* e : s.m_to_simplify) { pdd p = e->poly(); @@ -184,7 +184,7 @@ namespace dd { */ bool simplifier::simplify_cc_step() { TRACE("dd.solver", tout << "cc\n";); - IF_VERBOSE(2, verbose_stream() << "cc\n"); + IF_VERBOSE(3, verbose_stream() << "cc\n"); u_map los; bool reduced = false; unsigned j = 0; @@ -217,7 +217,7 @@ namespace dd { */ bool simplifier::simplify_leaf_step() { TRACE("dd.solver", tout << "leaf\n";); - IF_VERBOSE(2, verbose_stream() << "leaf\n"); + IF_VERBOSE(3, verbose_stream() << "leaf\n"); use_list_t use_list = get_use_list(); equation_vector leaves; for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) { @@ -262,7 +262,7 @@ namespace dd { */ bool simplifier::simplify_elim_pure_step() { TRACE("dd.solver", tout << "pure\n";); - IF_VERBOSE(2, verbose_stream() << "pure\n"); + IF_VERBOSE(3, verbose_stream() << "pure\n"); use_list_t use_list = get_use_list(); unsigned j = 0; for (equation* e : s.m_to_simplify) { diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index 63c5ad835..a3ce157fd 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -99,7 +99,7 @@ namespace dd { while (!done() && step()) { TRACE("dd.solver", display(tout);); DEBUG_CODE(invariant();); - IF_VERBOSE(3, display_statistics(verbose_stream())); + IF_VERBOSE(3, display_statistics(verbose_stream())); } DEBUG_CODE(invariant();); } @@ -322,7 +322,7 @@ namespace dd { SASSERT(curr->idx() != UINT_MAX); pdd const& p = curr->poly(); if (curr->state() == to_simplify && p.var() == v) { - if (!eq || is_simpler(*curr, *eq)) + if (!eq || is_simpler(*curr, *eq) || (curr->poly().is_linear() && !eq->poly().is_linear())) eq = curr; } } @@ -412,6 +412,11 @@ namespace dd { } bool solver::done() { + TRACE("dd.solver", + tout << "simplify.size + process.size >= eqs_threshold " << m_to_simplify.size() << " + " << m_processed.size() << " >= " << m_config.m_eqs_threshold << "\n"; + tout << "simplified >= max_simplified " << m_stats.simplified() << " >= " << m_config.m_max_simplified << "\n"; + tout << "canceled " << canceled() << "\n"; + tout << "compute_steps > max_steps " << m_stats.m_compute_steps << " > " << m_config.m_max_steps << "\n"); return m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || m_stats.simplified() >= m_config.m_max_simplified || diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index b3b7e09aa..c93aa2188 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -389,9 +389,9 @@ public: m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx); } bool column_corresponds_to_term(unsigned) const; - const lar_term & column_to_term(unsigned j) const { + const lar_term & column_index_to_term(unsigned j) const { SASSERT(column_corresponds_to_term(j)); - return get_term(column2tv(to_column_index(j))); + return get_term(column2tv(j)); } inline unsigned row_count() const { return A_r().row_count(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 07df58bcf..89c08354d 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -115,6 +115,7 @@ struct statistics { unsigned m_hnf_cutter_calls; unsigned m_hnf_cuts; unsigned m_nla_calls; + unsigned m_nla_bounds; unsigned m_horner_calls; unsigned m_horner_conflicts; unsigned m_cross_nested_forms; @@ -146,7 +147,7 @@ struct statistics { st.update("arith-grobner-propagations", m_grobner_propagations); st.update("arith-offset-eqs", m_offset_eqs); st.update("arith-fixed-eqs", m_fixed_eqs); - + st.update("arith-nla-bounds", m_nla_bounds); } }; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 053b33651..afee267c8 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -643,11 +643,11 @@ void core::trace_print_monic_and_factorization(const monic& rm, const factorizat bool core::var_has_positive_lower_bound(lpvar j) const { - return m_lar_solver.column_has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type(); + return has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type(); } bool core::var_has_negative_upper_bound(lpvar j) const { - return m_lar_solver.column_has_upper_bound(j) && m_lar_solver.get_upper_bound(j) < lp::zero_of_type(); + return has_upper_bound(j) && m_lar_solver.get_upper_bound(j) < lp::zero_of_type(); } bool core::var_is_separated_from_zero(lpvar j) const { @@ -811,6 +811,7 @@ void core::print_stats(std::ostream& out) { void core::clear() { m_lemma_vec->clear(); + m_literal_vec->clear(); } void core::init_search() { @@ -1501,11 +1502,53 @@ void core::check_bounded_divisions(vector& l_vec) { m_divisions.check_bounded_divisions(); } -lbool core::check(vector& l_vec) { +bool core::can_add_bound(unsigned j, u_map& bounds) { + unsigned count = 1; + if (bounds.find(j, count)) + ++count; + bounds.insert(j, count); + struct decrement : public trail { + u_map& bounds; + unsigned j; + decrement(u_map& bounds, unsigned j): + bounds(bounds), + j(j) + {} + void undo() override { + --bounds[j]; + } + }; + trail().push(decrement(bounds, j)); + return count < 3; +} + +void core::add_bounds() { + unsigned r = random(), sz = m_to_refine.size(); + for (unsigned k = 0; k < sz; k++) { + lpvar i = m_to_refine[(k + r) % sz]; + auto const& m = m_emons[i]; + for (lpvar j : m.vars()) { + //m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n"; + if (var_is_free(j)) + m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); + else if (has_lower_bound(j) && can_add_bound(j, m_lower_bounds_added)) + m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::LE, get_lower_bound(j))); + else if (has_upper_bound(j) && can_add_bound(j, m_upper_bounds_added)) + m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::GE, get_upper_bound(j))); + else + continue; + ++lp_settings().stats().m_nla_bounds; + return; + } + } +} + +lbool core::check(vector& lits, vector& l_vec) { lp_settings().stats().m_nla_calls++; TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";); m_lar_solver.get_rid_of_inf_eps(); m_lemma_vec = &l_vec; + m_literal_vec = &lits; if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE)) { TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";); @@ -1524,15 +1567,30 @@ lbool core::check(vector& l_vec) { bool run_horner = need_run_horner(); bool run_bounded_nlsat = should_run_bounded_nlsat(); + + if (l_vec.empty() && !done()) m_monomial_bounds(); + + + auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); }; + - if (l_vec.empty() && !done() && run_horner) - m_horner.horner_lemmas(); - - if (l_vec.empty() && !done() && run_grobner) - m_grobner(); + { + std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; + std::function check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); }; + std::function check3 = [&]() { if (no_effect()) add_bounds(); }; + std::pair> checks[] = + { {1, check1}, + {1, check2}, + {1, check3} }; + check_weighted(3, checks); + if (!l_vec.empty() || !lits.empty()) + return l_false; + } + + if (l_vec.empty() && !done()) m_basics.basic_lemma(true); @@ -1542,14 +1600,6 @@ lbool core::check(vector& l_vec) { if (l_vec.empty() && !done()) m_divisions.check(); -#if 0 - if (l_vec.empty() && !done() && !run_horner) - m_horner.horner_lemmas(); - - if (l_vec.empty() && !done() && !run_grobner) - m_grobner(); -#endif - if (!conflict_found() && !done() && run_bounded_nlsat) ret = bounded_nlsat(); @@ -1633,8 +1683,9 @@ bool core::no_lemmas_hold() const { } lbool core::test_check(vector& l) { + vector lits; m_lar_solver.set_status(lp::lp_status::OPTIMAL); - return check(l); + return check(lits, l); } std::ostream& core::print_terms(std::ostream& out) const { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e627f9d0a..800701308 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -84,6 +84,7 @@ class core { reslimit& m_reslim; std::function m_relevant; vector * m_lemma_vec; + vector * m_literal_vec = nullptr; lp::u_set m_to_refine; tangents m_tangents; basics m_basics; @@ -111,6 +112,10 @@ class core { void check_weighted(unsigned sz, std::pair>* checks); + u_map m_lower_bounds_added, m_upper_bounds_added; + bool can_add_bound(unsigned j, u_map& bounds); + void add_bounds(); + public: // constructor core(lp::lar_solver& s, reslimit&); @@ -381,7 +386,7 @@ public: bool conflict_found() const; - lbool check(vector& l_vec); + lbool check(vector& ineqs, vector& l_vec); lbool check_power(lpvar r, lpvar x, lpvar y, vector& l_vec); void check_bounded_divisions(vector&); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 0c3c98f1d..2fae62426 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -33,6 +33,9 @@ namespace nla { } void grobner::operator()() { + if (m_quota == 0) { + m_quota = 2*c().m_nla_settings.grobner_quota; + } if (m_quota <= c().m_nla_settings.grobner_quota) { ++m_quota; return; @@ -66,12 +69,12 @@ namespace nla { } - m_quota -= 3; + // m_quota -= 3; TRACE("grobner", tout << "saturated\n"); - IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << m_quota << "\n"); + IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n"); IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream())); #if 0 @@ -93,7 +96,7 @@ namespace nla { lp_settings().stats().m_grobner_conflicts++; TRACE("grobner", m_solver.display(tout)); - IF_VERBOSE(2, if (conflicts > 0) verbose_stream() << "grobner conflict\n"); + IF_VERBOSE(3, if (conflicts > 0) verbose_stream() << "grobner conflict\n"); return conflicts > 0; } @@ -184,8 +187,6 @@ namespace nla { if (vars.empty() || !q.is_linear()) return false; - // IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n"); - term t; while (!q.is_val()) { t.add_monomial(q.hi().val(), q.var()); @@ -287,15 +288,15 @@ namespace nla { lo_t.add_monomial(coeff, m.vars[0]); } else if (c().find_canonical_monic_of_vars(m.vars, j)) { - verbose_stream() << "canonical monic\n"; + //verbose_stream() << "canonical monic\n"; lo_t.add_monomial(coeff, j); } else return false; } - c().m_intervals.display(verbose_stream(), i); verbose_stream() << "\n"; - c().print_ineq(ineq(lo_t, lp::EQ, k), verbose_stream()) << "\n"; + //c().m_intervals.display(verbose_stream(), i); verbose_stream() << "\n"; + //c().print_ineq(ineq(lo_t, lp::EQ, k), verbose_stream()) << "\n"; new_lemma lemma(c(), "pdd-gcd"); add_dependencies(lemma, eq); @@ -306,7 +307,7 @@ namespace nla { lemma &= e; lemma |= ineq(lo_t, lp::EQ, k); - verbose_stream() << lemma << "\n"; + //verbose_stream() << lemma << "\n"; return true; } @@ -339,13 +340,13 @@ namespace nla { } } catch (...) { - IF_VERBOSE(2, verbose_stream() << "pdd throw\n"); + IF_VERBOSE(3, verbose_stream() << "pdd throw\n"); return; } TRACE("grobner", m_solver.display(tout)); #if 0 - IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream())); + IF_VERBOSE(3, m_pdd_grobner.display(verbose_stream())); dd::pdd_eval eval(m_pdd_manager); eval.var2val() = [&](unsigned j){ return val(j); }; for (auto* e : m_pdd_grobner.equations()) { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index df5862f62..66ab571fb 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -276,7 +276,7 @@ void intervals::set_var_interval(lpvar v, interval& b) { } if (ls().column_corresponds_to_term(v)) { - auto const& lt = ls().column_to_term(v); + auto const& lt = ls().column_index_to_term(v); scoped_dep_interval ti(m_dep_intervals), r(m_dep_intervals); if (interval_from_lar_term(lt, ti)) { m_dep_intervals.intersect(b, ti, r); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index bd0f1953c..9b3f3a762 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -45,8 +45,8 @@ namespace nla { bool solver::need_check() { return m_core->has_relevant_monomial(); } - lbool solver::check(vector& l) { - return m_core->check(l); + lbool solver::check(vector& lits, vector& lemmas) { + return m_core->check(lits, lemmas); } void solver::push(){ diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index d04ff8e51..09d8191ce 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -38,7 +38,7 @@ namespace nla { void push(); void pop(unsigned scopes); bool need_check(); - lbool check(vector&); + lbool check(vector& lits, vector&); lbool check_power(lpvar r, lpvar x, lpvar y, vector&); bool is_monic_var(lpvar) const; bool influences_nl_var(lpvar) const; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index f4693e1e8..24cfd4b46 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1414,30 +1414,40 @@ namespace arith { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); literal_vector core; - for (auto const& ineq : m_lemma.ineqs()) { - bool is_lower = true, pos = true, is_eq = false; - switch (ineq.cmp()) { - case lp::LE: is_lower = false; pos = false; break; - case lp::LT: is_lower = true; pos = true; break; - case lp::GE: is_lower = true; pos = false; break; - case lp::GT: is_lower = false; pos = true; break; - case lp::EQ: is_eq = true; pos = false; break; - case lp::NE: is_eq = true; pos = true; break; - default: UNREACHABLE(); - } - TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";); - // TBD utility: lp::lar_term term = mk_term(ineq.m_poly); - // then term is used instead of ineq.m_term - sat::literal lit; - if (is_eq) - lit = mk_eq(ineq.term(), ineq.rs()); - else - lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower)); - core.push_back(pos ? lit : ~lit); - } + for (auto const& ineq : m_lemma.ineqs()) + core.push_back(mk_ineq_literal(ineq)); set_conflict_or_lemma(core, false); } + void solver::assume_literals() { + for (auto const& ineq : m_nla_literals) + s().set_phase(mk_ineq_literal(ineq)); + } + + sat::literal solver::mk_ineq_literal(nla::ineq const& ineq) { + bool is_lower = true, pos = true, is_eq = false; + switch (ineq.cmp()) { + case lp::LE: is_lower = false; pos = false; break; + case lp::LT: is_lower = true; pos = true; break; + case lp::GE: is_lower = true; pos = false; break; + case lp::GT: is_lower = false; pos = true; break; + case lp::EQ: is_eq = true; pos = false; break; + case lp::NE: is_eq = true; pos = true; break; + default: UNREACHABLE(); + } + TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";); + // TBD utility: lp::lar_term term = mk_term(ineq.m_poly); + // then term is used instead of ineq.m_term + sat::literal lit; + if (is_eq) + lit = mk_eq(ineq.term(), ineq.rs()); + else + lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower)); + + return pos ? lit : ~lit; + } + + lbool solver::check_nla() { if (!m.inc()) { TRACE("arith", tout << "canceled\n";); @@ -1450,9 +1460,10 @@ namespace arith { return l_true; m_a1 = nullptr; m_a2 = nullptr; - lbool r = m_nla->check(m_nla_lemma_vector); + lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector); switch (r) { - case l_false: + case l_false: + assume_literals(); for (const nla::lemma& l : m_nla_lemma_vector) false_case_of_check_nla(l); break; diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 68d5f8025..076ff1308 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -253,6 +253,7 @@ namespace arith { // lemmas lp::explanation m_explanation; vector m_nla_lemma_vector; + vector m_nla_literals; literal_vector m_core, m_core2; svector m_eqs; vector m_params; @@ -465,6 +466,8 @@ namespace arith { void set_evidence(lp::constraint_index idx); void assign(literal lit, literal_vector const& core, svector const& eqs, euf::th_proof_hint const* pma); + void assume_literals(); + sat::literal mk_ineq_literal(nla::ineq const& ineq); void false_case_of_check_nla(const nla::lemma& l); void dbg_finalize_model(model& mdl); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6f85b50b1..c822b7caf 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2556,44 +2556,54 @@ public: } nla::lemma m_lemma; - + + literal mk_literal(nla::ineq const& ineq) { + bool is_lower = true, pos = true, is_eq = false; + switch (ineq.cmp()) { + case lp::LE: is_lower = false; pos = false; break; + case lp::LT: is_lower = true; pos = true; break; + case lp::GE: is_lower = true; pos = false; break; + case lp::GT: is_lower = false; pos = true; break; + case lp::EQ: is_eq = true; pos = false; break; + case lp::NE: is_eq = true; pos = true; break; + default: UNREACHABLE(); + } + TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";); + app_ref atom(m); + // TBD utility: lp::lar_term term = mk_term(ineq.m_poly); + // then term is used instead of ineq.m_term + if (is_eq) + atom = mk_eq(ineq.term(), ineq.rs()); + else + // create term >= 0 (or term <= 0) + atom = mk_bound(ineq.term(), ineq.rs(), is_lower); + return literal(ctx().get_bool_var(atom), pos); + } + void false_case_of_check_nla(const nla::lemma & l) { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); literal_vector core; for (auto const& ineq : m_lemma.ineqs()) { - bool is_lower = true, pos = true, is_eq = false; - switch (ineq.cmp()) { - case lp::LE: is_lower = false; pos = false; break; - case lp::LT: is_lower = true; pos = true; break; - case lp::GE: is_lower = true; pos = false; break; - case lp::GT: is_lower = false; pos = true; break; - case lp::EQ: is_eq = true; pos = false; break; - case lp::NE: is_eq = true; pos = true; break; - default: UNREACHABLE(); - } - TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";); - app_ref atom(m); - // TBD utility: lp::lar_term term = mk_term(ineq.m_poly); - // then term is used instead of ineq.m_term - if (is_eq) { - atom = mk_eq(ineq.term(), ineq.rs()); - } - else { - // create term >= 0 (or term <= 0) - atom = mk_bound(ineq.term(), ineq.rs(), is_lower); - } - literal lit(ctx().get_bool_var(atom), pos); + auto lit = mk_literal(ineq); core.push_back(~lit); } set_conflict_or_lemma(core, false); } + + void assume_literal(nla::ineq const& i) { + auto lit = mk_literal(i); + ctx().set_true_first_flag(lit.var()); + } final_check_status check_nla_continue() { m_a1 = nullptr; m_a2 = nullptr; - lbool r = m_nla->check(m_nla_lemma_vector); + lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector); + for (const nla::ineq& i : m_nla_literals) + return (assume_literal(i), FC_CONTINUE); + switch (r) { - case l_false: + case l_false: for (const nla::lemma & l : m_nla_lemma_vector) false_case_of_check_nla(l); return FC_CONTINUE; @@ -3751,6 +3761,7 @@ public: lp::explanation m_explanation; vector m_nla_lemma_vector; + vector m_nla_literals; literal_vector m_core; svector m_eqs; vector m_params;