sketch of internal propagation

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

src/math/lp/lar_solver.h

@@ -142,7 +142,9 @@ class lar_solver : public column_namer {
     void insert_to_columns_with_changed_bounds(unsigned j);
     void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
     void update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
+public:
     void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+private:
     void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
     void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
     void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);

src/math/lp/monomial_bounds.cpp

@@ -274,45 +274,47 @@ namespace nla {
         c().m_emons.set_propagated(m);
         
         rational k = fixed_var_product(m);
-        
+        lpvar w = non_fixed_var(m);
-        if (k == 0) {
+        if (w == null_lpvar)
-            ineq ineq(m.var(), lp::lconstraint_kind::EQ, 0);
+            propagate_fixed(m, k);
-            if (c().ineq_holds(ineq))
+        else
-                return;
+            propagate_nonfixed(m, k, w);
-
-            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);            
-            lemma |= ineq;
-        }
-        
     }
+
+    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);        
+    }
+
+    void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
+        vector<std::pair<lp::mpq, unsigned>> coeffs;        
+        coeffs.push_back(std::make_pair(-k, w));
+        coeffs.push_back(std::make_pair(rational::one(), m.var()));
+        lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
+        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, k, dep);
+    }
+
+    u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) {
+        u_dependency* dep = nullptr;
+        for (auto j : m.vars()) {
+            if (k == 0) {
+                if (c().var_is_fixed_to_zero(j)) {
+                    dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j));
+                    dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j));
+                    return dep;
+                }
+                continue;
+            }
+            if (c().var_is_fixed(j)) {
+                dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j));
+                dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j));
+            }
+        }
+        return dep;
+    }
+
     
     bool monomial_bounds::is_linear(monic const& m) {
         unsigned non_fixed = 0;

src/math/lp/monomial_bounds.h

@@ -25,6 +25,9 @@ namespace nla {
         bool propagate_value(dep_interval& range, lpvar v, unsigned power);
         void compute_product(unsigned start, monic const& m, scoped_dep_interval& i);
         bool propagate(monic const& m);
+        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);
         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

@@ -809,7 +809,7 @@ void core::print_stats(std::ostream& out) {
 
 void core::clear() {
     m_lemmas.clear();
-    m_literal_vec->clear();
+    m_literals.clear();
 }
     
 void core::init_search() {
@@ -1494,12 +1494,12 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
 }
 
 lbool core::check_power(lpvar r, lpvar x, lpvar y) {
-    m_lemmas.reset();
+    clear();
     return m_powers.check(r, x, y, m_lemmas);
 }
 
 void core::check_bounded_divisions() {
-    m_lemmas.reset();
+    clear();
     m_divisions.check_bounded_divisions();
 }
 // looking for a free variable inside of a monic to split
@@ -1511,18 +1511,17 @@ void core::add_bounds() {
         for (lpvar j : m.vars()) {
             if (!var_is_free(j)) continue;
             // split the free variable (j <= 0, or j > 0), and return
-            m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));  
+            m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));  
             ++lp_settings().stats().m_nla_bounds;
             return;
         }
     }    
 }
 
-lbool core::check(vector<ineq>& lits) {
+lbool core::check() {
     lp_settings().stats().m_nla_calls++;
     TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
     lra.get_rid_of_inf_eps();
-    m_literal_vec = &lits;
     if (!(lra.get_status() == lp::lp_status::OPTIMAL || 
           lra.get_status() == lp::lp_status::FEASIBLE)) {
         TRACE("nla_solver", tout << "unknown because of the lra.m_status = " << lra.get_status() << "\n";);
@@ -1542,7 +1541,7 @@ lbool core::check(vector<ineq>& lits) {
     bool run_bounded_nlsat = should_run_bounded_nlsat();
     bool run_bounds = params().arith_nl_branching();    
 
-    auto no_effect = [&]() { return !done() && m_lemmas.empty() && lits.empty(); };
+    auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty(); };
     
     if (no_effect())
         m_monomial_bounds.propagate();
@@ -1560,7 +1559,7 @@ lbool core::check(vector<ineq>& lits) {
               {1, check2},
               {1, check3} };
         check_weighted(3, checks);
-        if (!m_lemmas.empty() || !lits.empty())
+        if (!m_lemmas.empty() || !m_literals.empty())
             return l_false;
     }
                 
@@ -1639,9 +1638,8 @@ lbool core::bounded_nlsat() {
         m_nlsat_fails = 0;
         m_nlsat_delay /= 2;
     }
-    if (ret == l_true) {
+    if (ret == l_true) 
-        m_lemmas.reset();
+        clear();
-    }
     return ret;
 }
 
@@ -1655,10 +1653,10 @@ bool core::no_lemmas_hold() const {
     return true;
 }
     
+    
 lbool core::test_check() {
-    vector<ineq> lits;
     lra.set_status(lp::lp_status::OPTIMAL);
-    return check(lits);
+    return check();
 }
 
 std::ostream& core::print_terms(std::ostream& out) const {
@@ -1811,7 +1809,7 @@ bool core::improve_bounds() {
 }
     
 void core::propagate() {
-    m_lemmas.reset(); 
+    clear();
     m_monomial_bounds.unit_propagate();
 }
 

src/math/lp/nla_core.h

@@ -86,8 +86,8 @@ class core {
     smt_params_helper        m_params;
     std::function<bool(lpvar)> m_relevant;
     vector<lemma>            m_lemmas;
-    vector<ineq> *           m_literal_vec = nullptr;
+    vector<ineq>             m_literals;
-    indexed_uint_set                m_to_refine;
+    indexed_uint_set         m_to_refine;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
@@ -386,7 +386,7 @@ public:
 
     bool  conflict_found() const;
     
-    lbool check(vector<ineq>& ineqs);
+    lbool check();
     lbool check_power(lpvar r, lpvar x, lpvar y);
     void check_bounded_divisions();
 
@@ -428,7 +428,8 @@ public:
     void set_use_nra_model(bool m);
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
-    vector<nla::lemma> const& lemmas() const { return m_lemmas; } 
+    vector<nla::lemma> const& lemmas() const { return m_lemmas; }
+    vector<nla::ineq> const& literals() const { return m_literals; }
 private:
     void restore_patched_values();
     void constrain_nl_in_tableau();

src/math/lp/nla_solver.cpp

@@ -42,8 +42,8 @@ namespace nla {
     
     bool solver::need_check() { return m_core->has_relevant_monomial(); }
     
-    lbool solver::check(vector<ineq>& lits) {
+    lbool solver::check() {
-        return m_core->check(lits);
+        return m_core->check();
     }
 
     void solver::propagate() {
@@ -104,4 +104,8 @@ namespace nla {
     vector<nla::lemma> const& solver::lemmas() const {
         return m_core->lemmas();
     }
+    
+    vector<nla::ineq> const& solver::literals() const {
+        return m_core->literals();
+    }
 }

src/math/lp/nla_solver.h

@@ -36,7 +36,7 @@ namespace nla {
         void push();
         void pop(unsigned scopes);
         bool need_check();
-        lbool check(vector<ineq>& lits);
+        lbool check();
         void propagate();
         lbool check_power(lpvar r, lpvar x, lpvar y);
         bool is_monic_var(lpvar) const;
@@ -48,5 +48,6 @@ namespace nla {
         nlsat::anum const& am_value(lp::var_index v) const;
         void collect_statistics(::statistics & st);
         vector<nla::lemma> const& lemmas() const;
+        vector<nla::ineq> const& literals() const;
     };
 }

src/sat/smt/arith_solver.cpp

@@ -1416,7 +1416,7 @@ namespace arith {
     }
 
     void solver::assume_literals() {
-        for (auto const& ineq : m_nla_literals) {
+        for (auto const& ineq : m_nla->literals()) {
             auto lit = mk_ineq_literal(ineq);
             ctx.mark_relevant(lit);
             s().set_phase(lit);
@@ -1459,7 +1459,7 @@ namespace arith {
             return l_true;
 
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nla->check(m_nla_literals);
+        lbool r = m_nla->check();
         switch (r) {
         case l_false:
             assume_literals();

src/sat/smt/arith_solver.h

@@ -248,7 +248,6 @@ namespace arith {
 
         // lemmas
         lp::explanation     m_explanation;
-        vector<nla::ineq>   m_nla_literals;
         literal_vector      m_core, m_core2;
         vector<rational>    m_coeffs;
         svector<enode_pair> m_eqs;

src/smt/theory_lra.cpp

@@ -1602,8 +1602,7 @@ public:
         case l_true:
             return FC_DONE;
         case l_false:
-            for (const nla::lemma & l : m_nla->lemmas()) 
+            add_lemmas();
-                false_case_of_check_nla(l);
             return FC_CONTINUE;
         case l_undef:
             return FC_GIVEUP;
@@ -1800,8 +1799,7 @@ public:
         if (!m_nla)
             return true;
         m_nla->check_bounded_divisions();
-        for (auto & lemma : m_nla->lemmas())
+        add_lemmas();
-            false_case_of_check_nla(lemma);
         return m_nla->lemmas().empty();
     }
 
@@ -2000,7 +1998,7 @@ public:
             // create term >= 0 (or term <= 0)
             atom = mk_bound(ineq.term(), ineq.rs(), is_lower);
         return literal(ctx().get_bool_var(atom), pos);
-    }
+    }    
 
     void false_case_of_check_nla(const nla::lemma & l) {
         m_lemma = l; //todo avoid the copy
@@ -2021,14 +2019,11 @@ public:
     
     final_check_status check_nla_continue() {
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nla->check(m_nla_literals);
+        lbool r = m_nla->check();
 
         switch (r) {
         case l_false:
-            for (const nla::ineq& i : m_nla_literals)
+            add_lemmas();
-                assume_literal(i); 
-            for (const nla::lemma & l : m_nla->lemmas()) 
-                false_case_of_check_nla(l);
             return FC_CONTINUE;
         case l_true:
             return assume_eqs()? FC_CONTINUE: FC_DONE;
@@ -2158,10 +2153,16 @@ public:
     }
 
     void propagate_nla() {
-        if (!m_nla)
+        if (m_nla) {
-            return;
+            m_nla->propagate();
-        m_nla->propagate();
+            add_lemmas();
-        for (nla::lemma const& l : m_nla->lemmas())
+        }
+    }
+
+    void add_lemmas() {
+        for (const nla::ineq& i : m_nla->literals())
+            assume_literal(i); 
+        for (const nla::lemma & l : m_nla->lemmas()) 
             false_case_of_check_nla(l);
     }
 
@@ -3191,7 +3192,6 @@ public:
     }
  
     lp::explanation     m_explanation;
-    vector<nla::ineq>       m_nla_literals;
     literal_vector      m_core;
     svector<enode_pair> m_eqs;
     vector<parameter>   m_params;