From 0c641cdf9522533d2c647bb79da5d8d5da4c1492 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Feb 2013 16:53:56 -0800 Subject: [PATCH] hilbert basis experiment Signed-off-by: Nikolaj Bjorner --- src/muz_qe/hilbert_basis.cpp | 81 +++++++++++++++++++--------- src/muz_qe/hilbert_basis.h | 1 + src/test/hilbert_basis.cpp | 100 ++++++++++++++++++++++++++++------- 3 files changed, 139 insertions(+), 43 deletions(-) diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 09296f89d..59c9d5080 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -26,10 +26,10 @@ typedef u_map offset_refs_t; template class rational_map : public map {}; -class rational_lt { +class rational_abs_lt { vector & m_values; public: - rational_lt(vector & values): + rational_abs_lt(vector & values): m_values(values) { } bool operator()(int v1, int v2) const { @@ -41,8 +41,8 @@ public: class hilbert_basis::rational_heap { vector m_u2r; // [index |-> weight] rational_map m_r2u; // [weight |-> index] - rational_lt m_lt; // less_than on indices - heap m_heap; // binary heap over weights + rational_abs_lt m_lt; // less_than on indices + heap m_heap; // binary heap over weights public: rational_heap(): m_lt(m_u2r), m_heap(10, m_lt) {} @@ -76,9 +76,6 @@ public: m_heap.find_le(val, result); } - void find_le(numeral const& r, int_vector& result) { - find_le(m_r2u.find(r), result); - } }; class hilbert_basis::weight_map { @@ -97,11 +94,12 @@ class hilbert_basis::weight_map { unsigned m_cost; unsigned get_value(numeral const& w) { + numeral r = abs(w); unsigned val; - if (!m_heap.is_declared(w, val)) { - val = m_heap.declare(w); + if (!m_heap.is_declared(r, val)) { + val = m_heap.declare(r); SASSERT(val == m_offsets.size()); - if (w.is_nonneg()) { + if (r.is_nonneg()) { m_heap.insert(val); } m_offsets.push_back(unsigned_vector()); @@ -121,6 +119,14 @@ public: m_offsets[val].erase(idx.m_offset); } + unsigned get_size() const { + unsigned sz = 0; + for (unsigned i = 0; i < m_offsets.size(); ++i) { + sz += m_offsets[i].size(); + } + return sz; + } + void reset() { m_offsets.reset(); m_heap.reset(); @@ -129,6 +135,9 @@ public: unsigned get_cost() const { return m_cost; } + /** + retrieve + */ bool init_find(numeral const& w, offset_t idx) { m_le.reset(); m_found.reset(); @@ -143,7 +152,7 @@ public: m_le.push_back(val); } for (unsigned i = 0; i < m_le.size(); ++i) { - if (m_heap.u2r()[m_le[i]].is_zero() && w.is_pos()) { + if (m_heap.u2r()[m_le[i]].is_zero() && !w.is_zero()) { continue; } unsigned_vector const& offsets = m_offsets[m_le[i]]; @@ -159,16 +168,25 @@ public: } return !m_found.empty(); } + + unsigned get_find_cost(numeral const& w) { + m_le.reset(); + unsigned cost = 0; + unsigned val = get_value(w); + m_heap.find_le(val, m_le); + for (unsigned i = 0; i < m_le.size(); ++i) { + cost += m_offsets[m_le[i]].size(); + } + return cost; + } bool update_find(unsigned round, numeral const& w, offset_t idx) { - //std::cout << "update find: " << w << "\n"; m_found.reset(); m_le.reset(); m_cost = 0; - m_heap.find_le(w, m_le); - unsigned vl; + unsigned vl = get_value(w); + m_heap.find_le(vl, m_le); for (unsigned i = 0; i < m_le.size(); ++i) { - //std::cout << "insert update find: " << m_weights[m_le[i]] << "\n"; unsigned_vector const& offsets = m_offsets[m_le[i]]; for (unsigned j = 0; j < offsets.size(); ++j) { unsigned offs = offsets[j]; @@ -255,9 +273,17 @@ public: m_refs.reset(); bool found = m_weight.init_find(vs.value(), idx); TRACE("hilbert_basis", tout << "init: " << m_found.size() << " cost: " << m_weight.get_cost() << "\n";); +#if 0 + std::cout << vs.value() << " " << m_found.size() << " "; + for (unsigned i = 0; i < m_values.size(); ++i) { + std::cout << vs[i] << ": " << m_values[i]->get_find_cost(vs[i]) << " "; + } + std::cout << "\n"; +#endif #if 0 for (unsigned i = 0; found && i < m_values.size(); ++i) { found = m_values[i]->update_find(i, vs[i], idx); + std::cout << vs[i] << ": " << m_found.size() << " "; TRACE("hilbert_basis", tout << "update " << i << ": " << m_found.size() << " cost: " << m_values[i]->get_cost() << "\n";); } #else @@ -269,6 +295,7 @@ public: } return false; #endif + if (found) { found_idx = m_found[0]; } @@ -290,6 +317,7 @@ public: } st.update("hb.index.num_find", m_stats.m_num_find); st.update("hb.index.num_insert", m_stats.m_num_insert); + st.update("hb.index.size", m_weight.get_size()); } void reset_statistics() { @@ -363,12 +391,12 @@ public: */ class hilbert_basis::passive { - hilbert_basis& hb; - svector m_passive; - vector m_weights; - unsigned_vector m_free_list; - rational_lt m_lt; // less_than on indices - heap m_heap; // binary heap over weights + hilbert_basis& hb; + svector m_passive; + vector m_weights; + unsigned_vector m_free_list; + rational_abs_lt m_lt; // less_than on indices + heap m_heap; // binary heap over weights numeral get_weight(offset_t idx) { numeral w(0); @@ -487,6 +515,7 @@ void hilbert_basis::reset() { void hilbert_basis::collect_statistics(statistics& st) const { st.update("hb.num_subsumptions", m_stats.m_num_subsumptions); st.update("hb.num_resolves", m_stats.m_num_resolves); + st.update("hb.num_saturations", m_stats.m_num_saturations); m_index->collect_statistics(st); } @@ -566,9 +595,11 @@ lbool hilbert_basis::saturate() { init_basis(); for (unsigned i = 0; !m_cancel && i < m_ineqs.size(); ++i) { lbool r = saturate(m_ineqs[i]); + ++m_stats.m_num_saturations; if (r != l_true) { return r; } + } if (m_cancel) { return l_undef; @@ -650,6 +681,7 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) { u[k] = v[k] + w[k]; } u.value() = v.value() + w.value(); + // std::cout << "resolve: " << v.value() << " + " << w.value() << " = " << u.value() << "\n"; TRACE("hilbert_basis_verbose", display(tout, i); display(tout, j); @@ -674,11 +706,12 @@ hilbert_basis::offset_t hilbert_basis::alloc_vector() { void hilbert_basis::add_goal(offset_t idx) { values v = vec(idx); + if (is_subsumed(idx)) { + return; + } m_index->insert(idx, v); if (v.value().is_zero()) { - if (!is_subsumed(idx)) { - m_zero.push_back(idx); - } + m_zero.push_back(idx); } else { m_passive->insert(idx); diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index 73a9c89a5..f4529de85 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -50,6 +50,7 @@ private: struct stats { unsigned m_num_subsumptions; unsigned m_num_resolves; + unsigned m_num_saturations; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index 275aa486d..86b0f1bad 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -1,5 +1,78 @@ #include "hilbert_basis.h" +#include +#include +hilbert_basis* g_hb = 0; +static double g_start_time; + +static void display_statistics(hilbert_basis& hb) { + double time = static_cast(clock()) - g_start_time; + statistics st; + hb.collect_statistics(st); + st.display(std::cout); + std::cout << "time: " << (time / CLOCKS_PER_SEC) << " secs\n"; +} + +static void on_ctrl_c(int) { + signal (SIGINT, SIG_DFL); + display_statistics(*g_hb); + raise(SIGINT); +} + +static void saturate_basis(hilbert_basis& hb) { + signal(SIGINT, on_ctrl_c); + g_hb = &hb; + g_start_time = static_cast(clock()); + lbool is_sat = hb.saturate(); + + switch(is_sat) { + case l_true: + std::cout << "sat\n"; + hb.display(std::cout); + break; + case l_false: + std::cout << "unsat\n"; + break; + case l_undef: + std::cout << "undef\n"; + break; + } + display_statistics(hb); +} + +/** + n - number of variables. + k - subset of variables to be non-zero + bound - numeric value of upper and lower bound + num_ineqs - number of inequalities to create +*/ +static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound, unsigned num_ineqs) { + std::cout << "Gorrila test\n"; + random_gen rand(seed); + hilbert_basis hb; + SASSERT(0 < bound); + SASSERT(k <= n); + int ibound = static_cast(bound); + for (unsigned i = 0; i < num_ineqs; ++i) { + vector nv; + nv.resize(n); + rational a0; + unsigned num_selected = 0; + while (num_selected < k) { + unsigned s = rand(n); + if (nv[s].is_zero()) { + nv[s] = rational(ibound - static_cast(rand(2*bound+1))); + if (!nv[s].is_zero()) { + ++num_selected; + } + } + } + a0 = rational(ibound - static_cast(rand(2*bound+1))); + hb.add_ge(nv, a0); + } + hb.display(std::cout << "Saturate\n"); + saturate_basis(hb); +} static vector vec(int i, int j, int k) { vector nv; @@ -45,25 +118,6 @@ static vector vec(int i, int j, int k, int l, int x, int y, int z) { } -static void saturate_basis(hilbert_basis& hb) { - lbool is_sat = hb.saturate(); - - switch(is_sat) { - case l_true: - std::cout << "sat\n"; - hb.display(std::cout); - break; - case l_false: - std::cout << "unsat\n"; - break; - case l_undef: - std::cout << "undef\n"; - break; - } - statistics st; - hb.collect_statistics(st); - st.display(std::cout); -} // example 9, Ajili, Contenjean @@ -191,6 +245,7 @@ static void tst11() { void tst_hilbert_basis() { std::cout << "hilbert basis test\n"; +#if 0 tst1(); tst2(); tst3(); @@ -202,4 +257,11 @@ void tst_hilbert_basis() { tst9(); tst10(); tst11(); + gorrila_test(0, 4, 3, 20, 5); + gorrila_test(1, 4, 3, 20, 5); + gorrila_test(2, 4, 3, 20, 5); + gorrila_test(0, 4, 2, 20, 5); + gorrila_test(0, 4, 2, 20, 5); +#endif + gorrila_test(0, 10, 7, 20, 11); }