From 9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Sep 2023 00:52:26 -0700
Subject: [PATCH 01/10] debug output with the variable that is fixed and its
 value

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_nl.h | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index ae0af89ec..0a2b6e938 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -765,10 +765,8 @@ typename theory_arith<Ext>::numeral theory_arith<Ext>::get_monomial_fixed_var_pr
 template<typename Ext>
 expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
     SASSERT(is_pure_monomial(m));
-    for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
-        expr * arg = to_app(m)->get_arg(i);
-        theory_var _var = expr2var(arg);
-        if (!is_fixed(_var))
+    for (expr* arg : *to_app(m)) {
+        if (!is_fixed(expr2var(arg)))
             return arg;
     }
     return nullptr;
@@ -780,7 +778,7 @@ expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
-    TRACE("non_linear", tout << "checking whether v" << v << " became linear...\n";);
+    TRACE("non_linear_verbose", tout << "checking whether v" << v << " became linear...\n";);
     if (m_data[v].m_nl_propagated)
         return false; // already propagated this monomial.
     expr * m = var2expr(v);
@@ -819,6 +817,11 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
             ctx.mark_as_relevant(rhs);
         }
         TRACE("non_linear_bug", tout << "enode: " << ctx.get_enode(rhs) << " enode_id: " << ctx.get_enode(rhs)->get_owner_id() << "\n";);
+        IF_VERBOSE(3,
+                   for (auto* arg : *to_app(m)) 
+                       if (is_fixed(expr2var(arg)))
+                           verbose_stream() << mk_pp(arg, get_manager()) << " = " << -k << "\n");
+            
         theory_var new_v = expr2var(rhs);
         SASSERT(new_v != null_theory_var);
         new_lower    = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
@@ -906,7 +909,7 @@ bool theory_arith<Ext>::propagate_linear_monomials() {
         return false;
     if (!reflection_enabled())
         return false;
-    TRACE("non_linear", tout << "propagating linear monomials...\n";);
+    TRACE("non_linear_verbose", tout << "propagating linear monomials...\n";);
     bool p = false;
     // CMW: m_nl_monomials can grow during this loop, so
     // don't use iterators.

From 7207f0ff9c1cef27432b5345b60cc4ec85f57d70 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Sep 2023 20:40:55 -0700
Subject: [PATCH 02/10] sketch of internal propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/lar_solver.h        |  2 +
 src/math/lp/monomial_bounds.cpp | 78 +++++++++++++++++----------------
 src/math/lp/monomial_bounds.h   |  3 ++
 src/math/lp/nla_core.cpp        | 26 +++++------
 src/math/lp/nla_core.h          |  9 ++--
 src/math/lp/nla_solver.cpp      |  8 +++-
 src/math/lp/nla_solver.h        |  3 +-
 src/sat/smt/arith_solver.cpp    |  4 +-
 src/sat/smt/arith_solver.h      |  1 -
 src/smt/theory_lra.cpp          | 30 ++++++-------
 10 files changed, 87 insertions(+), 77 deletions(-)

diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index fc696d4b2..275f7446d 100644
--- a/src/math/lp/lar_solver.h
+++ b/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);
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 8e4ed6cef..96e4f9ba9 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -274,45 +274,47 @@ namespace nla {
         c().m_emons.set_propagated(m);
         
         rational k = fixed_var_product(m);
-        
-        if (k == 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);            
-            lemma |= ineq;
-        }
-        
+        lpvar w = non_fixed_var(m);
+        if (w == null_lpvar)
+            propagate_fixed(m, k);
+        else
+            propagate_nonfixed(m, k, w);
     }
+
+    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;
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 74c61dd5f..ae05e2026 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/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;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index f147640b8..cf0be88fd 100644
--- a/src/math/lp/nla_core.cpp
+++ b/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) {
-        m_lemmas.reset();
-    }
+    if (ret == l_true) 
+        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();
 }
 
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index b50e43b32..ddf6d0687 100644
--- a/src/math/lp/nla_core.h
+++ b/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;
-    indexed_uint_set                m_to_refine;
+    vector<ineq>             m_literals;
+    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();
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 5417d5d63..dfbdca4e7 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/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) {
-        return m_core->check(lits);
+    lbool solver::check() {
+        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();
+    }
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 9a1bf9d14..32a3b668e 100644
--- a/src/math/lp/nla_solver.h
+++ b/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;
     };
 }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 4c6e5b4be..d64af9bb9 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/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();
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index f21e41786..6a577e753 100644
--- a/src/sat/smt/arith_solver.h
+++ b/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;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fb84b265d..1cf476db4 100644
--- a/src/smt/theory_lra.cpp
+++ b/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()) 
-                false_case_of_check_nla(l);
+            add_lemmas();
             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())
