From d2651f1afc4e9ca614a0a5332c46f6129a6fffc4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Feb 2013 18:53:37 -0800 Subject: [PATCH 1/6] Keep consistent error messages Signed-off-by: Leonardo de Moura --- src/ast/ast.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 704ae9fc8..8d643a348 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1849,9 +1849,9 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c sort * given = get_sort(args[i]); if (!compatible_sorts(expected, given)) { std::ostringstream buff; - buff << "Invalid function application for " << decl->get_name() << ". "; - buff << "Sort mismatch on argument at position " << (i+1) << ". "; - buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m); + buff << "invalid function application for " << decl->get_name() << ", "; + buff << "sort mismatch on argument at position " << (i+1) << ", "; + buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); throw ast_exception(buff.str().c_str()); } } @@ -1865,9 +1865,9 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c sort * given = get_sort(args[i]); if (!compatible_sorts(expected, given)) { std::ostringstream buff; - buff << "Invalid function application for " << decl->get_name() << ". "; - buff << "Sort mismatch on argument at position " << (i+1) << ". "; - buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m); + buff << "invalid function application for " << decl->get_name() << ", "; + buff << "sort mismatch on argument at position " << (i+1) << ", "; + buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); throw ast_exception(buff.str().c_str()); } } From 0c0fe40446b017ec20ff52a355dd2bcbf1a42dd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Feb 2013 19:03:37 -0800 Subject: [PATCH 2/6] Fix Python 2.6 incompatibility at mk_util.py Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4e1a38af2..873c22b80 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -76,10 +76,7 @@ GPROF=False GIT_HASH=False def check_output(cmd): - try: - return subprocess.check_output(cmd, shell=True).rstrip('\r\n') - except: - return subprocess.check_output(cmd).rstrip('\r\n') + return subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0].rstrip('\r\n') def git_hash(): try: From 030aef5d5a0e75aff9ad92e3a4eafd511aa3d79a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Feb 2013 09:55:42 -0800 Subject: [PATCH 3/6] Fix bug reported by Andrey Kupriyanov Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/api/c++/z3++.h | 22 ++++++++++++---------- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 27c52140f..13957064e 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -59,6 +59,8 @@ Version 4.3.2 - Fixed http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model. +- Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov). + Version 4.3.1 ============= diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5c1e6ca0c..5af4bf60b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -619,6 +619,8 @@ namespace z3 { a.check_error(); return expr(a.ctx(), r); } + friend expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } + friend expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); } /** \brief Create the if-then-else expression ite(c, t, e) @@ -758,7 +760,7 @@ namespace z3 { return expr(a.ctx(), r); } friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); } - friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - a; } + friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; } friend expr operator<=(expr const & a, expr const & b) { check_context(a, b); @@ -777,7 +779,7 @@ namespace z3 { return expr(a.ctx(), r); } friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); } - friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= a; } + friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; } friend expr operator>=(expr const & a, expr const & b) { check_context(a, b); @@ -796,7 +798,7 @@ namespace z3 { return expr(a.ctx(), r); } friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); } - friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= a; } + friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; } friend expr operator<(expr const & a, expr const & b) { check_context(a, b); @@ -815,7 +817,7 @@ namespace z3 { return expr(a.ctx(), r); } friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); } - friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < a; } + friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; } friend expr operator>(expr const & a, expr const & b) { check_context(a, b); @@ -834,7 +836,7 @@ namespace z3 { return expr(a.ctx(), r); } friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); } - friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > a; } + friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; } friend expr operator&(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); } friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); } @@ -888,31 +890,31 @@ namespace z3 { */ inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); } inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); } - inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), a); } + inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); } /** \brief unsigned less than operator for bitvectors. */ inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); } inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); } - inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), a); } + inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); } /** \brief unsigned greater than or equal to operator for bitvectors. */ inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); } inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); } - inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), a); } + inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); } /** \brief unsigned greater than operator for bitvectors. */ inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); } inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); } - inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), a); } + inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); } /** \brief unsigned division operator for bitvectors. */ inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); } inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); } - inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), a); } + inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); } // Basic functions for creating quantified formulas. // The C API should be used for creating quantifiers with patterns, weights, many variables, etc. From 9d45d872a78d092e276aa6243fb4017ab5735940 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Feb 2013 10:26:15 -0800 Subject: [PATCH 4/6] Compress Z3 distribution zip files Signed-off-by: Leonardo de Moura --- scripts/mk_unix_dist.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 3b9511367..8256236cb 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -190,7 +190,7 @@ def mk_zip(): try: os.chdir(DIST_DIR) zfname = '%s.zip' % dist_path - ZIPOUT = zipfile.ZipFile(zfname, 'w') + ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED) os.path.walk(dist_path, mk_zip_visitor, '*') if is_verbose(): print "Generated '%s'" % zfname From 5e72cf0123f6c9c03ccab44d3aa1209603eb134f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Feb 2013 10:55:43 -0800 Subject: [PATCH 5/6] Compress windows distribution zip files Signed-off-by: Leonardo de Moura --- scripts/mk_win_dist.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 137ea431c..a52c8af43 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -205,7 +205,7 @@ def mk_zip_core(x64): try: os.chdir(DIST_DIR) zfname = '%s.zip' % dist_path - ZIPOUT = zipfile.ZipFile(zfname, 'w') + ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED) os.path.walk(dist_path, mk_zip_visitor, '*') if is_verbose(): print "Generated '%s'" % zfname From 6e7d04f94e1bcc05c0a72c5bf8c438caa7cd2ad2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Feb 2013 15:06:17 -0800 Subject: [PATCH 6/6] working on hilbert basis Signed-off-by: Nikolaj Bjorner --- src/muz_qe/hilbert_basis.cpp | 701 ++++++++++++++++++----------------- src/muz_qe/hilbert_basis.h | 37 +- src/test/hilbert_basis.cpp | 41 +- 3 files changed, 412 insertions(+), 367 deletions(-) diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 59c9d5080..b452fbc77 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -26,364 +26,219 @@ typedef u_map offset_refs_t; template class rational_map : public map {}; -class rational_abs_lt { - vector & m_values; -public: - rational_abs_lt(vector & values): - m_values(values) { - } - bool operator()(int v1, int v2) const { - return m_values[v1] < m_values[v2]; - } -}; - -class hilbert_basis::rational_heap { - vector m_u2r; // [index |-> weight] - rational_map m_r2u; // [weight |-> index] - rational_abs_lt m_lt; // less_than on indices - heap m_heap; // binary heap over weights -public: - - rational_heap(): m_lt(m_u2r), m_heap(10, m_lt) {} - - vector& u2r() { return m_u2r; } - - void insert(unsigned v) { - m_heap.insert(v); - } - - void reset() { - m_u2r.reset(); - m_r2u.reset(); - m_heap.reset(); - } - - bool is_declared(numeral const& r, unsigned& val) const { - return m_r2u.find(r, val); - } - - unsigned declare(numeral const& r) { - SASSERT(!m_r2u.contains(r)); - unsigned val = m_u2r.size(); - m_u2r.push_back(r); - m_r2u.insert(r, val); - m_heap.set_bounds(val+1); - return val; - } - - void find_le(unsigned val, int_vector & result) { - m_heap.find_le(val, result); - } - -}; - -class hilbert_basis::weight_map { +class hilbert_basis::value_index { struct stats { unsigned m_num_comparisons; + unsigned m_num_hit; + unsigned m_num_miss; + stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; - rational_heap m_heap; - vector m_offsets; // [index |-> offset-list] - int_vector m_le; // recycled set of indices with lesser weights - stats m_stats; - svector& m_found; - offset_refs_t& m_refs; - unsigned m_cost; + typedef int_hashtable > int_table; + hilbert_basis& hb; + int_table m_table; + stats m_stats; - unsigned get_value(numeral const& w) { - numeral r = abs(w); - unsigned val; - if (!m_heap.is_declared(r, val)) { - val = m_heap.declare(r); - SASSERT(val == m_offsets.size()); - if (r.is_nonneg()) { - m_heap.insert(val); - } - m_offsets.push_back(unsigned_vector()); - } - return val; - } public: - weight_map(svector& found, offset_refs_t& refs): m_found(found), m_refs(refs) {} - - void insert(offset_t idx, numeral const& w) { - unsigned val = get_value(w); - m_offsets[val].push_back(idx.m_offset); + value_index(hilbert_basis& hb): + hb(hb) + {} + + void insert(offset_t idx, values const& vs) { + m_table.insert(idx.m_offset); } - void remove(offset_t idx, numeral const& w) { - unsigned val = get_value(w); - m_offsets[val].erase(idx.m_offset); - } - - unsigned get_size() const { - unsigned sz = 0; - for (unsigned i = 0; i < m_offsets.size(); ++i) { - sz += m_offsets[i].size(); - } - return sz; + void remove(offset_t idx, values const& vs) { + m_table.remove(idx.m_offset); } void reset() { - m_offsets.reset(); - m_heap.reset(); - m_le.reset(); - } - - unsigned get_cost() const { return m_cost; } - - /** - retrieve - */ - bool init_find(numeral const& w, offset_t idx) { - m_le.reset(); - m_found.reset(); - m_cost = 0; - unsigned val = get_value(w); - // for positive values, the weights should be less or equal. - // for non-positive values, the weights have to be the same. - if (w.is_pos()) { - m_heap.find_le(val, m_le); - } - else { - m_le.push_back(val); - } - for (unsigned i = 0; i < m_le.size(); ++i) { - if (m_heap.u2r()[m_le[i]].is_zero() && !w.is_zero()) { - continue; - } - unsigned_vector const& offsets = m_offsets[m_le[i]]; - for (unsigned j = 0; j < offsets.size(); ++j) { - unsigned offs = offsets[j]; - ++m_stats.m_num_comparisons; - ++m_cost; - if (offs != idx.m_offset) { - m_refs.insert(offs, 0); - m_found.push_back(offset_t(offs)); - } - } - } - return !m_found.empty(); + m_table.reset(); } - unsigned get_find_cost(numeral const& w) { - m_le.reset(); - unsigned cost = 0; - unsigned val = get_value(w); - m_heap.find_le(val, m_le); - for (unsigned i = 0; i < m_le.size(); ++i) { - cost += m_offsets[m_le[i]].size(); - } - return cost; - } - - bool update_find(unsigned round, numeral const& w, offset_t idx) { - m_found.reset(); - m_le.reset(); - m_cost = 0; - unsigned vl = get_value(w); - m_heap.find_le(vl, m_le); - for (unsigned i = 0; i < m_le.size(); ++i) { - unsigned_vector const& offsets = m_offsets[m_le[i]]; - for (unsigned j = 0; j < offsets.size(); ++j) { - unsigned offs = offsets[j]; - ++m_stats.m_num_comparisons; - ++m_cost; - if (offs != idx.m_offset && m_refs.find(offs, vl) && vl == round) { - m_refs.insert(offs, round + 1); - m_found.push_back(offset_t(offs)); - } + bool find(offset_t idx, values const& vs, offset_t& found_idx) { + // 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 != idx.m_offset && hb.is_subsumed(idx, offs)) { + found_idx = offs; + ++m_stats.m_num_hit; + return true; } } - return !m_found.empty(); - } + ++m_stats.m_num_miss; + return false; + } void collect_statistics(statistics& st) const { st.update("hb.index.num_comparisons", m_stats.m_num_comparisons); + st.update("hb.index.num_hit", m_stats.m_num_hit); + st.update("hb.index.num_miss", m_stats.m_num_miss); } void reset_statistics() { m_stats.reset(); } + + unsigned size() const { + return m_table.size(); + } +private: + void display_profile(offset_t idx, std::ostream& out) { + unsigned_vector leq; + unsigned nv = hb.get_num_vars(); + values const& vs = hb.vec(idx); + leq.resize(nv+1); + numeral maxw(0); + for (unsigned i = 0; i < nv; ++i) { + if (!hb.is_abs_geq(maxw, vs[i])) { + maxw = vs[i]; + } + } + unsigned num_below_max = 0; + int_table::iterator it = m_table.begin(), end = m_table.end(); + for (; it != end; ++it) { + offset_t offs(*it); + values const& ws = hb.vec(offs); + if (ws.weight() <= vs.weight()) { + leq[0]++; + } + bool filtered = false; + for (unsigned i = 0; i < nv; ++i) { + if (hb.is_abs_geq(vs[i], ws[i])) { + leq[i+1]++; + } + if (!hb.is_abs_geq(maxw, ws[i])) { + filtered = true; + } + } + if (!filtered) { + ++num_below_max; + } + } + out << vs.weight() << ":" << leq[0] << " "; + for (unsigned i = 0; i < nv; ++i) { + out << vs[i] << ":" << leq[i+1] << " "; + } + out << " max<= " << num_below_max; + out << "\n"; + } }; + + class hilbert_basis::index { - // for each index, a heap of weights. - // for each weight a list of offsets + // for each non-positive weight a separate index. + // for positive weights a shared value index. struct stats { - unsigned m_num_comparisons; unsigned m_num_find; unsigned m_num_insert; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; - - hilbert_basis& hb; - offset_refs_t m_refs; - svector m_found; - ptr_vector m_values; - weight_map m_weight; - stats m_stats; + typedef rational_map value_map; + hilbert_basis& hb; + value_map m_neg; + value_index m_pos; + value_index m_zero; + stats m_stats; public: - - index(hilbert_basis& hb): hb(hb), m_weight(m_found, m_refs) {} - - ~index() { - for (unsigned i = 0; i < m_values.size(); ++i) { - dealloc(m_values[i]); - } - } - - void init(unsigned num_vars) { - if (m_values.empty()) { - for (unsigned i = 0; i < num_vars; ++i) { - m_values.push_back(alloc(weight_map, m_found, m_refs)); - } - } - SASSERT(m_values.size() == num_vars); - } + index(hilbert_basis& hb): hb(hb), m_pos(hb), m_zero(hb) {} void insert(offset_t idx, values const& vs) { ++m_stats.m_num_insert; -#if 0 - for (unsigned i = 0; i < m_values.size(); ++i) { - m_values[i]->insert(idx, vs[i]); + if (vs.weight().is_pos()) { + m_pos.insert(idx, vs); + } + else if (vs.weight().is_zero()) { + m_zero.insert(idx, vs); + } + else { + value_index* map = 0; + if (!m_neg.find(vs.weight(), map)) { + map = alloc(value_index, hb); + m_neg.insert(vs.weight(), map); + } + map->insert(idx, vs); } -#endif - m_weight.insert(idx, vs.value()); } void remove(offset_t idx, values const& vs) { -#if 0 - for (unsigned i = 0; i < m_values.size(); ++i) { - m_values[i]->remove(idx, vs[i]); + if (vs.weight().is_pos()) { + m_pos.remove(idx, vs); } -#endif - m_weight.remove(idx, vs.value()); + else if (vs.weight().is_zero()) { + m_zero.remove(idx, vs); + } + else { + m_neg.find(vs.weight())->remove(idx, vs); + } } - bool find(values const& vs, offset_t idx, offset_t& found_idx) { + bool find(offset_t idx, values const& vs, offset_t& found_idx) { ++m_stats.m_num_find; - m_refs.reset(); - bool found = m_weight.init_find(vs.value(), idx); - TRACE("hilbert_basis", tout << "init: " << m_found.size() << " cost: " << m_weight.get_cost() << "\n";); -#if 0 - std::cout << vs.value() << " " << m_found.size() << " "; - for (unsigned i = 0; i < m_values.size(); ++i) { - std::cout << vs[i] << ": " << m_values[i]->get_find_cost(vs[i]) << " "; + if (vs.weight().is_pos()) { + return m_pos.find(idx, vs, found_idx); } - std::cout << "\n"; -#endif -#if 0 - for (unsigned i = 0; found && i < m_values.size(); ++i) { - found = m_values[i]->update_find(i, vs[i], idx); - std::cout << vs[i] << ": " << m_found.size() << " "; - TRACE("hilbert_basis", tout << "update " << i << ": " << m_found.size() << " cost: " << m_values[i]->get_cost() << "\n";); + else if (vs.weight().is_zero()) { + return m_zero.find(idx, vs, found_idx); } -#else - for (unsigned i = 0; i < m_found.size(); ++i) { - if (is_subsumed(idx, m_found[i])) { - found_idx = m_found[i]; - return true; - } - } - return false; -#endif - - if (found) { - found_idx = m_found[0]; - } - return found; - } + else { + value_index* map; + return + m_neg.find(vs.weight(), map) && + map->find(idx, vs, found_idx); + } + } void reset() { - for (unsigned i = 0; i < m_values.size(); ++i) { - m_values[i]->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_weight.reset(); - m_refs.reset(); } void collect_statistics(statistics& st) const { - m_weight.collect_statistics(st); - for (unsigned i = 0; i < m_values.size(); ++i) { - m_values[i]->collect_statistics(st); - } - st.update("hb.index.num_find", m_stats.m_num_find); + m_pos.collect_statistics(st); + m_zero.collect_statistics(st); + value_map::iterator it = m_neg.begin(), end = m_neg.end(); + for (; it != end; ++it) { + it->m_value->collect_statistics(st); + } + st.update("hb.index.num_find", m_stats.m_num_find); st.update("hb.index.num_insert", m_stats.m_num_insert); - st.update("hb.index.size", m_weight.get_size()); + st.update("hb.index.size", size()); } void reset_statistics() { - m_stats.reset(); - m_weight.reset_statistics(); - for (unsigned i = 0; i < m_values.size(); ++i) { - m_values[i]->reset_statistics(); - } - } - - - /** - Vector v is subsumed by vector w if - - v[i] >= w[i] for each index i. - - a*v >= a*w for the evaluation of vectors with respect to a. - - a*v < 0 => a*v = a*w - - - Justification: - - let u := v - w, then - - u[i] >= 0 for each index i - - a*u = a*(v-w) >= 0 - - So v = u + w, where a*u >= 0, a*w >= 0. - - If a*v >= a*w >= 0 then v and w are linear - solutions of e_i, and also v-w is a solution. - - If a*v = a*w < 0, then a*(v-w) = 0, so v can be obtained from w + (v - w). - - */ - - bool is_subsumed(offset_t i, offset_t j) const { - values v = hb.vec(i); - values w = hb.vec(j); - numeral const& n = v.value(); - numeral const& m = w.value(); - bool r = - i.m_offset != j.m_offset && - n >= m && (!m.is_neg() || n == m) && - is_geq(v, w); - CTRACE("hilbert_basis", r, - hb.display(tout, i); - tout << " <= \n"; - hb.display(tout, j); - tout << "\n";); - return r; - } - - bool is_geq(values v, values w) const { - unsigned nv = hb.get_num_vars(); - for (unsigned i = 0; i < nv; ++i) { - if (v[i] < w[i]) { - return false; - } + m_pos.reset_statistics(); + m_zero.reset_statistics(); + value_map::iterator it = m_neg.begin(), end = m_neg.end(); + for (; it != end; ++it) { + it->m_value->reset_statistics(); } - return true; } - - + +private: + unsigned size() const { + unsigned sz = m_pos.size(); + sz += m_zero.size(); + value_map::iterator it = m_neg.begin(), end = m_neg.end(); + for (; it != end; ++it) { + sz += it->m_value->size(); + } + return sz; + } }; /** @@ -391,18 +246,25 @@ public: */ class hilbert_basis::passive { + struct lt { + passive& p; + lt(passive& p): p(p) {} + + bool operator()(int v1, int v2) const { + return p(v1, v2); + } + }; hilbert_basis& hb; svector m_passive; - vector m_weights; unsigned_vector m_free_list; - rational_abs_lt m_lt; // less_than on indices - heap m_heap; // binary heap over weights + lt m_lt; + heap m_heap; // binary heap over weights - numeral get_weight(offset_t idx) { + numeral get_value(offset_t idx) const { numeral w(0); unsigned nv = hb.get_num_vars(); for (unsigned i = 0; i < nv; ++i) { - w += hb.vec(idx)[i]; + w += abs(hb.vec(idx)[i]); } return w; } @@ -411,14 +273,13 @@ public: passive(hilbert_basis& hb): hb(hb) , - m_lt(m_weights), + m_lt(*this), m_heap(10, m_lt) {} void reset() { m_heap.reset(); m_free_list.reset(); - m_weights.reset(); m_passive.reset(); } @@ -440,14 +301,12 @@ public: if (m_free_list.empty()) { v = m_passive.size(); m_passive.push_back(idx); - m_weights.push_back(get_weight(idx)); m_heap.set_bounds(v+1); } else { v = m_free_list.back(); m_free_list.pop_back(); m_passive[v] = idx; - m_weights[v] = get_weight(idx); } m_heap.insert(v); } @@ -478,6 +337,43 @@ public: iterator end() { 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 + } + }; hilbert_basis::hilbert_basis(): @@ -529,9 +425,6 @@ void hilbert_basis::add_ge(num_vector const& v, numeral const& b) { num_vector w; w.push_back(-b); w.append(v); - if (m_ineqs.empty()) { - m_index->init(w.size()); - } m_ineqs.push_back(w); } @@ -561,6 +454,14 @@ void hilbert_basis::add_eq(num_vector const& v) { add_ge(v); } +void hilbert_basis::set_is_int(unsigned var_index) { + // + // The 0't index is reserved for the constant + // coefficient. Shift indices by 1. + // + m_ints.push_back(var_index+1); +} + unsigned hilbert_basis::get_num_vars() const { if (m_ineqs.empty()) { return 0; @@ -580,26 +481,34 @@ void hilbert_basis::init_basis() { m_free_list.reset(); unsigned num_vars = get_num_vars(); for (unsigned i = 0; i < num_vars; ++i) { - num_vector w(num_vars, numeral(0)); - w[i] = numeral(1); - offset_t idx = alloc_vector(); - values v = vec(idx); - for (unsigned i = 0; i < num_vars; ++i) { - v[i] = w[i]; - } - m_basis.push_back(idx); + add_unit_vector(i, numeral(1)); } + for (unsigned i = 0; i < m_ints.size(); ++i) { + add_unit_vector(m_ints[i], numeral(-1)); + } +} + +void hilbert_basis::add_unit_vector(unsigned i, numeral const& e) { + unsigned num_vars = get_num_vars(); + num_vector w(num_vars, numeral(0)); + w[i] = e; + offset_t idx = alloc_vector(); + values v = vec(idx); + for (unsigned j = 0; j < num_vars; ++j) { + v[j] = w[j]; + } + m_basis.push_back(idx); } lbool hilbert_basis::saturate() { - init_basis(); + init_basis(); for (unsigned i = 0; !m_cancel && i < m_ineqs.size(); ++i) { + select_inequality(i); lbool r = saturate(m_ineqs[i]); ++m_stats.m_num_saturations; if (r != l_true) { return r; - } - + } } if (m_cancel) { return l_undef; @@ -619,7 +528,7 @@ lbool hilbert_basis::saturate(num_vector const& ineq) { values v = vec(*it); set_eval(v, ineq); add_goal(*it); - if (v.value().is_nonneg()) { + if (v.weight().is_nonneg()) { has_non_negative = true; } } @@ -652,7 +561,7 @@ lbool hilbert_basis::saturate(num_vector const& ineq) { m_basis.append(m_zero); for (unsigned i = 0; i < m_active.size(); ++i) { offset_t idx = m_active[i]; - if (vec(idx).value().is_pos()) { + if (vec(idx).weight().is_pos()) { m_basis.push_back(idx); } else { @@ -666,6 +575,51 @@ lbool hilbert_basis::saturate(num_vector const& ineq) { return l_true; } +void hilbert_basis::select_inequality(unsigned i) { + SASSERT(i < m_ineqs.size()); + unsigned best = i; + unsigned non_zeros = get_num_nonzeros(m_ineqs[i]); + unsigned prod = get_ineq_product(m_ineqs[i]); + for (unsigned j = i+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]); + if (prod2 < prod || (prod2 == prod && non_zeros2 < non_zeros)) { + prod = prod2; + non_zeros = non_zeros2; + best = j; + } + } + if (best != i) { + std::swap(m_ineqs[i], m_ineqs[best]); + } +} + +unsigned hilbert_basis::get_num_nonzeros(num_vector const& ineq) { + unsigned count = 0; + for (unsigned i = 0; i < ineq.size(); ++i) { + if (!ineq[i].is_zero()) { + ++count; + } + } + return count; +} + +unsigned hilbert_basis::get_ineq_product(num_vector const& ineq) { + unsigned num_pos = 0, num_neg = 0; + iterator it = begin(); + for (; it != end(); ++it) { + values v = vec(*it); + set_eval(v, ineq); + if (v.weight().is_pos()) { + ++num_pos; + } + else if (v.weight().is_neg()) { + ++num_neg; + } + } + return num_pos * num_neg; +} + void hilbert_basis::recycle(offset_t idx) { m_index->remove(idx, vec(idx)); m_free_list.push_back(idx); @@ -680,8 +634,8 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) { for (unsigned k = 0; k < nv; ++k) { u[k] = v[k] + w[k]; } - u.value() = v.value() + w.value(); - // std::cout << "resolve: " << v.value() << " + " << w.value() << " = " << u.value() << "\n"; + u.weight() = v.weight() + w.weight(); + // std::cout << "resolve: " << v.weight() << " + " << w.weight() << " = " << u.weight() << "\n"; TRACE("hilbert_basis_verbose", display(tout, i); display(tout, j); @@ -694,7 +648,7 @@ hilbert_basis::offset_t hilbert_basis::alloc_vector() { if (m_free_list.empty()) { unsigned num_vars = get_num_vars(); unsigned idx = m_store.size(); - m_store.resize(idx + 1 + get_num_vars()); + m_store.resize(idx + 1 + num_vars); return offset_t(idx); } else { @@ -710,7 +664,7 @@ void hilbert_basis::add_goal(offset_t idx) { return; } m_index->insert(idx, v); - if (v.value().is_zero()) { + if (v.weight().is_zero()) { m_zero.push_back(idx); } else { @@ -721,12 +675,7 @@ void hilbert_basis::add_goal(offset_t idx) { bool hilbert_basis::is_subsumed(offset_t idx) { offset_t found_idx; - if (m_index->find(vec(idx), idx, found_idx)) { - TRACE("hilbert_basis", - display(tout, idx); - tout << " <= \n"; - display(tout, found_idx); - tout << "\n";); + if (m_index->find(idx, vec(idx), found_idx)) { ++m_stats.m_num_subsumptions; return true; } @@ -734,13 +683,30 @@ bool hilbert_basis::is_subsumed(offset_t idx) { } bool hilbert_basis::can_resolve(offset_t i, offset_t j) const { - sign_t s1 = get_sign(i); - sign_t s2 = get_sign(j); - return s1 != s2 && abs(vec(i)[0] + vec(j)[0]) <= numeral(1); + if (get_sign(i) == get_sign(j)) { + return false; + } + 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)) { + return false; + } + for (unsigned i = 0; i < m_ints.size(); ++i) { + unsigned j = m_ints[i]; + if (v1[j].is_pos() && v2[j].is_neg()) { + return false; + } + if (v1[j].is_neg() && v2[j].is_pos()) { + return false; + } + } + return true; } hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const { - numeral val = vec(idx).value(); + numeral val = vec(idx).weight(); if (val.is_pos()) { return pos; } @@ -756,7 +722,7 @@ void hilbert_basis::set_eval(values& val, num_vector const& ineq) const { for (unsigned i = 0; i < num_vars; ++i) { result += val[i]*ineq[i]; } - val.value() = result; + val.weight() = result; } void hilbert_basis::display(std::ostream& out) const { @@ -796,7 +762,7 @@ void hilbert_basis::display(std::ostream& out) const { void hilbert_basis::display(std::ostream& out, offset_t o) const { display(out, vec(o)); - out << " -> " << vec(o).value() << "\n"; + out << " -> " << vec(o).weight() << "\n"; } void hilbert_basis::display(std::ostream& out, values const& v) const { @@ -842,3 +808,68 @@ void hilbert_isl_basis::add_le(num_vector const& v, numeral bound) { } m_basis.add_le(w); } + + +/** + Vector v is subsumed by vector w if + + v[i] >= w[i] for each index i. + + a*v >= a*w for the evaluation of vectors with respect to a. + + . a*v < 0 => a*v = a*w + . a*v > 0 => a*w > 0 + . a*v = 0 => a*w = 0 + + Justification: + + let u := v - w, then + + u[i] >= 0 for each index i + + a*u = a*(v-w) >= 0 + + So v = u + w, where a*u >= 0, a*w >= 0. + + If a*v >= a*w >= 0 then v and w are linear + solutions of e_i, and also v-w is a solution. + + If a*v = a*w < 0, then a*(v-w) = 0, so v can be obtained from w + (v - w). + +*/ + +bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const { + values v = vec(i); + values w = vec(j); + numeral const& n = v.weight(); + numeral const& m = w.weight(); + bool r = + i.m_offset != j.m_offset && + n >= m && (!m.is_nonpos() || n == m) && + is_geq(v, w); + CTRACE("hilbert_basis", r, + display(tout, i); + tout << " <= \n"; + display(tout, j); + tout << "\n";); + return r; +} + +bool hilbert_basis::is_geq(values const& v, values const& w) const { + unsigned nv = get_num_vars(); + for (unsigned i = 0; i < nv; ++i) { + if (!is_abs_geq(v[i], w[i])) { + return false; + } + } + return true; +} + +bool hilbert_basis::is_abs_geq(numeral const& v, numeral const& w) const { + if (w.is_neg()) { + return v <= w; + } + else { + return v >= w; + } +} diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h index f4529de85..000f27ec8 100644 --- a/src/muz_qe/hilbert_basis.h +++ b/src/muz_qe/hilbert_basis.h @@ -34,10 +34,9 @@ public: typedef rational numeral; typedef vector num_vector; private: - class rational_heap; + class value_index; class index; class passive; - class weight_map; struct offset_t { unsigned m_offset; offset_t(unsigned o) : m_offset(o) {} @@ -58,25 +57,26 @@ private: numeral* m_values; public: values(numeral* v):m_values(v) {} - numeral& value() { return m_values[0]; } // value of a*x + numeral& weight() { return m_values[0]; } // value of a*x numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i - numeral const& value() const { return m_values[0]; } // value of a*x + 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 }; - vector m_ineqs; - num_vector m_store; - svector m_basis; - svector m_free_list; - svector m_active; - svector m_zero; - volatile bool m_cancel; + vector m_ineqs; // set of asserted inequalities + num_vector m_store; // store of vectors + svector m_basis; // vector of current basis + svector m_free_list; // free list of unused storage + svector m_active; // active set + svector m_zero; // zeros + passive* m_passive; // passive set + volatile bool m_cancel; stats m_stats; - index* m_index; - passive* m_passive; + index* m_index; // index of generated vectors + unsigned_vector m_ints; // indices that can be both positive and negative class iterator { hilbert_basis const& hb; - unsigned m_idx; + unsigned m_idx; public: iterator(hilbert_basis const& hb, unsigned idx): hb(hb), m_idx(idx) {} offset_t operator*() const { return hb.m_basis[m_idx]; } @@ -90,8 +90,15 @@ private: static bool is_invalid_offset(offset_t offs); lbool saturate(num_vector const& ineq); void init_basis(); + void select_inequality(unsigned i); + unsigned get_num_nonzeros(num_vector const& ineq); + unsigned get_ineq_product(num_vector const& ineq); + + void add_unit_vector(unsigned i, numeral const& e); unsigned get_num_vars() const; void set_eval(values& val, num_vector const& ineq) const; + bool is_geq(values const& v, values const& w) const; + 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); @@ -130,6 +137,8 @@ public: void add_le(num_vector const& v, numeral const& b); void add_eq(num_vector const& v, numeral const& b); + void set_is_int(unsigned var_index); + lbool saturate(); void set_cancel(bool f) { m_cancel = f; } diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index 86b0f1bad..8629e50be 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -245,23 +245,28 @@ static void tst11() { void tst_hilbert_basis() { std::cout << "hilbert basis test\n"; -#if 0 - tst1(); - tst2(); - tst3(); tst4(); - tst5(); - tst6(); - tst7(); - tst8(); - tst9(); - tst10(); - tst11(); - gorrila_test(0, 4, 3, 20, 5); - gorrila_test(1, 4, 3, 20, 5); - gorrila_test(2, 4, 3, 20, 5); - gorrila_test(0, 4, 2, 20, 5); - gorrila_test(0, 4, 2, 20, 5); -#endif - gorrila_test(0, 10, 7, 20, 11); + return; + + if (true) { + tst1(); + tst2(); + tst3(); + tst4(); + tst5(); + tst6(); + tst7(); + tst8(); + tst9(); + tst10(); + tst11(); + gorrila_test(0, 4, 3, 20, 5); + gorrila_test(1, 4, 3, 20, 5); + gorrila_test(2, 4, 3, 20, 5); + gorrila_test(0, 4, 2, 20, 5); + gorrila_test(0, 4, 2, 20, 5); + } + else { + gorrila_test(0, 10, 7, 20, 11); + } }