diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 702030c49..415544450 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1419,6 +1419,12 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul return BR_REWRITE1; } + // mod x -y = mod x y + if (m_util.is_mul(arg2, t1, t2) && m_util.is_numeral(t1, v1) && v1 == -1) { + result = m_util.mk_mod(arg1, t2); + return BR_REWRITE1; + } + return BR_FAILED; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index e039f8dc7..2f1bd85da 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -54,6 +54,7 @@ namespace nla { if (m_delay > 0) { --m_delay; + TRACE(grobner, tout << "delay " << m_delay << "\n"); return; } @@ -71,20 +72,20 @@ namespace nla { if (is_conflicting()) return; - if (propagate_eqs()) - return; - - if (propagate_factorization()) - return; - - if (propagate_linear_equations()) - return; - if (propagate_quotients()) return; if (propagate_gcd_test()) return; + + if (propagate_eqs()) + return; + + if (propagate_factorization()) + return; + + if (propagate_linear_equations()) + return; } catch (...) { @@ -147,9 +148,10 @@ namespace nla { ineq new_eq(v, llc::EQ, rational::zero()); if (c().ineq_holds(new_eq)) return false; - lemma_builder lemma(c(), "pdd-eq"); + lemma_builder lemma(c(), "grobner-eq"); add_dependencies(lemma, eq); lemma |= new_eq; + TRACE(grobner, lemma.display(tout);); return true; } if (p.is_offset()) { @@ -164,9 +166,10 @@ namespace nla { ineq new_eq(term(a, v), llc::EQ, b); if (c().ineq_holds(new_eq)) return false; - lemma_builder lemma(c(), "pdd-eq"); + lemma_builder lemma(c(), "grobner-eq"); add_dependencies(lemma, eq); lemma |= new_eq; + TRACE(grobner, lemma.display(tout);); return true; } @@ -196,7 +199,7 @@ namespace nla { if (c().ineq_holds(i)) return false; - lemma_builder lemma(c(), "pdd-factored"); + lemma_builder lemma(c(), "grobner-factored"); add_dependencies(lemma, eq); for (auto const& i : ineqs) lemma |= i; @@ -277,6 +280,8 @@ namespace nla { }; for (auto [x, k] : m_powers) { SASSERT(k > 1); + if (k > 4) // cut off at larger exponents. + continue; bool gcd_fail = true; dd::pdd kx = m.mk_var(x) * m.mk_val(k); for (unsigned r = 0; gcd_fail && r < k; r++) { @@ -286,7 +291,7 @@ namespace nla { gcd_fail = false; } if (gcd_fail) { - lemma_builder lemma(c(), "pdd-power"); + lemma_builder lemma(c(), "grobner-gcd-test"); add_dependencies(lemma, eq); return true; } @@ -329,6 +334,7 @@ namespace nla { eval.var2val() = [&](unsigned j) { return val(j); }; if (eval(p) == 0) return false; + TRACE(grobner, tout << "propagate_quotients " << p << "\n"); tracked_uint_set nl_vars; rational d(1); for (auto const& m : p) { @@ -339,6 +345,7 @@ namespace nla { nl_vars.insert(j); } + bool found_lemma = false; for (auto v : nl_vars) { auto& m = p.manager(); dd::pdd lc(m), r(m); @@ -364,70 +371,87 @@ namespace nla { continue; auto [t, offset] = linear_to_term(lc); auto [t2, offset2] = linear_to_term(r); - lemma_builder lemma(c(), "pdd-quotient"); + lemma_builder lemma(c(), "grobner-quotient"); add_dependencies(lemma, eq); // v = 0 or lc = 0 or r != 0 lemma |= ineq(v, llc::EQ, rational::zero()); lemma |= ineq(t, llc::EQ, -offset); lemma |= ineq(t2, llc::NE, -offset2); - return true; + TRACE(grobner, lemma.display(tout << "quotient1\n")); + found_lemma = true; + continue; } // r_value != 0 if (v_value == 0) { // v = 0 => r = 0 - lemma_builder lemma(c(), "pdd-quotient"); + lemma_builder lemma(c(), "grobner-quotient"); add_dependencies(lemma, eq); auto [t, offset] = linear_to_term(r); lemma |= ineq(v, llc::NE, rational::zero()); lemma |= ineq(t, llc::EQ, -offset); - return true; + TRACE(grobner, lemma.display(tout << "quotient2\n")); + found_lemma = true; + continue; } if (lc_value == 0) { if (!lc.is_linear()) continue; // lc = 0 => r = 0 - lemma_builder lemma(c(), "pdd-quotient"); + lemma_builder lemma(c(), "grobner-quotient"); add_dependencies(lemma, eq); auto [t, offset] = linear_to_term(lc); auto [t2, offset2] = linear_to_term(r); lemma |= ineq(t, llc::NE, -offset); lemma |= ineq(t2, llc::EQ, -offset2); - return true; + TRACE(grobner, lemma.display(tout << "quotient3\n")); + found_lemma = true; + continue; } if (divides(v_value, r_value)) continue; if (abs(v_value) > abs(r_value)) { // v*c + r = 0 & v > 0 => r >= v or -r >= v or r = 0 - lemma_builder lemma(c(), "pdd-quotient"); + lemma_builder lemma(c(), "grobner-quotient"); auto [t, offset] = linear_to_term(r); add_dependencies(lemma, eq); - if (v_value > 0) { - lemma |= ineq(v, llc::LE, rational::zero()); - lemma |= ineq(t, llc::EQ, -offset); + if (v_value > 0 && r_value > 0) { + // v*c + t = 0 => v <= 0 or v <= t or t <= 0 + lemma |= ineq(v, llc::LE, rational::zero()); // v <= 0 + lemma |= ineq(t, llc::LE, -offset); // t <= 0 t.add_monomial(rational(-1), v); - lemma |= ineq(t, llc::GE, -offset); - auto [t2, offset2] = linear_to_term(-r); - t2.add_monomial(rational(-1), v); - lemma |= ineq(t2, llc::GE, -offset2); + lemma |= ineq(t, llc::GE, -offset); // t - v >= 0 } - else { - // v*lc + r = 0 & v < 0 => r <= v or -r <= v or r = 0 - lemma |= ineq(v, llc::GE, rational::zero()); - lemma |= ineq(t, llc::EQ, -offset); + else if (v_value > 0 && r_value < 0) { + // v*c + t = 0 => v <= 0 or v <= -t or t >= 0 + lemma |= ineq(v, llc::LE, rational::zero()); // v <= 0 + lemma |= ineq(t, llc::GE, -offset); // t >= 0 + t.add_monomial(rational(1), v); + lemma |= ineq(t, llc::LE, -offset); // t + v <= 0 + } + else if (v_value < 0 && r_value > 0) { + // v*c + t = 0 => v >= 0 or -v <= t or t <= 0 + lemma |= ineq(v, llc::GE, rational::zero()); // v >= 0 + lemma |= ineq(t, llc::LE, -offset); // t <= 0 + t.add_monomial(rational(1), v); + lemma |= ineq(t, llc::GE, -offset); // t + v >= 0 + } + else if (v_value < 0 && r_value < 0) { + // v*c + t = 0 => v >= 0 or v >= t or t >= 0 + lemma |= ineq(v, llc::GE, rational::zero()); // v >= 0 + lemma |= ineq(t, llc::GE, -offset); // t >= 0 t.add_monomial(rational(-1), v); - lemma |= ineq(t, llc::LE, -offset); - auto [t2, offset2] = linear_to_term(-r); - t2.add_monomial(rational(-1), v); - lemma |= ineq(t2, llc::LE, -offset2); + lemma |= ineq(t, llc::LE, -offset); // t - v <= 0 } - return true; + TRACE(grobner, lemma.display(tout << "quotient4\n")); + found_lemma = true; + continue; } // other division lemmas are possible. // also extend to non-linear r, non-linear lc } - - return false; + CTRACE(grobner, !found_lemma, tout << "no lemmas found for " << p << "\n"); + return found_lemma; } void grobner::explain(dd::solver::equation const& eq, lp::explanation& exp) { @@ -542,24 +566,11 @@ namespace nla { }; scoped_dep_interval i(di), i_wd(di); evali.get_interval(e.poly(), i); - if (!di.separated_from_zero(i)) { - TRACE(grobner, m_solver.display(tout << "not separated from 0 ", e) << "\n"; - evali.get_interval_distributed(e.poly(), i); - tout << "separated from 0: " << di.separated_from_zero(i) << "\n"; - for (auto j : e.poly().free_vars()) { - scoped_dep_interval a(di); - c().m_intervals.set_var_interval(j, a); - c().m_intervals.display(tout << "j" << j << " ", a); tout << " "; - } - tout << "\n"); - - - if (add_horner_conflict(e)) + if (!di.separated_from_zero(i)) { + if (add_horner_conflict(e)) { + TRACE(grobner, m_solver.display(tout << "horner conflict ", e) << "\n"); return true; -#if 0 - if (add_nla_conflict(e)) - return true; -#endif + } return false; } evali.get_interval(e.poly(), i_wd); @@ -572,10 +583,6 @@ namespace nla { return true; } else { -#if 0 - if (add_nla_conflict(e)) - return true; -#endif TRACE(grobner, m_solver.display(tout << "no conflict ", e) << "\n"); return false; } @@ -662,7 +669,7 @@ namespace nla { if (!lra.var_is_int(k)) continue; // free integer columns are ignored unless m_add_all_eqs is set or we are doing gcd test. - if (!m_add_all_eqs && !m_config.m_gcd_test) + if (!m_add_all_eqs && !m_config.m_gcd_test && !m_config.m_propagate_quotients) continue; // a free integer column with integer coefficients can be assigned. if (!m_add_all_eqs && all_of(c().lra.get_row(row), [&](auto& ri) { return ri.coeff().is_int();})) diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 61f2f3234..d66318efa 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -88,6 +88,5 @@ namespace nla { grobner(core *core); void operator()(); void updt_params(params_ref const& p); - // dd::solver::equation_vector const& core_equations(bool all_eqs); }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a4e861008..39d0df70b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -601,6 +601,12 @@ class theory_lra::imp { ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params); } + void mk_clause(literal l1, literal l2, literal l3, literal l4, unsigned num_params, parameter* params) { + literal clause[4] = { l1, l2, l3, l4 }; + TRACE(arith, ctx().display_literals_smt2(tout, 4, clause); tout << "\n";); + ctx().mk_th_axiom(get_id(), 4, clause, num_params, params); + } + bool reflect(app* n) const { return params().m_arith_reflect || a.is_underspecified(n); @@ -1288,6 +1294,7 @@ public: else { expr_ref mone(a.mk_int(-1), m); + expr_ref minus_q(a.mk_mul(mone, q), m); literal eqz = mk_literal(m.mk_eq(q, zero)); literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); @@ -1296,12 +1303,13 @@ public: // q = 0 or (p mod q) >= 0 // q >= 0 or (p mod q) + q <= -1 // q <= 0 or (p mod q) - q <= -1 - // (p mod q) = (p mod -q) mk_axiom(eqz, eq); mk_axiom(eqz, mod_ge_0); - mk_axiom(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, a.mk_mul(mone, q)), mone))); + mk_axiom(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, minus_q), mone))); mk_axiom(mk_literal(a.mk_ge(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, q), mone))); + + expr* x = nullptr, * y = nullptr; if (false && !(a.is_mul(q, x, y) && mone == x)) mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_mul(mone, q))))); @@ -1420,12 +1428,21 @@ public: } } + void mk_axiom(literal l1, literal l2, literal l3, literal l4) { + mk_clause(l1, l2, l3, l4, 0, nullptr); + if (ctx().relevancy()) { + ctx().mark_as_relevant(l1); + ctx().mark_as_relevant(l2); + ctx().mark_as_relevant(l3); + ctx().mark_as_relevant(l4); + } + } + literal mk_literal(expr* e) { expr_ref pinned(e, m); TRACE(mk_bool_var, tout << pinned << " " << pinned->get_id() << "\n";); - if (!ctx().e_internalized(e)) { - ctx().internalize(e, false); - } + if (!ctx().e_internalized(e)) + ctx().internalize(e, false); return ctx().get_literal(e); }