-            false_case_of_check_nla(lemma);
+        add_lemmas();
         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)
-                assume_literal(i); 
-            for (const nla::lemma & l : m_nla->lemmas()) 
-                false_case_of_check_nla(l);
+            add_lemmas();
             return FC_CONTINUE;
         case l_true:
             return assume_eqs()? FC_CONTINUE: FC_DONE;
@@ -2158,10 +2153,16 @@ public:
     }
 
     void propagate_nla() {
-        if (!m_nla)
-            return;
-        m_nla->propagate();
-        for (nla::lemma const& l : m_nla->lemmas())
+        if (m_nla) {
+            m_nla->propagate();
+            add_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;

From 65e59e3ec4ebd9c06469c15739a308d3c5f22d08 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Sep 2023 20:43:38 -0700
Subject: [PATCH 03/10] sketch of internal propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/monomial_bounds.cpp | 28 +++++++++++++++-------------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 96e4f9ba9..22b7ed6c6 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -298,19 +298,21 @@ namespace nla {
 
     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));
-            }
+        auto update_dep = [&](unsigned 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;
+        };
+
+        if (k == 0) {
+            for (auto j : m.vars()) 
+                if (c().var_is_fixed_to_zero(j)) 
+                    return update_dep(j);
+        }
+        else {
+            for (auto j : m.vars()) 
+                if (c().var_is_fixed(j))
+                    update_dep(j);
         }
         return dep;
     }

From ddcd1ee992e999e061161e4541cf70d18d8d21b1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Sep 2023 09:25:36 -0700
Subject: [PATCH 04/10] non-fixed term should have bound 0

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/monomial_bounds.cpp | 2 +-
 src/smt/theory_lra.cpp          | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 22b7ed6c6..8e049f059 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -293,7 +293,7 @@ namespace nla {
         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);
+        c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
     }
 
     u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1cf476db4..14cb12890 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2144,7 +2144,7 @@ public:
         case l_true:
             propagate_basic_bounds();
             propagate_bounds_with_lp_solver();
-            // propagate_nla();
+            // propagate_nla(); 
             break;
         case l_undef:
             break;

From 50654f1f4620bf58e132d44d3a22e48a17630922 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Sep 2023 08:52:09 +0900
Subject: [PATCH 05/10] add theory propagation to linear monomial propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/monomial_bounds.cpp     | 20 +++++++++++++++++++-
 src/math/lp/monomial_bounds.h       |  1 +
 src/math/lp/nla_core.cpp            |  2 ++
 src/math/lp/nla_core.h              |  8 +++++++-
 src/math/lp/nla_solver.cpp          |  9 +++++++++
 src/math/lp/nla_solver.h            |  2 ++
 src/math/lp/nla_types.h             | 14 ++++++++++++++
 src/smt/smt_conflict_resolution.cpp |  1 +
 src/smt/theory_lra.cpp              | 27 ++++++++++++++++++++++++++-
 9 files changed, 81 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 8e049f059..e3b14d1b7 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/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) {
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index ae05e2026..747aca9a2 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/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;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index cf0be88fd..e65829ed7 100644
--- a/src/math/lp/nla_core.cpp
+++ b/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() {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index ddf6d0687..17aa304ac 100644
--- a/src/math/lp/nla_core.h
+++ b/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 @@ public:
     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();
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index dfbdca4e7..f4d09810e 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/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();
+    }
+
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 32a3b668e..fec27c32b 100644
--- a/src/math/lp/nla_solver.h
+++ b/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;
     };
 }
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index 8169266cc..3930a62a9 100644
--- a/src/math/lp/nla_types.h
+++ b/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)); }
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index d075c0652..2561fbb5a 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -601,6 +601,7 @@ namespace smt {
 
         finalize_resolve(conflict, not_l);
 
+
         return true;
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 14cb12890..1a64d4081 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2112,6 +2112,7 @@ public:
     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 @@ public:
         case l_true:
             propagate_basic_bounds();
             propagate_bounds_with_lp_solver();
-            // propagate_nla(); 
             break;
         case l_undef:
             break;
@@ -2156,9 +2156,34 @@ public:
         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); 

