From ab199dedf9f6bf21bd16c9e5869e7eb71575a58b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Nov 2020 12:13:19 -0800
Subject: [PATCH] debug arith/mbi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_ll_pp.cpp                       |  9 +++---
 src/cmd_context/CMakeLists.txt              |  1 -
 src/cmd_context/cmd_context.h               |  2 +-
 src/math/lp/lp_api.h                        |  2 ++
 src/sat/sat_solver.cpp                      |  1 +
 src/sat/smt/arith_axioms.cpp                | 22 +++++++++++++-
 src/sat/smt/arith_solver.cpp                | 15 +++++++---
 src/sat/smt/arith_solver.h                  | 11 +++----
 src/sat/smt/euf_solver.cpp                  | 33 +++++++++++++++++++--
 src/sat/smt/euf_solver.h                    |  2 ++
 src/sat/smt/q_mbi.cpp                       |  5 ++++
 src/sat/smt/q_mbi.h                         |  2 ++
 src/sat/smt/q_solver.cpp                    |  1 +
 src/sat/smt/sat_th.h                        |  1 +
 src/sat/tactic/sat_tactic.cpp               |  1 +
 src/smt/arith_eq_adapter.cpp                |  2 +-
 src/solver/CMakeLists.txt                   |  1 +
 src/{cmd_context => solver}/check_logic.cpp |  2 +-
 src/{cmd_context => solver}/check_logic.h   |  0
 src/tactic/tactic.h                         |  2 +-
 src/util/obj_pair_set.h                     |  5 ++--
 src/util/trail.h                            |  1 -
 22 files changed, 96 insertions(+), 25 deletions(-)
 rename src/{cmd_context => solver}/check_logic.cpp (99%)
 rename src/{cmd_context => solver}/check_logic.h (100%)

diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index c0d28a8ef..83d1fbf85 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -279,19 +279,18 @@ public:
             display_child(n);
             return;
         }
-        if (to_app(n)->get_num_args() > depth && to_app(n)->get_num_args() > 16) {
-            display_child(n);
-            return;
-        }
         unsigned num_args = to_app(n)->get_num_args();
+        
         if (num_args > 0) 
             m_out << "(";
         display_name(to_app(n)->get_decl());
         display_params(to_app(n)->get_decl());
-        for (unsigned i = 0; i < num_args; i++) {
+        for (unsigned i = 0; i < num_args && i < 16; i++) {
             m_out << " ";
             display(to_app(n)->get_arg(i), depth-1);
         }
+        if (num_args >= 16) 
+            m_out << " ...";
         if (num_args > 0)
             m_out << ")";
     }
