mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
fix hilbert_basis tests and add heap_trie index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
47342e5d0c
commit
306855ba55
355
src/muz_qe/heap_trie.h
Normal file
355
src/muz_qe/heap_trie.h
Normal file
|
|
@ -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<typename Key, typename Value>
|
||||
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<std::pair<Key,node*> > 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<node>& 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<ptr_vector<node> > 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<Value>& values) {
|
||||
++m_stats.m_num_find_le;
|
||||
ptr_vector<node> 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<trie*>(n);
|
||||
}
|
||||
|
||||
leaf* to_leaf(node* n) {
|
||||
SASSERT(n->type() == leaf_t);
|
||||
return static_cast<leaf*>(n);
|
||||
}
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -20,12 +20,13 @@ Revision History:
|
|||
#include "hilbert_basis.h"
|
||||
#include "heap.h"
|
||||
#include "map.h"
|
||||
#include "heap_trie.h"
|
||||
|
||||
template<typename Value>
|
||||
class rational_map : public map<rational, Value, rational::hash_proc, rational::eq_proc> {};
|
||||
|
||||
|
||||
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<numeral, unsigned>::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<numeral, unsigned> m_trie;
|
||||
vector<unsigned> 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<lt> 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]);
|
||||
|
|
|
|||
|
|
@ -32,7 +32,8 @@ public:
|
|||
typedef rational numeral;
|
||||
typedef vector<numeral> 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<num_vector> m_ineqs; // set of asserted inequalities
|
||||
|
|
|
|||
52
src/test/heap_trie.cpp
Normal file
52
src/test/heap_trie.cpp
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
#include "heap_trie.h"
|
||||
|
||||
|
||||
typedef heap_trie<unsigned, unsigned > heap_trie_t;
|
||||
|
||||
static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) {
|
||||
statistics st;
|
||||
vector<unsigned> 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);
|
||||
|
||||
}
|
||||
|
|
@ -16,6 +16,18 @@ class hilbert_basis_validate {
|
|||
|
||||
void validate_solution(hilbert_basis& hb, vector<rational> const& v, bool is_initial);
|
||||
|
||||
rational eval_ineq(hilbert_basis& hb, unsigned idx, vector<rational> const& v, bool& is_eq) {
|
||||
vector<rational> 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<rationa
|
|||
for (unsigned i = 0; i < sz; ++i) {
|
||||
bool is_eq;
|
||||
vector<rational> 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<rational> 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);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -208,6 +208,7 @@ int main(int argc, char ** argv) {
|
|||
TST(model2expr);
|
||||
TST(rcf);
|
||||
TST(hilbert_basis);
|
||||
TST(heap_trie);
|
||||
}
|
||||
|
||||
void initialize_mam() {}
|
||||
|
|
|
|||
Loading…
Reference in a new issue