From 306855ba55dc901d6e3f5137f5d4447a3cd21f47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2013 22:45:37 -0800 Subject: [PATCH] fix hilbert_basis tests and add heap_trie index Signed-off-by: Nikolaj Bjorner --- src/muz_qe/heap_trie.h | 355 +++++++++++++++++++++++++++++++++++ src/muz_qe/hilbert_basis.cpp | 175 +++++++++++------ src/muz_qe/hilbert_basis.h | 4 +- src/test/heap_trie.cpp | 52 +++++ src/test/hilbert_basis.cpp | 66 +++++-- src/test/main.cpp | 1 + 6 files changed, 579 insertions(+), 74 deletions(-) create mode 100644 src/muz_qe/heap_trie.h create mode 100644 src/test/heap_trie.cpp diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h new file mode 100644 index 000000000..04b7f08d2 --- /dev/null +++ b/src/muz_qe/heap_trie.h @@ -0,0 +1,355 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + heap_trie.h + +Abstract: + + Heap trie structure. + + Structure that lets you retrieve point-wise smaller entries + of a tuple. A lookup is to identify entries whose keys + are point-wise dominated by the lookup key. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-02-15. + +Notes: + + tries are unordered vectors of keys. This could be enhanced to use either + heaps or sorting. The problem with using the heap implementation directly is that there is no way to + retrieve elements less or equal to a key that is not already in the heap. + If nodes have only a few elements, then this would also be a bloated data-structure to maintain. + + Nodes are not de-allocated. Their reference count indicates if they are valid. + Possibly, add garbage collection. + + Maintaining sorted ranges for larger domains is another option. + +--*/ + +#ifndef _HEAP_TRIE_H_ +#define _HEAP_TRIE_H_ + +#include "map.h" +#include "vector.h" +#include "statistics.h" + + +template +class heap_trie { + + struct stats { + unsigned m_num_inserts; + unsigned m_num_removes; + unsigned m_num_find_eq; + unsigned m_num_find_le; + unsigned m_num_find_le_nodes; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + enum node_t { + trie_t, + leaf_t + }; + + class node { + node_t m_type; + unsigned m_ref; + public: + node(node_t t): m_type(t), m_ref(0) {} + virtual ~node() {} + node_t type() const { return m_type; } + void inc_ref() { ++m_ref; } + void dec_ref() { SASSERT(m_ref > 0); --m_ref; } + unsigned ref_count() const { return m_ref; } + virtual void display(std::ostream& out, unsigned indent) const = 0; + virtual unsigned size() const = 0; + }; + + class leaf : public node { + Value m_value; + public: + leaf(): node(leaf_t) {} + virtual ~leaf() {} + Value const& get_value() const { return m_value; } + void set_value(Value const& v) { m_value = v; } + virtual void display(std::ostream& out, unsigned indent) const { + out << " value: " << m_value; + } + virtual unsigned size() const { return 1; } + }; + + // lean trie node + class trie : public node { + vector > m_nodes; + public: + trie(): node(trie_t) {} + + virtual ~trie() { + for (unsigned i = 0; i < m_nodes.size(); ++i) { + dealloc(m_nodes[i].second); + } + } + + node* find_or_insert(Key k, node* n) { + for (unsigned i = 0; i < m_nodes.size(); ++i) { + if (m_nodes[i].first == k) { + return m_nodes[i].second; + } + } + m_nodes.push_back(std::make_pair(k, n)); + return n; + } + + bool find(Key k, node*& n) const { + for (unsigned i = 0; i < m_nodes.size(); ++i) { + if (m_nodes[i].first == k) { + n = m_nodes[i].second; + return n->ref_count() > 0; + } + } + return false; + } + + // push nodes whose keys are <= key into vector. + void find_le(Key key, ptr_vector& nodes) { + for (unsigned i = 0; i < m_nodes.size(); ++i) { + if (m_nodes[i].first <= key) { + node* n = m_nodes[i].second; + if (n->ref_count() > 0){ + nodes.push_back(n); + } + } + } + } + + virtual void display(std::ostream& out, unsigned indent) const { + for (unsigned j = 0; j < m_nodes.size(); ++j) { + out << "\n"; + for (unsigned i = 0; i < indent; ++i) { + out << " "; + } + node* n = m_nodes[j].second; + out << m_nodes[j].first << " count: " << n->ref_count(); + n->display(out, indent + 1); + } + } + + virtual unsigned size() const { + unsigned sz = 1; + for (unsigned j = 0; j < m_nodes.size(); ++j) { + sz += m_nodes[j].second->size(); + } + return sz; + } + + private: + bool contains(Key k) { + for (unsigned j = 0; j < m_nodes.size(); ++j) { + if (m_nodes[j].first == k) { + return true; + } + } + return false; + } + + }; + + unsigned m_num_keys; + node* m_root; + stats m_stats; + node* m_spare_leaf; + node* m_spare_trie; + vector > m_children; +public: + + heap_trie(): + m_num_keys(0), + m_root(0), + m_spare_leaf(0), + m_spare_trie(0) + {} + + ~heap_trie() { + dealloc(m_root); + dealloc(m_spare_leaf); + dealloc(m_spare_trie); + } + + unsigned size() const { + return m_root->size(); + } + + void reset(unsigned num_keys) { + dealloc(m_root); + dealloc(m_spare_leaf); + dealloc(m_spare_trie); + m_num_keys = num_keys; + m_root = mk_trie(); + m_spare_trie = mk_trie(); + m_spare_leaf = mk_leaf(); + } + + void insert(Key const* keys, Value const& val) { + ++m_stats.m_num_inserts; + insert(m_root, num_keys(), keys, val); + } + + bool find_eq(Key const* keys, Value& value) { + ++m_stats.m_num_find_eq; + node* n = m_root; + node* m; + for (unsigned i = 0; i < num_keys(); ++i) { + if (!to_trie(n)->find(keys[i], m)) { + return false; + } + n = m; + } + value = to_leaf(n)->get_value(); + return true; + } + + void find_le(Key const* keys, vector& values) { + ++m_stats.m_num_find_le; + ptr_vector todo[2]; + todo[0].push_back(m_root); + bool index = false; + 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]); + } + todo[index].reset(); + index = !index; + } + for (unsigned j = 0; j < todo[index].size(); ++j) { + values.push_back(to_leaf(todo[index][j])->get_value()); + } + } + + + // callback based find function + class check_value { + public: + virtual bool operator()(Value const& v) = 0; + }; + + bool find_le(Key const* keys, check_value& check) { + ++m_stats.m_num_find_le; + if (m_children.size() < num_keys()) { + m_children.resize(num_keys()); + } + return find_le(m_root, 0, keys, check); + } + + bool find_le(node* n, unsigned index, Key const* keys, check_value& check) { + ++m_stats.m_num_find_le_nodes; + if (index == num_keys()) { + SASSERT(n->ref_count() > 0); + return check(to_leaf(n)->get_value()); + } + else { + m_children[index].reset(); + to_trie(n)->find_le(keys[index], m_children[index]); + for (unsigned i = 0; i < m_children[index].size(); ++i) { + if (find_le(m_children[index][i], index + 1, keys, check)) { + return true; + } + } + return false; + } + } + + void remove(Key const* keys) { + ++m_stats.m_num_removes; + // assumption: key is in table. + node* n = m_root; + node* m; + for (unsigned i = 0; i < num_keys(); ++i) { + n->dec_ref(); + VERIFY (to_trie(n)->find(keys[i], m)); + n = m; + } + n->dec_ref(); + } + + void reset_statistics() { + m_stats.reset(); + } + + void collect_statistics(statistics& st) const { + st.update("heap_trie.num_inserts", m_stats.m_num_inserts); + st.update("heap_trie.num_removes", m_stats.m_num_removes); + 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); + } + + void display(std::ostream& out) { + m_root->display(out, 0); + out << "\n"; + } + +private: + + unsigned num_keys() const { + return m_num_keys; + } + + void insert(node* n, unsigned num_keys, Key const* keys, Value const& val) { + // assumption: key is not in table. + + while (true) { + n->inc_ref(); + if (num_keys == 0) { + to_leaf(n)->set_value(val); + SASSERT(n->ref_count() == 1); + break; + } + else { + n = insert_key(to_trie(n), (num_keys == 1), keys[0]); + --num_keys; + ++keys; + } + } + } + + node* insert_key(trie* n, bool is_leaf, Key const& key) { + node* m1 = is_leaf?m_spare_leaf:m_spare_trie; + node* m2 = n->find_or_insert(key, m1); + if (m1 == m2) { + if (is_leaf) { + m_spare_leaf = mk_leaf(); + } + else { + m_spare_trie = mk_trie(); + } + } + return m2; + } + + leaf* mk_leaf() { + return alloc(leaf); + } + + trie* mk_trie() { + return alloc(trie); + } + + trie* to_trie(node* n) { + SASSERT(n->type() == trie_t); + return static_cast(n); + } + + leaf* to_leaf(node* n) { + SASSERT(n->type() == leaf_t); + return static_cast(n); + } +}; + +#endif diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index dd0041fa9..10e222fcf 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -20,12 +20,13 @@ Revision History: #include "hilbert_basis.h" #include "heap.h" #include "map.h" +#include "heap_trie.h" template class rational_map : public map {}; -class hilbert_basis::value_index { +class hilbert_basis::value_index1 { struct stats { unsigned m_num_comparisons; unsigned m_num_hit; @@ -41,7 +42,7 @@ class hilbert_basis::value_index { stats m_stats; public: - value_index(hilbert_basis& hb): + value_index1(hilbert_basis& hb): hb(hb) {} @@ -128,12 +129,112 @@ private: } }; +class hilbert_basis::value_index2 { + struct checker : public heap_trie::check_value { + hilbert_basis* hb; + offset_t m_value; + offset_t m_found; + checker(): hb(0) {} + virtual bool operator()(unsigned const& v) { + if (m_value.m_offset != v && hb->is_subsumed(m_value, offset_t(v))) { + m_found = offset_t(v); + return true; + } + else { + return false; + } + } + }; + hilbert_basis& hb; + heap_trie m_trie; + vector m_found; + bool m_init; + checker m_checker; + + +public: + value_index2(hilbert_basis& hb): hb(hb), m_init(false) { + m_checker.hb = &hb; + } + + void insert(offset_t idx, values const& vs) { + init(); + m_trie.insert(vs()-1, idx.m_offset); + } + + void remove(offset_t idx, values const& vs) { + m_trie.remove(vs()-1); + } + + void reset() { + m_trie.reset(hb.get_num_vars()); + } + + bool find(offset_t idx, values const& vs, offset_t& found_idx) { + init(); + m_found.reset(); + m_checker.m_value = idx; + if (!m_trie.find_le(vs()-1, m_checker)) { + return false; + } + else { + found_idx = m_checker.m_found; + return true; + } + } + + bool find_old(offset_t idx, values const& vs, offset_t& found_idx) { + init(); + m_found.reset(); + m_trie.find_le(vs()-1, m_found); + std::cout << m_found.size() << " - "; + for (unsigned i = 0; i < m_found.size(); ++i) { + found_idx = offset_t(m_found[i]); + std::cout << i << " "; + if (m_found[i] != idx.m_offset && hb.is_subsumed(idx, found_idx)) { + TRACE("hilbert_basis", + hb.display(tout << "found:" , idx); + hb.display(tout << "-> ", found_idx); + m_trie.display(tout);); + std::cout << "\n"; + return true; + } + } + std::cout << "\n"; + TRACE("hilbert_basis", tout << "not found: "; hb.display(tout, idx); ); + return false; + } + + void collect_statistics(statistics& st) const { + m_trie.collect_statistics(st); + } + + void reset_statistics() { + m_trie.reset_statistics(); + } + + unsigned size() const { + return m_trie.size(); + } + +private: + void init() { + if (!m_init) { + reset(); + m_init = true; + } + } +}; + class hilbert_basis::index { // for each non-positive weight a separate index. // for positive weights a shared value index. + typedef value_index1 value_index; + // typedef value_index2 value_index; + struct stats { unsigned m_num_find; unsigned m_num_insert; @@ -184,7 +285,7 @@ public: bool find(offset_t idx, values const& vs, offset_t& found_idx) { ++m_stats.m_num_find; if (vs.weight().is_pos()) { - return m_pos.find(idx, vs, found_idx); + return m_pos.find(idx, vs, found_idx); } else if (vs.weight().is_zero()) { return m_zero.find(idx, vs, found_idx); @@ -198,12 +299,13 @@ public: } void reset() { - m_pos.reset(); - m_neg.reset(); value_map::iterator it = m_neg.begin(), end = m_neg.end(); for (; it != end; ++it) { it->m_value->reset(); } + m_pos.reset(); + m_zero.reset(); + m_neg.reset(); } void collect_statistics(statistics& st) const { @@ -257,7 +359,7 @@ class hilbert_basis::passive { lt m_lt; heap m_heap; // binary heap over weights - numeral get_value(offset_t idx) const { + numeral sum_abs(offset_t idx) const { numeral w(0); unsigned nv = hb.get_num_vars(); for (unsigned i = 0; i < nv; ++i) { @@ -325,7 +427,6 @@ public: 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() { @@ -336,42 +437,11 @@ public: return iterator(*this, m_passive.size()); } -public: - /** - Prefer positive weights to negative. - If both weights are positive, prefer the smallest weight. - If weights are the same, prefer the one that has smallest sum of values. - */ bool operator()(int v1, int v2) const { offset_t idx1 = m_passive[v1]; offset_t idx2 = m_passive[v2]; - return get_value(idx1) < get_value(idx2); -#if 0 - values const& vec1 = hb.vec(idx1); - values const& vec2 = hb.vec(idx2); - numeral const& w1 = vec1.weight(); - numeral const& w2 = vec2.weight(); - SASSERT(!w1.is_zero()); - SASSERT(!w2.is_zero()); - - if (w1.is_pos()) { - if (w2.is_neg()) { - return true; - } - if (w1 != w2) { - return w1 < w2; - } - } - else { - if (w2.is_pos()) { - return false; - } - } - SASSERT(w1 == w2); - return get_value(idx1) < get_value(idx2); -#endif + return sum_abs(idx1) < sum_abs(idx2); } - }; hilbert_basis::hilbert_basis(): @@ -420,7 +490,7 @@ void hilbert_basis::reset_statistics() { } void hilbert_basis::add_ge(num_vector const& v, numeral const& b) { - SASSERT(m_ineqs.empty() || v.size() + 1 == get_num_vars()); + SASSERT(m_ineqs.empty() || v.size() + 1 == m_ineqs.back().size()); num_vector w; w.push_back(-b); w.append(v); @@ -437,7 +507,7 @@ void hilbert_basis::add_le(num_vector const& v, numeral const& b) { } void hilbert_basis::add_eq(num_vector const& v, numeral const& b) { - SASSERT(m_ineqs.empty() || v.size() + 1 == get_num_vars()); + SASSERT(m_ineqs.empty() || v.size() + 1 == m_ineqs.back().size()); num_vector w; w.push_back(-b); w.append(v); @@ -474,6 +544,7 @@ unsigned hilbert_basis::get_num_vars() const { return 0; } else { + SASSERT(m_ineqs.back().size() > 1); return m_ineqs.back().size(); } } @@ -486,8 +557,8 @@ void hilbert_basis::init_basis() { m_basis.reset(); m_store.reset(); m_free_list.reset(); - unsigned num_vars = get_num_vars(); - for (unsigned i = 0; i < num_vars; ++i) { + unsigned nv = get_num_vars(); + for (unsigned i = 0; i < nv; ++i) { add_unit_vector(i, numeral(1)); } for (unsigned i = 0; i < m_ints.size(); ++i) { @@ -595,7 +666,7 @@ void hilbert_basis::get_basis_solution(unsigned i, num_vector& v, bool& is_initi void hilbert_basis::get_ge(unsigned i, num_vector& v, numeral& b, bool& is_eq) { v.reset(); - v.append(get_num_vars()-1, m_ineqs[i].c_ptr() + 1); + v.append(m_ineqs[i].size() - 1, m_ineqs[i].c_ptr() + 1); b = -m_ineqs[i][0]; is_eq = m_iseq[i]; } @@ -715,9 +786,7 @@ bool hilbert_basis::can_resolve(offset_t i, offset_t j) const { } values const& v1 = vec(i); values const& v2 = vec(j); - // index 0 is reserved for the constant coefficient. - // The value of it should either be 0 or 1. - if (abs(v1[0] + v2[0]) > numeral(1)) { + if (v1[0].is_one() && v2[0].is_one()) { return false; } for (unsigned i = 0; i < m_ints.size(); ++i) { @@ -798,8 +867,8 @@ void hilbert_basis::display(std::ostream& out, values const& v) const { } void hilbert_basis::display_ineq(std::ostream& out, num_vector const& v, bool is_eq) const { - unsigned nv = get_num_vars(); - for (unsigned j = 0; j < nv; ++j) { + unsigned nv = v.size(); + for (unsigned j = 1; j < nv; ++j) { if (!v[j].is_zero()) { if (j > 0) { if (v[j].is_pos()) { @@ -815,14 +884,14 @@ void hilbert_basis::display_ineq(std::ostream& out, num_vector const& v, bool is if (!v[j].is_one() && !v[j].is_minus_one()) { out << abs(v[j]) << "*"; } - out << "x" << j; + out << "x" << j; } } if (is_eq) { - out << " = 0\n"; + out << " = " << -v[0] << "\n"; } else { - out << " >= 0\n"; + out << " >= " << -v[0] << "\n"; } } @@ -862,7 +931,7 @@ bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const { numeral const& m = w.weight(); bool r = i.m_offset != j.m_offset && - n >= m && (!m.is_nonpos() || n == m) && + n >= m && (!m.is_neg() || n == m) && is_geq(v, w); for (unsigned k = 0; r && k < m_current_ineq; ++k) { r = get_weight(vec(i), m_ineqs[k]) >= get_weight(vec(j), m_ineqs[k]); diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index 8dd5e97cf..09839fc03 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -32,7 +32,8 @@ public: typedef rational numeral; typedef vector num_vector; private: - class value_index; + class value_index1; + class value_index2; class index; class passive; struct offset_t { @@ -59,6 +60,7 @@ private: numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i numeral const& weight() const { return m_values[0]; } // value of a*x numeral const& operator[](unsigned i) const { return m_values[i+1]; } // value of x_i + numeral const* operator()() const { return m_values + 1; } }; vector m_ineqs; // set of asserted inequalities diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp new file mode 100644 index 000000000..648a7662e --- /dev/null +++ b/src/test/heap_trie.cpp @@ -0,0 +1,52 @@ +#include "heap_trie.h" + + +typedef heap_trie heap_trie_t; + +static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) { + statistics st; + vector vals; + ht.find_le(keys, vals); + std::cout << "find_le: "; + for (unsigned i = 0; i < num_keys; ++i) { + std::cout << keys[i] << " "; + } + std::cout << " |-> "; + for (unsigned i = 0; i < vals.size(); ++i) { + std::cout << vals[i] << " "; + } + std::cout << "\n"; + ht.collect_statistics(st); + st.display(std::cout); + +} + +void tst_heap_trie() { + heap_trie_t ht; + + ht.reset(3); + unsigned keys1[3] = { 1, 2, 3}; + ht.insert(keys1, 1); + unsigned keys2[3] = { 2, 2, 3}; + ht.insert(keys2, 2); + unsigned keys3[3] = { 1, 1, 3}; + ht.insert(keys3, 3); + unsigned keys4[3] = { 2, 1, 3}; + unsigned keys5[3] = { 2, 3, 3}; + + unsigned val; + + VERIFY (ht.find_eq(keys1, val) && val == 1); + VERIFY (ht.find_eq(keys2, val) && val == 2); + VERIFY (ht.find_eq(keys3, val) && val == 3); + VERIFY (!ht.find_eq(keys4, val)); + + find_le(ht, 3, keys1); + find_le(ht, 3, keys2); + find_le(ht, 3, keys3); + find_le(ht, 3, keys4); + find_le(ht, 3, keys5); + + ht.display(std::cout); + +} diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index 7cf4d863b..d372572bd 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -16,6 +16,18 @@ class hilbert_basis_validate { void validate_solution(hilbert_basis& hb, vector const& v, bool is_initial); + rational eval_ineq(hilbert_basis& hb, unsigned idx, vector const& v, bool& is_eq) { + vector w; + rational bound; + hb.get_ge(idx, w, bound, is_eq); + rational sum(0); + for (unsigned j = 0; j < v.size(); ++j) { + sum += w[j]*v[j]; + } + sum -= bound; + return sum; + } + public: hilbert_basis_validate(ast_manager& m); @@ -35,37 +47,47 @@ void hilbert_basis_validate::validate_solution(hilbert_basis& hb, vector w; + rational bound; hb.get_ge(i, w, bound, is_eq); rational sum(0); for (unsigned j = 0; j < v.size(); ++j) { sum += w[j]*v[j]; } - if (bound > sum || - (is_eq && bound != sum)) { - // validation failed. - std::cout << "validation failed for inequality\n"; - for (unsigned j = 0; j < v.size(); ++j) { - std::cout << v[j] << " "; - } - std::cout << "\n"; - for (unsigned j = 0; j < w.size(); ++j) { - std::cout << w[j] << " "; - } - std::cout << (is_eq?" = ":" >= ") << bound << "\n"; - std::cout << "is initial: " << (is_initial?"true":"false") << "\n"; - std::cout << "sum: " << sum << "\n"; - } - } + if (sum >= bound && !is_eq) { + continue; + } + if (sum == bound && is_eq) { + continue; + } + // homogeneous solutions should be non-negative. + if (!is_initial && sum.is_nonneg()) { + continue; + } + + // validation failed. + std::cout << "validation failed\n"; + std::cout << "constraint: "; + for (unsigned j = 0; j < v.size(); ++j) { + std::cout << v[j] << " "; + } + std::cout << (is_eq?" = ":" >= ") << bound << "\n"; + std::cout << "vector: "; + for (unsigned j = 0; j < w.size(); ++j) { + std::cout << w[j] << " "; + } + std::cout << "\n"; + std::cout << "sum: " << sum << "\n"; + } } expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) { arith_util a(m); unsigned sz = hb.get_basis_size(); vector v; - bool is_initial; // check that claimed solution really satisfies inequalities: for (unsigned i = 0; i < sz; ++i) { + bool is_initial; hb.get_basis_solution(i, v, is_initial); validate_solution(hb, v, is_initial); } @@ -83,12 +105,14 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) { for (unsigned i = 0; i < sz; ++i) { + bool is_initial; hb.get_basis_solution(i, v, is_initial); for (unsigned j = 0; xs.size() < v.size(); ++j) { xs.push_back(m.mk_fresh_const("x", a.mk_int())); } + if (is_initial) { expr_ref_vector tmp(m); for (unsigned j = 0; j < v.size(); ++j) { @@ -200,6 +224,8 @@ static void validate_sat(hilbert_basis& hb) { expr_ref fml = val.mk_validate(hb); + return; + std::cout << mk_pp(fml, m) << "\n"; fml = m.mk_not(fml); @@ -221,7 +247,7 @@ static void saturate_basis(hilbert_basis& hb) { case l_true: std::cout << "sat\n"; hb.display(std::cout); - // validate_sat(hb); + validate_sat(hb); break; case l_false: std::cout << "unsat\n"; @@ -449,7 +475,7 @@ static void tst11() { // Sigma_9 table 1, Ajili, Contejean static void tst12() { hilbert_basis hb; - hb.add_eq(vec( 1,-2,-4,4), R(0)); + hb.add_eq(vec( 1,-2,-3,4), R(0)); hb.add_le(vec(100,45,-78,-67), R(0)); saturate_basis(hb); } @@ -465,7 +491,7 @@ static void tst13() { static void tst14() { hilbert_basis hb; hb.add_eq(vec(1, 0, -4, 8), R(2)); - hb.add_le(vec(12,19,-11,7), R(-7)); + hb.add_le(vec(12,19,-11,-7), R(-7)); saturate_basis(hb); } diff --git a/src/test/main.cpp b/src/test/main.cpp index dc253f36d..9dc12be1c 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -208,6 +208,7 @@ int main(int argc, char ** argv) { TST(model2expr); TST(rcf); TST(hilbert_basis); + TST(heap_trie); } void initialize_mam() {}