diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index edc8ad2a8..d88b28e74 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -239,9 +239,53 @@ namespace sat { // TBD } - void bdd_manager::sift_up(unsigned level) { + void bdd_manager::sift_up(unsigned lvl) { // exchange level and level + 1. - +#if 0 + m_relevel.reset(); // nodes to be re-leveled. + + for (unsigned n : m_level2nodes[lvl + 1]) { + BDD l = lo(n); + BDD h = hi(n); + if (l == 0 && h == 0) continue; + BDD a, b, c, d; + if (level(l) == lvl) { + a = lo(l); + b = hi(l); + } + else { + a = b = l; + } + if (level(h) == lvl) { + c = lo(h); + d = hi(h); + } + else { + c = d = h; + } + + push(make_node(lvl, a, c)); + push(make_node(lvl, b, d)); + m_node_table.remove(m_nodes[n]); + m_nodes[n].m_lo = read(2); + m_nodes[n].m_hi = read(1); + m_relevel.push_back(l); + m_relevel.push_back(r); + // TBD: read(2); read(1); should be inserted into m_level2nodes[lvl]; + pop(2); + m_node_table.insert(m_nodes[n]); + } + unsigned v = m_level2var[lvl]; + unsigned w = m_level2var[lvl+1]; + std::swap(m_level2var[lvl], m_level2var[lvl+1]); + std::swap(m_var2level[v], m_var2level[w]); + for (unsigned n : m_relevel) { + if (level(n) == lvl) { + // whoever points to n uses it as if it is level lvl + 1. + m_level2nodes[m_node2levelpos[n]]; + } + } +#endif } bdd bdd_manager::mk_var(unsigned i) { @@ -454,9 +498,14 @@ namespace sat { } for (unsigned i = m_nodes.size(); i-- > 2; ) { if (!reachable[i]) { + m_nodes[i].m_lo = m_nodes[i].m_hi = 0; m_free_nodes.push_back(i); } } + // sort free nodes so that adjacent nodes are picked in order of use + std::sort(m_free_nodes.begin(), m_free_nodes.end()); + m_free_nodes.reverse(); + for (auto* e : m_op_cache) { m_alloc.deallocate(sizeof(*e), e); } diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 471d314c1..c79cd2944 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -38,6 +38,22 @@ namespace sat { return *this; } + void model_converter::process_stack(model & m, literal_vector const& stack) const { + SASSERT(!stack.empty()); + unsigned sz = stack.size(); + SASSERT(stack[sz - 1] == null_literal); + for (unsigned i = sz - 1; i-- > 0; ) { + literal lit = stack[i]; // this is the literal that is pivoted on. It is repeated + bool sat = false; + for (; i > 0 && stack[--i] != null_literal;) { + if (sat) continue; + sat = value_at(stack[i], m) == l_true; + } + if (!sat) { + m[lit.var()] = lit.sign() ? l_false : l_true; + } + } + } void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); @@ -50,34 +66,20 @@ namespace sat { bool sat = false; bool var_sign = false; unsigned index = 0; - literal prev = null_literal; for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause - if (!sat && it->m_elim_sequence[index]) { - SASSERT(prev != null_literal); - m[prev.var()] = prev.sign() ? l_false : l_true; - elim_sequence* s = it->m_elim_sequence[index]; -#if 0 - while (!sat) { - SASSERT(s); - for (literal l2 : s->clause()) { - sat = value_at(l2, m) == l_true; - } - s->clause(); - } -#endif - NOT_IMPLEMENTED_YET(); - } if (!sat) { m[it->var()] = var_sign ? l_false : l_true; - break; + } + elim_stack* s = it->m_elim_stack[index]; + if (s) { + process_stack(m, s->stack()); } sat = false; ++index; - continue; + continue; } - prev = l; if (sat) continue; @@ -155,17 +157,16 @@ namespace sat { return e; } - void model_converter::insert(entry & e, clause const & c, elim_sequence* s) { + void model_converter::insert(entry & e, clause const & c) { SASSERT(c.contains(e.var())); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_sequence.push_back(s); + e.m_elim_stack.push_back(nullptr); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } - void model_converter::insert(entry & e, literal l1, literal l2) { SASSERT(l1.var() == e.var() || l2.var() == e.var()); SASSERT(m_entries.begin() <= &e); @@ -173,7 +174,7 @@ namespace sat { e.m_clauses.push_back(l1); e.m_clauses.push_back(l2); e.m_clauses.push_back(null_literal); - e.m_elim_sequence.push_back(nullptr); + e.m_elim_stack.push_back(nullptr); TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";); } @@ -185,10 +186,21 @@ namespace sat { for (unsigned i = 0; i < sz; ++i) e.m_clauses.push_back(c[i]); e.m_clauses.push_back(null_literal); - e.m_elim_sequence.push_back(nullptr); + e.m_elim_stack.push_back(nullptr); // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } + void model_converter::insert(entry & e, literal_vector const& c, literal_vector const& elims) { + SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true))); + SASSERT(m_entries.begin() <= &e); + SASSERT(&e < m_entries.end()); + for (literal l : c) e.m_clauses.push_back(l); + e.m_clauses.push_back(null_literal); + e.m_elim_stack.push_back(alloc(elim_stack, elims)); + TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); + } + + bool model_converter::check_invariant(unsigned num_vars) const { // After a variable v occurs in an entry n and the entry has kind ELIM_VAR, // then the variable must not occur in any other entry occurring after it. diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index c5cefe84e..00fd637b7 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -39,22 +39,18 @@ namespace sat { class model_converter { public: - class elim_sequence { + class elim_stack { unsigned m_refcount; - elim_sequence* m_next; - literal m_literal; - literal_vector m_clause; + literal_vector m_stack; public: - elim_sequence(literal l, literal_vector const& clause, elim_sequence* next): + elim_stack(literal_vector const& stack): m_refcount(0), - m_next(next), - m_literal(l), - m_clause(clause) { - if (m_next) m_next->inc_ref(); + m_stack(stack) { } - ~elim_sequence() { if (m_next) m_next->dec_ref(); } + ~elim_stack() { } void inc_ref() { ++m_refcount; } void dec_ref() { if (0 == --m_refcount) dealloc(this); } + literal_vector const& stack() const { return m_stack; } }; enum kind { ELIM_VAR = 0, BLOCK_LIT }; @@ -63,20 +59,23 @@ namespace sat { unsigned m_var:31; unsigned m_kind:1; literal_vector m_clauses; // the different clauses are separated by null_literal - sref_vector m_elim_sequence; + sref_vector m_elim_stack; entry(kind k, bool_var v):m_var(v), m_kind(k) {} public: entry(entry const & src): m_var(src.m_var), m_kind(src.m_kind), m_clauses(src.m_clauses), - m_elim_sequence(src.m_elim_sequence) { + m_elim_stack(src.m_elim_stack) { } bool_var var() const { return m_var; } kind get_kind() const { return static_cast(m_kind); } }; private: vector m_entries; + + void process_stack(model & m, literal_vector const& stack) const; + public: model_converter(); ~model_converter(); @@ -84,9 +83,10 @@ namespace sat { model_converter& operator=(model_converter const& other); entry & mk(kind k, bool_var v); - void insert(entry & e, clause const & c, elim_sequence* s = nullptr); + void insert(entry & e, clause const & c); void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); + void insert(entry & c, literal_vector const& covered_clause, literal_vector const& elim_stack); bool empty() const { return m_entries.empty(); } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 3bd5cefb9..b09d180c0 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1025,34 +1025,39 @@ namespace sat { return first; } - literal_vector m_added; + literal_vector m_covered_clause; literal_vector m_intersection; + literal_vector m_elim_stack; bool cla(literal lit) { bool is_tautology = false; - for (literal l : m_added) s.mark_visited(l); + for (literal l : m_covered_clause) s.mark_visited(l); unsigned num_iterations = 0, sz; + m_elim_stack.reset(); do { ++num_iterations; - sz = m_added.size(); - for (unsigned i = 0; i < m_added.size(); ++i) { - if (ri(m_added[i], m_intersection) && m_added[i] == lit) { + sz = m_covered_clause.size(); + for (unsigned i = 0; i < m_covered_clause.size(); ++i) { + m_intersection.reset(); + if (ri(m_covered_clause[i], m_intersection) && m_covered_clause[i] == lit) { is_tautology = true; break; } for (literal l : m_intersection) { if (!s.is_marked(l)) { s.mark_visited(l); - m_added.push_back(l); + m_covered_clause.push_back(l); } } - m_intersection.reset(); + if (!m_intersection.empty()) { + m_elim_stack.append(m_covered_clause); // the current clause + m_elim_stack.push_back(m_covered_clause[i]); // the pivot literal + m_elim_stack.push_back(null_literal); // null demarcation + } } } - while (m_added.size() > sz && !is_tautology); - for (literal l : m_added) s.unmark_visited(l); - m_intersection.reset(); - m_added.reset(); + while (m_covered_clause.size() > sz && !is_tautology); + for (literal l : m_covered_clause) s.unmark_visited(l); if (is_tautology) std::cout << "taut: " << num_iterations << "\n"; return is_tautology; } @@ -1061,13 +1066,15 @@ namespace sat { // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. bool cce(clause& c, literal lit) { - for (literal l : c) m_added.push_back(l); + m_covered_clause.reset(); + for (literal l : c) m_covered_clause.push_back(l); return cla(lit); } bool cce(literal lit, literal l2) { - m_added.push_back(lit); - m_added.push_back(l2); + m_covered_clause.reset(); + m_covered_clause.push_back(lit); + m_covered_clause.push_back(l2); return cla(lit); } @@ -1093,7 +1100,7 @@ namespace sat { s.m_num_blocked_clauses++; } else if (cce(c, l)) { - block_clause(c, l, new_entry); + block_covered_clause(c, l, new_entry); s.m_num_covered_clauses++; } it.next(); @@ -1121,7 +1128,7 @@ namespace sat { s.m_num_blocked_clauses++; } else if (cce(l, l2)) { - block_binary(it, l, new_entry); + block_covered_binary(it, l, new_entry); s.m_num_covered_clauses++; } else { @@ -1134,12 +1141,11 @@ namespace sat { } } - void block_clause(clause& c, literal l, model_converter::entry *& new_entry) { + void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) { TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); if (new_entry == 0) new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); m_to_remove.push_back(&c); - mc.insert(*new_entry, c); for (literal lit : c) { if (lit != l && process_var(lit.var())) { m_queue.decreased(~lit); @@ -1147,14 +1153,33 @@ namespace sat { } } - void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { + void block_clause(clause& c, literal l, model_converter::entry *& new_entry) { + prepare_block_clause(c, l, new_entry); + mc.insert(*new_entry, c); + } + + void block_covered_clause(clause& c, literal l, model_converter::entry *& new_entry) { + prepare_block_clause(c, l, new_entry); + mc.insert(*new_entry, m_covered_clause, m_elim_stack); + } + + void prepare_block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { if (new_entry == 0) new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); literal l2 = it->get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";); s.remove_bin_clause_half(l2, l, it->is_learned()); m_queue.decreased(~l2); - mc.insert(*new_entry, l, l2); + } + + void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { + prepare_block_binary(it, l, new_entry); + mc.insert(*new_entry, l, it->get_literal()); + } + + void block_covered_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { + prepare_block_binary(it, l, new_entry); + mc.insert(*new_entry, m_covered_clause, m_elim_stack); } bool all_tautology(literal l) {