From 00e79e6b6b25d5dbb908559bc2c6807830068f96 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Mar 2013 17:31:11 -0700 Subject: [PATCH] test hilbert-basis with fdds and checked integers Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_bit_blast.cpp | 7 +- src/muz_qe/fdd.cpp | 311 +++++++++++++++++++++++++++++++++ src/muz_qe/fdd.h | 169 ++++++++++++++++++ src/muz_qe/heap_trie.h | 12 +- src/muz_qe/hilbert_basis.cpp | 184 ++++++++++++------- src/muz_qe/hilbert_basis.h | 40 +++-- src/test/fdd.cpp | 87 +++++++++ src/test/heap_trie.cpp | 3 +- src/test/hilbert_basis.cpp | 7 + src/test/main.cpp | 1 + src/util/checked_int64.h | 231 ++++++++++++++++++++++++ 11 files changed, 969 insertions(+), 83 deletions(-) create mode 100644 src/muz_qe/fdd.cpp create mode 100644 src/muz_qe/fdd.h create mode 100644 src/test/fdd.cpp create mode 100644 src/util/checked_int64.h diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 1e984f254..ccba0d69f 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -212,6 +212,7 @@ namespace datalog { ast_manager & m; params_ref m_params; rule_ref_vector m_rules; + th_rewriter m_theory_rewriter; bit_blaster_rewriter m_blaster; expand_mkbv m_rewriter; @@ -219,6 +220,7 @@ namespace datalog { bool blast(expr_ref& fml) { proof_ref pr(m); expr_ref fml1(m), fml2(m); + m_theory_rewriter(fml); m_blaster(fml, fml1, pr); m_rewriter(fml1, fml2); TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";); @@ -241,8 +243,9 @@ namespace datalog { m(ctx.get_manager()), m_params(ctx.get_params().p), m_rules(ctx.get_rule_manager()), - m_blaster(ctx.get_manager(), m_params), - m_rewriter(ctx.get_manager(), ctx, m_rules) { + m_theory_rewriter(m, m_params), + m_blaster(m, m_params), + m_rewriter(m, ctx, m_rules) { m_params.set_bool("blast_full", true); m_params.set_bool("blast_quant", true); m_blaster.updt_params(m_params); diff --git a/src/muz_qe/fdd.cpp b/src/muz_qe/fdd.cpp new file mode 100644 index 000000000..afb5206cc --- /dev/null +++ b/src/muz_qe/fdd.cpp @@ -0,0 +1,311 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + fdd.cpp + +Abstract: + + Finite decision diagram trie. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-07-03. + +Revision History: + + +--*/ + +#include "fdd.h" +#include "hash.h" +#include "bit_vector.h" +#include "trace.h" + +#define OFFSET_OF(ty, field) (unsigned char*)(&((ty*)(0))->field) - (unsigned char*)(ty*)(0) + +using namespace fdd; + +unsigned node::get_hash() const { + return string_hash((char*)this, OFFSET_OF(node, m_ref_count), 11); +} + +bool node::operator==(node const& other) const { + return + m_var == other.m_var && + m_lo == other.m_lo && + m_hi == other.m_hi; +} + + +// ------------------------------------------ +// manager + +manager::manager() : + m_false(0), + m_true(1), + m_root(m_false), + m_alloc_node(2) +{ + m_nodes.push_back(node()); // false + m_nodes.push_back(node()); // true + inc_ref(m_false); + inc_ref(m_true); + alloc_node(); // pre-allocate a node. +} + +manager::~manager() { +} + +void manager::alloc_node() { + unsigned index; + while (!m_free.empty()) { + index = m_free.back(); + node& n = m_nodes[index]; + m_free.pop_back(); + if (n.get_ref_count() == 0) { + if (!is_leaf(n.lo())) { + m_free.push_back(n.lo()); + } + if (!is_leaf(n.hi())) { + m_free.push_back(n.hi()); + } + m_alloc_node = index; + m_table.erase(n); + return; + } + } + index = m_nodes.size(); + m_nodes.push_back(node()); + m_alloc_node = index; +} + +node_id manager::mk_node(unsigned var, node_id lo, node_id hi) { + if (lo == hi) { + return lo; + } + node n(var, lo, hi); + unsigned index = m_alloc_node; + + node_id result = m_table.insert_if_not_there(n, index).m_value; + + if (result == index) { + alloc_node(); + m_nodes[result] = n; + inc_ref(lo); + inc_ref(hi); + } + + TRACE("mtdd", tout << "mk_node: " << var << " " << lo << " " << hi << " -> " << result << "\n";); + + return result; +} + + +void manager::inc_ref(node_id n) { + TRACE("mtdd", tout << "incref: " << n << "\n";); + if (!is_leaf(n)) { + m_nodes[n].inc_ref(); + } +} + +void manager::dec_ref(node_id n) { + if (!is_leaf(n) && 0 == m_nodes[n].dec_ref()) { + m_free.push_back(n); + } +} + +void manager::setup_keys(Key const* keys) { + for (unsigned i = 0; i < m_num_keys; ++i) { + m_keys[i] = (uint64)keys[i]; + m_sign[i] = keys[i] < 0; + } + +} + +void manager::insert(Key const* keys) { + setup_keys(keys); + node_id result = insert_sign(m_num_idx + m_num_keys, m_root); + inc_ref(result); + dec_ref(m_root); + m_root = result; +} + +node_id manager::insert_sign(unsigned idx, node_id n) { + if (idx > m_num_idx) { + --idx; + bool s = idx2sign(idx); + node nd = m_nodes[n]; + if (!is_leaf(n) && nd.var() == idx) { + if (s) { + return mk_node(idx, insert_sign(idx, nd.lo()), nd.hi()); + } + else { + return mk_node(idx, nd.lo(), insert_sign(idx, nd.hi())); + } + } + else { + if (s) { + return mk_node(idx, insert_sign(idx, n), n); + } + else { + return mk_node(idx, n, insert_sign(idx, n)); + } + } + } + SASSERT(m_num_idx == idx); + return insert(idx, n); +} + +node_id manager::insert(unsigned idx, node_id n) { + node_id result; + SASSERT(0 <= idx && idx <= m_num_idx); + TRACE("mtdd", tout << "insert: " << idx << " " << n << "\n";); + if (is_leaf(n)) { + while (idx > 0) { + --idx; + if (idx2bit(idx) && !is_dont_care(idx2key(idx))) { + return mk_node(idx, n, insert(idx, n)); + } + } + return m_true; + } + + SASSERT(0 < idx); + --idx; + + config c(m_dont_cares, idx, n); + insert_cache::key_data & kd = m_insert_cache.insert_if_not_there2(c, 0)->get_data(); + if (kd.m_value != 0) { + return kd.m_value; + } + + node nd = m_nodes[n]; + SASSERT(idx >= nd.var()); + unsigned idx0 = idx; + while (idx > nd.var()) { + if (idx2bit(idx) && !is_dont_care(idx2key(idx))) { + return mk_node(idx, n, insert(idx, n)); + } + --idx; + } + SASSERT(nd.var() == idx); + unsigned key = idx2key(idx); + if (is_dont_care(key)) { + result = mk_node(idx, insert(idx, nd.lo()), insert(idx, nd.hi())); + } + else { + bool bit = idx2bit(idx); + node_id lo, hi; + if (bit) { + hi = insert(idx, nd.hi()); + lo = nd.lo(); + } + else { + lo = insert(idx, nd.lo()); + scoped_dont_cares _set(*this, key); + hi = insert(idx, nd.hi()); + } + result = mk_node(idx, lo, hi); + } + kd.m_value = result; + return result; +} + +void manager::set_dont_care(unsigned key) { + SASSERT(!is_dont_care(key)); + m_dont_cares |= (1ull << key); +} + +void manager::unset_dont_care(unsigned key) { + m_dont_cares &= ~(1ull << key); +} + +bool manager::is_dont_care(unsigned key) const { + return 0 != (m_dont_cares & (1ull << key)); +} + +void manager::collect_statistics(statistics& st) const { + st.update("fdd.num_nodes", m_nodes.size()); +} + + +void manager::reset(unsigned num_keys) { + m_num_keys = num_keys; + m_num_idx = m_num_keys * m_num_bits; + m_dont_cares = 0; + m_sign.resize(num_keys); + m_keys.resize(num_keys); + SASSERT(num_keys <= 8*sizeof(m_dont_cares)); +} + + + +bool manager::find_le(Key const* keys) { + setup_keys(keys); + unsigned idx = m_num_idx + m_num_keys; + node_id n = m_root; + node nc = m_nodes[n]; + while (n > 1 && idx > m_num_idx) { + --idx; + if (nc.var() == idx) { + if (idx2sign(idx)) { + n = nc.lo(); + } + else { + n = nc.hi(); + } + nc = m_nodes[n]; + } + } + while (n > 1) { + SASSERT(idx > 0); + --idx; + while (nc.var() < idx) { + if (idx2bit(idx)) { + set_dont_care(idx2key(idx)); + } + --idx; + } + if (is_dont_care(idx2key(idx)) || idx2bit(idx)) { + n = nc.hi(); + } + else { + n = nc.lo(); + } + nc = m_nodes[n]; + } + m_dont_cares = 0; + return n == 1; +} + + +std::ostream& manager::display(std::ostream& out, node_id n) const{ + svector mark; + svector nodes; + nodes.push_back(n); + while (!nodes.empty()) { + n = nodes.back(); + nodes.pop_back(); + if (mark.size() <= n) { + mark.resize(n+1, false); + } + node const& nc = m_nodes[n]; + if (is_leaf(n) || mark[n]) { + continue; + } + nodes.push_back(nc.lo()); + nodes.push_back(nc.hi()); + mark[n] = true; + + if (nc.var() >= m_num_idx) { + out << n << " if " << idx2key(nc.var()) << " then " << nc.hi() << " else " << nc.lo() << "\n"; + } + else { + out << n << " if " << idx2key(nc.var()) << ":" << idx2bitnum(nc.var()) << " then " << nc.hi() << " else " << nc.lo() << "\n"; + } + } + return out; +} + diff --git a/src/muz_qe/fdd.h b/src/muz_qe/fdd.h new file mode 100644 index 000000000..e6808375c --- /dev/null +++ b/src/muz_qe/fdd.h @@ -0,0 +1,169 @@ +/*++ +Copyright (c) 2007 Microsoft Corporation + +Module Name: + + fdd.h + +Abstract: + + Finite decision diagram. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-07-03. + +Revision History: + + +--*/ + +#ifndef __FDD_H__ +#define __FDD_H__ + +#include "hashtable.h" +#include "hash.h" +#include "map.h" +#include "vector.h" +#include "statistics.h" + +namespace fdd { + + + typedef unsigned node_id; + + class node { + unsigned m_var; + node_id m_lo; + node_id m_hi; + unsigned m_ref_count; + void reset(); + public: + node() : m_var(0), m_hi(0), m_lo(0), m_ref_count(0) {} + node(unsigned var, node_id l, node_id h): m_var(var), m_lo(l), m_hi(h), m_ref_count(0) {} + + unsigned get_hash() const; + bool operator==(node const& other) const; + + void inc_ref() { ++m_ref_count; } + unsigned dec_ref() { return --m_ref_count; } + unsigned get_ref_count() const { return m_ref_count; } + node_id lo() const { return m_lo; } + node_id hi() const { return m_hi; } + unsigned var() const { return m_var; } + + struct hash { unsigned operator()(node const& n) const { return n.get_hash(); } }; + struct eq { bool operator()(node const& l, node const& r) const { return l == r; } }; + std::ostream& display(std::ostream& out) const { return out << m_var << " " << m_lo << " " << m_hi << ""; } + }; + + inline std::ostream& operator<<(std::ostream& out, node const& n) { return n.display(out); } + + class config { + uint64 m_dont_cares; + unsigned m_idx; + node_id m_node; + public: + + config(): m_dont_cares(0), m_idx(0), m_node(0) {} + + config(uint64 dont_cares, unsigned idx, node_id n): + m_dont_cares(dont_cares), + m_idx(idx), + m_node(n) + {} + + struct hash { + unsigned operator()(config const& c) const { + return string_hash((char*)&c, sizeof(c), 12); + }; + }; + + struct eq { + bool operator()(config const& a, config const& b) const { + return + a.m_dont_cares == b.m_dont_cares && + a.m_idx == b.m_idx && + a.m_node == b.m_node; + } + }; + }; + + + class manager { + public: + typedef int64 Key; + private: + typedef map node_table; + typedef map insert_cache; + node_table m_table; + insert_cache m_insert_cache; + svector m_nodes; + unsigned_vector m_free; + unsigned m_alloc_node; + node_id m_false; + node_id m_true; + node_id m_root; + + static const unsigned m_num_bits = 64; + unsigned m_num_keys; + unsigned m_num_idx; // = m_num_keys * m_num_bits + + // state associated with insert. + svector m_keys; + svector m_sign; + + uint64 m_dont_cares; + + public: + manager(); + ~manager(); + + void reset(unsigned num_keys); + + void insert(Key const* keys); + + bool find_le(Key const* keys); + + void collect_statistics(statistics& st) const; + void reset_statistics() {} + unsigned size() const { return m_nodes.size(); } + + void display(std::ostream& out) const { display(out, m_root); } + + private: + void dec_ref(node_id n); + void inc_ref(node_id n); + node_id mk_node(unsigned var, node_id lo, node_id hi); + inline unsigned get_ref_count(node_id n) { return m_nodes[n].get_ref_count(); } + + std::ostream& display(std::ostream& out, node_id n) const; + + void setup_keys(Key const* keys); + node_id insert(unsigned idx, node_id n); + node_id insert_sign(unsigned idx, node_id n); + bool is_dont_care(unsigned idx) const; + + void set_dont_care(unsigned key); + void unset_dont_care(unsigned key); + + struct scoped_dont_cares { + manager& m; + unsigned m_key; + scoped_dont_cares(manager& m, unsigned key):m(m), m_key(key) { m.set_dont_care(key); } + ~scoped_dont_cares() { m.unset_dont_care(m_key); } + }; + + void alloc_node(); + + unsigned idx2key(unsigned i) const { return i % m_num_keys; } + unsigned idx2bitnum(unsigned i) const { SASSERT(i < m_num_idx); return (i / m_num_keys); } + bool idx2bit(unsigned i) const { return 0 != (m_keys[idx2key(i)] & (1LL << idx2bitnum(i))); } + bool idx2sign(unsigned i) const { return m_sign[idx2key(i)]; } + + bool is_leaf(node_id n) const { return n <= 1; } + + }; +}; + +#endif diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h index a99861359..c2a1c52d1 100644 --- a/src/muz_qe/heap_trie.h +++ b/src/muz_qe/heap_trie.h @@ -123,9 +123,9 @@ class heap_trie { } // push nodes whose keys are <= key into vector. - void find_le(Key key, ptr_vector& nodes) { + void find_le(KeyLE& le, Key key, ptr_vector& nodes) { for (unsigned i = 0; i < m_nodes.size(); ++i) { - if (KeyLE::le(m_nodes[i].first, key)) { + if (le.le(m_nodes[i].first, key)) { node* n = m_nodes[i].second; if (n->ref_count() > 0){ nodes.push_back(n); @@ -179,6 +179,7 @@ class heap_trie { }; small_object_allocator m_alloc; + KeyLE& m_le; unsigned m_num_keys; unsigned_vector m_keys; unsigned m_do_reshuffle; @@ -189,8 +190,9 @@ class heap_trie { public: - heap_trie(): + heap_trie(KeyLE& le): m_alloc("heap_trie"), + m_le(le), m_num_keys(0), m_do_reshuffle(4), m_root(0), @@ -255,7 +257,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(get_key(keys, i), todo[!index]); + to_trie(todo[index][j])->find_le(m_le, get_key(keys, i), todo[!index]); } todo[index].reset(); index = !index; @@ -577,7 +579,7 @@ private: 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 (m->ref_count() > 0 && m_le.le(nodes[i].first, key) && find_le(m, index+1, keys, check)) { if (i > 0) { std::swap(nodes[i], nodes[0]); } diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 9fbd8cc2e..221e9a706 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -21,6 +21,7 @@ Revision History: #include "heap.h" #include "map.h" #include "heap_trie.h" +#include "fdd.h" #include "stopwatch.h" @@ -58,14 +59,13 @@ public: m_table.reset(); } - bool find(offset_t idx, values const& vs, offset_t& found_idx) { + bool find(offset_t idx, values const& vs) { // display_profile(idx, std::cout); int_table::iterator it = m_table.begin(), end = m_table.end(); for (; it != end; ++it) { offset_t offs(*it); ++m_stats.m_num_comparisons; if (*it != static_cast(idx.m_offset) && hb.is_subsumed(idx, offs)) { - found_idx = offs; ++m_stats.m_num_hit; return true; } @@ -163,20 +163,21 @@ private: class hilbert_basis::value_index2 { struct key_le { - static bool le(numeral const& n1, numeral const& n2) { - return hilbert_basis::is_abs_geq(n2, n1); + hilbert_basis& hb; + key_le(hilbert_basis& hb): hb(hb) {} + bool le(numeral const& n1, numeral const& n2) const { + return hb.is_abs_geq(n2, n1); } }; typedef heap_trie ht; + struct checker : public ht::check_value { hilbert_basis* hb; offset_t m_value; - offset_t* m_found; - checker(): hb(0), m_found(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); + checker(): hb(0) {} + virtual bool operator()(unsigned const& v) { + if (m_value.m_offset != v) { // && hb->is_subsumed(m_value, offset_t(v))) { return true; } else { @@ -185,23 +186,25 @@ class hilbert_basis::value_index2 { } }; hilbert_basis& hb; + key_le m_le; ht m_trie; - vector m_found; - bool m_init; checker m_checker; - vector m_keys; + unsigned m_offset; numeral const* get_keys(values const& vs) { - return vs()-1; + return vs()-m_offset; } public: - value_index2(hilbert_basis& hb): hb(hb), m_init(false) { + value_index2(hilbert_basis& hb): + hb(hb), + m_le(hb), + m_trie(m_le), + m_offset(1) { m_checker.hb = &hb; } void insert(offset_t idx, values const& vs) { - init(); m_trie.insert(get_keys(vs), idx.m_offset); } @@ -209,15 +212,13 @@ public: m_trie.remove(get_keys(vs)); } - void reset() { - m_trie.reset(hb.get_num_vars()+1); - m_keys.resize(hb.get_num_vars()+1); + void reset(unsigned offset) { + m_offset = offset; + m_trie.reset(hb.get_num_vars()+m_offset); } - bool find(offset_t idx, values const& vs, offset_t& found_idx) { - init(); + bool find(offset_t idx, values const& vs) { m_checker.m_value = idx; - m_checker.m_found = &found_idx; return m_trie.find_le(get_keys(vs), m_checker); } @@ -237,15 +238,63 @@ public: // m_trie.display(out); } -private: - void init() { - if (!m_init) { - reset(); - m_init = true; - } - } + }; +class hilbert_basis::value_index3 { + hilbert_basis& hb; + fdd::manager m_fdd; + unsigned m_offset; + svector m_keys; + + int64 const* get_keys(values const& vs) { + numeral const* nums = vs()-m_offset; + for (unsigned i = 0; i < m_keys.size(); ++i) { + m_keys[i] = nums[i].get_int64(); + } + return m_keys.c_ptr(); + } + +public: + + value_index3(hilbert_basis & hb): hb(hb), m_offset(1) {} + + void insert(offset_t, values const& vs) { + m_fdd.insert(get_keys(vs)); + } + + bool find(offset_t, values const& vs) { + return m_fdd.find_le(get_keys(vs)); + } + + void reset(unsigned offset) { + m_offset = offset; + m_fdd.reset(hb.get_num_vars()+m_offset); + m_keys.resize(hb.get_num_vars()+m_offset); + } + + void collect_statistics(statistics& st) const { + m_fdd.collect_statistics(st); + } + + void reset_statistics() { + m_fdd.reset_statistics(); + } + + unsigned size() const { + return m_fdd.size(); + } + + void remove(offset_t idx, values const& vs) { + UNREACHABLE(); + } + + void display(std::ostream& out) const { + // m_fdd.display(out); + } + + +}; class hilbert_basis::index { @@ -253,7 +302,8 @@ class hilbert_basis::index { // for positive weights a shared value index. // typedef value_index1 value_index; - typedef value_index2 value_index; + // typedef value_index2 value_index; + typedef value_index3 value_index; struct stats { unsigned m_num_find; @@ -271,9 +321,10 @@ class hilbert_basis::index { value_index m_pos; value_index m_zero; stats m_stats; + unsigned m_num_ineqs; public: - index(hilbert_basis& hb): hb(hb), m_pos(hb), m_zero(hb) {} + index(hilbert_basis& hb): hb(hb), m_pos(hb), m_zero(hb), m_num_ineqs(0) {} void insert(offset_t idx, values const& vs) { ++m_stats.m_num_insert; @@ -287,6 +338,7 @@ public: value_index* map = 0; if (!m_neg.find(vs.weight(), map)) { map = alloc(value_index, hb); + map->reset(m_num_ineqs); m_neg.insert(vs.weight(), map); } map->insert(idx, vs); @@ -305,29 +357,30 @@ public: } } - bool find(offset_t idx, values const& vs, offset_t& found_idx) { + bool find(offset_t idx, values const& vs) { ++m_stats.m_num_find; if (vs.weight().is_pos()) { - return m_pos.find(idx, vs, found_idx); + return m_pos.find(idx, vs); } else if (vs.weight().is_zero()) { - return m_zero.find(idx, vs, found_idx); + return m_zero.find(idx, vs); } else { value_index* map; return m_neg.find(vs.weight(), map) && - map->find(idx, vs, found_idx); + map->find(idx, vs); } } - void reset() { + void reset(unsigned num_ineqs) { value_map::iterator it = m_neg.begin(), end = m_neg.end(); for (; it != end; ++it) { - it->m_value->reset(); + dealloc(it->m_value); } - m_pos.reset(); - m_zero.reset(); + m_pos.reset(num_ineqs); + m_zero.reset(num_ineqs); + m_num_ineqs = num_ineqs; m_neg.reset(); } @@ -685,7 +738,7 @@ void hilbert_basis::reset() { m_passive->reset(); m_passive2->reset(); m_zero.reset(); - m_index->reset(); + m_index->reset(1); m_ints.reset(); m_cancel = false; } @@ -703,42 +756,46 @@ void hilbert_basis::reset_statistics() { m_index->reset_statistics(); } -void hilbert_basis::add_ge(num_vector const& v, numeral const& b) { +void hilbert_basis::add_ge(rational_vector const& v, rational const& b) { SASSERT(m_ineqs.empty() || v.size() + 1 == m_ineqs.back().size()); num_vector w; - w.push_back(-b); - w.append(v); + w.push_back(to_numeral(-b)); + for (unsigned i = 0; i < v.size(); ++i) { + w.push_back(to_numeral(v[i])); + } m_ineqs.push_back(w); m_iseq.push_back(false); } -void hilbert_basis::add_le(num_vector const& v, numeral const& b) { - num_vector w(v); +void hilbert_basis::add_le(rational_vector const& v, rational const& b) { + rational_vector w(v); for (unsigned i = 0; i < w.size(); ++i) { w[i].neg(); } add_ge(w, -b); } -void hilbert_basis::add_eq(num_vector const& v, numeral const& b) { +void hilbert_basis::add_eq(rational_vector const& v, rational const& b) { SASSERT(m_ineqs.empty() || v.size() + 1 == m_ineqs.back().size()); num_vector w; - w.push_back(-b); - w.append(v); + w.push_back(to_numeral(-b)); + for (unsigned i = 0; i < v.size(); ++i) { + w.push_back(to_numeral(v[i])); + } m_ineqs.push_back(w); m_iseq.push_back(true); } -void hilbert_basis::add_ge(num_vector const& v) { - add_ge(v, numeral(0)); +void hilbert_basis::add_ge(rational_vector const& v) { + add_ge(v, rational(0)); } -void hilbert_basis::add_le(num_vector const& v) { - add_le(v, numeral(0)); +void hilbert_basis::add_le(rational_vector const& v) { + add_le(v, rational(0)); } -void hilbert_basis::add_eq(num_vector const& v) { - add_eq(v, numeral(0)); +void hilbert_basis::add_eq(rational_vector const& v) { + add_eq(v, rational(0)); } void hilbert_basis::set_is_int(unsigned var_index) { @@ -824,7 +881,7 @@ lbool hilbert_basis::saturate_orig(num_vector const& ineq, bool is_eq) { m_active.reset(); m_passive->reset(); m_zero.reset(); - m_index->reset(); + m_index->reset(m_current_ineq+1); int_table support; TRACE("hilbert_basis", display_ineq(tout, ineq, is_eq);); iterator it = begin(); @@ -896,7 +953,7 @@ bool hilbert_basis::vector_lt(offset_t idx1, offset_t idx2) const { lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { m_zero.reset(); - m_index->reset(); + m_index->reset(m_current_ineq+1); m_passive2->reset(); m_sos.reset(); TRACE("hilbert_basis", display_ineq(tout, ineq, is_eq);); @@ -975,19 +1032,21 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { return m_basis.empty()?l_false:l_true; } -void hilbert_basis::get_basis_solution(unsigned i, num_vector& v, bool& is_initial) { +void hilbert_basis::get_basis_solution(unsigned i, rational_vector& v, bool& is_initial) { offset_t offs = m_basis[i]; v.reset(); for (unsigned i = 1; i < get_num_vars(); ++i) { - v.push_back(vec(offs)[i]); + v.push_back(to_rational(vec(offs)[i])); } is_initial = !vec(offs)[0].is_zero(); } -void hilbert_basis::get_ge(unsigned i, num_vector& v, numeral& b, bool& is_eq) { +void hilbert_basis::get_ge(unsigned i, rational_vector& v, rational& b, bool& is_eq) { v.reset(); - v.append(m_ineqs[i].size() - 1, m_ineqs[i].c_ptr() + 1); - b = -m_ineqs[i][0]; + for (unsigned j = 1; j < m_ineqs[i].size(); ++j) { + v.push_back(to_rational(m_ineqs[i][j])); + } + b = to_rational(-m_ineqs[i][0]); is_eq = m_iseq[i]; } @@ -1122,8 +1181,7 @@ bool hilbert_basis::add_goal(offset_t idx) { bool hilbert_basis::is_subsumed(offset_t idx) { - offset_t found_idx; - if (m_index->find(idx, vec(idx), found_idx)) { + if (m_index->find(idx, vec(idx))) { ++m_stats.m_num_subsumptions; return true; } @@ -1317,7 +1375,7 @@ bool hilbert_basis::is_geq(values const& v, values const& w) const { return true; } -bool hilbert_basis::is_abs_geq(numeral const& v, numeral const& w) { +bool hilbert_basis::is_abs_geq(numeral const& v, numeral const& w) const { if (w.is_neg()) { return v <= w; } diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index bad4b1fbd..abb59be2d 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -18,6 +18,11 @@ Author: Revision History: + Hilbert basis can be templatized + based on traits that define numeral: + as rational, mpz, checked_int64 + (checked or unchecked). + --*/ #ifndef _HILBERT_BASIS_H_ @@ -26,14 +31,25 @@ Revision History: #include "rational.h" #include "lbool.h" #include "statistics.h" +#include "checked_int64.h" + +typedef vector rational_vector; class hilbert_basis { -public: - typedef rational numeral; + + static const bool check = false; + typedef checked_int64 numeral; typedef vector num_vector; -private: + static checked_int64 to_numeral(rational const& r) { + return checked_int64(r.get_int64()); + } + static rational to_rational(checked_int64 const& i) { + return rational(i.get_int64(), rational::i64()); + } + class value_index1; class value_index2; + class value_index3; class index; class passive; class passive2; @@ -112,7 +128,7 @@ private: unsigned get_num_vars() const; numeral get_weight(values const & val, num_vector const& ineq) const; bool is_geq(values const& v, values const& w) const; - static bool is_abs_geq(numeral const& v, numeral const& w); + bool is_abs_geq(numeral const& v, numeral const& w) const; bool is_subsumed(offset_t idx); bool is_subsumed(offset_t i, offset_t j) const; void recycle(offset_t idx); @@ -147,16 +163,16 @@ public: // add inequality v*x >= 0 // add inequality v*x <= 0 // add equality v*x = 0 - void add_ge(num_vector const& v); - void add_le(num_vector const& v); - void add_eq(num_vector const& v); + void add_ge(rational_vector const& v); + void add_le(rational_vector const& v); + void add_eq(rational_vector const& v); // add inequality v*x >= b // add inequality v*x <= b // add equality v*x = b - void add_ge(num_vector const& v, numeral const& b); - void add_le(num_vector const& v, numeral const& b); - void add_eq(num_vector const& v, numeral const& b); + void add_ge(rational_vector const& v, rational const& b); + void add_le(rational_vector const& v, rational const& b); + void add_eq(rational_vector const& v, rational const& b); void set_is_int(unsigned var_index); bool get_is_int(unsigned var_index) const; @@ -164,10 +180,10 @@ public: lbool saturate(); unsigned get_basis_size() const { return m_basis.size(); } - void get_basis_solution(unsigned i, num_vector& v, bool& is_initial); + void get_basis_solution(unsigned i, rational_vector& v, bool& is_initial); unsigned get_num_ineqs() const { return m_ineqs.size(); } - void get_ge(unsigned i, num_vector& v, numeral& b, bool& is_eq); + void get_ge(unsigned i, rational_vector& v, rational& b, bool& is_eq); void set_cancel(bool f) { m_cancel = f; } diff --git a/src/test/fdd.cpp b/src/test/fdd.cpp new file mode 100644 index 000000000..2a0079456 --- /dev/null +++ b/src/test/fdd.cpp @@ -0,0 +1,87 @@ +#include "fdd.h" + +static void test1() { + fdd::manager m; + + m.reset(2); + int64 keys1[2] = { 1, 2 }; + m.insert(keys1); + m.display(std::cout << "test1\n"); +} + +static void test2() { + fdd::manager m; + + m.reset(2); + int64 keys2[2] = { 2, 1 }; + m.insert(keys2); + m.display(std::cout << "test2\n"); + +} + +static void test3() { + fdd::manager m; + + m.reset(2); + int64 keys1[2] = { 1, 2 }; + int64 keys2[2] = { 2, 1 }; + m.insert(keys1); + m.insert(keys2); + m.display(std::cout << "test3\n"); +} + +static void test4() { + fdd::manager m; + + std::cout << "test4\n"; + + m.reset(2); + int64 keys1[2] = { 1, 2 }; + int64 keys2[2] = { 2, 1 }; + int64 keys3[2] = { 1, 1 }; + int64 keys4[2] = { 2, 2 }; + int64 keys5[2] = { 2, 3 }; + int64 keys6[2] = { 3, 1 }; + int64 keys7[2] = { 3, 4 }; + m.insert(keys1); + m.insert(keys2); + std::cout << m.find_le(keys1) << "\n"; + std::cout << m.find_le(keys2) << "\n"; + std::cout << m.find_le(keys3) << "\n"; + std::cout << m.find_le(keys4) << "\n"; + std::cout << m.find_le(keys5) << "\n"; + std::cout << m.find_le(keys6) << "\n"; + std::cout << m.find_le(keys7) << "\n"; + + SASSERT(m.find_le(keys1)); + SASSERT(m.find_le(keys2)); + SASSERT(!m.find_le(keys3)); + SASSERT(m.find_le(keys4)); + SASSERT(m.find_le(keys5)); + SASSERT(m.find_le(keys6)); + SASSERT(m.find_le(keys7)); +} + +static void test5() { + fdd::manager m; + + std::cout << "test5\n"; + + m.reset(2); + int64 keys1[2] = { 1, 2 }; + int64 keys2[2] = { 2, 1 }; + m.insert(keys1); + m.insert(keys2); + m.insert(keys2); + + m.display(std::cout); + +} + +void tst_fdd() { + test1(); + test2(); + test3(); + test4(); + test5(); +} diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp index dd04f7b98..92ef97f72 100644 --- a/src/test/heap_trie.cpp +++ b/src/test/heap_trie.cpp @@ -27,7 +27,8 @@ static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) { void tst_heap_trie() { - heap_trie_t ht; + unsigned_le le; + heap_trie_t ht(le); ht.reset(3); unsigned keys1[3] = { 1, 2, 3}; diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index bd5d20f8d..a5f554e5e 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -508,6 +508,12 @@ static void tst15() { saturate_basis(hb); } +static void tst16() { + hilbert_basis hb; + hb.add_le(vec(1, 0), R(100)); + saturate_basis(hb); +} + void tst_hilbert_basis() { std::cout << "hilbert basis test\n"; @@ -537,6 +543,7 @@ void tst_hilbert_basis() { tst13(); tst14(); tst15(); + tst16(); gorrila_test(0, 4, 3, 20, 5); gorrila_test(1, 4, 3, 20, 5); //gorrila_test(2, 4, 3, 20, 5); diff --git a/src/test/main.cpp b/src/test/main.cpp index c48f4529e..6ecfd6d4f 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -210,6 +210,7 @@ int main(int argc, char ** argv) { TST(hilbert_basis); TST(heap_trie); TST(karr); + TST(fdd); } void initialize_mam() {} diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h new file mode 100644 index 000000000..3772e5ab0 --- /dev/null +++ b/src/util/checked_int64.h @@ -0,0 +1,231 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + checked_int64.h + +Abstract: + + A class for wrapping checked (and unchecked) int64 operations. + Note: the mpfx class defines a more general class of fixed-point operations. + A tradeoff is that it relies on a manager. + This class several of the most common operations from rational, so + it can be swapped for rational. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-03-25. + +Revision History: + +--*/ + +#ifndef __CHECKED_INT64_H_ +#define __CHECKED_INT64_H_ + +#include"z3_exception.h" +#include"rational.h" + +template +class checked_int64 { + int64 m_value; + typedef checked_int64 ci; + + rational r64(int64 i) { return rational(i, rational::i64()); } + +public: + + checked_int64(): m_value(0) {} + checked_int64(int64 v): m_value(v) {} + checked_int64(checked_int64 const& other) { m_value = other.m_value; } + + class overflow_exception : public z3_exception { + virtual char const * msg() const { return "checked_int64 overflow/underflow";} + }; + + bool is_zero() const { return m_value == 0; } + bool is_pos() const { return m_value > 0; } + bool is_neg() const { return m_value < 0; } + bool is_one() const { return m_value == 1; } + bool is_minus_one() const { return m_value == -1; } + bool is_nonneg() const { return m_value >= 0; } + bool is_nonpos() const { return m_value <= 0; } + bool is_even() const { return 0 == (m_value ^ 0x1); } + + static checked_int64 zero() { return ci(0); } + static checked_int64 one() { return ci(1); } + static checked_int64 minus_one() { return ci(-1);} + + int64 get_int64() const { return m_value; } + + checked_int64 abs() const { + if (m_value >= 0) { + return *this; + } + if (CHECK && m_value == INT64_MIN) { + throw overflow_exception(); + } + return ci(-m_value); + } + + checked_int64& neg() { + if (CHECK && m_value == INT64_MIN) { + throw overflow_exception(); + } + m_value = -m_value; + return *this; + } + + unsigned hash() const { return static_cast(m_value); } + + struct hash_proc { unsigned operator()(checked_int64 const& r) const { return r.hash(); } }; + + struct eq_proc { bool operator()(checked_int64 const& r1, checked_int64 const& r2) const { return r1 == r2; } }; + + friend inline std::ostream& operator<<(std::ostream& out, checked_int64 const& i) { + return out << i.m_value; + } + + friend inline bool operator==(checked_int64 const& a, checked_int64 const& b) { + return a.m_value == b.m_value; + } + + friend inline bool operator<(checked_int64 const& a, checked_int64 const& b) { + return a.m_value < b.m_value; + } + + checked_int64 & operator++() { + if (CHECK && INT64_MAX == m_value) { + throw overflow_exception(); + } + ++m_value; + return *this; + } + + const checked_int64 operator++(int) { checked_int64 tmp(*this); ++(*this); return tmp; } + + checked_int64 & operator--() { + if (CHECK && m_value == INT64_MIN) { + throw overflow_exception(); + } + --m_value; + return *this; + } + + const checked_int64 operator--(int) { checked_int64 tmp(*this); --(*this); return tmp; } + + checked_int64& operator+=(checked_int64 const& other) { + if (CHECK && m_value > 0 && other.m_value > 0 && + (m_value > INT_MAX || other.m_value > INT_MAX)) { + rational r(r64(m_value) + r64(other.m_value)); + if (!r.is_int64()) { + throw overflow_exception(); + } + m_value = r.get_int64(); + return *this; + } + if (CHECK && m_value < 0 && other.m_value < 0 && + (m_value < INT_MIN || other.m_value < INT_MIN)) { + rational r(r64(m_value) + r64(other.m_value)); + if (!r.is_int64()) { + throw overflow_exception(); + } + m_value = r.get_int64(); + return *this; + } + m_value += other.m_value; + return *this; + } + + checked_int64& operator-=(checked_int64 const& other) { + if (CHECK && m_value > 0 && other.m_value < 0 && + (m_value > INT_MAX || other.m_value < INT_MIN)) { + rational r(r64(m_value) - r64(other.m_value)); + if (!r.is_int64()) { + throw overflow_exception(); + } + m_value = r.get_int64(); + return *this; + } + if (CHECK && m_value < 0 && other.m_value > 0 && + (m_value < INT_MIN || other.m_value > INT_MAX)) { + rational r(r64(m_value) - r64(other.m_value)); + if (!r.is_int64()) { + throw overflow_exception(); + } + m_value = r.get_int64(); + return *this; + } + m_value -= other.m_value; + return *this; + } + + checked_int64& operator*=(checked_int64 const& other) { + if (CHECK) { + rational r(r64(m_value) * r64(other.m_value)); + if (!r.is_int64()) { + throw overflow_exception(); + } + m_value = r.get_int64(); + } + else { + m_value *= other.m_value; + } + return *this; + } + + friend inline checked_int64 abs(checked_int64 const& i) { + return i.abs(); + } + +}; + +template +inline bool operator!=(checked_int64 const & i1, checked_int64 const & i2) { + return !operator==(i1, i2); +} + +template +inline bool operator>(checked_int64 const & i1, checked_int64 const & i2) { + return operator<(i2, i1); +} + +template +inline bool operator<=(checked_int64 const & i1, checked_int64 const & i2) { + return !operator>(i1, i2); +} + +template +inline bool operator>=(checked_int64 const & i1, checked_int64 const & i2) { + return !operator<(i1, i2); +} + +template +inline checked_int64 operator-(checked_int64 const& i) { + checked_int64 result(i); + return result.neg(); +} + +template +inline checked_int64 operator+(checked_int64 const& a, checked_int64 const& b) { + checked_int64 result(a); + result += b; + return result; +} + +template +inline checked_int64 operator-(checked_int64 const& a, checked_int64 const& b) { + checked_int64 result(a); + result -= b; + return result; +} + +template +inline checked_int64 operator*(checked_int64 const& a, checked_int64 const& b) { + checked_int64 result(a); + result *= b; + return result; +} + +#endif