add theory propagation to linear monomial propagation

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

src/math/lp/monomial_bounds.cpp

@@ -10,6 +10,7 @@
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/nla_intervals.h"
+#include "math/lp/numeric_pair.h"
 
 namespace nla {
 
@@ -281,9 +282,21 @@ namespace nla {
             propagate_nonfixed(m, k, w);
     }
 
+    lp::explanation monomial_bounds::get_explanation(u_dependency* dep) {
+        lp::explanation exp;
+        svector<lp::constraint_index> cs;
+        c().lra.dep_manager().linearize(dep, cs);
+        for (auto d : cs)
+            exp.add_pair(d, mpq(1));
+        return exp;
+    }
+
     void monomial_bounds::propagate_fixed(monic const& m, rational const& k) {
         auto* dep = explain_fixed(m, k);
-        c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);        
+        c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
+        // propagate fixed equality
+        auto exp = get_explanation(dep);
+        c().add_fixed_equality(m.var(), k, exp);
     }
 
     void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
@@ -294,6 +307,11 @@ namespace nla {
         auto* dep = explain_fixed(m, k);
         term_index = c().lra.map_term_index_to_column_index(term_index);
         c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
+
+        if (k == 1) {
+            lp::explanation exp = get_explanation(dep);
+            c().add_equality(m.var(), w, exp);
+        }
     }
 
     u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) {

src/math/lp/monomial_bounds.h

@@ -28,6 +28,7 @@ namespace nla {
         void propagate_fixed(monic const& m, rational const& k);
         void propagate_nonfixed(monic const& m, rational const& k, lpvar w);
         u_dependency* explain_fixed(monic const& m, rational const& k);
+        lp::explanation get_explanation(u_dependency* dep);
         bool propagate_down(monic const& m, dep_interval& mi, lpvar v, unsigned power, dep_interval& product);
         void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const;
         bool is_free(lpvar v) const;

src/math/lp/nla_core.cpp

@@ -810,6 +810,8 @@ void core::print_stats(std::ostream& out) {
 void core::clear() {
     m_lemmas.clear();
     m_literals.clear();
+    m_fixed_equalities.clear();
+    m_equalities.clear();
 }
 
 void core::init_search() {

src/math/lp/nla_core.h

@@ -44,7 +44,6 @@ bool try_insert(const A& elem, B& collection) {
     return true;
 }
 
-
 class core {
     friend struct common;
     friend class new_lemma;
@@ -87,6 +86,8 @@ class core {
     std::function<bool(lpvar)> m_relevant;
     vector<lemma>            m_lemmas;
     vector<ineq>             m_literals;
+    vector<equality>         m_equalities;
+    vector<fixed_equality>   m_fixed_equalities;
     indexed_uint_set         m_to_refine;
     tangents                 m_tangents;
     basics                   m_basics;
@@ -430,6 +431,11 @@ class core {
     void collect_statistics(::statistics&);
     vector<nla::lemma> const& lemmas() const { return m_lemmas; }
     vector<nla::ineq> const& literals() const { return m_literals; }
+    vector<equality> const& equalities() const { return m_equalities; }
+    vector<fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
+
+    void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
+    void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }
 private:
     void restore_patched_values();
     void constrain_nl_in_tableau();

src/math/lp/nla_solver.cpp

@@ -108,4 +108,13 @@ namespace nla {
     vector<nla::ineq> const& solver::literals() const {
         return m_core->literals();
     }
+
+    vector<nla::equality> const& solver::equalities() const {
+        return m_core->equalities();
+    }
+
+    vector<nla::fixed_equality> const& solver::fixed_equalities() const {
+        return m_core->fixed_equalities();
+    }
+
 }

src/math/lp/nla_solver.h

@@ -49,5 +49,7 @@ namespace nla {
         void collect_statistics(::statistics & st);
         vector<nla::lemma> const& lemmas() const;
         vector<nla::ineq> const& literals() const;
+        vector<nla::fixed_equality> const& fixed_equalities() const;
+        vector<nla::equality> const& equalities() const;
     };
 }

src/math/lp/nla_types.h

@@ -24,6 +24,20 @@ namespace nla {
     typedef lp::explanation          expl_set;
     typedef lp::var_index            lpvar;
     const lpvar null_lpvar = UINT_MAX;
+
+    struct equality {
+        lp::lpvar i, j;
+        lp::explanation e;
+        equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e):i(i),j(j),e(e) {}
+    };
+
+    struct fixed_equality {
+        lp::lpvar v;
+        rational       k;
+        lp::explanation e;
+        fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e):v(v),k(k),e(e) {}
+    };
+
 
     inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); }
     inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); }

src/smt/smt_conflict_resolution.cpp

@@ -601,6 +601,7 @@ namespace smt {
 
         finalize_resolve(conflict, not_l);
 
+
         return true;
     }
 

src/smt/theory_lra.cpp

@@ -2112,6 +2112,7 @@ class theory_lra::imp {
     bool propagate_core() {
         m_model_is_initialized = false;
         flush_bound_axioms();
+        // disabled in master: propagate_nla(); 
         if (!can_propagate_core())
             return false;
         m_new_def = false;        
@@ -2144,7 +2145,6 @@ class theory_lra::imp {
         case l_true:
             propagate_basic_bounds();
             propagate_bounds_with_lp_solver();
-            // propagate_nla(); 
             break;
         case l_undef:
             break;
@@ -2156,9 +2156,34 @@ class theory_lra::imp {
         if (m_nla) {
             m_nla->propagate();
             add_lemmas();
+            add_equalities();
         }
     }
 
+    void add_equalities() {
+        for (auto const& [v,k,e] : m_nla->fixed_equalities())
+            add_equality(v, k, e);
+        for (auto const& [i,j,e] : m_nla->equalities())
+            add_eq(i,j,e,false);
+    }
+
+    void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
+        verbose_stream() << "equality " << j << " " << k << "\n";
+        TRACE("arith", tout << "equality " << j << " " << k << "\n");
+        theory_var v;
+        if (k == 1)
+            v = m_one_var;
+        else if (k == 0)
+            v = m_zero_var;
+        else if (!m_value2var.find(k, v))
+            return;
+        theory_var w = lp().local_to_external(j);
+        if (w < 0)
+            return;
+        lpvar i = register_theory_var_in_lar_solver(v);
+        add_eq(i, j, exp, true);
+    }
+
     void add_lemmas() {
         for (const nla::ineq& i : m_nla->literals())
             assume_literal(i);