From 562ae7bec53b4f0dea2bf6926a82ff377aee822c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Feb 2013 21:52:10 -0800 Subject: [PATCH] faster saturation without backwards subsumption and using SOS-style set Signed-off-by: Nikolaj Bjorner --- src/muz_qe/heap_trie.h | 283 +++++++++++++++++++++++++++--- src/muz_qe/hilbert_basis.cpp | 327 +++++++++++++++++++++++++++++++++-- src/muz_qe/hilbert_basis.h | 19 +- src/test/heap_trie.cpp | 3 +- src/test/hilbert_basis.cpp | 20 +++ 5 files changed, 607 insertions(+), 45 deletions(-) diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h index 25689e930..ba7ab72f9 100644 --- a/src/muz_qe/heap_trie.h +++ b/src/muz_qe/heap_trie.h @@ -44,7 +44,7 @@ Notes: #include "small_object_allocator.h" -template +template class heap_trie { struct stats { @@ -180,6 +180,8 @@ class heap_trie { small_object_allocator m_alloc; unsigned m_num_keys; + unsigned_vector m_keys; + unsigned m_do_reshuffle; node* m_root; stats m_stats; node* m_spare_leaf; @@ -190,6 +192,7 @@ public: heap_trie(): m_alloc("heap_trie"), m_num_keys(0), + m_do_reshuffle(4), m_root(0), m_spare_leaf(0), m_spare_trie(0) @@ -202,7 +205,7 @@ public: } unsigned size() const { - return m_root->num_leaves(); + return m_root?m_root->num_leaves():0; } void reset(unsigned num_keys) { @@ -210,6 +213,10 @@ public: del_node(m_spare_leaf); del_node(m_spare_trie); m_num_keys = num_keys; + m_keys.resize(num_keys); + for (unsigned i = 0; i < num_keys; ++i) { + m_keys[i] = i; + } m_root = mk_trie(); m_spare_trie = mk_trie(); m_spare_leaf = mk_leaf(); @@ -217,7 +224,13 @@ public: void insert(Key const* keys, Value const& val) { ++m_stats.m_num_inserts; - insert(m_root, num_keys(), keys, val); + insert(m_root, num_keys(), keys, m_keys.c_ptr(), val); +#if 0 + if (m_stats.m_num_inserts == (1 << m_do_reshuffle)) { + m_do_reshuffle++; + reorder_keys(); + } +#endif } bool find_eq(Key const* keys, Value& value) { @@ -225,7 +238,7 @@ public: node* n = m_root; node* m; for (unsigned i = 0; i < num_keys(); ++i) { - if (!to_trie(n)->find(keys[i], m)) { + if (!to_trie(n)->find(get_key(keys, i), m)) { return false; } n = m; @@ -242,7 +255,7 @@ public: for (unsigned i = 0; i < num_keys(); ++i) { for (unsigned j = 0; j < todo[index].size(); ++j) { ++m_stats.m_num_find_le_nodes; - to_trie(todo[index][j])->find_le(keys[i], todo[!index]); + to_trie(todo[index][j])->find_le(get_key(keys, i), todo[!index]); } todo[index].reset(); index = !index; @@ -271,7 +284,7 @@ public: node* m; for (unsigned i = 0; i < num_keys(); ++i) { n->dec_ref(); - VERIFY (to_trie(n)->find(keys[i], m)); + VERIFY (to_trie(n)->find(get_key(keys, i), m)); n = m; } n->dec_ref(); @@ -287,14 +300,14 @@ public: st.update("heap_trie.num_find_eq", m_stats.m_num_find_eq); st.update("heap_trie.num_find_le", m_stats.m_num_find_le); st.update("heap_trie.num_find_le_nodes", m_stats.m_num_find_le_nodes); - st.update("heap_trie.num_nodes", m_root->num_nodes()); + if (m_root) st.update("heap_trie.num_nodes", m_root->num_nodes()); unsigned_vector nums; ptr_vector todo; - todo.push_back(m_root); + if (m_root) todo.push_back(m_root); while (!todo.empty()) { node* n = todo.back(); todo.pop_back(); - if (n->type() == trie_t) { + if (is_trie(n)) { trie* t = to_trie(n); unsigned sz = t->nodes().size(); if (nums.size() <= sz) { @@ -334,38 +347,252 @@ public: out << "\n"; } + class iterator { + ptr_vector m_path; + unsigned_vector m_idx; + vector m_keys; + unsigned m_count; + public: + iterator(node* n) { + if (!n) { + m_count = UINT_MAX; + } + else { + m_count = 0; + first(n); + } + } + Key const* keys() { + return m_keys.c_ptr(); + } + + Value const& value() const { + return to_leaf(m_path.back())->get_value(); + } + iterator& operator++() { fwd(); return *this; } + iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } + bool operator==(iterator const& it) const {return m_count == it.m_count; } + bool operator!=(iterator const& it) const {return m_count != it.m_count; } + + private: + void first(node* r) { + SASSERT(r->ref_count() > 0); + while (is_trie(r)) { + trie* t = to_trie(r); + m_path.push_back(r); + unsigned sz = t->nodes().size(); + for (unsigned i = 0; i < sz; ++i) { + r = t->nodes()[i].second; + if (r->ref_count() > 0) { + m_idx.push_back(i); + m_keys.push_back(t->nodes()[i].first); + break; + } + } + } + SASSERT(is_leaf(r)); + m_path.push_back(r); + } + + void fwd() { + if (m_path.empty()) { + m_count = UINT_MAX; + return; + } + m_path.pop_back(); + while (!m_path.empty()) { + trie* t = to_trie(m_path.back()); + unsigned idx = m_idx.back(); + unsigned sz = t->nodes().size(); + m_idx.pop_back(); + m_keys.pop_back(); + for (unsigned i = idx+1; i < sz; ++i) { + node* r = t->nodes()[i].second; + if (r->ref_count() > 0) { + m_idx.push_back(i); + m_keys.push_back(t->nodes()[i].first); + first(r); + ++m_count; + return; + } + } + m_path.pop_back(); + } + m_count = UINT_MAX; + } + }; + + iterator begin() const { + return iterator(m_root); + } + + iterator end() const { + return iterator(0); + } + + private: - unsigned num_keys() const { + inline unsigned num_keys() const { return m_num_keys; } + inline Key const& get_key(Key const* keys, unsigned i) const { + return keys[m_keys[i]]; + } + + struct KeyEq { + bool operator()(Key const& k1, Key const& k2) const { + return k1 == k2; + } + }; + + + typedef hashtable key_set; + + struct key_info { + unsigned m_index; + unsigned m_index_size; + key_info(unsigned i, unsigned sz): + m_index(i), + m_index_size(sz) + {} + + bool operator<(key_info const& other) const { + return + (m_index_size < other.m_index_size) || + ((m_index_size == other.m_index_size) && + (m_index < other.m_index)); + } + }; + + void reorder_keys() { + vector weights; + weights.resize(num_keys()); + unsigned_vector depth; + ptr_vector nodes; + depth.push_back(0); + nodes.push_back(m_root); + while (!nodes.empty()) { + node* n = nodes.back(); + unsigned d = depth.back(); + nodes.pop_back(); + depth.pop_back(); + if (is_trie(n)) { + trie* t = to_trie(n); + unsigned sz = t->nodes().size(); + for (unsigned i = 0; i < sz; ++i) { + nodes.push_back(t->nodes()[i].second); + depth.push_back(d+1); + weights[d].insert(t->nodes()[i].first); + } + } + } + SASSERT(weights.size() == num_keys()); + svector infos; + unsigned sz = 0; + bool is_sorted = true; + for (unsigned i = 0; i < weights.size(); ++i) { + unsigned sz2 = weights[i].size(); + if (sz > sz2) { + is_sorted = false; + } + sz = sz2; + infos.push_back(key_info(i, sz)); + } + if (is_sorted) { + return; + } + std::sort(infos.begin(), infos.end()); + unsigned_vector sorted_keys, new_keys; + for (unsigned i = 0; i < num_keys(); ++i) { + unsigned j = infos[i].m_index; + sorted_keys.push_back(j); + new_keys.push_back(m_keys[j]); + } + // m_keys: i |-> key_index + // new_keys: i |-> new_key_index + // permutation: key_index |-> new_key_index + SASSERT(sorted_keys.size() == num_keys()); + SASSERT(new_keys.size() == num_keys()); + SASSERT(m_keys.size() == num_keys()); + iterator it = begin(); + trie* new_root = mk_trie(); + IF_VERBOSE(1, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";); + for (; it != end(); ++it) { + IF_VERBOSE(2, + for (unsigned i = 0; i < num_keys(); ++i) { + for (unsigned j = 0; j < num_keys(); ++j) { + if (m_keys[j] == i) { + verbose_stream() << it.keys()[j] << " "; + break; + } + } + } + verbose_stream() << " |-> " << it.value() << "\n";); + + insert(new_root, num_keys(), it.keys(), sorted_keys.c_ptr(), it.value()); + } + del_node(m_root); + m_root = new_root; + for (unsigned i = 0; i < m_keys.size(); ++i) { + m_keys[i] = new_keys[i]; + } + + IF_VERBOSE(1, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";); + IF_VERBOSE(2, + it = begin(); + for (; it != end(); ++it) { + for (unsigned i = 0; i < num_keys(); ++i) { + for (unsigned j = 0; j < num_keys(); ++j) { + if (m_keys[j] == i) { + verbose_stream() << it.keys()[j] << " "; + break; + } + } + } + verbose_stream() << " |-> " << it.value() << "\n"; + }); + } + bool find_le(node* n, unsigned index, Key const* keys, check_value& check) { if (index == num_keys()) { SASSERT(n->ref_count() > 0); - return check(to_leaf(n)->get_value()); + bool r = check(to_leaf(n)->get_value()); + IF_VERBOSE(1, + for (unsigned j = 0; j < index; ++j) { + verbose_stream() << " "; + } + verbose_stream() << to_leaf(n)->get_value() << (r?" hit\n":" miss\n");); + return r; } else { - Key key = keys[index]; - children_t const& nodes = to_trie(n)->nodes(); + Key const& key = get_key(keys, index); + children_t& nodes = to_trie(n)->nodes(); for (unsigned i = 0; i < nodes.size(); ++i) { ++m_stats.m_num_find_le_nodes; - if (KeyLE::le(nodes[i].first, key)) { - node* m = nodes[i].second; - if (m->ref_count() > 0 && find_le(m, index+1, keys, check)) { - return true; + node* m = nodes[i].second; + IF_VERBOSE(1, + for (unsigned j = 0; j < index; ++j) { + verbose_stream() << " "; + } + verbose_stream() << nodes[i].first << " <=? " << key << " rc:" << m->ref_count() << "\n";); + if (m->ref_count() > 0 && KeyLE::le(nodes[i].first, key) && find_le(m, index+1, keys, check)) { + if (i > 0) { + std::swap(nodes[i], nodes[0]); } + return true; } } return false; } } - void insert(node* n, unsigned num_keys, Key const* keys, Value const& val) { + void insert(node* n, unsigned num_keys, Key const* keys, unsigned const* permutation, Value const& val) { // assumption: key is not in table. for (unsigned i = 0; i < num_keys; ++i) { n->inc_ref(); - n = insert_key(to_trie(n), (i + 1 == num_keys), keys[i]); + n = insert_key(to_trie(n), (i + 1 == num_keys), keys[permutation[i]]); } n->inc_ref(); to_leaf(n)->set_value(val); @@ -400,7 +627,7 @@ private: if (!n) { return; } - if (n->type() == trie_t) { + if (is_trie(n)) { trie* t = to_trie(n); for (unsigned i = 0; i < t->nodes().size(); ++i) { del_node(t->nodes()[i].second); @@ -415,15 +642,23 @@ private: } } - trie* to_trie(node* n) const { - SASSERT(n->type() == trie_t); + static trie* to_trie(node* n) { + SASSERT(is_trie(n)); return static_cast(n); } - leaf* to_leaf(node* n) const { - SASSERT(n->type() == leaf_t); + static leaf* to_leaf(node* n) { + SASSERT(is_leaf(n)); return static_cast(n); } + + static bool is_leaf(node* n) { + return n->type() == leaf_t; + } + + static bool is_trie(node* n) { + return n->type() == trie_t; + } }; #endif diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 7d15a1958..49bf20746 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -25,6 +25,8 @@ Revision History: template class rational_map : public map {}; +typedef int_hashtable > int_table; + class hilbert_basis::value_index1 { struct stats { @@ -36,7 +38,6 @@ class hilbert_basis::value_index1 { void reset() { memset(this, 0, sizeof(*this)); } }; - typedef int_hashtable > int_table; hilbert_basis& hb; int_table m_table; stats m_stats; @@ -167,7 +168,9 @@ class hilbert_basis::value_index2 { return hilbert_basis::is_abs_geq(n2, n1); } }; - struct checker : public heap_trie::check_value { + + typedef heap_trie ht; + struct checker : public ht::check_value { hilbert_basis* hb; offset_t m_value; offset_t* m_found; @@ -183,7 +186,7 @@ class hilbert_basis::value_index2 { } }; hilbert_basis& hb; - heap_trie m_trie; + ht m_trie; vector m_found; bool m_init; checker m_checker; @@ -483,16 +486,168 @@ public: } }; + +class hilbert_basis::vector_lt_t { + hilbert_basis& hb; +public: + vector_lt_t(hilbert_basis& hb): hb(hb) {} + bool operator()(offset_t idx1, offset_t idx2) const { + return hb.vector_lt(idx1, idx2); + } +}; + + +class hilbert_basis::passive2 { + struct lt { + passive2** p; + lt(passive2** p): p(p) {} + bool operator()(int v1, int v2) const { + return (**p)(v1, v2); + } + }; + hilbert_basis& hb; + svector const& m_sos; + unsigned_vector m_psos; + svector m_pas; + vector m_weight; + unsigned_vector m_free_list; + passive2* m_this; + lt m_lt; + heap m_heap; // binary heap over weights + + numeral sum_abs(offset_t idx) const { + numeral w(0); + unsigned nv = hb.get_num_vars(); + for (unsigned i = 0; i < nv; ++i) { + w += abs(hb.vec(idx)[i]); + } + return w; + } + +public: + passive2(hilbert_basis& hb): + hb(hb), + m_sos(hb.m_sos), + m_lt(&m_this), + m_heap(10, m_lt) + { + m_this = this; + } + + void reset() { + m_heap.reset(); + m_free_list.reset(); + m_psos.reset(); + m_pas.reset(); + m_weight.reset(); + } + + void insert(offset_t idx, unsigned offset) { + SASSERT(!m_sos.empty()); + unsigned v; + numeral w = sum_abs(idx) + sum_abs(m_sos[0]); + if (m_free_list.empty()) { + v = m_pas.size(); + m_pas.push_back(idx); + m_psos.push_back(offset); + m_weight.push_back(w); + m_heap.set_bounds(v+1); + } + else { + v = m_free_list.back(); + m_free_list.pop_back(); + m_pas[v] = idx; + m_psos[v] = offset; + m_weight[v] = w; + } + next_resolvable(v); + } + + bool empty() const { + return m_heap.empty(); + } + + unsigned pop(offset_t& sos, offset_t& pas) { + SASSERT (!empty()); + unsigned val = static_cast(m_heap.erase_min()); + unsigned psos = m_psos[val]; + sos = m_sos[psos]; + pas = m_pas[val]; + m_psos[val]++; + next_resolvable(val); + numeral old_weight = hb.vec(pas).weight(); + numeral new_weight = hb.vec(sos).weight() + old_weight; + if (new_weight.is_pos() != old_weight.is_pos()) { + psos = 0; + } + return psos; + } + + bool operator()(int v1, int v2) const { + return m_weight[v1] < m_weight[v2]; + } + + class iterator { + passive2& p; + unsigned m_idx; + void fwd() { + while (m_idx < p.m_pas.size() && + is_invalid_offset(p.m_pas[m_idx])) { + ++m_idx; + } + } + public: + iterator(passive2& p, unsigned i): p(p), m_idx(i) { fwd(); } + offset_t pas() const { return p.m_pas[m_idx]; } + offset_t sos() const { return p.m_sos[p.m_psos[m_idx]]; } + iterator& operator++() { ++m_idx; fwd(); return *this; } + iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } + bool operator==(iterator const& it) const {return m_idx == it.m_idx; } + bool operator!=(iterator const& it) const {return m_idx != it.m_idx; } + }; + + iterator begin() { + return iterator(*this, 0); + } + + iterator end() { + return iterator(*this, m_pas.size()); + } +private: + void next_resolvable(unsigned v) { + offset_t pas = m_pas[v]; + while (m_psos[v] < m_sos.size()) { + offset_t sos = m_sos[m_psos[v]]; + if (hb.can_resolve(sos, pas)) { + m_weight[v] = sum_abs(pas) + sum_abs(sos); + m_heap.insert(v); + return; + } + ++m_psos[v]; + } + // add pas to free-list for hb if it is not in sos. + m_free_list.push_back(v); + m_psos[v] = UINT_MAX; + m_pas[v] = mk_invalid_offset(); + } +}; + + hilbert_basis::hilbert_basis(): - m_cancel(false) + m_cancel(false), + m_use_support(true), + m_use_ordered_support(true), + m_use_ordered_subsumption(true) { m_index = alloc(index, *this); m_passive = alloc(passive, *this); + m_passive2 = alloc(passive2, *this); } hilbert_basis::~hilbert_basis() { dealloc(m_index); dealloc(m_passive); + dealloc(m_passive2); } hilbert_basis::offset_t hilbert_basis::mk_invalid_offset() { @@ -510,6 +665,7 @@ void hilbert_basis::reset() { m_free_list.reset(); m_active.reset(); m_passive->reset(); + m_passive2->reset(); m_zero.reset(); m_index->reset(); m_cancel = false; @@ -621,6 +777,7 @@ lbool hilbert_basis::saturate() { init_basis(); m_current_ineq = 0; while (!m_cancel && m_current_ineq < m_ineqs.size()) { + IF_VERBOSE(1, { statistics st; collect_statistics(st); st.display(verbose_stream()); }); select_inequality(); lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]); ++m_stats.m_num_saturations; @@ -635,27 +792,26 @@ lbool hilbert_basis::saturate() { return l_true; } -lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { +lbool hilbert_basis::saturate_orig(num_vector const& ineq, bool is_eq) { m_active.reset(); m_passive->reset(); m_zero.reset(); m_index->reset(); + int_table support; TRACE("hilbert_basis", display_ineq(tout, ineq, is_eq);); - bool has_non_negative = false; iterator it = begin(); for (; it != end(); ++it) { - values v = vec(*it); + offset_t idx = *it; + values v = vec(idx); v.weight() = get_weight(v, ineq); - add_goal(*it); - if (v.weight().is_nonneg()) { - has_non_negative = true; + add_goal(idx); + if (m_use_support) { + support.insert(idx.m_offset); } } TRACE("hilbert_basis", display(tout);); - if (!has_non_negative) { - return l_false; - } // resolve passive into active + offset_t j = alloc_vector(); while (!m_passive->empty()) { if (m_cancel) { return l_undef; @@ -667,14 +823,16 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { continue; } for (unsigned i = 0; !m_cancel && i < m_active.size(); ++i) { - if (can_resolve(idx, m_active[i])) { - offset_t j = alloc_vector(); + if ((!m_use_support || support.contains(m_active[i].m_offset)) && can_resolve(idx, m_active[i])) { resolve(idx, m_active[i], j); - add_goal(j); + if (add_goal(j)) { + j = alloc_vector(); + } } } m_active.push_back(idx); } + m_free_list.push_back(j); // Move positive from active and zeros to new basis. m_basis.reset(); m_basis.append(m_zero); @@ -691,7 +849,103 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { m_passive->reset(); m_zero.reset(); TRACE("hilbert_basis", display(tout);); - return l_true; + return m_basis.empty()?l_false:l_true; +} + +bool hilbert_basis::vector_lt(offset_t idx1, offset_t idx2) const { + values v = vec(idx1); + values w = vec(idx2); + numeral a(0), b(0); + for (unsigned i = 0; i < get_num_vars(); ++i) { + a += abs(v[i]); + b += abs(w[i]); + } + return a < b; +} + +lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { + m_zero.reset(); + m_index->reset(); + m_passive2->reset(); + m_sos.reset(); + TRACE("hilbert_basis", display_ineq(tout, ineq, is_eq);); + unsigned init_basis_size = 0; + for (unsigned i = 0; i < m_basis.size(); ++i) { + offset_t idx = m_basis[i]; + values v = vec(idx); + v.weight() = get_weight(v, ineq); + m_index->insert(idx, v); + if (v.weight().is_zero()) { + m_zero.push_back(idx); + } + else { + if (v.weight().is_pos()) { + m_basis[init_basis_size++] = idx; + } + m_sos.push_back(idx); + } + } + m_basis.resize(init_basis_size); + // ASSERT basis is sorted by weight. + + // initialize passive + for (unsigned i = 0; (init_basis_size > 0) && i < m_sos.size(); ++i) { + if (vec(m_sos[i]).weight().is_neg()) { + m_passive2->insert(m_sos[i], 0); + } + } + + TRACE("hilbert_basis", display(tout);); + // resolve passive into active + offset_t idx = alloc_vector(); + while (!m_cancel && !m_passive2->empty()) { + offset_t sos, pas; + TRACE("hilbert_basis", display(tout); ); + unsigned offset = m_passive2->pop(sos, pas); + SASSERT(can_resolve(sos, pas)); + resolve(sos, pas, idx); + if (is_subsumed(idx)) { + continue; + } + values v = vec(idx); + m_index->insert(idx, v); + if (v.weight().is_zero()) { + m_zero.push_back(idx); + } + else { + if (!m_use_ordered_support) { + offset = 0; + } + m_passive2->insert(idx, offset); + if (v.weight().is_pos()) { + m_basis.push_back(idx); + } + } + idx = alloc_vector(); + } + if (m_cancel) { + return l_undef; + } + + m_free_list.push_back(idx); + // remove positive values from basis if we are looking for an equality. + while (is_eq && !m_basis.empty()) { + m_free_list.push_back(m_basis.back()); + m_basis.pop_back(); + } + for (unsigned i = 0; i < init_basis_size; ++i) { + offset_t idx = m_basis[i]; + if (vec(idx).weight().is_neg()) { + m_basis[i] = m_basis.back(); + m_basis.pop_back(); + + } + } + m_basis.append(m_zero); + std::sort(m_basis.begin(), m_basis.end(), vector_lt_t(*this)); + m_zero.reset(); + TRACE("hilbert_basis", display(tout);); + return m_basis.empty()?l_false:l_true; } void hilbert_basis::get_basis_solution(unsigned i, num_vector& v, bool& is_initial) { @@ -716,11 +970,20 @@ void hilbert_basis::select_inequality() { unsigned best = m_current_ineq; unsigned non_zeros = get_num_nonzeros(m_ineqs[best]); unsigned prod = get_ineq_product(m_ineqs[best]); + //numeral diff = get_ineq_diff(m_ineqs[best]); for (unsigned j = best+1; prod != 0 && j < m_ineqs.size(); ++j) { unsigned non_zeros2 = get_num_nonzeros(m_ineqs[j]); unsigned prod2 = get_ineq_product(m_ineqs[j]); + //numeral diff2 = get_ineq_diff(m_ineqs[j]); + if (prod2 == 0) { + prod = prod2; + non_zeros = non_zeros2; + best = j; + break; + } if (non_zeros2 < non_zeros || (non_zeros2 == non_zeros && prod2 < prod)) { prod = prod2; + // diff = diff2; non_zeros = non_zeros2; best = j; } @@ -757,6 +1020,22 @@ unsigned hilbert_basis::get_ineq_product(num_vector const& ineq) { return num_pos * num_neg; } +hilbert_basis::numeral hilbert_basis::get_ineq_diff(num_vector const& ineq) { + numeral max_pos(0), min_neg(0); + iterator it = begin(); + for (; it != end(); ++it) { + values v = vec(*it); + numeral w = get_weight(v, ineq); + if (w > max_pos) { + max_pos = w; + } + else if (w < min_neg) { + min_neg = w; + } + } + return max_pos - min_neg; +} + void hilbert_basis::recycle(offset_t idx) { m_index->remove(idx, vec(idx)); m_free_list.push_back(idx); @@ -794,11 +1073,11 @@ hilbert_basis::offset_t hilbert_basis::alloc_vector() { } } -void hilbert_basis::add_goal(offset_t idx) { +bool hilbert_basis::add_goal(offset_t idx) { TRACE("hilbert_basis", display(tout, idx);); values v = vec(idx); if (is_subsumed(idx)) { - return; + return false; } m_index->insert(idx, v); if (v.weight().is_zero()) { @@ -807,6 +1086,7 @@ void hilbert_basis::add_goal(offset_t idx) { else { m_passive->insert(idx); } + return true; } bool hilbert_basis::is_subsumed(offset_t idx) { @@ -885,6 +1165,15 @@ void hilbert_basis::display(std::ostream& out) const { display(out, *it); } } + if (!m_passive2->empty()) { + passive2::iterator it = m_passive2->begin(); + passive2::iterator end = m_passive2->end(); + out << "passive:\n"; + for (; it != end; ++it) { + display(out << "sos:", it.sos()); + display(out << "pas:", it.pas()); + } + } if (!m_zero.empty()) { out << "zero:\n"; for (unsigned i = 0; i < m_zero.size(); ++i) { diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index 567d72fbc..78d4d7cec 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -36,6 +36,7 @@ private: class value_index2; class index; class passive; + class passive2; struct offset_t { unsigned m_offset; offset_t(unsigned o) : m_offset(o) {} @@ -69,13 +70,20 @@ private: svector m_basis; // vector of current basis svector m_free_list; // free list of unused storage svector m_active; // active set + svector m_sos; // set of support svector m_zero; // zeros passive* m_passive; // passive set + passive2* m_passive2; // passive set volatile bool m_cancel; stats m_stats; index* m_index; // index of generated vectors unsigned_vector m_ints; // indices that can be both positive and negative unsigned m_current_ineq; + + bool m_use_support; // parameter: (associativity) resolve only against vectors that are initially in basis. + bool m_use_ordered_support; // parameter: (commutativity) resolve in order + bool m_use_ordered_subsumption; // parameter + class iterator { hilbert_basis const& hb; unsigned m_idx; @@ -91,10 +99,12 @@ private: static offset_t mk_invalid_offset(); static bool is_invalid_offset(offset_t offs); lbool saturate(num_vector const& ineq, bool is_eq); + lbool saturate_orig(num_vector const& ineq, bool is_eq); void init_basis(); void select_inequality(); unsigned get_num_nonzeros(num_vector const& ineq); unsigned get_ineq_product(num_vector const& ineq); + numeral get_ineq_diff(num_vector const& ineq); void add_unit_vector(unsigned i, numeral const& e); unsigned get_num_vars() const; @@ -106,12 +116,15 @@ private: void recycle(offset_t idx); bool can_resolve(offset_t i, offset_t j) const; sign_t get_sign(offset_t idx) const; - void add_goal(offset_t idx); + bool add_goal(offset_t idx); offset_t alloc_vector(); void resolve(offset_t i, offset_t j, offset_t r); iterator begin() const { return iterator(*this,0); } iterator end() const { return iterator(*this, m_basis.size()); } + class vector_lt_t; + bool vector_lt(offset_t i, offset_t j) const; + values vec(offset_t offs) const; void display(std::ostream& out, offset_t o) const; @@ -125,6 +138,10 @@ public: void reset(); + void set_use_support(bool b) { m_use_support = b; } + void set_use_ordered_support(bool b) { m_use_ordered_support = b; } + void set_use_ordered_subsumption(bool b) { m_use_ordered_subsumption = b; } + // add inequality v*x >= 0 // add inequality v*x <= 0 // add equality v*x = 0 diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp index ad3cd0a8d..7b57f97f2 100644 --- a/src/test/heap_trie.cpp +++ b/src/test/heap_trie.cpp @@ -4,7 +4,8 @@ struct unsigned_le { static bool le(unsigned i, unsigned j) { return i <= j; } }; -typedef heap_trie heap_trie_t; + +typedef heap_trie heap_trie_t; static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) { statistics st; diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index b02c8c90c..e2d1d337e 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -10,6 +10,9 @@ #include #include +static bool g_use_ordered_support = false; +static bool g_use_ordered_subsumption = false; +static bool g_use_support = false; class hilbert_basis_validate { ast_manager& m; @@ -241,6 +244,9 @@ static void saturate_basis(hilbert_basis& hb) { signal(SIGINT, on_ctrl_c); g_hb = &hb; g_start_time = static_cast(clock()); + hb.set_use_ordered_support(g_use_ordered_support); + hb.set_use_support(g_use_support); + hb.set_use_ordered_subsumption(g_use_ordered_subsumption); lbool is_sat = hb.saturate(); switch(is_sat) { @@ -505,6 +511,10 @@ static void tst15() { void tst_hilbert_basis() { std::cout << "hilbert basis test\n"; +// tst3(); +// return; + + g_use_ordered_support = true; if (true) { tst1(); @@ -531,4 +541,14 @@ void tst_hilbert_basis() { else { gorrila_test(0, 10, 7, 20, 11); } + + return; + std::cout << "ordered support\n"; + g_use_ordered_support = true; + tst4(); + + std::cout << "non-ordered support\n"; + g_use_ordered_support = false; + tst4(); + }