From 8ea49eed8ec34b8743fd097707d1ecb83bf317e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Jan 2023 20:12:14 -0800 Subject: [PATCH] convert reduce-args to a simplifier - convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed. - bug fixes in model_reconstruction trail - allow multiple defs to be added with same pool of removed formulas - fix tracking of function symbols instead of expressions to filter replay - add nla_divisions to track (cheap) divisibility lemmas. - --- src/ast/ast_util.h | 2 + src/ast/converters/generic_model_converter.h | 2 - src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/dependent_expr_state.cpp | 7 +- src/ast/simplifiers/dependent_expr_state.h | 2 +- .../model_reconstruction_trail.cpp | 36 +- .../simplifiers/model_reconstruction_trail.h | 49 +- .../simplifiers/reduce_args_simplifier.cpp | 428 ++++++++++++++++++ src/ast/simplifiers/reduce_args_simplifier.h | 16 + src/math/lp/CMakeLists.txt | 1 + src/math/lp/nla_core.cpp | 9 + src/math/lp/nla_core.h | 4 + src/math/lp/nla_divisions.cpp | 65 +++ src/math/lp/nla_divisions.h | 31 ++ src/math/lp/nla_solver.cpp | 4 + src/math/lp/nla_solver.h | 1 + src/math/lp/var_eqs.h | 3 +- src/sat/sat_solver/sat_smt_solver.cpp | 72 ++- src/smt/theory_lra.cpp | 7 + src/tactic/core/reduce_args_tactic.cpp | 10 +- src/tactic/core/reduce_args_tactic.h | 10 + src/tactic/dependent_expr_state_tactic.h | 56 ++- src/util/bit_vector.h | 16 + 23 files changed, 740 insertions(+), 92 deletions(-) create mode 100644 src/ast/simplifiers/reduce_args_simplifier.cpp create mode 100644 src/ast/simplifiers/reduce_args_simplifier.h create mode 100644 src/math/lp/nla_divisions.cpp create mode 100644 src/math/lp/nla_divisions.h diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index 1c56b64b3..8e07ccd27 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -101,6 +101,8 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx); */ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args); app * mk_and(ast_manager & m, unsigned num_args, app * const * args); +inline expr * mk_and(ast_manager & m, ptr_vector const& args) { return mk_and(m, args.size(), args.data()); } +inline expr * mk_and(ast_manager & m, ptr_buffer const& args) { return mk_and(m, args.size(), args.data()); } inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); } inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); } inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); } diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h index cf551c92a..8a1c62347 100644 --- a/src/ast/converters/generic_model_converter.h +++ b/src/ast/converters/generic_model_converter.h @@ -68,8 +68,6 @@ public: void get_units(obj_map& units) override; vector const& entries() const { return m_entries; } - - void shrink(unsigned j) { m_entries.shrink(j); } }; typedef ref generic_model_converter_ref; diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 826717c5a..127db786a 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -19,6 +19,7 @@ z3_add_component(simplifiers max_bv_sharing.cpp model_reconstruction_trail.cpp propagate_values.cpp + reduce_args_simplifier.cpp solve_context_eqs.cpp solve_eqs.cpp COMPONENT_DEPENDENCIES diff --git a/src/ast/simplifiers/dependent_expr_state.cpp b/src/ast/simplifiers/dependent_expr_state.cpp index fec6d28cf..d784e6fe4 100644 --- a/src/ast/simplifiers/dependent_expr_state.cpp +++ b/src/ast/simplifiers/dependent_expr_state.cpp @@ -31,8 +31,13 @@ void dependent_expr_state::freeze(func_decl* f) { } void dependent_expr_state::freeze(expr* term) { - if (is_app(term)) + if (is_app(term) && to_app(term)->get_num_args() == 0) freeze(to_app(term)->get_decl()); + else { + ast_mark visited; + freeze_terms(term, false, visited); + } + } /** diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index c3b5043a5..0fedf484c 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -80,7 +80,7 @@ public: m_trail.push(value_trail(m_qhead)); m_trail.push(thaw(*this)); } - void pop(unsigned n) { m_trail.pop_scope(n); } + void pop(unsigned n) { m_trail.pop_scope(n); } void advance_qhead() { freeze_prefix(); m_suffix_frozen = false; m_has_quantifiers = l_undef; m_qhead = qtail(); } unsigned num_exprs(); diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index e3cfc5c6f..893af7106 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -13,6 +13,7 @@ Author: #include "ast/for_each_expr.h" +#include "ast/ast_ll_pp.h" #include "ast/rewriter/macro_replacer.h" #include "ast/simplifiers/model_reconstruction_trail.h" #include "ast/simplifiers/dependent_expr_state.h" @@ -24,6 +25,10 @@ Author: // TODO: add filters to skip sections of the trail that do not touch the current free variables. void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) { + TRACE("simplifier", + for (unsigned i = qhead; i < st.qtail(); ++i) + tout << mk_bounded_pp(st[i].fml(), m) << "\n"; + ); ast_mark free_vars; scoped_ptr rp = mk_default_expr_replacer(m, false); for (unsigned i = qhead; i < st.qtail(); ++i) @@ -32,6 +37,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt add_vars(a, free_vars); for (auto& t : m_trail) { + TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << "\n"); if (!t->m_active) continue; @@ -56,15 +62,17 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt if (t->is_def()) { macro_replacer mrp(m); - app_ref head(m); - func_decl* d = t->m_decl; - ptr_buffer args; - for (unsigned i = 0; i < d->get_arity(); ++i) - args.push_back(m.mk_var(i, d->get_domain(i))); - head = m.mk_app(d, args); - mrp.insert(head, t->m_def, t->m_dep); - dependent_expr de(m, t->m_def, nullptr, t->m_dep); - add_vars(de, free_vars); + for (auto const& [d, def, dep] : t->m_defs) { + app_ref head(m); + ptr_buffer args; + for (unsigned i = 0; i < d->get_arity(); ++i) + args.push_back(m.mk_var(i, d->get_domain(i))); + head = m.mk_app(d, args); + mrp.insert(head, def, dep); + TRACE("simplifier", tout << d << " " << def << " " << dep << "\n"); + dependent_expr de(m, def, nullptr, dep); + add_vars(de, free_vars); + } for (unsigned i = qhead; i < st.qtail(); ++i) { auto [f, p, dep1] = st[i](); @@ -140,6 +148,7 @@ model_converter_ref model_reconstruction_trail::get_model_converter() { * Append model conversions starting at index i */ void model_reconstruction_trail::append(generic_model_converter& mc, unsigned& i) { + TRACE("simplifier", display(tout)); for (; i < m_trail.size(); ++i) { auto* t = m_trail[i]; if (!t->m_active) @@ -147,7 +156,8 @@ void model_reconstruction_trail::append(generic_model_converter& mc, unsigned& i else if (t->is_hide()) mc.hide(t->m_decl); else if (t->is_def()) - mc.add(t->m_decl, t->m_def); + for (auto const& [f, def, dep] : t->m_defs) + mc.add(f, def); else { for (auto const& [v, def] : t->m_subst->sub()) mc.add(v, def); @@ -167,8 +177,10 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const { continue; else if (t->is_hide()) out << "hide " << t->m_decl->get_name() << "\n"; - else if (t->is_def()) - out << t->m_decl->get_name() << " <- " << mk_pp(t->m_def, m) << "\n"; + else if (t->is_def()) { + for (auto const& [f, def, dep] : t->m_defs) + out << f->get_name() << " <- " << mk_pp(def, m) << "\n"; + } else { for (auto const& [v, def] : t->m_subst->sub()) out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n"; diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index 4bc09e646..c1b045a43 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -39,34 +39,46 @@ class model_reconstruction_trail { scoped_ptr m_subst; vector m_removed; func_decl_ref m_decl; - expr_ref m_def; - expr_dependency_ref m_dep; + vector> m_defs; + bool m_active = true; entry(ast_manager& m, expr_substitution* s, vector const& rem) : - m_subst(s), m_removed(rem), m_decl(m), m_def(m), m_dep(m) {} + m_subst(s), m_removed(rem), m_decl(m) {} - entry(ast_manager& m, func_decl* h) : m_decl(h, m), m_def(m), m_dep(m) {} + entry(ast_manager& m, func_decl* h) : m_decl(h, m) {} entry(ast_manager& m, func_decl* f, expr* def, expr_dependency* dep, vector const& rem) : - m_removed(rem), m_decl(f, m), m_def(def, m), m_dep(dep, m) {} + m_removed(rem), + m_decl(m){ + m_defs.push_back({ func_decl_ref(f, m), expr_ref(def, m), expr_dependency_ref(dep, m) }); + } + + entry(ast_manager& m, vector> const& defs, vector const& rem) : + m_removed(rem), + m_decl(m), + m_defs(defs) { + } bool is_loose() const { return !m_removed.empty(); } bool intersects(ast_mark const& free_vars) const { if (is_hide()) return false; - if (is_def()) - return free_vars.is_marked(m_decl); - for (auto const& [k, v] : m_subst->sub()) - if (free_vars.is_marked(k)) + for (auto const& [f, def, dep] : m_defs) + if (free_vars.is_marked(f)) return true; + if (m_subst) { + for (auto const& [k, v] : m_subst->sub()) + if (free_vars.is_marked(k)) + return true; + } return false; } - bool is_hide() const { return m_decl && !m_def; } - bool is_def() const { return m_decl && m_def; } - bool is_subst() const { return !m_decl; } + bool is_hide() const { return m_decl && m_defs.empty(); } + bool is_def() const { return !m_defs.empty(); } + bool is_subst() const { return m_subst && !m_subst->empty(); } }; ast_manager& m; @@ -76,7 +88,8 @@ class model_reconstruction_trail { void add_vars(expr* e, ast_mark& free_vars) { for (expr* t : subterms::all(expr_ref(e, m))) - free_vars.mark(t, true); + if (is_app(t)) + free_vars.mark(to_app(t)->get_decl(), true); } void add_vars(dependent_expr const& d, ast_mark& free_vars) { @@ -86,7 +99,7 @@ class model_reconstruction_trail { bool intersects(ast_mark const& free_vars, dependent_expr const& d) { expr_ref term(d.fml(), m); auto iter = subterms::all(term); - return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); }); + return any_of(iter, [&](expr* t) { return is_app(t) && free_vars.is_marked(to_app(t)->get_decl()); }); } bool intersects(ast_mark const& free_vars, vector const& added) { @@ -126,6 +139,14 @@ public: m_trail_stack.push(push_back_vector(m_trail)); } + /** + * add definitions + */ + void push(vector> const& defs, vector const& removed) { + m_trail.push_back(alloc(entry, m, defs, removed)); + m_trail_stack.push(push_back_vector(m_trail)); + } + /** * register a new depedent expression, update the trail * by removing substitutions that are not equivalence preserving. diff --git a/src/ast/simplifiers/reduce_args_simplifier.cpp b/src/ast/simplifiers/reduce_args_simplifier.cpp new file mode 100644 index 000000000..4ebd49127 --- /dev/null +++ b/src/ast/simplifiers/reduce_args_simplifier.cpp @@ -0,0 +1,428 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + reduce_args_simplifier.cpp + +Abstract: + + Reduce the number of arguments in function applications. + +Author: + + Leonardo (leonardo) 2012-02-19 + +Notes: + +--*/ + +#include "util/map.h" +#include "ast/ast_smt2_pp.h" +#include "ast/ast_util.h" +#include "ast/has_free_vars.h" +#include "ast/rewriter/rewriter_def.h" +#include "ast/simplifiers/dependent_expr_state.h" + +/** + \brief Reduce the number of arguments in function applications. + + Example, suppose we have a function f with 2 arguments. + There are 1000 applications of this function, but the first argument is always "a", "b" or "c". + Thus, we replace the f(t1, t2) + with + f_a(t2) if t1 = a + f_b(t2) if t2 = b + f_c(t2) if t2 = c + + Since f_a, f_b, f_c are new symbols, satisfiability is preserved. + + This transformation is very similar in spirit to the Ackermman's reduction. + + This transformation should work in the following way: + + 1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)] + means that f is a declaration with 3 arguments where the first and third arguments are always values. + 2- Traverse the formula and populate the mapping. + For each function application f(t1, ..., tn) do + a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do + the logical-and with the tuple that is already in the mapping. If there is no such tuple + in the mapping, we just add a new entry. + + If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable. + + Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry, + but it is the same for the same declaration. + For example, suppose we have [f -> (true, false, true)] in decl2arg_map, and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula. + Then, decl2arg_map would contain + (f, 1, 2) -> f_1_2 + (f, 1, 3) -> f_1_3 + (f, 2, 3) -> f_2_3 + where f_1_2, f_1_3 and f_2_3 are new function symbols. + Using the new map, we can replace the occurrences of f. +*/ + +class reduce_args_simplifier : public dependent_expr_simplifier { + bv_util m_bv; + + static bool is_var_plus_offset(ast_manager& m, bv_util& bv, expr* e, expr*& base) { + expr *lhs, *rhs; + if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) + base = rhs; + else + base = e; + return !has_free_vars(base); + } + + static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { + base = nullptr; + return m.is_unique_value(e) || is_var_plus_offset(m, bv, e, base); + } + + static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e) { + expr* base; + return may_be_unique(m, bv, e, base); + } + + struct find_non_candidates_proc { + ast_manager & m; + bv_util & m_bv; + obj_hashtable & m_non_candidates; + + find_non_candidates_proc(ast_manager & m, bv_util & bv, obj_hashtable & non_candidates): + m(m), + m_bv(bv), + m_non_candidates(non_candidates) { + } + + void operator()(var * n) {} + + void operator()(quantifier *n) {} + + void operator()(app * n) { + if (!is_uninterp(n)) + return; + func_decl * d; + if (n->get_num_args() == 0) + return; // ignore constants + d = n->get_decl(); + if (m_non_candidates.contains(d)) + return; // it is already in the set. + for (expr* arg : *n) + if (may_be_unique(m, m_bv, arg)) + return; + m_non_candidates.insert(d); + } + }; + + /** + \brief Populate the table non_candidates with function declarations \c f + such that there is a function application (f t1 ... tn) where t1 ... tn are not values. + */ + void find_non_candidates(obj_hashtable & non_candidates) { + non_candidates.reset(); + find_non_candidates_proc proc(m, m_bv, non_candidates); + expr_fast_mark1 visited; + for (auto i : indices()) + quick_for_each_expr(proc, visited, m_fmls[i].fml()); + + TRACE("reduce_args", tout << "non_candidates:\n"; for (func_decl* d : non_candidates) tout << d->get_name() << "\n";); + } + + struct populate_decl2args_proc { + reduce_args_simplifier& m_owner; + ast_manager & m; + bv_util & m_bv; + obj_hashtable & m_non_candidates; + obj_map & m_decl2args; + obj_map > m_decl2base; // for args = base + offset + + populate_decl2args_proc(reduce_args_simplifier& o, ast_manager & m, bv_util & bv, obj_hashtable & nc, obj_map & d): + m_owner(o), m(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {} + + void operator()(var * n) {} + void operator()(quantifier * n) {} + void operator()(app * n) { + if (n->get_num_args() == 0) + return; // ignore constants + func_decl * d = n->get_decl(); + if (d->get_family_id() != null_family_id) + return; // ignore interpreted symbols + if (m_non_candidates.contains(d)) + return; // declaration is not a candidate + if (m_owner.m_fmls.frozen(d)) + return; + + unsigned j = n->get_num_args(); + obj_map::iterator it = m_decl2args.find_iterator(d); + expr* base; + if (it == m_decl2args.end()) { + m_decl2args.insert(d, bit_vector()); + svector& bases = m_decl2base.insert_if_not_there(d, svector()); + bases.resize(j); + it = m_decl2args.find_iterator(d); + SASSERT(it != m_decl2args.end()); + it->m_value.reserve(j); + while (j > 0) { + --j; + it->m_value.set(j, may_be_unique(m, m_bv, n->get_arg(j), base)); + bases[j] = base; + } + } else { + svector& bases = m_decl2base[d]; + SASSERT(j == it->m_value.size()); + while (j > 0) { + --j; + it->m_value.set(j, it->m_value.get(j) && may_be_unique(m, m_bv, n->get_arg(j), base) && bases[j] == base); + } + } + } + }; + + void populate_decl2args(obj_hashtable & non_candidates, + obj_map & decl2args) { + expr_fast_mark1 visited; + decl2args.reset(); + populate_decl2args_proc proc(*this, m, m_bv, non_candidates, decl2args); + for (auto i : indices()) + quick_for_each_expr(proc, visited, m_fmls[i].fml()); + + // Remove all cases where the simplification is not applicable. + ptr_buffer bad_decls; + for (auto const& [k, v] : decl2args) + if (all_of(v, [&](auto b) { return !b;})) + bad_decls.push_back(k); + + for (func_decl* a : bad_decls) + decl2args.erase(a); + + TRACE("reduce_args", tout << "decl2args:" << std::endl; + for (auto const& [k, v] : decl2args) { + tout << k->get_name() << ": "; + for (unsigned i = 0; i < v.size(); ++i) + tout << (v.get(i) ? "1" : "0"); + tout << std::endl; + }); + } + + struct arg2func_hash_proc { + bit_vector const & m_bv; + + arg2func_hash_proc(bit_vector const & bv):m_bv(bv) {} + unsigned operator()(app const * n) const { + // compute the hash-code using only the arguments where m_bv is true. + unsigned a = 0x9e3779b9; + unsigned num_args = n->get_num_args(); + for (unsigned i = 0; i < num_args; i++) { + if (!m_bv.get(i)) + continue; // ignore argument + a = hash_u_u(a, n->get_arg(i)->get_id()); + } + return a; + } + }; + + struct arg2func_eq_proc { + bit_vector const & m_bv; + + arg2func_eq_proc(bit_vector const & bv):m_bv(bv) {} + bool operator()(app const * n1, app const * n2) const { + // compare only the arguments where m_bv is true + SASSERT(n1->get_num_args() == n2->get_num_args()); + unsigned num_args = n1->get_num_args(); + for (unsigned i = 0; i < num_args; i++) { + if (!m_bv.get(i)) + continue; // ignore argument + if (n1->get_arg(i) != n2->get_arg(i)) + return false; + } + return true; + } + }; + + typedef map arg2func; + typedef obj_map decl2arg2func_map; + + struct reduce_args_ctx { + ast_manager & m; + decl2arg2func_map m_decl2arg2funcs; + + reduce_args_ctx(ast_manager & m): m(m) { + } + + ~reduce_args_ctx() { + for (auto const& [_, map] : m_decl2arg2funcs) { + for (auto const& [k, v] : *map) { + m.dec_ref(k); + m.dec_ref(v); + } + dealloc(map); + } + } + }; + + struct reduce_args_rw_cfg : public default_rewriter_cfg { + ast_manager & m; + reduce_args_simplifier& m_owner; + obj_map & m_decl2args; + decl2arg2func_map & m_decl2arg2funcs; + + reduce_args_rw_cfg(reduce_args_simplifier& owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): + m(owner.m), + m_owner(owner), + m_decl2args(decl2args), + m_decl2arg2funcs(decl2arg2funcs) { + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result_pr = nullptr; + if (f->get_arity() == 0) + return BR_FAILED; // ignore constants + if (f->get_family_id() != null_family_id) + return BR_FAILED; // ignore interpreted symbols + obj_map::iterator it = m_decl2args.find_iterator(f); + if (it == m_decl2args.end()) + return BR_FAILED; + + bit_vector & bv = it->m_value; + arg2func *& map = m_decl2arg2funcs.insert_if_not_there(f, 0); + if (!map) { + map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv)); + } + + app_ref tmp(m.mk_app(f, num, args), m); + func_decl *& new_f = map->insert_if_not_there(tmp, nullptr); + if (!new_f) { + // create fresh symbol + ptr_buffer domain; + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < arity; ++i) { + if (!bv.get(i)) + domain.push_back(f->get_domain(i)); + } + new_f = m.mk_fresh_func_decl(f->get_name(), symbol::null, domain.size(), domain.data(), f->get_range()); + m.inc_ref(tmp); + m.inc_ref(new_f); + } + + ptr_buffer new_args; + for (unsigned i = 0; i < num; i++) { + if (!bv.get(i)) + new_args.push_back(args[i]); + } + result = m.mk_app(new_f, new_args.size(), new_args.data()); + return BR_DONE; + } + }; + + struct reduce_args_rw : rewriter_tpl { + reduce_args_rw_cfg m_cfg; + public: + reduce_args_rw(reduce_args_simplifier & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): + rewriter_tpl(owner.m, false, m_cfg), + m_cfg(owner, decl2args, decl2arg2funcs) { + } + }; + + void mk_mc(obj_map & decl2args, decl2arg2func_map & decl2arg2funcs, vector const& removed) { + ptr_buffer new_args; + var_ref_vector new_vars(m); + ptr_buffer new_eqs; + generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args"); + for (auto const& [f, map] : decl2arg2funcs) + for (auto const& [t, new_def] : *map) + m_fmls.model_trail().hide(new_def); + + vector> defs; + for (auto const& [f, map] : decl2arg2funcs) { + expr * def = nullptr; + SASSERT(decl2args.contains(f)); + bit_vector & bv = decl2args.find(f); + new_vars.reset(); + new_args.reset(); + for (unsigned i = 0; i < f->get_arity(); i++) { + new_vars.push_back(m.mk_var(i, f->get_domain(i))); + if (!bv.get(i)) + new_args.push_back(new_vars.back()); + } + for (auto const& [t, new_def] : *map) { + SASSERT(new_def->get_arity() == new_args.size()); + app * new_t = m.mk_app(new_def, new_args); + if (def == nullptr) { + def = new_t; + } + else { + new_eqs.reset(); + for (unsigned i = 0; i < f->get_arity(); i++) + if (bv.get(i)) + new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i))); + SASSERT(new_eqs.size() > 0); + expr * cond = mk_and(m, new_eqs); + def = m.mk_ite(cond, new_t, def); + } + } + SASSERT(def); + expr_dependency* dep = nullptr; + defs.push_back({ func_decl_ref(f,m), expr_ref(def, m), expr_dependency_ref(dep, m) }); + } + m_fmls.model_trail().push(defs, removed); + } + + unsigned m_num_decls = 0; + +public: + reduce_args_simplifier(ast_manager& m, dependent_expr_state& st, params_ref const& p) : + dependent_expr_simplifier(m, st), + m_bv(m) + {} + + ~reduce_args_simplifier() override {} + + char const* name() const override { return "reduce-args"; } + + void collect_statistics(statistics& st) const override { + st.update("reduced-funcs", m_num_decls); + } + + void reset_statistics() override { + m_num_decls = 0; + } + + void reduce() override { + m_fmls.freeze_suffix(); + + obj_hashtable non_candidates; + obj_map decl2args; + find_non_candidates(non_candidates); + populate_decl2args(non_candidates, decl2args); + + if (decl2args.empty()) + return; + + m_num_decls += decl2args.size(); + + reduce_args_ctx ctx(m); + reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs); + vector removed; + // if not global scope then what? + // cannot just use in incremental mode. + for (auto i : indices()) { + auto [f, p, d] = m_fmls[i](); + if (p) + continue; + expr_ref new_f(m); + rw(f, new_f); + if (f != new_f) { + removed.push_back(m_fmls[i]); + m_fmls.update(i, dependent_expr(m, new_f, p, d)); + } + } + mk_mc(decl2args, ctx.m_decl2arg2funcs, removed); + } + +}; + +dependent_expr_simplifier* mk_reduce_args_simplifier(ast_manager & m, dependent_expr_state& st, params_ref const & p) { + return alloc(reduce_args_simplifier, m, st, p); +} + diff --git a/src/ast/simplifiers/reduce_args_simplifier.h b/src/ast/simplifiers/reduce_args_simplifier.h new file mode 100644 index 000000000..f6c4dd785 --- /dev/null +++ b/src/ast/simplifiers/reduce_args_simplifier.h @@ -0,0 +1,16 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + reduce_args_simplifier.h + +Abstract: + + Reduce the number of arguments in function applications. + +--*/ +#pragma once + +dependent_expr_simplifier* mk_reduce_args_simplifier(ast_manager & m, dependent_expr_state& st, params_ref const & p); + diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 477577345..9f0fae6bc 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -34,6 +34,7 @@ z3_add_component(lp nla_basics_lemmas.cpp nla_common.cpp nla_core.cpp + nla_divisions.cpp nla_grobner.cpp nla_intervals.cpp nla_monotone_lemmas.cpp diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index b072112f0..0ec7d42c0 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -30,6 +30,7 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_order(this), m_monotone(this), m_powers(*this), + m_divisions(*this), m_intervals(this, lim), m_monomial_bounds(this), m_horner(this), @@ -136,6 +137,11 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) { } m_emons.add(v, m_add_buffer); } + +void core::add_idivision(lpvar r, lpvar x, lpvar y) { + m_divisions.add_idivision(r, x, y); +} + void core::push() { TRACE("nla_solver_verbose", tout << "\n";); @@ -1519,6 +1525,9 @@ lbool core::check(vector& l_vec) { if (l_vec.empty() && !done()) m_basics.basic_lemma(false); + if (l_vec.empty() && !done()) + m_divisions.check(l_vec); + #if 0 if (l_vec.empty() && !done() && !run_horner) m_horner.horner_lemmas(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 1e66e4cd7..c595a0b0f 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -20,6 +20,7 @@ #include "math/lp/nla_monotone_lemmas.h" #include "math/lp/nla_grobner.h" #include "math/lp/nla_powers.h" +#include "math/lp/nla_divisions.h" #include "math/lp/emonics.h" #include "math/lp/nla_settings.h" #include "math/lp/nex.h" @@ -88,6 +89,7 @@ class core { order m_order; monotone m_monotone; powers m_powers; + divisions m_divisions; intervals m_intervals; monomial_bounds m_monomial_bounds; nla_settings m_nla_settings; @@ -199,8 +201,10 @@ public: void deregister_monic_from_tables(const monic & m, unsigned i); void add_monic(lpvar v, unsigned sz, lpvar const* vs); + void add_idivision(lpvar r, lpvar x, lpvar y); void push(); void pop(unsigned n); + trail_stack& trail() { return m_emons.get_trail_stack(); } rational mon_value_by_vars(unsigned i) const; rational product_value(const monic & m) const; diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp new file mode 100644 index 000000000..dd58fcd59 --- /dev/null +++ b/src/math/lp/nla_divisions.cpp @@ -0,0 +1,65 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + nla_divisions.cpp + +Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + +Description: + + Check divisions + +--*/ +#include "math/lp/nla_core.h" + +namespace nla { + + void divisions::add_idivision(lpvar r, lpvar x, lpvar y) { + m_idivisions.push_back({r, x, y}); + m_core.trail().push(push_back_vector(m_idivisions)); + } + + typedef lp::lar_term term; + + // y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2 + // y2 <= y1 < 0 & x1 >= x2 => x1/y1 <= x2/y2 + void divisions::check(vector& lemmas) { + core& c = m_core; + if (c.use_nra_model()) + return; + + for (auto const & [r, x, y] : m_idivisions) { + auto xval = c.val(x); + auto yval = c.val(y); + auto rval = c.val(r); + if (!c.var_is_int(x)) + continue; + if (yval == 0) + continue; + // idiv semantics + if (rval == div(xval, yval)) + continue; + for (auto const& [r2, x2, y2] : m_idivisions) { + if (r2 == r) + continue; + auto x2val = c.val(x2); + auto y2val = c.val(y2); + auto r2val = c.val(r2); + if (yval >= y2val && y2val > 0 && xval <= x2val && rval > r2val) { + new_lemma lemma(c, "y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2"); + lemma |= ineq(term(y, rational(-1), y2), llc::LT, rational::zero()); + lemma |= ineq(y2, llc::LE, rational::zero()); + lemma |= ineq(term(x, rational(-1), x2), llc::GT, rational::zero()); + lemma |= ineq(term(r, rational(-1), r2), llc::LE, rational::zero()); + return; + } + } + } + + } + +} diff --git a/src/math/lp/nla_divisions.h b/src/math/lp/nla_divisions.h new file mode 100644 index 000000000..8eb5c676b --- /dev/null +++ b/src/math/lp/nla_divisions.h @@ -0,0 +1,31 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + nla_divisions.h + +Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + +Description: + Check division constraints. + +--*/ + +#include "math/lp/nla_types.h" + +namespace nla { + + class core; + + class divisions { + core& m_core; + vector> m_idivisions; + public: + divisions(core& c):m_core(c) {} + void add_idivision(lpvar r, lpvar x, lpvar y); + void check(vector&); + }; +} diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index b5a030a92..eb7e5283d 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -22,6 +22,10 @@ namespace nla { void solver::add_monic(lpvar v, unsigned sz, lpvar const* vs) { m_core->add_monic(v, sz, vs); } + + void solver::add_idivision(lpvar r, lpvar x, lpvar y) { + m_core->add_idivision(r, x, y); + } bool solver::is_monic_var(lpvar v) const { return m_core->is_monic_var(v); diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index f372410d8..9379939db 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -25,6 +25,7 @@ namespace nla { core* m_core; public: void add_monic(lpvar v, unsigned sz, lpvar const* vs); + void add_idivision(lpvar r, lpvar x, lpvar y); solver(lp::lar_solver& s, reslimit& limit); ~solver(); nla_settings& settings(); diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 5a2eb5b5f..998779dc6 100644 --- a/src/math/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -68,8 +68,7 @@ class var_eqs { T* m_merge_handler; union_find m_uf; - lp::incremental_vector> - m_trail; + lp::incremental_vector> m_trail; vector> m_eqs; // signed_var.index() -> the edges adjacent to signed_var.index() trail_stack m_stack; diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index 8d99153da..4e5f8fd37 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -161,7 +161,6 @@ class sat_smt_solver : public solver { expr_ref_vector m_assumptions, m_core, m_ors, m_aux_fmls, m_internalized_fmls; atom2bool_var m_map; generic_model_converter_ref m_mc; - unsigned m_mc_size = 0; mutable model_converter_ref m_cached_mc; mutable ref m_sat_mc; std::string m_unknown = "no reason given"; @@ -180,8 +179,7 @@ public: m_trail(m_preprocess_state.m_trail), m_dep(m, m_trail), m_assumptions(m), m_core(m), m_ors(m), m_aux_fmls(m), m_internalized_fmls(m), - m_map(m), - m_mc(alloc(generic_model_converter, m, "sat-smt-solver")) { + m_map(m) { updt_params(p); init_preprocess(); m_solver.set_incremental(true); @@ -211,7 +209,6 @@ public: for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f)); if (m_mc) result->m_mc = dynamic_cast(m_mc->translate(tr)); result->m_dep.copy(tr, m_dep); - result->m_mc_size = m_mc_size; if (m_sat_mc) result->m_sat_mc = dynamic_cast(m_sat_mc->translate(tr)); result->m_internalized_converted = m_internalized_converted; return result; @@ -291,7 +288,6 @@ public: m_preprocess.push(); m_trail.push(restore_vector(m_assumptions)); m_trail.push(restore_vector(m_fmls)); - m_trail.push(value_trail(m_mc_size)); } void pop(unsigned n) override { @@ -302,7 +298,6 @@ public: m_map.pop(n); m_goal2sat.user_pop(n); m_solver.user_pop(n); - m_mc->shrink(m_mc_size); } void set_phase(expr* e) override { @@ -549,6 +544,7 @@ public: model_converter_ref get_model_converter() const override { const_cast(this)->convert_internalized(); + verbose_stream() << "get model converter " << (m_cached_mc.get() != nullptr) << "\n"; if (m_cached_mc) return m_cached_mc; if (is_internalized() && m_internalized_converted) { @@ -660,6 +656,7 @@ private: if (!m.inc()) return l_undef; m_preprocess_state.advance_qhead(); + m_mc = alloc(generic_model_converter, m, "sat-model-converter"); m_preprocess_state.append(*m_mc); m_solver.pop_to_base_level(); m_aux_fmls.reset(); @@ -754,42 +751,43 @@ private: if (m_sat_mc) (*m_sat_mc)(mdl); m_goal2sat.update_model(mdl); - TRACE("sat", m_mc->display(tout);); - (*m_mc)(mdl); + TRACE("sat", model_smt2_pp(tout, m, *mdl, 0);); - if (!gparams::get_ref().get_bool("model_validate", false)) - return; - IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";); - model_evaluator eval(*mdl); - eval.set_model_completion(true); - bool all_true = true; - for (dependent_expr const& d : m_fmls) { - if (has_quantifiers(d.fml())) - continue; - expr_ref tmp(m); - eval(d.fml(), tmp); - if (m.limit().is_canceled()) - return; - CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(d.fml(), m) << " to " << tmp << "\n"; - model_smt2_pp(tout, m, *(mdl.get()), 0);); - if (m.is_false(tmp)) { - IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(d.fml(), m) << "\n"); - IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n"); - all_true = false; + if (gparams::get_ref().get_bool("model_validate", false)) { + IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";); + model_evaluator eval(*mdl); + eval.set_model_completion(true); + bool all_true = true; + for (dependent_expr const& d : m_fmls) { + if (has_quantifiers(d.fml())) + continue; + expr_ref tmp(m); + eval(d.fml(), tmp); + if (m.limit().is_canceled()) + return; + CTRACE("sat", !m.is_true(tmp), + tout << "Evaluation failed: " << mk_pp(d.fml(), m) << " to " << tmp << "\n"; + model_smt2_pp(tout, m, *(mdl.get()), 0);); + if (m.is_false(tmp)) { + IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(d.fml(), m) << "\n"); + IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n"); + all_true = false; + } + } + if (!all_true) { + IF_VERBOSE(0, verbose_stream() << m_params << "\n"); + IF_VERBOSE(0, if (m_mc) m_mc->display(verbose_stream() << "mc0\n")); + IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n"); + exit(0); + } + else { + IF_VERBOSE(1, verbose_stream() << "solution verified\n"); } } - if (!all_true) { - IF_VERBOSE(0, verbose_stream() << m_params << "\n"); - IF_VERBOSE(0, if (m_mc) m_mc->display(verbose_stream() << "mc0\n")); - IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n"); - exit(0); - } - else { - IF_VERBOSE(1, verbose_stream() << "solution verified\n"); - } + TRACE("sat", m_mc->display(tout);); + (*m_mc)(mdl); } }; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 29f34655a..880026610 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -435,6 +435,13 @@ class theory_lra::imp { app_ref mod(a.mk_mod(n1, n2), m); ctx().internalize(mod, false); if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod); +#if 0 + // shortcut to create non-linear division axioms. + theory_var r = mk_var(n); + theory_var x = mk_var(n1); + theory_var y = mk_var(n2); + m_nla->add_idivision(get_lpvar(n), get_lpvar(n1), get_lpvar(n2)); +#endif } else if (a.is_mod(n, n1, n2)) { if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index d31fb8387..0a57e6b70 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "tactic/tactical.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_util.h" #include "ast/array_decl_plugin.h" #include "ast/has_free_vars.h" #include "util/map.h" @@ -397,7 +398,7 @@ struct reduce_args_tactic::imp { ptr_buffer new_args; var_ref_vector new_vars(m); ptr_buffer new_eqs; - generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args"); + generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args"); for (auto const& [f, map] : decl2arg2funcs) for (auto const& [t, new_def] : *map) f_mc->hide(new_def); @@ -414,7 +415,6 @@ struct reduce_args_tactic::imp { new_args.push_back(new_vars.back()); } for (auto const& [t, new_def] : *map) { - // f_mc->hide(new_def); SASSERT(new_def->get_arity() == new_args.size()); app * new_t = m.mk_app(new_def, new_args); if (def == nullptr) { @@ -427,11 +427,7 @@ struct reduce_args_tactic::imp { new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i))); } SASSERT(new_eqs.size() > 0); - expr * cond; - if (new_eqs.size() == 1) - cond = new_eqs[0]; - else - cond = m.mk_and(new_eqs); + expr * cond = mk_and(m, new_eqs); def = m.mk_ite(cond, new_t, def); } } diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h index 749aadd9c..fa90837bf 100644 --- a/src/tactic/core/reduce_args_tactic.h +++ b/src/tactic/core/reduce_args_tactic.h @@ -63,6 +63,8 @@ It creates a fresh function for each of the different values at position `i`. #pragma once #include "util/params.h" +#include "ast/simplifiers/reduce_args_simplifier.h" +#include "tactic/dependent_expr_state_tactic.h" class ast_manager; class tactic; @@ -71,3 +73,11 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p = params_re ADD_TACTIC("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic(m, p)") */ +inline tactic* mk_reduce_args_tactic2(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return mk_reduce_args_simplifier(m, s, p); }); +} +/* + ADD_TACTIC("reduce-args2", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic2(m, p)") +*/ + diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index 931fc7c26..347e147fb 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -23,13 +23,14 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { public: using factoryTy = dependent_expr_simplifier(*(*)(ast_manager& m, params_ref const& p, dependent_expr_state& s)); private: - ast_manager& m; + ast_manager& m; params_ref m_params; trail_stack m_trail; goal_ref m_goal; dependent_expr m_dep; statistics m_st; factoryTy m_factory; + expr_ref_vector m_frozen; scoped_ptr m_simp; scoped_ptr m_model_trail; @@ -37,6 +38,9 @@ private: if (!m_simp) { m_simp = m_factory(m, m_params, *this); m_st.reset(); + push(); + for (expr* e : m_frozen) + freeze(e); } if (!m_model_trail) m_model_trail = alloc(model_reconstruction_trail, m, m_trail); @@ -44,14 +48,20 @@ private: public: - dependent_expr_state_tactic(ast_manager& m, params_ref const& p, factoryTy f): + dependent_expr_state_tactic(ast_manager& m, params_ref const& p, factoryTy f) : dependent_expr_state(m), m(m), m_params(p), m_dep(m, m.mk_true(), nullptr, nullptr), - m_factory(f) + m_factory(f), + m_frozen(m) {} + ~dependent_expr_state_tactic() override { + if (m_simp) + pop(1); + } + /** * size(), [](), update() and inconsisent() implement the abstract interface of dependent_expr_state */ @@ -61,14 +71,14 @@ public: m_dep = dependent_expr(m, m_goal->form(i), m_goal->pr(i), m_goal->dep(i)); return m_dep; } - + void update(unsigned i, dependent_expr const& j) override { if (inconsistent()) return; auto [f, p, d] = j(); m_goal->update(i, f, p, d); } - + void add(dependent_expr const& j) override { if (inconsistent()) return; @@ -83,10 +93,10 @@ public: model_reconstruction_trail& model_trail() override { return *m_model_trail; } - - char const* name() const override { return m_simp?m_simp->name():"null"; } - void updt_params(params_ref const & p) override { + char const* name() const override { return m_simp ? m_simp->name() : "null"; } + + void updt_params(params_ref const& p) override { m_params.append(p); init(); m_simp->updt_params(m_params); @@ -97,12 +107,12 @@ public: m_simp->collect_param_descrs(r); } - tactic * translate(ast_manager & m) override { + tactic* translate(ast_manager& m) override { return alloc(dependent_expr_state_tactic, m, m_params, m_factory); } - void operator()(goal_ref const & in, - goal_ref_buffer & result) override { + void operator()(goal_ref const& in, + goal_ref_buffer& result) override { init(); statistics_report sreport(*this); tactic_report report(name(), *in); @@ -124,25 +134,39 @@ public: } void cleanup() override { - if (m_simp) + if (m_simp) { m_simp->collect_statistics(m_st); + pop(1); + } m_simp = nullptr; m_model_trail = nullptr; m_goal = nullptr; m_dep = dependent_expr(m, m.mk_true(), nullptr, nullptr); } - void collect_statistics(statistics & st) const override { - if (m_simp) + void collect_statistics(statistics& st) const override { + if (m_simp) m_simp->collect_statistics(st); else st.copy(m_st); } - + void reset_statistics() override { if (m_simp) m_simp->reset_statistics(); m_st.reset(); } -}; + void user_propagate_register_expr(expr* e) override { + freeze(e); + m_frozen.push_back(e); + } + + void user_propagate_clear() override { + if (m_simp) { + pop(1); + push(); + } + m_frozen.reset(); + } +}; diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 31cb00281..cb29bdd9c 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -211,6 +211,22 @@ public: bool contains(const bit_vector & other) const; + class iterator { + bit_vector const& b; + unsigned m_curr; + public: + iterator(bit_vector const& b, unsigned i) : b(b), m_curr(i) {} + bool operator*(unsigned i) const { return b.get(m_curr); } + bool operator*() const { return b.get(m_curr); } + iterator& operator++() { ++m_curr; return *this; } + iterator operator++(int) { iterator tmp = *this; ++* this; return tmp; } + bool operator==(iterator const& it) const { return m_curr == it.m_curr; } + bool operator!=(iterator const& it) const { return m_curr != it.m_curr; } + }; + + iterator begin() const { return iterator(*this, 0); } + iterator end() const { return iterator(*this, size()); } + }; inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {