Fix crash exposed in QF_UFNIA

NikolajBjorner · NikolajBjorner · commit f6e7dcff47b7 · 2025-01-24T15:31:10.000-08:00
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
@@ -543,7 +543,7 @@ namespace sls {
     bool arith_base<num_t>::find_lin_moves(sat::literal lit) {
         m_updates.reset();
         auto* ineq = get_ineq(lit.var());
-        num_t a, b;
+        num_t a(0), b(0);
         if (!ineq)
             return false;
         if (!ineq->m_is_linear) {
@@ -947,6 +947,9 @@ namespace sls {
         m_vars[v].m_def_idx = idx;
         m_vars[v].m_op = k;
         m_vars[v].set_value(val);
+        m_vars[vx].m_ops.push_back(v);
+        if (vy != vx)
+            m_vars[vy].m_ops.push_back(v);
         return v;
     }
 
@@ -1854,7 +1857,7 @@ namespace sls {
         for (auto const& [x, nl] : ineq->m_nonlinear) {
             if (is_fixed(x))
                 continue;
-            if (is_add(x) || is_mul(x))
+            if (is_add(x) || is_mul(x) || is_op(x))
                 ;
             else if (is_linear(x, nl, b))
                 find_linear_moves(*ineq, x, b);
@@ -1905,7 +1908,7 @@ namespace sls {
     bool arith_base<num_t>::find_reset_moves(sat::literal lit) {
         m_updates.reset();
         auto* ineq = get_ineq(lit.var());        
-        num_t a, b;
+        num_t a(0), b(0);
         if (!ineq)
             return false;
         for (auto const& [x, nl] : ineq->m_nonlinear) 
@@ -2853,25 +2856,6 @@ namespace sls {
         m_fixed_atoms.insert(bv);
     }
 
-    template<typename num_t>
-    void arith_base<num_t>::add_lookahead(sat::bool_var bv) {
-        auto* ineq = get_ineq(bv);
-        if (!ineq)
-            return;
-        num_t na, nb;
-        for (auto const& [x, nl] : ineq->m_nonlinear) {
-            if (is_fixed(x))
-                continue;
-            if (is_add(x) || is_mul(x))
-                ;
-            else if (is_linear(x, nl, nb))
-                find_linear_moves(*ineq, x, nb);
-            else if (is_quadratic(x, nl, na, nb))
-                find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value);
-            else
-                ;
-        }
-    }
 
     // for every variable e, for every atom containing e
     // add lookahead for e.
@@ -3211,19 +3195,21 @@ namespace sls {
         for (auto const& idx : vi.m_muls) {
             auto& [x, monomial] = m_muls[idx];
             num_t new_prod(1);
-            for (auto [w, p] : monomial) 
-                new_prod *= power_of(v == w ? new_value : value(w), p);            
+            for (auto [w, p] : monomial)
+                new_prod *= power_of(value(w), p);
             update_args_value(x, new_prod);
         }
 
         for (auto const& idx : vi.m_adds) {
             auto& ad = m_adds[idx];
             num_t new_sum(ad.m_coeff);
             for (auto [c, w] : ad.m_args)
-                new_sum += c * (v == w ? new_value : value(w));
+                new_sum += c * value(w);
             update_args_value(ad.m_var, new_sum);
         }
 
+        for (auto const& x : vi.m_ops) 
+            update_args_value(x, value1(x));        
 
         for (auto const& [coeff, bv] : vi.m_linear_occurs) {
             auto& ineq = *get_ineq(bv);
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
@@ -122,8 +122,7 @@ namespace sls {
             vector<std::pair<num_t, sat::bool_var>> m_linear_occurs;
             sat::bool_var_vector m_bool_vars_of;
             unsigned_vector m_clauses_of;
-            unsigned_vector m_muls;
-            unsigned_vector m_adds;
+            unsigned_vector m_muls, m_adds, m_ops;
             optional<bound> m_lo, m_hi;
             vector<num_t> m_finite_domain;
 
@@ -277,6 +276,7 @@ namespace sls {
 
         bool is_mul(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_MUL; }
         bool is_add(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_ADD; }
+        bool is_op(var_t v) const { return m_vars[v].m_op != arith_op_kind::LAST_ARITH_OP && m_vars[v].m_op != arith_op_kind::OP_MUL && m_vars[v].m_op != arith_op_kind::OP_ADD; }
         mul_def const& get_mul(var_t v) const { SASSERT(is_mul(v));  return m_muls[m_vars[v].m_def_idx]; }
         add_def const& get_add(var_t v) const { SASSERT(is_add(v));  return m_adds[m_vars[v].m_def_idx]; }
 
@@ -385,7 +385,6 @@ namespace sls {
         double lookahead(expr* e, bool update_score);
         void add_lookahead(bool_info& i, expr* e);
         void add_lookahead(bool_info& i, sat::bool_var bv);
-        void add_lookahead(sat::bool_var bv);
         ptr_vector<expr> const& get_fixable_exprs(expr* e);
         bool apply_move(expr* f, ptr_vector<expr> const& vars, arith_move_type t);
         expr* get_candidate_unsat();
diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
@@ -127,10 +127,30 @@ namespace sls {
         tout << "\n";);
 
         for (auto v : ctx.unsat_vars()) 
-            a.add_lookahead(v);
+            add_lookahead(v);
         
     }
 
+    template<typename num_t>
+    void arith_clausal<num_t>::add_lookahead(sat::bool_var bv) {
+        auto* ineq = a.get_ineq(bv);
+        if (!ineq)
+            return;
+        num_t na, nb;
+        for (auto const& [x, nl] : ineq->m_nonlinear) {
+            if (a.is_fixed(x))
+                continue;
+            if (a.is_add(x) || a.is_mul(x) || a.is_op(x))
+                ;
+            else if (a.is_linear(x, nl, nb))
+                a.find_linear_moves(*ineq, x, nb);
+            else if (a.is_quadratic(x, nl, na, nb))
+                a.find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value);
+            else
+                ;
+        }
+    }
+
     /**
     * \brief walk over literals that are false in some clause.
     * Try to determine if flipping them to true improves the overall score.
@@ -162,7 +182,7 @@ namespace sls {
                 --sz;
                 a.m_bool_var_atoms.swap_elems(idx, sz);
                 if (occurs_negative(bv))
-                    a.add_lookahead(bv);
+                    add_lookahead(bv);
                 else
                     ++i;
             }
@@ -171,7 +191,7 @@ namespace sls {
             for (unsigned i = 0; i < sz; ++i) {
                 bv = a.m_bool_var_atoms[i];
                 if (occurs_negative(bv))
-                    a.add_lookahead(bv);
+                    add_lookahead(bv);
             }
         }
     }
diff --git a/src/ast/sls/sls_arith_clausal.h b/src/ast/sls/sls_arith_clausal.h
@@ -64,6 +64,7 @@ namespace sls {
         void critical_move(var_t v, num_t const& delta, move_t mt);
         void lookahead(var_t v, num_t const& delta);
         double get_score(var_t v, num_t const& delta);
+        void add_lookahead(sat::bool_var bv);
         
 
         unsigned m_no_improve_bool = 0;
