throttle monomial unit prop and and nl params

Z3Prover · Sep 25, 2023 · 6ff4856 · 6ff4856
1 parent 896aba3
commit 6ff4856
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 3 deletions.
diff --git 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<lpvar>& 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<lpvar>& 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
@@ -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<unsigned, std::function<void(void)>>* checks);
     void add_bounds();
     std_vector<lp::implied_bound> & m_implied_bounds;
@@ -438,6 +438,7 @@ class core {
     bool is_linear(const svector<lpvar>& 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<lpvar>& vars, lpvar non_fixed, const rational& k);
+    void core::propagate_monic_non_fixed_with_lemma(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);
     void propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k);
     void add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);
     void add_upper_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);    

diff --git 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
@@ -3209,7 +3209,7 @@ class theory_lra::imp {
     svector<enode_pair> m_eqs;
     vector<parameter>   m_params;
 
-    void reset_evidence() {
+        void reset_evidence() {
         m_core.reset();
         m_eqs.reset();
         m_params.reset();