fix #3334

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

src/ast/rewriter/rewriter_def.h

@@ -294,8 +294,6 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
               tout << "st: " << st;
               if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
               tout << "\n";);
-        if (st != BR_FAILED && m().get_sort(m_r) != m().get_sort(t))
-            std::cout << mk_bounded_pp(t, m()) << "\n" << mk_bounded_pp(m_r, m()) << "\n";
         SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
         if (st != BR_FAILED) {
             result_stack().shrink(fr.m_spos);

src/math/lp/emonics.cpp

@@ -159,8 +159,8 @@ monic const* emonics::find_canonical(svector<lpvar> const& vars) const {
     m_find_key = vars;
     std::sort(m_find_key.begin(), m_find_key.end());
     monic const* result = nullptr;
-    lpvar w;
+    if (m_cg_table.contains(UINT_MAX) && !m_cg_table[UINT_MAX].empty()) {
-    if (m_cg_table.find(UINT_MAX, w)) {
+        lpvar w = m_cg_table[UINT_MAX][0];
         result = &m_monics[m_var2index[w]];
     }
     return result;
@@ -188,11 +188,20 @@ void emonics::remove_cg(lpvar v) {
 }
 
 void emonics::remove_cg_mon(const monic& m) {
-    lpvar u = m.var(), w;
+    lpvar u = m.var();
     // equivalence class of u:
-    if (m_cg_table.find(u, w) && u == w) {
+    auto& v = m_cg_table[u];
-        TRACE("nla_solver_mons", tout << "erase << " << m << "\n";);
+    SASSERT(v.contains(u));
-        m_cg_table.erase(u);
+    if (v.size() == 1) {
+        m_cg_table.remove(u);
+    }
+    else if (v[0] == u) {
+        v.erase(u);
+        m_cg_table.remove(u);
+        m_cg_table.insert(v[0], v);
+    }
+    else {
+        v.erase(u);
     }
 }
 
@@ -269,11 +278,14 @@ void emonics::insert_cg_mon(monic & m) {
     do_canonize(m);
     lpvar v = m.var(), w;
     TRACE("nla_solver_mons", tout << m << " hash: " << m_cg_hash(v) << "\n";);
-    if (m_cg_table.find(v, w)) {
+    auto* entry = m_cg_table.insert_if_not_there2(v, unsigned_vector());
-        if (v == w) {
+    auto& vec = entry->get_data().m_value;
-            TRACE("nla_solver_mons", tout << "found "  << v << "\n";);
+    if (vec.empty()) {
-            return;
+        vec.push_back(v);
     }
+    else if (!vec.contains(v)) {
+        w = vec[0];
+        vec.push_back(v);
         unsigned v_idx = m_var2index[v];
         unsigned w_idx = m_var2index[w];
         unsigned max_i = std::max(v_idx, w_idx);
@@ -283,8 +295,7 @@ void emonics::insert_cg_mon(monic & m) {
         m_u_f.merge(v_idx, w_idx);
     }
     else {
-        TRACE("nla_solver_mons", tout << "insert " << m << "\n";);
+        TRACE("nla_solver_mons", tout << "found "  << v << "\n";);
-        m_cg_table.insert(v);
     }
 }
 
@@ -450,7 +461,7 @@ std::ostream& emonics::display(std::ostream& out) const {
     //display_uf(out);
     out << "table:\n";
     for (auto const& k : m_cg_table) {
-        out << k << "\n";
+        out << k.m_key << ": " << k.m_value << "\n";
     }
     return out;
 }
@@ -549,6 +560,7 @@ bool emonics::invariant() const {
     for (auto const& m : m_monics) {
         CTRACE("nla_solver_mons", !m_cg_table.contains(m.var()), tout << "removed " << m << "\n";);
         SASSERT(m_cg_table.contains(m.var()));
+        SASSERT(m_cg_table[m.var()].contains(m.var()));
         for (auto v : m.vars()) {
             if (!find_index(v, idx))
                 return false;
@@ -560,6 +572,18 @@ bool emonics::invariant() const {
         }
         idx++;
     }
+    
+    // the table of monic representatives is such that the
+    // first entry in the vector is the equivalence class
+    // representative.
+    for (auto const& k : m_cg_table) {
+        auto const& v = k.m_value;
+        if (!v.empty() && v[0] != k.m_key) {
+            TRACE("nla_solver_mons", tout << "bad table entry: " << k.m_key << ": " << k.m_value << "\n";);
+            return false;
+        }
+    }
+
     return true;
 }
 

src/math/lp/emonics.h

@@ -24,6 +24,7 @@
 #include "math/lp/var_eqs.h"
 #include "math/lp/monic.h"
 #include "util/region.h"
+#include "util/map.h"
 
 namespace nla {
 
@@ -93,7 +94,7 @@ class emonics {
     hash_canonical               m_cg_hash;
     eq_canonical                 m_cg_eq;
     unsigned_vector              m_vs;            // temporary buffer of canonized variables
-    hashtable<lpvar, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
+    map<lpvar, unsigned_vector, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
 
 
     void inc_visited() const;
@@ -129,7 +130,7 @@ public:
         m_visited(0), 
         m_cg_hash(*this),
         m_cg_eq(*this),
-        m_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq) { 
+        m_cg_table(m_cg_hash, m_cg_eq) { 
         m_ve.set_merge_handler(this); 
     }
 
@@ -172,8 +173,7 @@ public:
     */
 
     monic const& rep(monic const& sv) const {
-        unsigned j = -1;
+        unsigned j = m_cg_table[sv.var()][0];
-        m_cg_table.find(sv.var(), j);
         return m_monics[m_var2index[j]];
     }
 

src/smt/smt_model_generator.cpp

@@ -424,7 +424,6 @@ namespace smt {
                 SASSERT(m_model->has_interpretation(f));
                 SASSERT(m_model->get_func_interp(f) == fi);
                 // The entry must be new because n->get_cg() == n
-                SASSERT(f->get_range() == m.get_sort(result));
                 TRACE("model", 
                       tout << "insert new entry for:\n" << mk_ismt2_pp(n->get_owner(), m) << "\nargs: ";
                       for (unsigned i = 0; i < num_args; i++) {

src/smt/theory_lra.cpp

@@ -3120,8 +3120,8 @@ public:
     void fixed_var_eh(theory_var v1, rational const& bound) {
         theory_var v2;
         value_sort_pair key(bound, is_int(v1));
-        if (m_fixed_var_table.find(key, v2) && is_int(v1) == is_int(v2)) {
+        if (m_fixed_var_table.find(key, v2)) {
-            if (static_cast<unsigned>(v2) < th.get_num_vars() && !is_equal(v1, v2)) {
+            if (static_cast<unsigned>(v2) < th.get_num_vars() && !is_equal(v1, v2) && is_int(v1) == is_int(v2)) {
                 auto vi1 = register_theory_var_in_lar_solver(v1);
                 auto vi2 = register_theory_var_in_lar_solver(v2);
                 lp::constraint_index ci1, ci2, ci3, ci4;