Imp fix (#10304)

For every row with only one non-fixed variable in nla_core.cpp,
core::propagate, fix this variable.

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>

src/math/lp/lar_solver.cpp

@@ -1150,6 +1150,38 @@ namespace lp {
             ex.push_back(ci);
     }
 
+    u_dependency* lar_solver::get_bound_constraint_witnesses_for_fixed_in_row(unsigned row_index) {
+        u_dependency* dep = nullptr;
+        for (auto const& e : get_row(row_index))
+            if (column_is_fixed(e.var()))
+                dep = join_deps(dep, get_bound_constraint_witnesses_for_column(e.var()));
+        return dep;
+    }
+
+    /**
+       \brief A row is an equality sum_j a_j x_j = 0. If every column in it is fixed
+       except one, that row determines the remaining column: a_k x_k = - sum_{j != k} a_j v_j.
+       Set j to that column and value to -(sum a_j v_j) / a_k, and return true.
+    */
+    bool lar_solver::row_determines_column(unsigned row_index, lpvar& j, mpq& value) const {
+        j = null_lpvar;
+        mpq coeff, sum(0);
+        for (auto const& e : get_row(row_index)) {
+            if (column_is_fixed(e.var())) {
+                sum += e.coeff() * get_lower_bound(e.var()).x;
+                continue;
+            }
+            if (j != null_lpvar)
+                return false;
+            j = e.var();
+            coeff = e.coeff();
+        }
+        if (j == null_lpvar || coeff.is_zero())
+            return false;
+        value = -sum / coeff;
+        return true;
+    }
+
     void lar_solver::remove_fixed_vars_from_base() {
         // this will allow to disable and restore the tracking of the touched rows
         flet<indexed_uint_set*> f(get_core_solver().m_r_solver.m_touched_rows, nullptr);

src/math/lp/lar_solver.h

@@ -516,6 +516,9 @@ public:
         return dep;
     }
 
+    u_dependency* get_bound_constraint_witnesses_for_fixed_in_row(unsigned row_index);
+    bool row_determines_column(unsigned row_index, lpvar& j, mpq& value) const;
+
     std::ostream& print_expl(std::ostream& out, const explanation& exp) const {
         for (auto p : exp)
             constraints().display(

src/math/lp/monomial_bounds.cpp

@@ -677,6 +677,62 @@ namespace nla {
         return new_bound;
     }
 
+    /**
+       \brief Fix the columns determined by rows that are already all but fixed.
+
+       lar_solver::row_determines_column finds a row in which every column but one
+       is fixed together with the value that row forces on the remaining column;
+       both bounds of that column are then set to it. This is constant folding
+       over the row, with no simplex involved.
+
+       Only columns occurring in a monomial are considered: the point is the
+       effect on nonlinear reasoning, not tighter arithmetic in general.
+       is_linear takes a monic with at most one non-fixed factor out of nonlinear
+       reasoning altogether, so fixing one column can linearize every monomial it
+       occurs in at once. lar_solver does not derive these values on its own,
+       since it only analyzes rows touched by a pivot and theory_lra drops an
+       implied bound with no matching atom.
+
+       Only one pass is made. A fixpoint loop would find strictly more, but this
+       runs on every nonlinear propagation, so a later round mostly finds what the
+       next call would have found anyway. Fixing every determined column measured
+       better than capping how many one call may fix.
+    */
+    bool monomial_bounds::propagate_fixed_rows() {
+        auto& lra = c().lra;
+        if (!c().params().arith_nl_propagate_fixed_rows())
+            return false;
+
+        indexed_uint_set nl_vars;
+        for (auto const& m : c().emons()) {
+            nl_vars.insert(m.var());
+            for (lpvar k : m.vars())
+                nl_vars.insert(k);
+        }
+
+        bool propagated = false;
+        for (unsigned i = 0; i < lra.row_count(); ++i) {
+            if (lra.get_row(i).size() > 32)
+                continue;
+            lpvar free_j;
+            rational value;
+            if (!lra.row_determines_column(i, free_j, value))
+                continue;
+            if (!nl_vars.contains(free_j))
+                continue;
+            if (lra.column_has_lower_bound(free_j) && lra.column_has_upper_bound(free_j) &&
+                lra.get_lower_bound(free_j).x == value && lra.get_upper_bound(free_j).x == value)
+                continue;
+            u_dependency* dep = lra.get_bound_constraint_witnesses_for_fixed_in_row(i);
+            lra.update_column_type_and_bound(free_j, lp::lconstraint_kind::GE, value, dep);
+            lra.update_column_type_and_bound(free_j, lp::lconstraint_kind::LE, value, dep);
+            propagated = true;
+        }
+        if (propagated)
+            lra.find_feasible_solution();
+        return propagated;
+    }
+
     // ================================================================
     // max_min: incremental LP bound optimization.
     //

src/math/lp/monomial_bounds.h

@@ -89,6 +89,7 @@ namespace nla {
         void generate_lemmas();
         bool tighten_lp_bounds();
         bool propagate_changed_bounds();
+        bool propagate_fixed_rows();
 
         // Maximize (is_lower == false) or minimize (is_lower == true) column j
         // over the LP tableau and, if the resulting bound improves j's current

src/math/lp/nla_core.cpp

@@ -1540,8 +1540,12 @@ void core::set_use_nra_model(bool m) {
     
 bool core::propagate() {
     clear();
-    bool propagated = m_monomial_bounds.tighten_lp_bounds();
-    if (m_monomial_bounds.propagate_changed_bounds())
+	bool propagated = false;
+    if (m_monomial_bounds.propagate_fixed_rows())
+        propagated = true;
+    if (m_monomial_bounds.tighten_lp_bounds())
+		propagated = true;
+    if (m_monomial_bounds.propagate_changed_bounds()) 
         propagated = true;
     m_monics_with_changed_bounds.reset();
     if (propagated)

src/params/smt_params_helper.pyg

@@ -101,6 +101,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
                           ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
                           ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
+                          ('arith.nl.propagate_fixed_rows', BOOL, True, 'scan LP rows for fixed variables'), 
                           ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'),
                           ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                           ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),