From 6ff4856e38fffa278c2a076ba18038199cddd12a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 25 Sep 2023 16:47:34 -0700 Subject: [PATCH] throttle monomial unit prop and and nl params --- src/math/lp/nla_core.cpp | 31 +++++++++++++++++++++++++++- src/math/lp/nla_core.h | 3 ++- src/smt/params/smt_params_helper.pyg | 2 ++ src/smt/theory_lra.cpp | 2 +- 4 files changed, 35 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 365f81774..0788510ef 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1913,6 +1913,10 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std: } void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k) { + if (params().arith_nl_use_lemmas_in_unit_prop()) { + propagate_monic_non_fixed_with_lemma(monic_var, vars, non_fixed, k); + return; + } lp::impq bound_value; bool is_strict; auto& lps = lra; @@ -2002,13 +2006,38 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std: add_lower_bound_monic(monic_var, lp::mpq(0), false, lambda); add_upper_bound_monic(monic_var, lp::mpq(0), false, lambda); } + + void core::propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k) { + lp::impq bound_value; + new_lemma lemma(*this, "propagate monic with non fixed"); + // using += to not assert thath the inequality does not hold + lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0); + lp::explanation exp; + for (auto v : m_emons[monic_var].vars()) { + if (v == non_fixed) continue; + u_dependency* dep = lra.get_column_lower_bound_witness(v); + for (auto ci : lra.flatten(dep)) { + exp.push_back(ci); + } + dep = lra.get_column_upper_bound_witness(v); + for (auto ci : lra.flatten(dep)) { + exp.push_back(ci); + } + } + lemma &= exp; + } void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var) { + m_propagated.reserve(monic_var + 1, false); + bool throttle = params().arith_nl_throttle_unit_prop(); + if (throttle && m_propagated[monic_var]) + return; lpvar non_fixed, zero_var; const auto& vars = m_emons[monic_var].vars(); if (!is_linear(vars, zero_var, non_fixed)) return; - + if (throttle) + trail().push(set_bitvector_trail(m_propagated, monic_var)); if (zero_var != null_lpvar) add_bounds_for_zero_var(monic_var, zero_var); else { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 90bfa18ca..e1fae2aff 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -114,7 +114,7 @@ class core { bool m_cautious_patching = true; lpvar m_patched_var = 0; monic const* m_patched_monic = nullptr; - + bool_vector m_propagated; void check_weighted(unsigned sz, std::pair>* checks); void add_bounds(); std_vector & m_implied_bounds; @@ -438,6 +438,7 @@ public: bool is_linear(const svector& m, lpvar& zero_var, lpvar& non_fixed); void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var); void propagate_monic_with_non_fixed(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k); + void core::propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k); void propagate_monic_with_all_fixed(lpvar monic_var, const svector& vars, const rational& k); void add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function explain_dep); void add_upper_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function explain_dep); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f059dccb8..ab9f56c96 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -71,6 +71,8 @@ def_module_params(module_name='smt', ('arith.nl.grobner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), ('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'), ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'), + ('arith.nl.use_lemmas_in_unit_prop', BOOL, False, 'use lemmas in monomial unit propagation'), + ('arith.nl.throttle_unit_prop', BOOL, True, 'unit propogate a monomial only once per scope'), ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '), ('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'), ('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3b6a71b3d..e85b2722a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3209,7 +3209,7 @@ public: svector m_eqs; vector m_params; - void reset_evidence() { + void reset_evidence() { m_core.reset(); m_eqs.reset(); m_params.reset();