From ab8fe199c59ac7721c0a8fe03c79af7aa77dd8a5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Oct 2023 18:41:23 +0900
Subject: [PATCH 06/10] fix case for 0 multiplier in monomial_bounds

disabled in master - it violates invariants in the lra solver.
---
 src/math/lp/monomial_bounds.cpp   |  7 ++++++-
 src/sat/smt/euf_proof_checker.cpp |  6 ++----
 src/smt/smt_clause_proof.cpp      | 22 +++++++++++++++-------
 src/smt/smt_clause_proof.h        |  6 +++---
 src/smt/smt_internalizer.cpp      |  6 +++---
 src/smt/theory_lra.cpp            | 13 +++++++++----
 6 files changed, 38 insertions(+), 22 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index e3b14d1b7..9bc49fc43 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -276,7 +276,7 @@ namespace nla {
         
         rational k = fixed_var_product(m);
         lpvar w = non_fixed_var(m);
-        if (w == null_lpvar)
+        if (w == null_lpvar || k == 0)
             propagate_fixed(m, k);
         else
             propagate_nonfixed(m, k, w);
@@ -293,6 +293,10 @@ namespace nla {
 
     void monomial_bounds::propagate_fixed(monic const& m, rational const& k) {
         auto* dep = explain_fixed(m, k);
+        if (!c().lra.is_base(m.var())) {
+            lp::impq val(k);
+            c().lra.set_value_for_nbasic_column(m.var(), val);
+        }
         c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
         // propagate fixed equality
         auto exp = get_explanation(dep);
@@ -300,6 +304,7 @@ namespace nla {
     }
 
     void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
+        VERIFY(k != 0);
         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()));
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index a538b2a80..42cda4bfb 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -501,8 +501,9 @@ namespace euf {
         for (expr* arg : clause)
             std::cout << "\n " << mk_bounded_pp(arg, m);
         std::cout << ")\n";
+        std::cout.flush();
 
-        if (is_rup(proof_hint)) 
+        if (false && is_rup(proof_hint)) 
             diagnose_rup_failure(clause);
             
         add_clause(clause);
@@ -527,9 +528,6 @@ namespace euf {
             for (expr* f : core)
                 std::cout << mk_pp(f, m) << "\n";
         }
-        SASSERT(false);
-        
-        exit(0);
     }
 
     void smt_proof_checker::collect_statistics(statistics& st) const {
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 777961334..bf27777c4 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -90,14 +90,14 @@ namespace smt {
         return proof_ref(m);
     }
 
-    void clause_proof::add(clause& c) {
+    void clause_proof::add(clause& c, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         justification* j = c.get_justification();
         auto st = kind2st(c.get_kind());
         auto pr = justification2proof(st, j);
         CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
-        update(c, st, pr);        
+        update(c, st, pr, simp_lits);        
     }
 
     void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
@@ -137,12 +137,15 @@ namespace smt {
         update(st, m_lits, pr);
     }
 
-    void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) {
+    void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         m_lits.reset();
         m_lits.push_back(ctx.literal2expr(lit1));
         m_lits.push_back(ctx.literal2expr(lit2));
+        if (simp_lits) 
+            for (auto lit : *simp_lits)
+                m_lits.push_back(ctx.literal2expr(~lit));
         auto st = kind2st(k);
         auto pr = justification2proof(st, j);
         update(st, m_lits, pr);
@@ -160,7 +163,7 @@ namespace smt {
     }
 
     void clause_proof::del(clause& c) {
-        update(c, status::deleted, justification2proof(status::deleted, nullptr));
+        update(c, status::deleted, justification2proof(status::deleted, nullptr), nullptr);
     }
 
     std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) {
@@ -190,7 +193,9 @@ namespace smt {
         if (ctx.get_fparams().m_clause_proof)
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
-            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());        
+            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
+        static unsigned s_count = 0;
+        
         if (m_has_log) {
             init_pp_out();
             auto& out = *m_pp_out;
@@ -220,12 +225,15 @@ namespace smt {
         }
     }
 
-    void clause_proof::update(clause& c, status st, proof* p) {
+    void clause_proof::update(clause& c, status st, proof* p, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         m_lits.reset();
         for (literal lit : c) 
-            m_lits.push_back(ctx.literal2expr(lit));        
+            m_lits.push_back(ctx.literal2expr(lit));
+        if (simp_lits) 
+            for (auto lit : *simp_lits)
+                m_lits.push_back(ctx.literal2expr(~lit));
         update(st, m_lits, p);        
     }
 
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index 1c5931136..d7cc421cf 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -68,7 +68,7 @@ namespace smt {
         void init_pp_out();
         
         void update(status st, expr_ref_vector& v, proof* p);
-        void update(clause& c, status st, proof* p);
+        void update(clause& c, status st, proof* p, literal_buffer const* simp_lits);
         status kind2st(clause_kind k);
         proof_ref justification2proof(status st, justification* j);
         void log(status st, proof* p);
@@ -79,8 +79,8 @@ namespace smt {
         clause_proof(context& ctx);
         void shrink(clause& c, unsigned new_size);
         void add(literal lit, clause_kind k, justification* j);
-        void add(literal lit1, literal lit2, clause_kind k, justification* j);
-        void add(clause& c);
+        void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr);
+        void add(clause& c, literal_buffer const* simp_lits = nullptr);
         void add(unsigned n, literal const* lits, clause_kind k, justification* j);
         void propagate(literal lit, justification const& j, literal_vector const& ante);
         void del(clause& c);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 0e9e39996..b6d1e2f2b 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1378,12 +1378,12 @@ namespace smt {
     clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) {
         TRACE("mk_clause", display_literals_verbose(tout << "creating clause: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
         m_clause_proof.add(num_lits, lits, k, j);
+        literal_buffer simp_lits;
         switch (k) {
         case CLS_TH_AXIOM:
             dump_axiom(num_lits, lits);
             Z3_fallthrough;
         case CLS_AUX: {
-            literal_buffer simp_lits;
             if (m_searching)
                 dump_lemma(num_lits, lits);
             if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) {
@@ -1451,7 +1451,7 @@ namespace smt {
                 else if (get_assignment(l2) == l_false) {
                     assign(l1, b_justification(~l2));
                 }
-                m_clause_proof.add(l1, l2, k, j);
+                m_clause_proof.add(l1, l2, k, j, &simp_lits);
                 m_stats.m_num_mk_bin_clause++;
                 return nullptr;
             }
@@ -1464,7 +1464,7 @@ namespace smt {
             bool reinit         = save_atoms;
             SASSERT(!lemma || j == 0 || !j->in_region());
             clause * cls = clause::mk(m, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.data());
-            m_clause_proof.add(*cls);
+            m_clause_proof.add(*cls, &simp_lits);
             if (lemma) {
                 cls->set_activity(activity);
                 if (k == CLS_LEARNED) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1a64d4081..96cd3dd47 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2112,7 +2112,8 @@ public:
     bool propagate_core() {
         m_model_is_initialized = false;
         flush_bound_axioms();
-        // disabled in master: propagate_nla(); 
+        // disabled in master:
+        // propagate_nla(); 
         if (!can_propagate_core())
             return false;
         m_new_def = false;        
@@ -2161,6 +2162,8 @@ public:
     }
 
     void add_equalities() {
+        if (!propagate_eqs()) 
+            return;
         for (auto const& [v,k,e] : m_nla->fixed_equalities())
             add_equality(v, k, e);
         for (auto const& [i,j,e] : m_nla->equalities())
@@ -2168,7 +2171,7 @@ public:
     }
 
     void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
-        verbose_stream() << "equality " << j << " " << k << "\n";
+        //verbose_stream() << "equality " << j << " " << k << "\n";
         TRACE("arith", tout << "equality " << j << " " << k << "\n");
         theory_var v;
         if (k == 1)
@@ -3174,8 +3177,7 @@ public:
         std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
         scoped_trace_stream _sts(th, fn);
 
-       
-        // SASSERT(validate_eq(x, y));
+        //VERIFY(validate_eq(x, y));
         ctx().assign_eq(x, y, eq_justification(js));
     }
     
@@ -3288,6 +3290,7 @@ public:
               display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto ev : m_explanation) 
             set_evidence(ev.ci(), m_core, m_eqs);
+
         
         // SASSERT(validate_conflict(m_core, m_eqs));
         if (is_conflict) {
@@ -3543,6 +3546,8 @@ public:
         lbool r = nctx.check();
         if (r == l_true) {
             nctx.display_asserted_formulas(std::cout);
+            std::cout.flush();
+            std::cout.flush();
         }
         return l_true != r;
     }

From 4133a1cc5a94e1be0b7853b46fd7efa48358e8fb Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Tue, 3 Oct 2023 02:51:02 +0200
Subject: [PATCH 07/10] Fix UP registration in final callback (#6929)

* Fix registration in final

* Don't make it too complicated...
---
 src/smt/theory_user_propagator.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 7c72419c1..6735272a1 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -62,8 +62,7 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
-
-
+    
     theory_var v = mk_var(n);
     m_var2expr.reserve(v + 1);
     m_var2expr[v] = term;
@@ -146,7 +145,7 @@ final_check_status theory_user_propagator::final_check_eh() {
         return FC_DONE;
     force_push();
     unsigned sz1 = m_prop.size();
-    unsigned sz2 = m_expr2var.size();
+    unsigned sz2 = get_num_vars();
     try {
         m_final_eh(m_user_context, this);
     }
@@ -157,7 +156,7 @@ final_check_status theory_user_propagator::final_check_eh() {
     propagate();
     CTRACE("user_propagate", ctx.inconsistent(), tout << "inconsistent\n");
     // check if it became inconsistent or something new was propagated/registered
-    bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
+    bool done = (sz1 == m_prop.size()) && (sz2 == get_num_vars()) && !ctx.inconsistent();
     return done ? FC_DONE : FC_CONTINUE;
 }
 

From b0df74c1c1f4ab17b4aba4891bd7ab9b3457b748 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Oct 2023 17:23:03 +0900
Subject: [PATCH 08/10] #6930

simplify assumptions and only replay assumptions after constraints are simplified. This allows simplifying assumptions with the current set of constraints independently of whether there is another check-sat.
---
 src/smt/theory_lra.cpp           |  6 ++++--
 src/solver/simplifier_solver.cpp | 20 ++++++++++++++++----
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 96cd3dd47..b33688209 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2113,7 +2113,10 @@ public:
         m_model_is_initialized = false;
         flush_bound_axioms();
         // disabled in master:
-        // propagate_nla(); 
+        // propagate_nla();
+        if (ctx().inconsistent())
+            return true;
+        
         if (!can_propagate_core())
             return false;
         m_new_def = false;        
@@ -3547,7 +3550,6 @@ public:
         if (r == l_true) {
             nctx.display_asserted_formulas(std::cout);
             std::cout.flush();
-            std::cout.flush();
         }
         return l_true != r;
     }
diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp
index 0c4c2a7b6..bac75f1e5 100644
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@@ -24,6 +24,7 @@ Author:
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/simplifiers/dependent_expr_state.h"
 #include "ast/simplifiers/then_simplifier.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "solver/solver.h"
 #include "solver/simplifier_solver.h"
 #include "solver/solver_preprocess.h"
@@ -62,7 +63,16 @@ class simplifier_solver : public solver {
             if (s.m.is_false(f))
                 s.set_inconsistent();
         }        
-        void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
+        void replay(unsigned qhead, expr_ref_vector& assumptions) {
+            m_reconstruction_trail.replay(qhead, assumptions, *this);
+            th_rewriter rw(s.m);
+            expr_ref tmp(s.m);
+            for (unsigned i = 0; i < assumptions.size(); ++i) {
+                tmp = assumptions.get(i);
+                rw(tmp);
+                assumptions[i] = tmp;
+            }                    
+        }
         void flatten_suffix() override {
             expr_mark seen;
             unsigned j = qhead();
@@ -109,15 +119,16 @@ class simplifier_solver : public solver {
         unsigned qhead = m_preprocess_state.qhead();
         expr_ref_vector orig_assumptions(assumptions);
         m_core_replace.reset();
-        if (qhead < m_fmls.size() || !assumptions.empty()) {
-            m_preprocess_state.replay(qhead, assumptions);   
-            m_preprocess_state.freeze(assumptions);
+        if (qhead < m_fmls.size()) {
             m_preprocess.reduce();
             if (!m.inc())
                 return;
             TRACE("solver", tout << "qhead " << qhead << "\n";
                   m_preprocess_state.display(tout));
             m_preprocess_state.advance_qhead();
+        }
+        if (!assumptions.empty()) {
+            m_preprocess_state.replay(m_preprocess_state.qhead(), assumptions);   
             for (unsigned i = 0; i < assumptions.size(); ++i) 
                 m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));            
         }
@@ -203,6 +214,7 @@ public:
     lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override { 
         expr_ref_vector _assumptions(m, num_assumptions, assumptions);
         flush(_assumptions);
+        TRACE("simplifier", tout << _assumptions);
         return s->check_sat_core(num_assumptions, _assumptions.data()); 
     }
 

From 23de8056d70c38de5a0aee04ff1332a51bdb6040 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <christoph@imandra.ai>
Date: Fri, 6 Oct 2023 03:49:22 +0100
Subject: [PATCH 09/10] Add RCF functions to OCaml API (#6932)

---
 examples/ml/ml_example.ml | 17 ++++++++-
 src/api/ml/z3.ml          | 37 +++++++++++++++++++
 src/api/ml/z3.mli         | 75 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 128 insertions(+), 1 deletion(-)

diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml
index 5b4e6e9ed..b6a71b69d 100644
--- a/examples/ml/ml_example.ml
+++ b/examples/ml/ml_example.ml
@@ -315,7 +315,21 @@ let fpa_example ( ctx : context ) =
 	  Printf.printf "Test passed.\n"
   ) 
 
-let _ = 
+(**
+	A basic example of RCF usage
+**)
+let rcf_example ( ctx : context ) =
+  Printf.printf "RCFExample\n" ;
+  let pi = RCF.mk_pi ctx in
+  let e = RCF.mk_e ctx in
+  (Printf.printf "e: %s,  pi: %s, e==pi: %b, e < pi: %b\n"
+    (RCF.num_to_string ctx e true false)
+    (RCF.num_to_string ctx pi true false)
+    (RCF.eq ctx e pi)
+    (RCF.lt ctx e pi)) ;
+  Printf.printf "Test passed.\n"
+
+let _ =
   try (
     if not (Log.open_ "z3.log") then
       raise (TestFailedException "Log couldn't be opened.")
@@ -340,6 +354,7 @@ let _ =
 	basic_tests ctx ;
 	quantifier_example1 ctx ;
 	fpa_example ctx ;
+  rcf_example ctx ;
 	Printf.printf "Disposing...\n";
 	Gc.full_major ()
       );
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 98807bedd..4d195a0b1 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -2077,6 +2077,43 @@ struct
 end
 
 
+module RCF =
+struct
+  type rcf_num = Z3native.rcf_num
+
+  let del (ctx:context) (a:rcf_num) = Z3native.rcf_del ctx a
+  let mk_rational (ctx:context) (v:string) = Z3native.rcf_mk_rational ctx v
+  let mk_small_int (ctx:context) (v:int) = Z3native.rcf_mk_small_int ctx v
+
+  let mk_pi (ctx:context) = Z3native.rcf_mk_pi ctx
+  let mk_e (ctx:context) = Z3native.rcf_mk_e ctx
+  let mk_infinitesimal (ctx:context) = Z3native.rcf_mk_infinitesimal ctx
+
+  let mk_roots (ctx:context) (n:int) (a:rcf_num list) = let n, r = Z3native.rcf_mk_roots ctx n a in r
+
+  let add (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_add ctx a b
+  let sub (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_sub ctx a b
+  let mul (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_mul ctx a b
+  let div (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_div ctx a b
+
+  let neg (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+  let inv (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+
+  let power (ctx:context) (a:rcf_num) (k:int) = Z3native.rcf_power ctx a k
+
+  let lt (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_lt ctx a b
+  let gt (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_gt ctx a b
+  let le (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_le ctx a b
+  let ge (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_ge ctx a b
+  let eq (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_eq ctx a b
+  let neq (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_neq ctx a b
+
+  let num_to_string (ctx:context) (a:rcf_num) (compact:bool) (html:bool) = Z3native.rcf_num_to_string ctx a compact html
+  let num_to_decimal_string (ctx:context) (a:rcf_num) (prec:int) = Z3native.rcf_num_to_decimal_string ctx a prec
+  let get_numerator_denominator (ctx:context) (a:rcf_num) = Z3native.rcf_get_numerator_denominator ctx a
+end
+
+
 let set_global_param = Z3native.global_param_set
 
 let get_global_param id =
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 53e92b491..006ee6051 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3535,6 +3535,81 @@ sig
   val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
 end
 
+(** Real closed field *)
+module RCF :
+sig
+    type rcf_num
+
+    (** Delete a RCF numeral created using the RCF API. *)
+    val del : context -> rcf_num -> unit
+
+    (** Return a RCF rational using the given string. *)
+    val mk_rational : context -> string -> rcf_num
+
+    (** Return a RCF small integer. *)
+    val mk_small_int : context -> int -> rcf_num
+
+    (** Return Pi *)
+    val mk_pi : context -> rcf_num
+
+    (** Return e (Euler's constant) *)
+    val mk_e : context -> rcf_num
+
+    (** Return a new infinitesimal that is smaller than all elements in the Z3 field. *)
+    val mk_infinitesimal : context -> rcf_num
+
+    (** Extract the roots of a polynomial. Precondition: The input polynomial is not the zero polynomial. *)
+    val mk_roots : context -> int -> rcf_num list -> rcf_num list
+
+    (** Addition *)
+    val add : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Subtraction *)
+    val sub : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Multiplication *)
+    val mul : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Division *)
+    val div : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Negation *)
+    val neg : context -> rcf_num -> rcf_num
+
+    (** Multiplicative Inverse *)
+    val inv : context -> rcf_num -> rcf_num
+
+    (** Power *)
+    val power : context -> rcf_num -> int -> rcf_num
+
+    (** less-than *)
+    val lt : context -> rcf_num -> rcf_num -> bool
+
+    (** greater-than *)
+    val gt : context -> rcf_num -> rcf_num -> bool
+
+    (** less-than or equal *)
+    val le : context -> rcf_num -> rcf_num -> bool
+
+    (** greater-than or equal *)
+    val ge : context -> rcf_num -> rcf_num -> bool
+
+    (** equality *)
+    val eq : context -> rcf_num -> rcf_num -> bool
+
+    (** not equal *)
+    val neq : context -> rcf_num -> rcf_num -> bool
+
+    (** Convert the RCF numeral into a string. *)
+    val num_to_string : context -> rcf_num -> bool -> bool -> string
+
+    (** Convert the RCF numeral into a string in decimal notation. *)
+    val num_to_decimal_string : context -> rcf_num -> int -> string
+
+    (** Extract the "numerator" and "denominator" of the given RCF numeral.
+        We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions. *)
+    val get_numerator_denominator : context -> rcf_num -> (rcf_num * rcf_num)
+end
 
 (** Set a global (or module) parameter, which is shared by all Z3 contexts.
 

From 19e921290e5c08c547b4ebe73752df262166b12c Mon Sep 17 00:00:00 2001
From: LufyCZ <Lukasczk@seznam.cz>
Date: Fri, 6 Oct 2023 04:49:54 +0200
Subject: [PATCH 10/10] increase wasm stack size (#6931)

---
 src/api/js/scripts/build-wasm.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts
index 0f51c84d3..5bdbdea3b 100644
--- a/src/api/js/scripts/build-wasm.ts
+++ b/src/api/js/scripts/build-wasm.ts
@@ -69,7 +69,7 @@ const fns = JSON.stringify(exportedFuncs());
 const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
 const libz3a = path.normalize('../../../build/libz3.a');
 spawnSync(
-  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -I z3/src/api/ -o build/z3-built.js`,
+  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
 );
 
 fs.rmSync(ccWrapperPath);