diff --git a/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt
index 3f869966c..f8c1aa38f 100644
--- a/src/cmd_context/CMakeLists.txt
+++ b/src/cmd_context/CMakeLists.txt
@@ -1,7 +1,6 @@
 z3_add_component(cmd_context
   SOURCES
     basic_cmds.cpp
-    check_logic.cpp
     cmd_context.cpp
     cmd_context_to_goal.cpp
     cmd_util.cpp
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 6a67cf0b4..2642fc763 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -35,10 +35,10 @@ Notes:
 #include "ast/rewriter/seq_rewriter.h"
 #include "tactic/generic_model_converter.h"
 #include "solver/solver.h"
+#include "solver/check_logic.h"
 #include "solver/progress_callback.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
-#include "cmd_context/check_logic.h"
 #include "params/context_params.h"
 
 
diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h
index f8c655b08..354328bd6 100644
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@@ -104,6 +104,7 @@ namespace lp_api {
         unsigned m_bound_propagations1;
         unsigned m_bound_propagations2;
         unsigned m_assert_diseq;
+        unsigned m_assert_eq;
         unsigned m_gomory_cuts;
         unsigned m_assume_eqs;
         unsigned m_branch;
@@ -123,6 +124,7 @@ namespace lp_api {
             st.update("arith-bound-propagations-lp", m_bound_propagations1);
             st.update("arith-bound-propagations-cheap", m_bound_propagations2);
             st.update("arith-diseq", m_assert_diseq);
+            st.update("arith-eq",    m_assert_eq);
             st.update("arith-gomory-cuts", m_gomory_cuts);
             st.update("arith-assume-eqs", m_assume_eqs);
             st.update("arith-branch", m_branch);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 67fce084d..9d3371ee5 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -424,6 +424,7 @@ namespace sat {
             }
         }       
 
+
         switch (num_lits) {
         case 0:
             set_conflict();
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 14cd8b23b..997de9ae2 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -296,15 +296,34 @@ namespace arith {
         return lp::EQ;
     }
 
-    void solver::mk_eq_axiom(bool is_eq, theory_var v1, theory_var v2) {
+    void solver::mk_eq_axiom(bool is_eq, euf::th_eq const& e) {
+        theory_var v1 = e.v1();
+        theory_var v2 = e.v2();
         if (is_bool(v1))
             return;
+        force_push();
         expr* e1 = var2expr(v1);
         expr* e2 = var2expr(v2);
+        if (e1->get_id() > e2->get_id())
+            std::swap(e1, e2);
+            
         if (is_eq && m.are_equal(e1, e2))
             return;
         if (!is_eq && m.are_distinct(e1, e2))
             return;       
+
+        if (is_eq) {       
+            ++m_stats.m_assert_eq;
+            euf::enode* n1 = var2enode(v1);
+            euf::enode* n2 = var2enode(v2);
+            lpvar w1 = register_theory_var_in_lar_solver(v1);
+            lpvar w2 = register_theory_var_in_lar_solver(v2);
+            auto cs = lp().add_equality(w1, w2);            
+            add_eq_constraint(cs.first, n1, n2);
+            add_eq_constraint(cs.second, n1, n2);
+            m_new_eq = true;
+            return;
+        }
         literal le, ge;
         if (a.is_numeral(e1))
             std::swap(e1, e2);
@@ -332,6 +351,7 @@ namespace arith {
             le = mk_literal(a.mk_le(diff, zero));
             ge = mk_literal(a.mk_ge(diff, zero));
         }
+        ++m_stats.m_assert_diseq;  
         add_clause(~eq, le);
         add_clause(~eq, ge);
         add_clause(~le, ~ge, eq);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 489ff66c9..712e7d719 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -86,9 +86,10 @@ namespace arith {
     }
 
     bool solver::unit_propagate() {
-        if (m_new_bounds.empty() && m_asserted_qhead == m_asserted.size())
+        if (!m_new_eq && m_new_bounds.empty() && m_asserted_qhead == m_asserted.size())
             return false;
 
+        m_new_eq = false;
         flush_bound_axioms();
 
         unsigned qhead = m_asserted_qhead;
@@ -911,6 +912,8 @@ namespace arith {
             theory_var v = (i + start) % sz;
             if (is_bool(v))
                 continue;
+            if (!ctx.is_shared(var2enode(v)))
+                continue;
             ensure_column(v);
             if (!can_get_ivalue(v))
                 continue;
@@ -945,7 +948,7 @@ namespace arith {
                 continue;
             if (n1->get_root() == n2->get_root())
                 continue;
-            literal eq = eq_internalize(n1->get_expr(), n2->get_expr());
+            literal eq = eq_internalize(n1, n2);
             if (s().value(eq) != l_true)
                 return true;
         }
@@ -1040,7 +1043,6 @@ namespace arith {
         SASSERT(m_nla->use_nra_model());
         auto t = get_tv(v);
         if (t.is_term()) {
-
             m_todo_terms.push_back(std::make_pair(t, rational::one()));
             TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";);
             TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n";
@@ -1193,8 +1195,13 @@ namespace arith {
         TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto const& ev : m_explanation)
             set_evidence(ev.ci(), m_core, m_eqs);
+        DEBUG_CODE(
+            if (is_conflict) {
+                for (literal c : m_core) VERIFY(s().value(c) == l_false);
+                for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());
+            });
         for (auto const& eq : m_eqs)
-            m_core.push_back(eq_internalize(eq.first->get_expr(), eq.second->get_expr()));
+            m_core.push_back(eq_internalize(eq.first, eq.second));
         for (literal& c : m_core)
             c.neg();
         add_clause(m_core);
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index a3dca72dd..6aff1528a 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -16,8 +16,8 @@ Author:
 --*/
 #pragma once
 
+#include "util/obj_pair_set.h"
 #include "ast/ast_trail.h"
-#include "sat/smt/sat_th.h"
 #include "ast/arith_decl_plugin.h"
 #include "math/lp/lp_solver.h"
 #include "math/lp/lp_primal_simplex.h"
@@ -29,6 +29,7 @@ Author:
 #include "math/lp/lp_api.h"
 #include "math/polynomial/algebraic_numbers.h"
 #include "math/polynomial/polynomial.h"
+#include "sat/smt/sat_th.h"
 
 namespace euf {
     class solver;
@@ -90,7 +91,7 @@ namespace arith {
         };
         int_hashtable<var_value_hash, var_value_eq>   m_model_eqs;
 
-
+        bool                m_new_eq { false };
 
 
         // temporary values kept during internalization
@@ -303,7 +304,7 @@ namespace arith {
         void refine_bound(theory_var v, const lp::implied_bound& be);
         literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const;
         void assert_bound(bool is_true, api_bound& b);
-        void mk_eq_axiom(bool is_eq, theory_var v1, theory_var v2);
+        void mk_eq_axiom(bool is_eq, euf::th_eq const& eq);
         void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r);
         api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
         lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);
@@ -424,8 +425,8 @@ namespace arith {
         void collect_statistics(statistics& st) const override;
         euf::th_solver* clone(euf::solver& ctx) override;
         bool use_diseqs() const override { return true; }
-        void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(true, eq.v1(), eq.v2()); }
-        void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(false, de.v1(), de.v2()); }
+        void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(true, eq); }
+        void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(false, de); }
         bool unit_propagate() override;
         void init_model() override { init_variable_values(); }
         void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 302e1edd0..ee15e93c4 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -83,6 +83,7 @@ namespace euf {
         if (ext)
             return ext;
         ext = alloc(q::solver, *this, fid);
+        m_qsolver = ext;
         add_solver(ext);
         return ext;
     }
@@ -364,11 +365,33 @@ namespace euf {
         }
     }
 
+    bool solver::is_self_propagated(th_eq const& e) {
+        if (!e.is_eq())
+            return false;
+        
+        m_egraph.begin_explain();
+        m_explain.reset();
+        m_egraph.explain_eq<size_t>(m_explain, e.child(), e.root());
+        m_egraph.end_explain();
+        for (auto p : m_explain) {
+            if (is_literal(p))
+                return false;
+
+            size_t idx = get_justification(p);
+            auto* ext = sat::constraint_base::to_extension(idx);                
+            if (ext->get_id() != e.id())
+                return false;
+        }
+        return true;
+    }
+
     void solver::propagate_th_eqs() {
         for (; m_egraph.has_th_eq() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_th_eq()) {
             th_eq eq = m_egraph.get_th_eq();
-            if (eq.is_eq())
-                m_id2solver[eq.id()]->new_eq_eh(eq);    
+            if (eq.is_eq()) {
+                if (!is_self_propagated(eq))
+                    m_id2solver[eq.id()]->new_eq_eh(eq);    
+            }
             else
                 m_id2solver[eq.id()]->new_diseq_eh(eq);
         }
@@ -404,16 +427,22 @@ namespace euf {
         for (auto* e : m_solvers) {
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
+            if (e == m_qsolver)
+                continue;
             switch (e->check()) {
             case sat::check_result::CR_CONTINUE: cont = true; break;
             case sat::check_result::CR_GIVEUP: give_up = true; break;
             default: break;
             }
+            if (s().inconsistent())
+                return sat::check_result::CR_CONTINUE;
         }
         if (cont)
             return sat::check_result::CR_CONTINUE;
         if (give_up)
             return sat::check_result::CR_GIVEUP;
+        if (m_qsolver)
+            return m_qsolver->check();
         TRACE("after_search", s().display(tout););
         return sat::check_result::CR_DONE;
     }
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index d8f10c992..9b43810a3 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -93,6 +93,7 @@ namespace euf {
         scoped_ptr<euf::ackerman>   m_ackerman;
         scoped_ptr<sat::dual_solver> m_dual_solver;
         user::solver*          m_user_propagator{ nullptr };
+        th_solver*             m_qsolver { nullptr };
 
         ptr_vector<expr>                                m_bool_var2expr;
         ptr_vector<size_t>                              m_explain;
@@ -147,6 +148,7 @@ namespace euf {
         // solving
         void propagate_literals();
         void propagate_th_eqs();
+        bool is_self_propagated(th_eq const& e);
         void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
         void new_diseq(enode* a, enode* b, literal lit);
 
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 9f0dbda26..acbf1585d 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -387,4 +387,9 @@ namespace q {
         m_plugins.set(fid, p);
     }
 
+    void mbqi::collect_statistics(statistics& st) const {
+        if (m_solver)
+            m_solver->collect_statistics(st);
+    }
+
 }
diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h
index 33bce61d9..49fccbb3c 100644
--- a/src/sat/smt/q_mbi.h
+++ b/src/sat/smt/q_mbi.h
@@ -79,6 +79,8 @@ namespace q {
         void init_search();
 
         void finalize_model(model& mdl);
+
+        void collect_statistics(statistics& st) const;
     };
 
 }
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index a31ac5f78..588277ab4 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -60,6 +60,7 @@ namespace q {
 
     void solver::collect_statistics(statistics& st) const {
         st.update("quantifier asserts", m_stats.m_num_quantifier_asserts);
+        m_mbqi.collect_statistics(st);
     }
 
     euf::th_solver* solver::clone(euf::solver& ctx) {
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index af04df97b..882b0ac23 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -150,6 +150,7 @@ namespace euf {
         bool is_true(sat::literal a, sat::literal b, sat::literal c, sat::literal d) { return is_true(a) || is_true(b, c, c); }
 
         sat::literal eq_internalize(expr* a, expr* b);
+        sat::literal eq_internalize(enode* a, enode* b) { return eq_internalize(a->get_expr(), b->get_expr()); }
 
         euf::enode* e_internalize(expr* e); 
         euf::enode* mk_enode(expr* e, bool suppress_args = false);
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index c9afc4578..3a1f19fe7 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -208,6 +208,7 @@ public:
         }
         catch (z3_exception& ex) {
             (void)ex;
+            proc.m_solver->collect_statistics(m_stats);
             TRACE("sat", tout << ex.msg() << "\n";);            
             throw;
         }
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index 77b4d7cc4..6b704568c 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -118,7 +118,7 @@ namespace smt {
         // after n1 and n2 are marked as relevant.
         //
         data d;
-        if (m_already_processed.find(n1, n2, d))
+        if (m_already_processed.find(n1, n2, d)) 
             return;
         
         TRACE("arith_eq_adapter_profile", tout << "mk #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " " <<
diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt
index 281a34018..67549c46b 100644
--- a/src/solver/CMakeLists.txt
+++ b/src/solver/CMakeLists.txt
@@ -1,6 +1,7 @@
 z3_add_component(solver
   SOURCES
     check_sat_result.cpp
+    check_logic.cpp
     combined_solver.cpp
     mus.cpp
     parallel_tactic.cpp
diff --git a/src/cmd_context/check_logic.cpp b/src/solver/check_logic.cpp
similarity index 99%
rename from src/cmd_context/check_logic.cpp
rename to src/solver/check_logic.cpp
index 9a69d4e6d..b35e49665 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/solver/check_logic.cpp
@@ -16,7 +16,7 @@ Author:
 Revision History:
 
 --*/
-#include "cmd_context/check_logic.h"
+#include "solver/check_logic.h"
 #include "solver/smt_logics.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
diff --git a/src/cmd_context/check_logic.h b/src/solver/check_logic.h
similarity index 100%
rename from src/cmd_context/check_logic.h
rename to src/solver/check_logic.h
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index a044dcd32..37a211cb4 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -62,7 +62,7 @@ public:
     */
     virtual void operator()(goal_ref const & in, goal_ref_buffer& result) = 0;
 
-    virtual void collect_statistics(statistics & st) const {}
+    virtual void collect_statistics(statistics & st) const { }
     virtual void reset_statistics() {}
     virtual void cleanup() = 0;
     virtual void reset() { cleanup(); }
diff --git a/src/util/obj_pair_set.h b/src/util/obj_pair_set.h
index 6b08d6fad..83cc00bd8 100644
--- a/src/util/obj_pair_set.h
+++ b/src/util/obj_pair_set.h
@@ -39,8 +39,9 @@ public:
     void insert(obj_pair const & p) { m_set.insert(p); }
     bool insert_if_not_there(T1 * t1, T2 * t2) { return m_set.insert_if_not_there2(obj_pair(t1, t2)); }
     bool insert_if_not_there(obj_pair const & p) { return m_set.insert_if_not_there2(p); }
-    void erase(T1 * t1, T2 * t2) { return m_set.erase(obj_pair(t1, t2)); }
-    void erase(obj_pair const & p) { return m_set.erase(p); }
+    void erase(T1 * t1, T2 * t2) { m_set.erase(obj_pair(t1, t2)); }
+    void erase(obj_pair const & p) { m_set.erase(p); }
+    void remove(obj_pair const & p) { erase(p); }
     bool contains(T1 * t1, T2 * t2) const { return m_set.contains(obj_pair(t1, t2)); }
     bool contains(obj_pair const & p) const { return m_set.contains(p); }
     void reset() { m_set.reset(); }
diff --git a/src/util/trail.h b/src/util/trail.h
index 1cdd07ef9..b822b2456 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -376,7 +376,6 @@ public:
 };
 
 
-
 template<typename Ctx, typename T>
 class remove_obj_trail : public trail<Ctx> {
     obj_hashtable<T>& m_table;