diff --git a/scripts/mk_project.py b/scripts/mk_project.py index ce1014ebe..9ceec29eb 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -66,8 +66,9 @@ def init_project_def(): add_lib('clp', ['muz', 'transforms'], 'muz/clp') add_lib('tab', ['muz', 'transforms'], 'muz/tab') add_lib('bmc', ['muz', 'transforms'], 'muz/bmc') + add_lib('ddnf', ['muz', 'transforms'], 'muz/ddnf') add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality') - add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp') + add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 859d4419f..774db6c6a 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -712,6 +712,8 @@ namespace datalog { check_existential_tail(r); check_positive_predicates(r); break; + case DDNF_ENGINE: + break; case LAST_ENGINE: default: UNREACHABLE(); @@ -932,6 +934,9 @@ namespace datalog { else if (e == symbol("duality")) { m_engine_type = DUALITY_ENGINE; } + else if (e == symbol("ddnf")) { + m_engine_type = DDNF_ENGINE; + } if (m_engine_type == LAST_ENGINE) { expr_fast_mark1 mark; @@ -980,6 +985,7 @@ namespace datalog { case QBMC_ENGINE: case TAB_ENGINE: case CLP_ENGINE: + case DDNF_ENGINE: flush_add_rules(); break; case DUALITY_ENGINE: diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index eaeebe979..21a07fcb0 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -30,8 +30,9 @@ namespace datalog { QBMC_ENGINE, TAB_ENGINE, CLP_ENGINE, - LAST_ENGINE, - DUALITY_ENGINE + DUALITY_ENGINE, + DDNF_ENGINE, + LAST_ENGINE }; class engine_base { diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp new file mode 100644 index 000000000..92e01bd2f --- /dev/null +++ b/src/muz/ddnf/ddnf.cpp @@ -0,0 +1,620 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + ddnf.cpp + +Abstract: + + DDNF based engine. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-08-21 + +Revision History: + + - inherits from Nuno Lopes Hassel utilities + and Garvit Juniwal's DDNF engine. + +--*/ + +#include "ddnf.h" +#include "trail.h" +#include "dl_rule_set.h" +#include "dl_context.h" +#include "dl_mk_rule_inliner.h" +#include "smt_kernel.h" +#include "qe_lite.h" +#include "bool_rewriter.h" +#include "th_rewriter.h" +#include "datatype_decl_plugin.h" +#include "for_each_expr.h" +#include "matcher.h" +#include "scoped_proof.h" +#include "fixedpoint_params.hpp" + + +namespace datalog { + +#define BIT_0 ((0<<1)|1) +#define BIT_1 ((1<<1)|0) +#define BIT_x ((1<<1)|1) +#define BIT_z 0 + + class tbv : private bit_vector { + public: + tbv(): bit_vector() {} + tbv(unsigned n): bit_vector(2*n) {} + tbv(tbv const& other): bit_vector(other) {} + tbv(unsigned n, unsigned val): bit_vector() { + SASSERT(val <= 3); + resize(n, val); + } + tbv(uint64 val, unsigned n) : bit_vector(2*n) { + for (unsigned bit = n; bit > 0;) { + --bit; + if (val & (1ULL << bit)) { + set(bit, BIT_1); + } else { + set(bit, BIT_0); + } + } + } + + tbv(rational const& v, unsigned n) : bit_vector(2*n) { + if (v.is_uint64() && n <= 64) { + tbv tmp(v.get_uint64(), n); + *this = tmp; + return; + } + + for (unsigned bit = n; bit > 0; ) { + --bit; + if (bitwise_and(v, rational::power_of_two(bit)).is_zero()) { + set(bit, BIT_0); + } else { + set(bit, BIT_1); + } + } + } + + tbv& operator=(tbv const& other) { + bit_vector::operator=(other); + return *this; + } + + bool operator!=(tbv const& other) const { + return bit_vector::operator!=(other); + } + + bool operator==(tbv const& other) const { + return bit_vector::operator==(other); + } + + void resize(unsigned n, unsigned val) { + while (size() < n) { + bit_vector::push_back((val & 2) != 0); + bit_vector::push_back((val & 1) != 0); + } + } + + bool empty() const { return false; } // TBD + + bool is_subset(tbv const& other) const { + SASSERT(size() == other.size()); + return other.contains(*this); + } + + bool is_superset(tbv const& other) const { + SASSERT(size() == other.size()); + return contains(other); + } + + unsigned size() const { return bit_vector::size()/2; } + + void display(std::ostream& out) const { + for (unsigned i = 0; i < size(); ++i) { + switch (get(i)) { + case BIT_0: + out << '0'; + break; + case BIT_1: + out << '1'; + break; + case BIT_x: + out << 'x'; + break; + case BIT_z: + out << 'z'; + break; + default: + UNREACHABLE(); + } + } + } + + private: + void set(unsigned index, unsigned value) { + SASSERT(value <= 3); + bit_vector::set(2*index, (value & 2) != 0); + bit_vector::set(2*index+1, (value & 1) != 0); + } + + unsigned get(unsigned index) const { + index *= 2; + return (bit_vector::get(index) << 1) | (unsigned)bit_vector::get(index+1); + } + + }; + + class dot { + tbv m_pos; + vector m_negs; + public: + dot(tbv const& pos, vector const& negs): + m_pos(pos), m_negs(negs) {} + + bool operator==(dot const& other) const { + if (m_pos != other.m_pos) return false; + if (m_negs.size() != other.m_negs.size()) return false; + for (unsigned i = 0; i < m_negs.size(); ++i) { + if (m_negs[i] != other.m_negs[i]) return false; + } + return true; + } + void display(std::ostream& out) { + out << "<"; + m_pos.display(out); + out << "\\"; + for (unsigned i = 0; i < m_negs.size(); ++i) { + m_negs[i].display(out); + if (i + 1 < m_negs.size()) out << " u "; + } + out << ">"; + } + }; + + class ddnf_mgr; + class ddnf_node; + typedef ref_vector ddnf_node_vector; + + class ddnf_node { + tbv m_tbv; + ddnf_node_vector m_children; + vector m_pos; + vector m_neg; + unsigned m_refs; + + public: + ddnf_node(ddnf_mgr& m, tbv const& tbv): + m_tbv(tbv), + m_children(m), + m_refs(0) { + } + + unsigned inc_ref() { + return ++m_refs; + } + + unsigned dec_ref() { + SASSERT(m_refs > 0); + return --m_refs; + } + + unsigned num_children() const { return m_children.size(); } + + ddnf_node* operator[](unsigned index) { return m_children[index].get(); } + + tbv const& get_tbv() const { return m_tbv; } + + void add_child(ddnf_node* n); + + void remove_child(ddnf_node* n); + + bool contains_child(ddnf_node* n) const; + + }; + + class ddnf_mgr { + unsigned m_num_bits; + ddnf_node* m_root; + ddnf_node_vector m_nodes; + vector m_dots; + public: + ddnf_mgr(unsigned n): m_num_bits(n), m_nodes(*this) { + m_root = alloc(ddnf_node, *this, tbv(n, BIT_x)); + m_nodes.push_back(m_root); + } + + void inc_ref(ddnf_node* n) { + n->inc_ref(); + } + + void dec_ref(ddnf_node* n) { + unsigned count = n->dec_ref(); + NOT_IMPLEMENTED_YET(); + } + + private: + void insert_new(ddnf_node& root, ddnf_node* new_n, + ptr_vector& new_intersections) { + SASSERT(root.get_tbv().is_superset(new_n->get_tbv())); +// if (root == *new_n) return; + bool inserted = false; + for (unsigned i = 0; i < root.num_children(); ++i) { + ddnf_node& child = *(root[i]); + if (child.get_tbv().is_superset(new_n->get_tbv())) { + inserted = true; + insert_new(child, new_n, new_intersections); + } + } + if (inserted) return; + ddnf_node_vector subset_children(*this); + for (unsigned i = 0; i < root.num_children(); ++i) { + ddnf_node& child = *(root[i]); + // cannot be superset + // checking for subset + if (child.get_tbv().is_subset(new_n->get_tbv())) { + subset_children.push_back(&child); + } + // this means there is a non-full intersection + else { + tbv intr; + // TBD intersect(child.get_tbv(), new_n->get_tbv(), intr); + if (!intr.empty()) { + // TBD new_intersections.push_back(intr); + } + } + } + for (unsigned i = 0; i < subset_children.size(); ++i) { + root.remove_child(subset_children[i].get()); + new_n->add_child(subset_children[i].get()); + } + root.add_child(new_n); + } + + +#if 0 + + DDNFNode InsertTBV(TernaryBitVector aTbv) + { + foreach (DDNFNode node in allNodes) + { + if (node.tbv.IsEqualset(aTbv)) + { + return node; + } + } + DDNFNode newNode = new DDNFNode(aTbv); + this.allNodes.Add(newNode); + List newIntersections = new List(); + InsertNewNode(this.root, newNode, newIntersections); + + // add the TBVs corresponding to new intersections + foreach (TernaryBitVector newIntr in newIntersections) + { + // this assert guarantees termination since you can only + // insert smaller tbvs recursively + Debug.Assert(!newIntr.IsSupset(aTbv)); + + InsertTBV(newIntr); + } + + return newNode; + } + + public void InsertDot(DOT aDot) + { + this.allDots.Add(aDot); + DDNFNode posNode = InsertTBV(aDot.pos); + List negNodes = new List(); + foreach (TernaryBitVector neg in aDot.negs) + { + negNodes.Add(InsertTBV(neg)); + } + + posNode.posDots.Add(aDot); + foreach (DDNFNode negNode in negNodes) + { + negNode.negDots.Add(aDot); + } + } + + // remove all negNodes for each dot in dot2Nodes + void RemoveNegNodesForAllDots(DDNFNode aNode, HashSet activeDots, + ref Dictionary> dot2Nodes) + { + foreach (DOT negDot in aNode.negDots) + { + activeDots.Add(negDot); + } + + foreach (DOT activeDot in activeDots) + { + dot2Nodes[activeDot].Remove(aNode); + } + + foreach (DDNFNode child in aNode.children) + + { + RemoveNegNodesForAllDots(child, new HashSet(activeDots), ref dot2Nodes); + } + } + + // add all posNodes for each dot in dot2Nodes + void AddPosNodesForAllDots(DDNFNode aNode, HashSet activeDots, + ref Dictionary> dot2Nodes) + { + foreach (DOT posDot in aNode.posDots) + { + activeDots.Add(posDot); + } + + foreach (DOT activeDot in activeDots) + { + dot2Nodes[activeDot].Add(aNode); + } + + foreach (DDNFNode child in aNode.children) + { + AddPosNodesForAllDots(child, new HashSet(activeDots), ref dot2Nodes); + } + } + + public Dictionary> NodesForAllDots() + { + Dictionary> dot2Nodes = + new Dictionary>(); + + foreach (DOT dot in allDots) + { + dot2Nodes[dot] = new HashSet(); + } + AddPosNodesForAllDots(this.root, new HashSet(), ref dot2Nodes); + RemoveNegNodesForAllDots(this.root, new HashSet(), ref dot2Nodes); + + return dot2Nodes; + + } + public string PrintNodes() + { + StringBuilder retVal = new StringBuilder(); + retVal.Append("").ToString(); + } + } + + +} + +#endif + + }; + +void ddnf_node::add_child(ddnf_node* n) { + SASSERT(!m_tbv.is_subset(n->m_tbv)); + m_children.push_back(n); +} + +void ddnf_node::remove_child(ddnf_node* n) { + m_children.erase(n); +} + +bool ddnf_node::contains_child(ddnf_node* n) const { + return m_children.contains(n); +} + + + + class ddnf::imp { + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + context& m_ctx; + ast_manager& m; + rule_manager& rm; + volatile bool m_cancel; + ptr_vector m_todo; + ast_mark m_visited1, m_visited2; + stats m_stats; + + public: + imp(context& ctx): + m_ctx(ctx), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + m_cancel(false) + { + } + + ~imp() {} + + lbool query(expr* query) { + m_ctx.ensure_opened(); + if (!can_handle_rules()) { + return l_undef; + } + IF_VERBOSE(0, verbose_stream() << "rules are OK\n";); + return run(); + } + + void cancel() { + m_cancel = true; + } + + void cleanup() { + m_cancel = false; + } + + void reset_statistics() { + m_stats.reset(); + } + + void collect_statistics(statistics& st) const { + } + + void display_certificate(std::ostream& out) const { + expr_ref ans = get_answer(); + out << mk_pp(ans, m) << "\n"; + } + + expr_ref get_answer() const { + UNREACHABLE(); + return expr_ref(m.mk_true(), m); + } + private: + + proof_ref get_proof() const { + scoped_proof sp(m); + proof_ref pr(m); + return pr; + } + + lbool run() { + return l_undef; + } + + bool can_handle_rules() { + m_visited1.reset(); + m_todo.reset(); + rule_set const& rules = m_ctx.get_rules(); + datalog::rule_set::iterator it = rules.begin(); + datalog::rule_set::iterator end = rules.end(); + for (; it != end; ++it) { + if (!can_handle_rule(**it)) { + return false; + } + } + return true; + } + + bool can_handle_rule(rule const& r) { + // all predicates are monadic. + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned sz = r.get_tail_size(); + for (unsigned i = utsz; i < sz; ++i) { + m_todo.push_back(r.get_tail(i)); + } + if (check_monadic()) { + return true; + } + else { + r.display(m_ctx, std::cout); + return false; + } + } + + bool check_monadic() { + expr* e1, *e2; + while (!m_todo.empty()) { + expr* e = m_todo.back(); + m_todo.pop_back(); + if (m_visited1.is_marked(e)) { + continue; + } + m_visited1.mark(e, true); + if (is_var(e)) { + continue; + } + if (is_quantifier(e)) { + return false; + } + if (m.is_and(e) || + m.is_or(e) || + m.is_iff(e) || + m.is_not(e) || + m.is_implies(e)) { + m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + continue; + } + if (m.is_eq(e, e1, e2)) { + if (is_var(e1) && is_ground(e2)) { + continue; + } + if (is_var(e2) && is_ground(e1)) { + continue; + } + if (is_var(e1) && is_var(e2)) { + continue; + } + } + if (is_ground(e)) { + continue; + } + if (is_unary(e)) { + continue; + } + IF_VERBOSE(0, verbose_stream() << "Could not handle: " << mk_pp(e, m) << "\n";); + return false; + } + return true; + } + + bool is_unary(expr* e) { + var* v = 0; + m_visited2.reset(); + unsigned sz = m_todo.size(); + m_todo.push_back(e); + while (m_todo.size() > sz) { + expr* e = m_todo.back(); + m_todo.pop_back(); + if (m_visited2.is_marked(e)) { + continue; + } + m_visited2.mark(e, true); + if (is_var(e)) { + if (v && v != e) { + return false; + } + v = to_var(e); + } + else if (is_app(e)) { + m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + return false; + } + } + return true; + } + + }; + + ddnf::ddnf(context& ctx): + datalog::engine_base(ctx.get_manager(),"tabulation"), + m_imp(alloc(imp, ctx)) { + } + ddnf::~ddnf() { + dealloc(m_imp); + } + lbool ddnf::query(expr* query) { + return m_imp->query(query); + } + void ddnf::cancel() { + m_imp->cancel(); + } + void ddnf::cleanup() { + m_imp->cleanup(); + } + void ddnf::reset_statistics() { + m_imp->reset_statistics(); + } + void ddnf::collect_statistics(statistics& st) const { + m_imp->collect_statistics(st); + } + void ddnf::display_certificate(std::ostream& out) const { + m_imp->display_certificate(out); + } + expr_ref ddnf::get_answer() { + return m_imp->get_answer(); + } + +}; diff --git a/src/muz/ddnf/ddnf.h b/src/muz/ddnf/ddnf.h new file mode 100644 index 000000000..8121dc090 --- /dev/null +++ b/src/muz/ddnf/ddnf.h @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + ddnf.h + +Abstract: + + DDNF based engine. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-08-21 + +Revision History: + +--*/ +#ifndef _DDNF__H_ +#define _DDNF__H_ + +#include "ast.h" +#include "lbool.h" +#include "statistics.h" +#include "dl_engine_base.h" + +namespace datalog { + class context; + + class ddnf : public engine_base { + class imp; + imp* m_imp; + public: + ddnf(context& ctx); + ~ddnf(); + virtual lbool query(expr* query); + virtual void cancel(); + virtual void cleanup(); + virtual void reset_statistics(); + virtual void collect_statistics(statistics& st) const; + virtual void display_certificate(std::ostream& out) const; + virtual expr_ref get_answer(); + }; +}; + +#endif diff --git a/src/muz/fp/dl_register_engine.cpp b/src/muz/fp/dl_register_engine.cpp index 57413b7cb..6e1ba40ce 100644 --- a/src/muz/fp/dl_register_engine.cpp +++ b/src/muz/fp/dl_register_engine.cpp @@ -22,6 +22,7 @@ Revision History: #include "tab_context.h" #include "rel_context.h" #include "pdr_dl_interface.h" +#include "ddnf.h" #include "duality_dl_interface.h" namespace datalog { @@ -43,6 +44,8 @@ namespace datalog { return alloc(clp, *m_ctx); case DUALITY_ENGINE: return alloc(Duality::dl_interface, *m_ctx); + case DDNF_ENGINE: + return alloc(ddnf, *m_ctx); case LAST_ENGINE: UNREACHABLE(); return 0; diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 231c72578..be3470ad8 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -82,6 +82,7 @@ private: expr_ref_vector m_trail; strategy_t m_st; rational m_max_upper; + bool m_hill_climb; public: maxres(context& c, @@ -92,7 +93,8 @@ public: m_mus(m_s, m), m_mss(m_s, m), m_trail(m), - m_st(st) + m_st(st), + m_hill_climb(true) { } @@ -299,7 +301,21 @@ public: TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()); display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr());); - is_sat = s().check_sat(asms.size(), asms.c_ptr()); + + if (m_hill_climb) { + /** + Give preference to cores that have large minmal values. + */ + sort_assumptions(asms); + unsigned index = 0; + while (index < asms.size() && is_sat != l_false) { + index = next_index(asms, index); + is_sat = s().check_sat(index, asms.c_ptr()); + } + } + else { + is_sat = s().check_sat(asms.size(), asms.c_ptr()); + } } TRACE("opt", tout << "num cores: " << cores.size() << "\n"; @@ -315,6 +331,36 @@ public: } + struct compare_asm { + maxres& mr; + compare_asm(maxres& mr):mr(mr) {} + bool operator()(expr* a, expr* b) const { + return mr.get_weight(a) > mr.get_weight(b); + } + }; + + void sort_assumptions(expr_ref_vector& _asms) { + compare_asm comp(*this); + ptr_vector asms(_asms.size(), _asms.c_ptr()); + expr_ref_vector trail(_asms); + std::sort(asms.begin(), asms.end(), comp); + _asms.reset(); + _asms.append(asms.size(), asms.c_ptr()); + DEBUG_CODE( + for (unsigned i = 0; i + 1 < asms.size(); ++i) { + SASSERT(get_weight(asms[i]) >= get_weight(asms[i+1])); + }); + } + + unsigned next_index(expr_ref_vector const& asms, unsigned index) { + if (index < asms.size()) { + rational w = get_weight(asms[index]); + ++index; + for (; index < asms.size() && w == get_weight(asms[index]); ++index); + } + return index; + } + lbool process_sat(ptr_vector& corr_set) { expr_ref fml(m), tmp(m); TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr());); @@ -379,7 +425,7 @@ public: return l_true; } - rational get_weight(expr* e) { + rational get_weight(expr* e) const { return m_asm2weight.find(e); } diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index e582a9f5c..74f17f8ea 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -71,7 +71,7 @@ namespace sat { literal lit = core.back(); core.pop_back(); unsigned sz = mus.size(); - // mus.push_back(~lit); // TBD: measure + mus.push_back(~lit); // TBD: measure mus.append(core); lbool is_sat = s.check(mus.size(), mus.c_ptr()); TRACE("sat", tout << "mus: " << mus << "\n";); @@ -102,6 +102,7 @@ namespace sat { core.push_back(lit); } } + IF_VERBOSE(2, verbose_stream() << "reduced core: " << core.size() << "\n";); break; } } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1c0cc145a..d21c49b0c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -902,6 +902,11 @@ namespace sat { m_assumption_set.reset(); push(); + propagate(false); + if (inconsistent()) { + return; + } + TRACE("sat", for (unsigned i = 0; i < num_lits; ++i) tout << lits[i] << " "; @@ -916,15 +921,17 @@ namespace sat { m_assumption_set.insert(_l_); \ m_assumptions.push_back(_l_); \ assign(_l_, justification()); \ +// propagate(false); \ + + for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { + literal nlit = ~m_user_scope_literals[i]; + _INSERT_LIT(nlit); + } for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; _INSERT_LIT(lit); } - for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { - literal nlit = ~m_user_scope_literals[i]; - _INSERT_LIT(nlit); - } } void solver::reinit_assumptions() { diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index 6885b93e8..207d22d6a 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -208,6 +208,22 @@ void bit_vector::display(std::ostream & out) const { #endif } +bool bit_vector::contains(bit_vector const& other) const { + unsigned n = num_words(); + if (n == 0) + return true; + + for (unsigned i = 0; i < n - 1; ++i) { + if ((m_data[i] & other.m_data[i]) != other.m_data[i]) + return false; + } + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1U << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + unsigned other_data = other.m_data[n-1] & mask; + return (m_data[n-1] & other_data) == other_data; +} + void fr_bit_vector::reset() { unsigned sz = size(); unsigned_vector::const_iterator it = m_one_idxs.begin(); diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 0ccdeae9e..c703f524b 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -200,6 +200,9 @@ public: bit_vector & operator&=(bit_vector const & source); void display(std::ostream & out) const; + + bool contains(const bit_vector & other) const; + }; inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {