re-introduce simple implementation of linear monomial propagation for evaluation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/emonics.cpp

@@ -596,7 +596,7 @@ bool emonics::invariant() const {
 }
 
 
-void emonics::set_propagated(monic& m) {
+void emonics::set_propagated(monic const& m) {
     struct set_unpropagated : public trail {
         emonics& em;
         unsigned var;
@@ -607,7 +607,7 @@ void emonics::set_propagated(monic& m) {
         }
     };
     SASSERT(!m.is_propagated());
-    m.set_propagated(true);
+    (*this)[m.var()].set_propagated(true);
     m_u_f_stack.push(set_unpropagated(*this, m.var()));
 }
 

src/math/lp/emonics.h

@@ -142,7 +142,7 @@ public:
     void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
     void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
 
-    void set_propagated(monic& m);
+    void set_propagated(monic const& m);
 
     // this method is required by union_find
     trail_stack & get_trail_stack() { return m_u_f_stack; }

src/math/lp/monomial_bounds.cpp

@@ -263,40 +263,53 @@ namespace nla {
             unit_propagate(m);
     }
 
+
     void monomial_bounds::unit_propagate(monic const& m) {
-        m_propagated.reserve(m.var() + 1, false);
-        if (m_propagated[m.var()])
+        if (m.is_propagated())
             return;
 
         if (!is_linear(m))
             return;
-        
-        c().trail().push(set_bitvector_trail(m_propagated, m.var()));
+
+        c().m_emons.set_propagated(m);
         
         rational k = fixed_var_product(m);
         
-        new_lemma lemma(c(), "fixed-values");
         if (k == 0) {
-            for (auto v : m) {
-                if (c().var_is_fixed(v) && c().val(v).is_zero()) {
-                    lemma.explain_fixed(v);
-                    break;
-                }
-            }
-            lemma |= ineq(m.var(), lp::lconstraint_kind::EQ, 0);
+            ineq ineq(m.var(), lp::lconstraint_kind::EQ, 0);
+            if (c().ineq_holds(ineq))
+                return;
+
+            lpvar zero_var = find<monic,lpvar>(m, [&](lpvar v) { return c().var_is_fixed(v) && c().val(v).is_zero(); });
+
+            IF_VERBOSE(2, verbose_stream() << "zero " << m.var() << "\n");
+            
+            new_lemma lemma(c(), "fixed-values");
+            lemma.explain_fixed(zero_var);
+            lemma |= ineq;
         }
         else {
+            lpvar w = non_fixed_var(m);
+            lp::lar_term term;
+            term.add_monomial(m.rat_sign(), m.var());
+
+            if (w != null_lpvar) {
+                IF_VERBOSE(2, verbose_stream() << "linear " << m.var() << " " << k << " " << w << "\n");
+                term.add_monomial(-k, w);
+                k = 0;
+            }
+            else 
+                IF_VERBOSE(2, verbose_stream() << "fixed " << m.var() << " " << k << "\n");
+                           
+            ineq ineq(term, lp::lconstraint_kind::EQ, k);
+            if (c().ineq_holds(ineq))
+                return;
+            
+            new_lemma lemma(c(), "linearized-fixed-values");
             for (auto v : m) 
                 if (c().var_is_fixed(v)) 
-                    lemma.explain_fixed(v);
-            
-            lpvar w = non_fixed_var(m);
-            SASSERT(w != null_lpvar);
-            
-            lp::lar_term term;
-            term.add_monomial(-m.rat_sign(), m.var());
-            term.add_monomial(k, w);
-            lemma |= ineq(term, lp::lconstraint_kind::EQ, 0);
+                    lemma.explain_fixed(v);            
+            lemma |= ineq;
         }
         
     }

src/math/lp/monomial_bounds.h

@@ -31,7 +31,6 @@ namespace nla {
         bool is_zero(lpvar v) const;
 
         // monomial propagation
-        bool_vector m_propagated;
         void unit_propagate(monic const& m);
         bool is_linear(monic const& m);
         rational fixed_var_product(monic const& m);

src/math/lp/nla_core.cpp

@@ -1811,13 +1811,8 @@ bool core::improve_bounds() {
 }
     
 void core::propagate() {
-    // disable for now
-    return;
-   // propagate linear monomials
-    m_lemmas.reset();
- 
+    m_lemmas.reset(); 
     m_monomial_bounds.unit_propagate();
-   
 }
 
 

src/smt/theory_lra.cpp

@@ -2149,9 +2149,9 @@ public:
         case l_true:
             propagate_basic_bounds();
             propagate_bounds_with_lp_solver();
+            // propagate_nla();
             break;
         case l_undef:
-            propagate_nla();
             break;
         }
         return true;            

src/util/util.h

@@ -378,6 +378,14 @@ bool all_of(S const& set, T const& p) {
     return true;
 }
 
+template<typename S, typename R>
+R find(S const& set, std::function<bool(R)> p) {
+    for (auto const& s : set)
+        if (p(s))
+            return s;
+    throw default_exception("element not found");
+}
+
 /**
    \brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]).
    it contains the current value.