move fixed variable propagation to nla_core/monomial_bounds

src/math/lp/monomial_bounds.cpp

@@ -16,14 +16,62 @@ namespace nla {
 
     monomial_bounds::monomial_bounds(core* c):
         common(c), 
-        dep(c->m_intervals.get_dep_intervals()) {}
+        dep(c->m_intervals.get_dep_intervals()) {
+
+        std::function<void(lpvar v)> fixed_eh = [&](lpvar v) {
+            c->trail().push(push_back_vector(m_fixed_var_trail));
+            m_fixed_var_trail.push_back(v);
+        };
+// uncomment to enable:
+//        c->lra.m_fixed_var_eh = fixed_eh;
+    }
 
     void monomial_bounds::propagate() {
         for (lpvar v : c().m_to_refine) {
             propagate(c().emon(v));
             if (add_lemma()) 
                 break;
         }
+        propagate_fixed_vars();
+    }
+
+    void monomial_bounds::propagate_fixed_vars() {
+        if (m_fixed_var_qhead == m_fixed_var_trail.size())
+            return;
+        c().trail().push(value_trail(m_fixed_var_qhead));
+        while (m_fixed_var_qhead < m_fixed_var_trail.size()) 
+            propagate_fixed_var(m_fixed_var_trail[m_fixed_var_qhead++]);        
+    }
+
+    void monomial_bounds::propagate_fixed_var(lpvar v) {
+        SASSERT(c().var_is_fixed(v));
+        TRACE("nla_solver", tout << "propagate fixed var: " << c().var_str(v) << "\n";);
+        for (auto const& m : c().emons().get_use_list(v)) 
+            propagate_fixed_var(m, v);
+    }
+
+    void monomial_bounds::propagate_fixed_var(monic const& m, lpvar v) {
+        unsigned num_free = 0;
+        lpvar free_var = null_lpvar;
+        for (auto w : m)
+            if (!c().var_is_fixed(w))
+                ++num_free, free_var = w;
+        if (num_free != 1)
+            return;
+        u_dependency* d = nullptr;
+        auto& lra = c().lra;
+        lp::mpq coeff(1);
+        for (auto w : m) {
+            if (c().var_is_fixed(w)) {
+                d = lra.join_deps(d, lra.join_deps(lra.get_column_lower_bound_witness(w), lra.get_column_upper_bound_witness(w)));
+                coeff += lra.get_column_value(w).x;
+            }
+        }
+        vector<std::pair<lp::mpq, lpvar>> coeffs;
+        coeffs.push_back({coeff, free_var});
+        coeffs.push_back({mpq(-1), v});
+        lpvar j = lra.add_term(coeffs, UINT_MAX);
+        lra.update_column_type_and_bound(j, llc::EQ, mpq(0), d);
     }
 
     bool monomial_bounds::is_too_big(mpq const& q) const {

src/math/lp/monomial_bounds.h

@@ -43,6 +43,13 @@ namespace nla {
         bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero);
         rational fixed_var_product(monic const& m, lpvar w);
         lpvar non_fixed_var(monic const& m);
+
+        // fixed variable propagation
+        unsigned m_fixed_var_qhead = 0;
+        unsigned_vector m_fixed_var_trail;
+        void propagate_fixed_vars();
+        void propagate_fixed_var(lpvar v);
+        void propagate_fixed_var(monic const& m, lpvar v);
     public:
         monomial_bounds(core* core);
         void propagate();

src/math/lp/nla_core.h

@@ -100,11 +100,15 @@ class core {
     nra::solver              m_nra;
     bool                     m_cautious_patching = true;
     lpvar                    m_patched_var = 0;
-    monic const*             m_patched_monic = nullptr;      
+    monic const*             m_patched_monic = nullptr; 
+
+
 
     void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
     void add_bounds();
 
+
+
 public:    
     // constructor
     core(lp::lar_solver& s, params_ref const& p, reslimit&);

src/smt/theory_lra.cpp

@@ -254,45 +254,6 @@ class theory_lra::imp {
         return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
     }
 
-    svector<theory_var> m_fixed_vars;
-    unsigned       m_fixed_vars_head = 0;
-
-    bool propagate_fixed_vars() {
-        if (m_fixed_vars_head == m_fixed_vars.size())
-            return false;
-        ctx().push_trail(value_trail(m_fixed_vars_head));
-        bool propagated = false;
-        while (m_fixed_vars_head < m_fixed_vars.size()) {
-            theory_var v = m_fixed_vars[m_fixed_vars_head++];
-            enode* n = th.get_enode(v);
-            for (enode* p : n->get_parents()) {
-                expr* e = p->get_expr();
-                expr* x, * y;
-                if (!a.is_mul(e, x, y))
-                    continue;
-                if (a.is_numeral(x) || a.is_numeral(y))
-                    continue;
-                if (x == n->get_expr()) 
-                    std::swap(x, y);                
-                if (y != n->get_expr())
-                    continue;
-
-                // comment out to enable propagation:
-                continue;
-
-                expr_ref k(a.mk_numeral(get_value(v), a.is_int(y)), m);
-                literal eq1 = th.mk_eq(y, k, false);
-                literal eq2 = th.mk_eq(e, a.mk_mul(x, k), false);
-                ctx().mk_th_axiom(get_id(), ~eq1, eq2);
-
-                // v2 could perform propagation directly
-                // v3 could consider multiplication of more than two variables.
-                // such as e := x * y * z. If both x, y become fixed we have e = z * value(x) * value(y)
-//                verbose_stream() << mk_bounded_pp(e, m) << " - " << mk_bounded_pp(n->get_expr(), m) << "\n";
-            }
-        }
-        return propagated;
-    }
     void ensure_nla() {
         if (!m_nla) {
             m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
@@ -913,18 +874,6 @@ class theory_lra::imp {
         lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
         m_lia = alloc(lp::int_solver, *m_solver.get());
-
-        std::function<void(lpvar)> new_fixed = [&](lpvar v) {
-            theory_var u = lp().local_to_external(v);
-            if (u == null_theory_var)
-                return;
-            expr* var = th.get_expr(u);
-            if (a.is_numeral(var))
-                return;
-            m_fixed_vars.push_back(u);
-            ctx().push_trail(push_back_vector(m_fixed_vars));
-        };
-        lp().m_fixed_var_eh = new_fixed;
     }
 
     void internalize_is_int(app * n) {
@@ -2135,7 +2084,7 @@ class theory_lra::imp {
     }
 
     bool propagate() {
-        return process_atoms() && propagate_core() && propagate_fixed_vars();
+        return process_atoms() && propagate_core();
     }
 
     bool propagate_core() {