diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 3f97cfefe..f228a216b 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -294,8 +294,6 @@ void rewriter_tpl::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); diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index 2a463ecbf..2d080032a 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -159,8 +159,8 @@ monic const* emonics::find_canonical(svector 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.find(UINT_MAX, w)) { + if (m_cg_table.contains(UINT_MAX) && !m_cg_table[UINT_MAX].empty()) { + 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) { - TRACE("nla_solver_mons", tout << "erase << " << m << "\n";); - m_cg_table.erase(u); + auto& v = m_cg_table[u]; + SASSERT(v.contains(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)) { - if (v == w) { - TRACE("nla_solver_mons", tout << "found " << v << "\n";); - return; - } + auto* entry = m_cg_table.insert_if_not_there2(v, unsigned_vector()); + auto& vec = entry->get_data().m_value; + if (vec.empty()) { + 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,9 +295,8 @@ void emonics::insert_cg_mon(monic & m) { m_u_f.merge(v_idx, w_idx); } else { - TRACE("nla_solver_mons", tout << "insert " << m << "\n";); - m_cg_table.insert(v); - } + TRACE("nla_solver_mons", tout << "found " << v << "\n";); + } } void emonics::set_visited(monic& m) const { @@ -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; } @@ -547,8 +558,9 @@ bool emonics::invariant() const { }; unsigned idx = 0; for (auto const& m : m_monics) { - CTRACE("nla_solver_mons", !m_cg_table.contains(m.var()), tout << "removed " << m << "\n";); + 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; } diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index 5b12f24b2..866ad3c73 100644 --- a/src/math/lp/emonics.h +++ b/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 m_cg_table; // congruence (canonical) table. + map 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; - m_cg_table.find(sv.var(), j); + unsigned j = m_cg_table[sv.var()][0]; return m_monics[m_var2index[j]]; } diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index f22dcfca4..d49cd25b3 100644 --- a/src/smt/smt_model_generator.cpp +++ b/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++) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a7979864d..ab2168503 100644 --- a/src/smt/theory_lra.cpp +++ b/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 (static_cast(v2) < th.get_num_vars() && !is_equal(v1, v2)) { + if (m_fixed_var_table.find(key, v2)) { + if (static_cast(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;