From 708e8669fa3e522f5bbe383e06ea1323b77b32d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Oct 2017 07:41:31 -0700 Subject: [PATCH 01/21] fix faulty merge Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 9a0740cb5..c9552d5d2 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1626,6 +1626,7 @@ namespace sat { pop_lookahead1(lit, num_units); if (unsat) { TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); + lookahead_backtrack(); assign(~lit); propagate(); change = true; From 4d48811efddaf583ff3112f0174b9ae7cc62c5b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Oct 2017 11:22:47 -0700 Subject: [PATCH 02/21] updates Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 17 ++++--- src/sat/tactic/goal2sat.cpp | 2 + src/tactic/portfolio/parallel_tactic.cpp | 62 ++++++++++++++++-------- 3 files changed, 54 insertions(+), 27 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index e0c1b1696..faa9b639e 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1288,7 +1288,6 @@ namespace sat { if (!create_asserting_lemma()) { goto bail_out; } - active2card(); DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); @@ -1347,6 +1346,7 @@ namespace sat { } bool ba_solver::create_asserting_lemma() { + bool adjusted = false; adjust_conflict_level: int64 bound64 = m_bound; @@ -1354,7 +1354,6 @@ namespace sat { for (bool_var v : m_active_vars) { slack += get_abs_coeff(v); } - m_lemma.reset(); m_lemma.push_back(null_literal); unsigned num_skipped = 0; @@ -1389,26 +1388,32 @@ namespace sat { } } } - if (slack >= 0) { IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); return false; } - + if (m_overflow) { + return false; + } if (m_lemma[0] == null_literal) { if (m_lemma.size() == 1) { s().set_conflict(justification()); return false; } + return false; unsigned old_level = m_conflict_lvl; m_conflict_lvl = 0; for (unsigned i = 1; i < m_lemma.size(); ++i) { m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i])); } - IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); + adjusted = true; goto adjust_conflict_level; } - return !m_overflow; + if (!adjusted) { + active2card(); + } + return true; } /* diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 3db2908ed..d7b0e0892 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1153,6 +1153,8 @@ struct sat2goal::imp { } } } + //s.display(std::cout); + //r.display(std::cout); } void add_clause(sat::literal_vector const& lits, expr_ref_vector& lemmas) { diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 9bacbe6a0..4eb2fbbe9 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -63,12 +63,16 @@ class parallel_tactic : public tactic { unsigned num_units() const { return m_units; } + unsigned cube_size() const { return m_cube.size(); } + solver& get_solver() { return *m_solver; } solver const& get_solver() const { return *m_solver; } params_ref const& params() const { return m_params; } + params_ref& params() { return m_params; } + solver_state* clone(params_ref const& p, expr* cube) { ast_manager& m = m_solver->get_manager(); ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); @@ -114,7 +118,7 @@ private: m_conflicts_decay_rate = 75; m_max_conflicts = m_conflicts_lower_bound; m_progress = 0; - m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. + m_num_threads = 2 * omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. } unsigned get_max_conflicts() { @@ -175,16 +179,14 @@ private: } } - lbool simplify(solver& s) { - params_ref p; - p.copy(m_params); - p.set_uint("max_conflicts", 10); - p.set_bool("lookahead_simplify", true); - s.updt_params(p); - lbool is_sat = s.check_sat(0,0); - p.set_uint("max_conflicts", get_max_conflicts()); - p.set_bool("lookahead_simplify", false); - s.updt_params(p); + lbool simplify(solver_state& s) { + s.params().set_uint("max_conflicts", 10); + s.params().set_bool("lookahead_simplify", true); + s.get_solver().updt_params(s.params()); + lbool is_sat = s.get_solver().check_sat(0,0); + s.params().set_uint("max_conflicts", get_max_conflicts()); + s.params().set_bool("lookahead_simplify", false); + s.get_solver().updt_params(s.params()); return is_sat; } @@ -228,12 +230,10 @@ private: return l_undef; } - lbool solve(solver& s) { - params_ref p; - p.copy(m_params); - p.set_uint("max_conflicts", get_max_conflicts()); - s.updt_params(p); - return s.check_sat(0, 0); + lbool solve(solver_state& s) { + s.params().set_uint("max_conflicts", get_max_conflicts()); + s.get_solver().updt_params(s.params()); + return s.get_solver().check_sat(0, 0); } void remove_unsat(svector& unsat) { @@ -260,6 +260,25 @@ private: } lbool solve(model_ref& mdl) { + + { + solver_state& st = *m_solvers[0]; + st.params().set_uint("restart.max", 200); + st.get_solver().updt_params(st.params()); + lbool is_sat = st.get_solver().check_sat(0, 0); + st.params().set_uint("restart.max", UINT_MAX); + st.get_solver().updt_params(st.params()); + switch (is_sat) { + case l_true: + get_model(mdl, 0); + return l_true; + case l_false: + return l_false; + default: + break; + } + } + while (true) { int sz = pick_solvers(); @@ -276,7 +295,7 @@ private: #pragma omp parallel for for (int i = 0; i < sz; ++i) { - lbool is_sat = simplify(m_solvers[i]->get_solver()); + lbool is_sat = simplify(*m_solvers[i]); switch (is_sat) { case l_false: #pragma omp critical (parallel_tactic) @@ -305,7 +324,7 @@ private: #pragma omp parallel for for (int i = 0; i < sz; ++i) { - lbool is_sat = solve(m_solvers[i]->get_solver()); + lbool is_sat = solve(*m_solvers[i]); switch (is_sat) { case l_false: #pragma omp critical (parallel_tactic) @@ -328,6 +347,7 @@ private: remove_unsat(unsat); sz = std::min(max_num_splits(), sz); + sz = std::min(static_cast(m_num_threads/2), sz); if (sz == 0) continue; @@ -360,9 +380,9 @@ private: } std::ostream& display(std::ostream& out) { + out << "branches: " << m_solvers.size() << "\n"; for (solver_state* s : m_solvers) { - out << "solver units " << s->num_units() << "\n"; - out << "cube " << s->cube() << "\n"; + out << "cube " << s->cube_size() << " units " << s->num_units() << "\n"; } m_stats.display(out); return out; From 64ea473bc7425f62a0064711a446890a84faeb0e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Oct 2017 18:03:35 -0700 Subject: [PATCH 03/21] adding bdd Signed-off-by: Nikolaj Bjorner --- src/sat/CMakeLists.txt | 1 + src/sat/sat_bdd.cpp | 260 +++++++++++++++++++++++++++++++++++++++++ src/sat/sat_bdd.h | 170 +++++++++++++++++++++++++++ src/sat/sat_params.pyg | 1 + 4 files changed, 432 insertions(+) create mode 100644 src/sat/sat_bdd.cpp create mode 100644 src/sat/sat_bdd.h diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index c506c04e0..7be6ffb45 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(sat ba_solver.cpp dimacs.cpp sat_asymm_branch.cpp + sat_bdd.cpp sat_clause.cpp sat_clause_set.cpp sat_clause_use_list.cpp diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp new file mode 100644 index 000000000..fc3f94a25 --- /dev/null +++ b/src/sat/sat_bdd.cpp @@ -0,0 +1,260 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_bdd.cpp + +Abstract: + + Simple BDD package modeled after BuDDy, which is modeled after CUDD. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-13 + +Revision History: + +--*/ + +#include "sat/sat_bdd.h" + +namespace sat { + + bdd_manager::bdd_manager(unsigned num_vars, unsigned cache_size) { + for (BDD a = 0; a < 2; ++a) { + for (BDD b = 0; b < 2; ++b) { + for (unsigned op = bdd_and_op; op < bdd_no_op; ++op) { + unsigned index = a + 2*b + 4*op; + m_apply_const.reserve(index+1); + m_apply_const[index] = apply_const(a, b, static_cast(op)); + } + } + } + // add two dummy nodes for true_bdd and false_bdd + m_nodes.push_back(bdd_node(0,0,0)); + m_nodes.push_back(bdd_node(0,0,0)); + m_nodes[0].m_refcount = max_rc; + m_nodes[1].m_refcount = max_rc; + + // add variables + for (unsigned i = 0; i < num_vars; ++i) { + m_var2bdd.push_back(make_node(i, false_bdd, true_bdd)); + m_var2bdd.push_back(make_node(i, true_bdd, false_bdd)); + m_nodes[m_var2bdd[2*i]].m_refcount = max_rc; + m_nodes[m_var2bdd[2*i+1]].m_refcount = max_rc; + m_var2level.push_back(i); + m_level2var.push_back(i); + } + + m_spare_entry = nullptr; + } + + bdd_manager::BDD bdd_manager::apply_const(BDD a, BDD b, bdd_op op) { + switch (op) { + case bdd_and_op: + return (a == 1 && b == 1) ? 1 : 0; + case bdd_or_op: + return (a == 1 || b == 1) ? 1 : 0; + case bdd_iff_op: + return (a == b) ? 1 : 0; + default: + UNREACHABLE(); + return 0; + } + } + + + bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) { + return apply_rec(arg1, arg2, op); + } + + bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) { + switch (op) { + case bdd_and_op: + if (a == b) return a; + if (is_false(a) || is_false(b)) return false_bdd; + if (is_true(a)) return b; + if (is_true(b)) return a; + break; + case bdd_or_op: + if (a == b) return a; + if (is_false(a)) return b; + if (is_false(b)) return a; + if (is_true(a) || is_true(b)) return true_bdd; + break; + case bdd_iff_op: + if (a == b) return true_bdd; + if (is_true(a)) return b; + if (is_true(b)) return a; + break; + default: + UNREACHABLE(); + break; + } + if (is_const(a) && is_const(b)) { + return m_apply_const[a + 2*b + 4*op]; + } + cache_entry * e1 = pop_entry(hash2(a, b, op)); + cache_entry const* e2 = m_cache.insert_if_not_there(e1); + if (e2->m_op == op && e2->m_bdd1 == a && e2->m_bdd2 == b) { + push_entry(e1); + return e2->m_result; + } + BDD r; + if (level(a) == level(b)) { + push(apply_rec(lo(a), lo(b), op)); + push(apply_rec(hi(a), hi(b), op)); + r = make_node(level(a), read(2), read(1)); + } + else if (level(a) < level(b)) { + push(apply_rec(lo(a), b, op)); + push(apply_rec(hi(a), b, op)); + r = make_node(level(a), read(2), read(1)); + } + else { + push(apply_rec(a, lo(b), op)); + push(apply_rec(a, hi(b), op)); + r = make_node(level(b), read(2), read(1)); + } + e1->m_result = r; + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = op; + return r; + } + + void bdd_manager::push(BDD b) { + m_bdd_stack.push_back(b); + } + + void bdd_manager::pop(unsigned num_scopes) { + m_bdd_stack.shrink(m_bdd_stack.size() - num_scopes); + } + + bdd_manager::BDD bdd_manager::read(unsigned index) { + return m_bdd_stack[m_bdd_stack.size() - index]; + } + + + bdd_manager::cache_entry* bdd_manager::pop_entry(unsigned hash) { + cache_entry* result = 0; + if (m_spare_entry) { + result = m_spare_entry; + m_spare_entry = 0; + result->m_hash = hash; + } + else { + void * mem = m_alloc.allocate(sizeof(cache_entry)); + result = new (mem) cache_entry(hash); + } + return result; + } + + void bdd_manager::push_entry(cache_entry* e) { + SASSERT(!m_spare_entry); + m_spare_entry = e; + } + + + bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) { + if (l == r) { + return l; + } +#if 0 + // TBD + unsigned hash = node_hash(level, l, r); + bdd result = m_ +#endif + int sz = m_nodes.size(); + m_nodes.push_back(bdd_node(level, l, r)); + return sz; + } + +#if 0 + void bdd_manager::bdd_reorder(int) { + + } +#endif + + bdd bdd_manager::mk_var(unsigned i) { + return bdd(m_var2bdd[2*i+1], this); + } + + bdd bdd_manager::mk_nvar(unsigned i) { + return bdd(m_var2bdd[2*i+1], this); + } + + unsigned bdd_manager::hash2(BDD a, BDD b, bdd_op op) const { + return mk_mix(a, b, op); + } + + bdd bdd_manager::mk_not(bdd b) { + return bdd(mk_not_rec(b.root), this); + } + + bdd_manager::BDD bdd_manager::mk_not_rec(BDD b) { + if (is_true(b)) return false_bdd; + if (is_false(b)) return true_bdd; + cache_entry* e1 = pop_entry(hash1(b, bdd_not_op)); + cache_entry const* e2 = m_cache.insert_if_not_there(e1); + if (e2->m_bdd1 == b && e2->m_op == bdd_not_op) { + push_entry(e1); + return e2->m_result; + } + push(mk_not_rec(lo(b))); + push(mk_not_rec(hi(b))); + BDD r = make_node(level(b), read(2), read(1)); + pop(2); + e1->m_bdd1 = b; + e1->m_bdd2 = b; + e1->m_op = bdd_not_op; + e1->m_result = r; + return r; + } + +#if 0 + bdd bdd_manager::mk_exists(bdd vars, bdd b) { + + } + + bdd bdd_manager::mk_forall(bdd vars, bdd b) { + + } + + bdd bdd_manager::mk_ite(bdd c, bdd t, bdd e) { + + } + + double bdd_manager::path_count(bdd b) { + + } + +#endif + + std::ostream& bdd_manager::display(std::ostream& out, bdd b) { + + return out; + } + + std::ostream& bdd_manager::display(std::ostream& out) { + + return out; + } + + bdd::bdd(int root, bdd_manager* m): + root(root), m(m) { + m->inc_ref(root); + } + + bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } + + + bdd::~bdd() { + m->dec_ref(root); + } + +#if 0 +#endif + +} diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h new file mode 100644 index 000000000..4df0433fd --- /dev/null +++ b/src/sat/sat_bdd.h @@ -0,0 +1,170 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_bdd + +Abstract: + + Simple BDD package modeled after BuDDy, which is modeled after CUDD. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-13 + +Revision History: + +--*/ +#ifndef SAT_BDD_H_ +#define SAT_BDD_H_ + +#include "util/vector.h" +#include "util/map.h" +#include "util/small_object_allocator.h" + +namespace sat { + + struct bdd_pair { + int* m_bdd; + int m_last; + int m_id; + bdd_pair* m_next; + }; + + class bdd_manager; + + class bdd { + friend class bdd_manager; + int root; + bdd_manager* m; + bdd(int root, bdd_manager* m); + public: + bdd(bdd & other); + ~bdd(); + // bdd operator!() { return m->mk_not(*this); } + }; + + class bdd_manager { + friend bdd; + + typedef int BDD; + + enum bdd_op { + bdd_and_op = 0, + bdd_or_op, + bdd_iff_op, + bdd_not_op, + bdd_no_op + }; + + struct bdd_node { + bdd_node(unsigned level, int lo, int hi): + m_refcount(0), + m_level(level), + m_lo(lo), + m_hi(hi) + {} + unsigned m_refcount : 10; + unsigned m_level : 22; + int m_lo; + int m_hi; + //unsigned m_hash; + //unsigned m_next; + }; + + struct cache_entry { + cache_entry(unsigned hash): + m_bdd1(0), + m_bdd2(0), + m_op(bdd_no_op), + m_result(0), + m_hash(hash) + {} + + BDD m_bdd1; + BDD m_bdd2; + bdd_op m_op; + BDD m_result; + unsigned m_hash; + }; + + struct hash_entry { + unsigned operator()(cache_entry* e) const { return e->m_hash; } + }; + + struct eq_entry { + bool operator()(cache_entry * a, cache_entry * b) const { + return a->m_hash == b->m_hash; + } + }; + + svector m_nodes; + ptr_hashtable m_cache; + unsigned_vector m_apply_const; + svector m_bdd_stack; + cache_entry* m_spare_entry; + svector m_var2bdd; + unsigned_vector m_var2level, m_level2var; + small_object_allocator m_alloc; + + BDD make_node(unsigned level, BDD l, BDD r); + + BDD apply_const(BDD a, BDD b, bdd_op op); + BDD apply(BDD arg1, BDD arg2, bdd_op op); + BDD apply_rec(BDD arg1, BDD arg2, bdd_op op); + + void push(BDD b); + void pop(unsigned num_scopes); + BDD read(unsigned index); + + cache_entry* pop_entry(unsigned hash); + void push_entry(cache_entry* e); + + // void bdd_reorder(int); + + BDD mk_not_rec(BDD b); + + unsigned hash1(BDD b, bdd_op op) const { return hash2(b, b, op); } + unsigned hash2(BDD a, BDD b, bdd_op op) const; + unsigned hash3(BDD a, BDD b, BDD c, bdd_op op) const; + + static const BDD false_bdd = 0; + static const BDD true_bdd = 1; + static const unsigned max_rc = (1 << 10) - 1; + + inline bool is_true(BDD b) const { return b == true_bdd; } + inline bool is_false(BDD b) const { return b == false_bdd; } + inline bool is_const(BDD b) const { return 0 <= b && b <= 1; } + + unsigned level(BDD b) const { return m_nodes[b].m_level; } + BDD lo(BDD b) const { return m_nodes[b].m_lo; } + BDD hi(BDD b) const { return m_nodes[b].m_hi; } + void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; } + void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc && m_nodes[b].m_refcount > 0) m_nodes[b].m_refcount--; } + + BDD mk_true() { return 1; } + BDD mk_false() { return 0; } + + public: + bdd_manager(unsigned nodes, unsigned cache_size); + + bdd mk_var(unsigned i); + bdd mk_nvar(unsigned i); + + bdd mk_not(bdd b); + bdd mk_exist(bdd vars, bdd b); + bdd mk_forall(bdd vars, bdd b); + bdd mk_and(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } + bdd mk_or(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } + bdd mk_iff(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } + bdd mk_ite(bdd c, bdd t, bdd e); + + double path_count(bdd b); + + std::ostream& display(std::ostream& out, bdd b); + std::ostream& display(std::ostream& out); + }; +} + +#endif diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 296c75180..d803617f5 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -39,6 +39,7 @@ def_module_params('sat', ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'), ('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'), ('lookahead_search', BOOL, False, 'use lookahead solver'), + ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'), ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'), From d7b6373601c46ba3dc928c59280298b6e18be2e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 10:41:17 -0700 Subject: [PATCH 04/21] adding bdd package Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 428 ++++++++++++++++++++++++++++++++-------- src/sat/sat_bdd.h | 135 ++++++++----- src/test/CMakeLists.txt | 1 + src/test/bdd.cpp | 40 ++++ src/test/main.cpp | 1 + 5 files changed, 476 insertions(+), 129 deletions(-) create mode 100644 src/test/bdd.cpp diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index fc3f94a25..50fc3f1d9 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -32,10 +32,16 @@ namespace sat { } } // add two dummy nodes for true_bdd and false_bdd - m_nodes.push_back(bdd_node(0,0,0)); - m_nodes.push_back(bdd_node(0,0,0)); - m_nodes[0].m_refcount = max_rc; - m_nodes[1].m_refcount = max_rc; + for (unsigned i = 0; i <= bdd_no_op; ++i) { + m_nodes.push_back(bdd_node(0,0,0)); + m_nodes.back().m_refcount = max_rc; + m_nodes.back().m_index = m_nodes.size()-1; + } + + m_spare_entry = nullptr; + m_max_num_bdd_nodes = 1 << 24; // up to 16M nodes + m_mark_level = 0; + alloc_free_nodes(1024); // add variables for (unsigned i = 0; i < num_vars; ++i) { @@ -45,28 +51,44 @@ namespace sat { m_nodes[m_var2bdd[2*i+1]].m_refcount = max_rc; m_var2level.push_back(i); m_level2var.push_back(i); - } - - m_spare_entry = nullptr; + } + } + + bdd_manager::~bdd_manager() { + if (m_spare_entry) { + m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry); + } + for (auto* e : m_op_cache) { + m_alloc.deallocate(sizeof(*e), e); + } } bdd_manager::BDD bdd_manager::apply_const(BDD a, BDD b, bdd_op op) { + SASSERT(is_const(a) && is_const(b)); switch (op) { case bdd_and_op: - return (a == 1 && b == 1) ? 1 : 0; + return (a == true_bdd && b == true_bdd) ? true_bdd : false_bdd; case bdd_or_op: - return (a == 1 || b == 1) ? 1 : 0; + return (a == true_bdd || b == true_bdd) ? true_bdd : false_bdd; case bdd_iff_op: - return (a == b) ? 1 : 0; + return (a == b) ? true_bdd : false_bdd; default: - UNREACHABLE(); - return 0; + return false_bdd; } } - bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) { - return apply_rec(arg1, arg2, op); + bool first = true; + while (true) { + try { + return apply_rec(arg1, arg2, op); + } + catch (bdd_exception) { + try_reorder(); + if (!first) throw; + first = false; + } + } } bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) { @@ -95,11 +117,17 @@ namespace sat { if (is_const(a) && is_const(b)) { return m_apply_const[a + 2*b + 4*op]; } - cache_entry * e1 = pop_entry(hash2(a, b, op)); - cache_entry const* e2 = m_cache.insert_if_not_there(e1); - if (e2->m_op == op && e2->m_bdd1 == a && e2->m_bdd2 == b) { - push_entry(e1); - return e2->m_result; + op_entry * e1 = pop_entry(a, b, op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (e2 != e1) { + if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == op) { + push_entry(e1); + return e2->m_result; + } + e1 = const_cast(e2); + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = op; } BDD r; if (level(a) == level(b)) { @@ -107,7 +135,7 @@ namespace sat { push(apply_rec(hi(a), hi(b), op)); r = make_node(level(a), read(2), read(1)); } - else if (level(a) < level(b)) { + else if (level(a) > level(b)) { push(apply_rec(lo(a), b, op)); push(apply_rec(hi(a), b, op)); r = make_node(level(a), read(2), read(1)); @@ -117,10 +145,8 @@ namespace sat { push(apply_rec(a, hi(b), op)); r = make_node(level(b), read(2), read(1)); } + pop(2); e1->m_result = r; - e1->m_bdd1 = a; - e1->m_bdd2 = b; - e1->m_op = op; return r; } @@ -136,46 +162,63 @@ namespace sat { return m_bdd_stack[m_bdd_stack.size() - index]; } - - bdd_manager::cache_entry* bdd_manager::pop_entry(unsigned hash) { - cache_entry* result = 0; + bdd_manager::op_entry* bdd_manager::pop_entry(BDD l, BDD r, BDD op) { + op_entry* result = nullptr; if (m_spare_entry) { result = m_spare_entry; - m_spare_entry = 0; - result->m_hash = hash; + m_spare_entry = nullptr; + result->m_bdd1 = l; + result->m_bdd2 = r; + result->m_op = op; } else { - void * mem = m_alloc.allocate(sizeof(cache_entry)); - result = new (mem) cache_entry(hash); + void * mem = m_alloc.allocate(sizeof(op_entry)); + result = new (mem) op_entry(l, r, op); } + result->m_result = -1; return result; } - void bdd_manager::push_entry(cache_entry* e) { + void bdd_manager::push_entry(op_entry* e) { SASSERT(!m_spare_entry); m_spare_entry = e; } - bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) { if (l == r) { return l; } -#if 0 - // TBD - unsigned hash = node_hash(level, l, r); - bdd result = m_ -#endif - int sz = m_nodes.size(); - m_nodes.push_back(bdd_node(level, l, r)); - return sz; + + bdd_node n(level, l, r); + node_table::entry* e = m_node_table.insert_if_not_there2(n); + if (e->get_data().m_index != 0) { + return e->get_data().m_index; + } + e->get_data().m_refcount = 0; + if (m_free_nodes.empty()) { + gc(); + e = m_node_table.insert_if_not_there2(n); + e->get_data().m_refcount = 0; + } + if (m_free_nodes.empty()) { + if (m_nodes.size() > m_max_num_bdd_nodes) { + throw bdd_exception(); + } + e->get_data().m_index = m_nodes.size(); + m_nodes.push_back(e->get_data()); + alloc_free_nodes(m_nodes.size()/2); + } + else { + e->get_data().m_index = m_free_nodes.back(); + m_nodes[e->get_data().m_index] = e->get_data(); + m_free_nodes.pop_back(); + } + return e->get_data().m_index; } -#if 0 - void bdd_manager::bdd_reorder(int) { - + void bdd_manager::try_reorder() { + // TBD } -#endif bdd bdd_manager::mk_var(unsigned i) { return bdd(m_var2bdd[2*i+1], this); @@ -185,76 +228,301 @@ namespace sat { return bdd(m_var2bdd[2*i+1], this); } - unsigned bdd_manager::hash2(BDD a, BDD b, bdd_op op) const { - return mk_mix(a, b, op); - } - bdd bdd_manager::mk_not(bdd b) { - return bdd(mk_not_rec(b.root), this); + bool first = true; + while (true) { + try { + return bdd(mk_not_rec(b.root), this); + } + catch (bdd_exception) { + try_reorder(); + if (!first) throw; + first = false; + } + } } bdd_manager::BDD bdd_manager::mk_not_rec(BDD b) { if (is_true(b)) return false_bdd; if (is_false(b)) return true_bdd; - cache_entry* e1 = pop_entry(hash1(b, bdd_not_op)); - cache_entry const* e2 = m_cache.insert_if_not_there(e1); - if (e2->m_bdd1 == b && e2->m_op == bdd_not_op) { - push_entry(e1); - return e2->m_result; + op_entry* e1 = pop_entry(b, b, bdd_not_op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (e2 != e1) { + if (e2->m_bdd1 == b && e2->m_bdd2 == b && e2->m_op == bdd_not_op) { + push_entry(e1); + return e2->m_result; + } + e1 = const_cast(e2); + e1->m_bdd1 = b; + e1->m_bdd2 = b; + e1->m_op = bdd_not_op; } push(mk_not_rec(lo(b))); push(mk_not_rec(hi(b))); BDD r = make_node(level(b), read(2), read(1)); pop(2); - e1->m_bdd1 = b; - e1->m_bdd2 = b; - e1->m_op = bdd_not_op; e1->m_result = r; return r; } -#if 0 - bdd bdd_manager::mk_exists(bdd vars, bdd b) { + bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { + bool first = true; + while (true) { + try { + return bdd(mk_ite_rec(c.root, t.root, e.root), this); + } + catch (bdd_exception) { + try_reorder(); + if (!first) throw; + first = false; + } + } + } + + bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) { + if (is_true(a)) return b; + if (is_false(a)) return c; + if (b == c) return b; + if (is_true(b)) return apply(a, c, bdd_or_op); + if (is_false(c)) return apply(a, b, bdd_and_op); + if (is_false(b)) return apply(mk_not_rec(a), c, bdd_and_op); + if (is_true(c)) return apply(mk_not_rec(a), b, bdd_or_op); + SASSERT(!is_const(a) && !is_const(b) && !is_const(c)); + op_entry * e1 = pop_entry(a, b, c); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (e2 != e1) { + if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) { + push_entry(e1); + return e2->m_result; + } + e1 = const_cast(e2); + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = c; + } + unsigned la = level(a), lb = level(b), lc = level(c); + BDD r; + BDD a1, b1, c1, a2, b2, c2; + unsigned lvl = la; + if (la >= lb && la >= lc) { + a1 = lo(a), a2 = hi(a); + lvl = la; + } + else { + a1 = a, a2 = a; + } + if (lb >= la && lb >= lc) { + b1 = lo(b), b2 = hi(b); + lvl = lb; + } + else { + b1 = b, b2 = b; + } + if (lc >= la && lc >= lb) { + c1 = lo(c), c2 = hi(c); + lvl = lc; + } + else { + c1 = c, c2 = c; + } + push(mk_ite_rec(a1, b1, c1)); + push(mk_ite_rec(a2, b2, c2)); + r = make_node(lvl, read(2), read(1)); + pop(2); + e1->m_result = r; + return r; + } + + bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) { + return bdd(mk_quant(n, vars, b.root, bdd_or_op), this); + } + + bdd bdd_manager::mk_forall(unsigned n, unsigned const* vars, bdd const& b) { + return bdd(mk_quant(n, vars, b.root, bdd_and_op), this); + } + + bdd_manager::BDD bdd_manager::mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op) { + BDD result = b; + for (unsigned i = 0; i < n; ++i) { + result = mk_quant_rec(m_var2level[vars[i]], result, op); + } + return result; + } + + bdd_manager::BDD bdd_manager::mk_quant_rec(unsigned l, BDD b, bdd_op op) { + unsigned lvl = level(b); + + if (lvl == l) { + return apply(lo(b), hi(b), op); + } + else if (lvl < l) { + return b; + } + else { + BDD a = level2bdd(l); + bdd_op q_op = op == bdd_and_op ? bdd_and_proj_op : bdd_or_proj_op; + op_entry * e1 = pop_entry(a, b, q_op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (e1 != e2) { + if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == q_op) { + push_entry(e1); + return e2->m_result; + } + e1 = const_cast(e2); + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = q_op; + } + push(mk_quant_rec(l, lo(b), op)); + push(mk_quant_rec(l, hi(b), op)); + BDD r = make_node(lvl, read(2), read(1)); + pop(2); + e1->m_result = r; + return r; + } + } + + double bdd_manager::path_count(bdd const& b) { + init_mark(); + m_path_count.resize(m_nodes.size()); + m_path_count[0] = 0; + m_path_count[1] = 1; + set_mark(0); + set_mark(1); + m_todo.push_back(b.root); + while (!m_todo.empty()) { + BDD r = m_todo.back(); + if (is_marked(r)) { + m_todo.pop_back(); + } + else if (!is_marked(lo(r))) { + m_todo.push_back(lo(r)); + } + else if (!is_marked(hi(r))) { + m_todo.push_back(hi(r)); + } + else { + m_path_count[r] = m_path_count[lo(r)] + m_path_count[hi(r)]; + set_mark(r); + m_todo.pop_back(); + } + } + return m_path_count[b.root]; } - bdd bdd_manager::mk_forall(bdd vars, bdd b) { - + void bdd_manager::alloc_free_nodes(unsigned n) { + for (unsigned i = 0; i < n; ++i) { + m_free_nodes.push_back(m_nodes.size()); + m_nodes.push_back(bdd_node()); + m_nodes.back().m_index = m_nodes.size() - 1; + } + m_free_nodes.reverse(); } - bdd bdd_manager::mk_ite(bdd c, bdd t, bdd e) { - + void bdd_manager::gc() { + IF_VERBOSE(1, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";); + SASSERT(m_free_nodes.empty()); + svector reachable(m_nodes.size(), false); + for (unsigned i = m_bdd_stack.size(); i-- > 0; ) { + reachable[m_bdd_stack[i]] = true; + m_todo.push_back(m_bdd_stack[i]); + } + for (unsigned i = m_nodes.size(); i-- > 2; ) { + if (m_nodes[i].m_refcount > 0) { + reachable[i] = true; + m_todo.push_back(i); + } + } + while (!m_todo.empty()) { + BDD b = m_todo.back(); + m_todo.pop_back(); + SASSERT(reachable[b]); + if (is_const(b)) continue; + if (!reachable[lo(b)]) { + reachable[lo(b)] = true; + m_todo.push_back(lo(b)); + } + if (!reachable[hi(b)]) { + reachable[hi(b)] = true; + m_todo.push_back(hi(b)); + } + } + for (unsigned i = m_nodes.size(); i-- > 2; ) { + if (!reachable[i]) { + m_free_nodes.push_back(i); + } + } + for (auto* e : m_op_cache) { + m_alloc.deallocate(sizeof(*e), e); + } + m_op_cache.reset(); + m_node_table.reset(); + // re-populate node cache + for (unsigned i = m_nodes.size(); i-- > 2; ) { + if (reachable[i]) { + SASSERT(m_nodes[i].m_index == i); + m_node_table.insert(m_nodes[i]); + } + } } - double bdd_manager::path_count(bdd b) { - + void bdd_manager::init_mark() { + m_mark.resize(m_nodes.size()); + ++m_mark_level; + if (m_mark_level == 0) { + m_mark.fill(0); + } } -#endif - - std::ostream& bdd_manager::display(std::ostream& out, bdd b) { - + std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) { + init_mark(); + m_todo.push_back(b.root); + while (!m_todo.empty()) { + BDD r = m_todo.back(); + if (is_marked(r)) { + m_todo.pop_back(); + } + else if (lo(r) == 0 && hi(r) == 0) { + set_mark(r); + m_todo.pop_back(); + } + else if (!is_marked(lo(r))) { + m_todo.push_back(lo(r)); + } + else if (!is_marked(hi(r))) { + m_todo.push_back(hi(r)); + } + else { + out << r << " : " << var(r) << " " << lo(r) << " " << hi(r) << "\n"; + set_mark(r); + m_todo.pop_back(); + } + } return out; } std::ostream& bdd_manager::display(std::ostream& out) { - + for (unsigned i = 0; i < m_nodes.size(); ++i) { + bdd_node const& n = m_nodes[i]; + if (n.m_lo == 0 && n.m_hi == 0) continue; + out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; + } return out; } - bdd::bdd(int root, bdd_manager* m): - root(root), m(m) { - m->inc_ref(root); - } - + bdd::bdd(int root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } + bdd::~bdd() { m->dec_ref(root); } + bdd bdd::operator!() { return m->mk_not(*this); } + bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); } + bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); } + std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } - - bdd::~bdd() { - m->dec_ref(root); + std::ostream& operator<<(std::ostream& out, bdd const& b) { + return b.display(out); } -#if 0 -#endif + } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 4df0433fd..767fd5111 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -42,20 +42,29 @@ namespace sat { public: bdd(bdd & other); ~bdd(); - // bdd operator!() { return m->mk_not(*this); } + bdd operator!(); + bdd operator&&(bdd const& other); + bdd operator||(bdd const& other); + std::ostream& display(std::ostream& out) const; + bool operator==(bdd const& other) const { return root == other.root; } + bool operator!=(bdd const& other) const { return root != other.root; } }; + std::ostream& operator<<(std::ostream& out, bdd const& b); + class bdd_manager { friend bdd; typedef int BDD; enum bdd_op { - bdd_and_op = 0, - bdd_or_op, - bdd_iff_op, - bdd_not_op, - bdd_no_op + bdd_and_op = 2, + bdd_or_op = 3, + bdd_iff_op = 4, + bdd_not_op = 5, + bdd_and_proj_op = 6, + bdd_or_proj_op = 7, + bdd_no_op = 8, }; struct bdd_node { @@ -63,71 +72,99 @@ namespace sat { m_refcount(0), m_level(level), m_lo(lo), - m_hi(hi) + m_hi(hi), + m_index(0) {} + bdd_node(): m_level(0), m_lo(0), m_hi(0), m_index(0) {} unsigned m_refcount : 10; unsigned m_level : 22; int m_lo; int m_hi; - //unsigned m_hash; - //unsigned m_next; + unsigned m_index; + unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } + }; + + struct hash_node { + unsigned operator()(bdd_node const& n) const { return n.hash(); } + }; + + struct eq_node { + bool operator()(bdd_node const& a, bdd_node const& b) const { + return a.m_lo == b.m_lo && a.m_hi == b.m_hi && a.m_level == b.m_level; + } }; - struct cache_entry { - cache_entry(unsigned hash): - m_bdd1(0), - m_bdd2(0), - m_op(bdd_no_op), - m_result(0), - m_hash(hash) + typedef hashtable node_table; + + struct op_entry { + op_entry(BDD l, BDD r, BDD op): + m_bdd1(l), + m_bdd2(r), + m_op(op), + m_result(0) {} BDD m_bdd1; BDD m_bdd2; - bdd_op m_op; + BDD m_op; BDD m_result; - unsigned m_hash; + unsigned hash() const { return mk_mix(m_bdd1, m_bdd2, m_op); } }; struct hash_entry { - unsigned operator()(cache_entry* e) const { return e->m_hash; } + unsigned operator()(op_entry* e) const { return e->hash(); } }; struct eq_entry { - bool operator()(cache_entry * a, cache_entry * b) const { - return a->m_hash == b->m_hash; + bool operator()(op_entry * a, op_entry * b) const { + return a->hash() == b->hash(); } }; - svector m_nodes; - ptr_hashtable m_cache; + typedef ptr_hashtable op_table; + + svector m_nodes; + op_table m_op_cache; + node_table m_node_table; unsigned_vector m_apply_const; svector m_bdd_stack; - cache_entry* m_spare_entry; + op_entry* m_spare_entry; svector m_var2bdd; unsigned_vector m_var2level, m_level2var; + unsigned_vector m_free_nodes; small_object_allocator m_alloc; + mutable svector m_mark; + mutable unsigned m_mark_level; + mutable svector m_path_count; + mutable svector m_todo; + + unsigned m_max_num_bdd_nodes; BDD make_node(unsigned level, BDD l, BDD r); BDD apply_const(BDD a, BDD b, bdd_op op); BDD apply(BDD arg1, BDD arg2, bdd_op op); + BDD mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op); + BDD apply_rec(BDD arg1, BDD arg2, bdd_op op); + BDD mk_not_rec(BDD b); + BDD mk_ite_rec(BDD a, BDD b, BDD c); + BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op); void push(BDD b); void pop(unsigned num_scopes); BDD read(unsigned index); - cache_entry* pop_entry(unsigned hash); - void push_entry(cache_entry* e); + op_entry* pop_entry(BDD l, BDD r, BDD op); + void push_entry(op_entry* e); - // void bdd_reorder(int); + void gc(); + void alloc_free_nodes(unsigned n); + void init_mark(); + void set_mark(unsigned i) { m_mark[i] = m_mark_level; } + bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; } - BDD mk_not_rec(BDD b); - - unsigned hash1(BDD b, bdd_op op) const { return hash2(b, b, op); } - unsigned hash2(BDD a, BDD b, bdd_op op) const; - unsigned hash3(BDD a, BDD b, BDD c, bdd_op op) const; + void try_reorder(); static const BDD false_bdd = 0; static const BDD true_bdd = 1; @@ -136,33 +173,33 @@ namespace sat { inline bool is_true(BDD b) const { return b == true_bdd; } inline bool is_false(BDD b) const { return b == false_bdd; } inline bool is_const(BDD b) const { return 0 <= b && b <= 1; } + inline unsigned level(BDD b) const { return m_nodes[b].m_level; } + inline unsigned var(BDD b) const { return m_level2var[level(b)]; } + inline BDD lo(BDD b) const { return m_nodes[b].m_lo; } + inline BDD hi(BDD b) const { return m_nodes[b].m_hi; } + inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; } + inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; } + inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; } - unsigned level(BDD b) const { return m_nodes[b].m_level; } - BDD lo(BDD b) const { return m_nodes[b].m_lo; } - BDD hi(BDD b) const { return m_nodes[b].m_hi; } - void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; } - void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc && m_nodes[b].m_refcount > 0) m_nodes[b].m_refcount--; } - - BDD mk_true() { return 1; } - BDD mk_false() { return 0; } - + struct bdd_exception {}; public: bdd_manager(unsigned nodes, unsigned cache_size); + ~bdd_manager(); bdd mk_var(unsigned i); bdd mk_nvar(unsigned i); bdd mk_not(bdd b); - bdd mk_exist(bdd vars, bdd b); - bdd mk_forall(bdd vars, bdd b); - bdd mk_and(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } - bdd mk_or(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } - bdd mk_iff(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } - bdd mk_ite(bdd c, bdd t, bdd e); + bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } + bdd mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } + bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } + bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); - double path_count(bdd b); + double path_count(bdd const& b); - std::ostream& display(std::ostream& out, bdd b); + std::ostream& display(std::ostream& out, bdd const& b); std::ostream& display(std::ostream& out); }; } diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 1c1665363..b487fe9ba 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -16,6 +16,7 @@ add_executable(test-z3 arith_rewriter.cpp arith_simplifier_plugin.cpp ast.cpp + bdd.cpp bit_blaster.cpp bits.cpp bit_vector.cpp diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp new file mode 100644 index 000000000..91d837f08 --- /dev/null +++ b/src/test/bdd.cpp @@ -0,0 +1,40 @@ +#include "sat/sat_bdd.h" + +namespace sat { + static void test1() { + bdd_manager m(20, 1000); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + bdd c1 = v0 && v1 && v2; + bdd c2 = v2 && v0 && v1; + std::cout << c1 << "\n"; + SASSERT(c1 == c2); + + c1 = v0 || v1 || v2; + c2 = v2 || v1 || v0; + std::cout << c1 << "\n"; + std::cout << c2 << "\n"; + SASSERT(c1 == c2); + } + + static void test2() { + bdd_manager m(20, 1000); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1)); + SASSERT(m.mk_ite(v0,v1,v1) == v1); + SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1)); + SASSERT(m.mk_ite(v1,v0,v0) == v0); + SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); + SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); + SASSERT(!(v0 && v1) == (!v0 || !v1)); + SASSERT(!(v0 || v1) == (!v0 && !v1)); + } +} + +void tst_bdd() { + sat::test1(); + sat::test2(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 4aeba26c5..33d0abae5 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -245,6 +245,7 @@ int main(int argc, char ** argv) { TST_ARGV(sat_lookahead); TST_ARGV(sat_local_search); TST_ARGV(cnf_backbones); + TST(bdd); //TST_ARGV(hs); } From 09fdfcc963c4171e9003ca025078a3b675a00dca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 11:40:20 -0700 Subject: [PATCH 05/21] adding bdd package Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 104 +++++++++++++++++++------------------------- src/sat/sat_bdd.h | 44 ++++++++++--------- src/test/bdd.cpp | 3 +- 3 files changed, 69 insertions(+), 82 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 50fc3f1d9..216eec32f 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -24,15 +24,16 @@ namespace sat { bdd_manager::bdd_manager(unsigned num_vars, unsigned cache_size) { for (BDD a = 0; a < 2; ++a) { for (BDD b = 0; b < 2; ++b) { - for (unsigned op = bdd_and_op; op < bdd_no_op; ++op) { + for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) { unsigned index = a + 2*b + 4*op; m_apply_const.reserve(index+1); m_apply_const[index] = apply_const(a, b, static_cast(op)); } } } - // add two dummy nodes for true_bdd and false_bdd - for (unsigned i = 0; i <= bdd_no_op; ++i) { + + // add dummy nodes for operations, and true, false bdds. + for (unsigned i = 0; i <= bdd_no_op + 2; ++i) { m_nodes.push_back(bdd_node(0,0,0)); m_nodes.back().m_refcount = max_rc; m_nodes.back().m_index = m_nodes.size()-1; @@ -41,7 +42,7 @@ namespace sat { m_spare_entry = nullptr; m_max_num_bdd_nodes = 1 << 24; // up to 16M nodes m_mark_level = 0; - alloc_free_nodes(1024); + alloc_free_nodes(1024 + num_vars); // add variables for (unsigned i = 0; i < num_vars; ++i) { @@ -91,6 +92,20 @@ namespace sat { } } + bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { + if (e1 != e2) { + if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) { + push_entry(e1); + return true; + } + e1 = const_cast(e2); + } + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = c; + return false; + } + bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) { switch (op) { case bdd_and_op: @@ -119,15 +134,8 @@ namespace sat { } op_entry * e1 = pop_entry(a, b, op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); - if (e2 != e1) { - if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == op) { - push_entry(e1); - return e2->m_result; - } - e1 = const_cast(e2); - e1->m_bdd1 = a; - e1->m_bdd2 = b; - e1->m_op = op; + if (check_result(e1, e2, a, b, op)) { + return e2->m_result; } BDD r; if (level(a) == level(b)) { @@ -221,7 +229,7 @@ namespace sat { } bdd bdd_manager::mk_var(unsigned i) { - return bdd(m_var2bdd[2*i+1], this); + return bdd(m_var2bdd[2*i], this); } bdd bdd_manager::mk_nvar(unsigned i) { @@ -247,16 +255,8 @@ namespace sat { if (is_false(b)) return true_bdd; op_entry* e1 = pop_entry(b, b, bdd_not_op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); - if (e2 != e1) { - if (e2->m_bdd1 == b && e2->m_bdd2 == b && e2->m_op == bdd_not_op) { - push_entry(e1); - return e2->m_result; - } - e1 = const_cast(e2); - e1->m_bdd1 = b; - e1->m_bdd2 = b; - e1->m_op = bdd_not_op; - } + if (check_result(e1, e2, b, b, bdd_not_op)) + return e2->m_result; push(mk_not_rec(lo(b))); push(mk_not_rec(hi(b))); BDD r = make_node(level(b), read(2), read(1)); @@ -264,8 +264,8 @@ namespace sat { e1->m_result = r; return r; } - - bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { + + bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { bool first = true; while (true) { try { @@ -290,16 +290,8 @@ namespace sat { SASSERT(!is_const(a) && !is_const(b) && !is_const(c)); op_entry * e1 = pop_entry(a, b, c); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); - if (e2 != e1) { - if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) { - push_entry(e1); - return e2->m_result; - } - e1 = const_cast(e2); - e1->m_bdd1 = a; - e1->m_bdd2 = b; - e1->m_op = c; - } + if (check_result(e1, e2, a, b, c)) + return e2->m_result; unsigned la = level(a), lb = level(b), lc = level(c); BDD r; BDD a1, b1, c1, a2, b2, c2; @@ -363,16 +355,8 @@ namespace sat { bdd_op q_op = op == bdd_and_op ? bdd_and_proj_op : bdd_or_proj_op; op_entry * e1 = pop_entry(a, b, q_op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); - if (e1 != e2) { - if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == q_op) { - push_entry(e1); - return e2->m_result; - } - e1 = const_cast(e2); - e1->m_bdd1 = a; - e1->m_bdd2 = b; - e1->m_op = q_op; - } + if (check_result(e1, e2, a, b, q_op)) + return e2->m_result; push(mk_quant_rec(l, lo(b), op)); push(mk_quant_rec(l, hi(b), op)); BDD r = make_node(lvl, read(2), read(1)); @@ -382,11 +366,11 @@ namespace sat { } } - double bdd_manager::path_count(bdd const& b) { + double bdd_manager::count(bdd const& b, unsigned z) { init_mark(); - m_path_count.resize(m_nodes.size()); - m_path_count[0] = 0; - m_path_count[1] = 1; + m_count.resize(m_nodes.size()); + m_count[0] = z; + m_count[1] = 1-z; set_mark(0); set_mark(1); m_todo.push_back(b.root); @@ -402,13 +386,12 @@ namespace sat { m_todo.push_back(hi(r)); } else { - m_path_count[r] = m_path_count[lo(r)] + m_path_count[hi(r)]; + m_count[r] = m_count[lo(r)] + m_count[hi(r)]; set_mark(r); m_todo.pop_back(); } } - return m_path_count[b.root]; - + return m_count[b.root]; } void bdd_manager::alloc_free_nodes(unsigned n) { @@ -472,6 +455,7 @@ namespace sat { ++m_mark_level; if (m_mark_level == 0) { m_mark.fill(0); + ++m_mark_level; } } @@ -514,15 +498,15 @@ namespace sat { bdd::bdd(int root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } bdd::~bdd() { m->dec_ref(root); } + bdd bdd::lo() const { return bdd(m->lo(root), m); } + bdd bdd::hi() const { return bdd(m->hi(root), m); } + unsigned bdd::var() const { return m->var(root); } + bool bdd::is_true() const { return root == bdd_manager::true_bdd; } + bool bdd::is_false() const { return root == bdd_manager::false_bdd; } bdd bdd::operator!() { return m->mk_not(*this); } bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); } bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); } - std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } - - std::ostream& operator<<(std::ostream& out, bdd const& b) { - return b.display(out); - } - - + std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } + std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 767fd5111..04aa1e8d7 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -25,13 +25,6 @@ Revision History: namespace sat { - struct bdd_pair { - int* m_bdd; - int m_last; - int m_id; - bdd_pair* m_next; - }; - class bdd_manager; class bdd { @@ -42,6 +35,12 @@ namespace sat { public: bdd(bdd & other); ~bdd(); + bdd lo() const; + bdd hi() const; + unsigned var() const; + bool is_true() const; + bool is_false() const; + bdd operator!(); bdd operator&&(bdd const& other); bdd operator||(bdd const& other); @@ -123,22 +122,21 @@ namespace sat { typedef ptr_hashtable op_table; - svector m_nodes; - op_table m_op_cache; - node_table m_node_table; - unsigned_vector m_apply_const; - svector m_bdd_stack; - op_entry* m_spare_entry; - svector m_var2bdd; - unsigned_vector m_var2level, m_level2var; - unsigned_vector m_free_nodes; - small_object_allocator m_alloc; + svector m_nodes; + op_table m_op_cache; + node_table m_node_table; + unsigned_vector m_apply_const; + svector m_bdd_stack; + op_entry* m_spare_entry; + svector m_var2bdd; + unsigned_vector m_var2level, m_level2var; + unsigned_vector m_free_nodes; + small_object_allocator m_alloc; mutable svector m_mark; mutable unsigned m_mark_level; - mutable svector m_path_count; + mutable svector m_count; mutable svector m_todo; - - unsigned m_max_num_bdd_nodes; + unsigned m_max_num_bdd_nodes; BDD make_node(unsigned level, BDD l, BDD r); @@ -157,7 +155,10 @@ namespace sat { op_entry* pop_entry(BDD l, BDD r, BDD op); void push_entry(op_entry* e); + bool check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c); + double count(bdd const& b, unsigned z); + void gc(); void alloc_free_nodes(unsigned n); void init_mark(); @@ -197,7 +198,8 @@ namespace sat { bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); - double path_count(bdd const& b); + double dnf_size(bdd const& b) { return count(b, 0); } + double cnf_size(bdd const& b) { return count(b, 1); } std::ostream& display(std::ostream& out, bdd const& b); std::ostream& display(std::ostream& out); diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 91d837f08..319f05bf8 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -10,12 +10,13 @@ namespace sat { bdd c2 = v2 && v0 && v1; std::cout << c1 << "\n"; SASSERT(c1 == c2); + std::cout << "cnf size: " << m.cnf_size(c1) << "\n"; c1 = v0 || v1 || v2; c2 = v2 || v1 || v0; std::cout << c1 << "\n"; - std::cout << c2 << "\n"; SASSERT(c1 == c2); + std::cout << "cnf size: " << m.cnf_size(c1) << "\n"; } static void test2() { From d36406f845cc761edd81f2628a21bdf602a8b509 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 15:12:02 -0700 Subject: [PATCH 06/21] adding BDD-based variable elimination routine Signed-off-by: Nikolaj Bjorner --- src/sat/CMakeLists.txt | 1 + src/sat/sat_bdd.cpp | 1 + src/sat/sat_bdd.h | 7 + src/sat/sat_elim_vars.cpp | 289 +++++++++++++++++++++++++++++++++++++ src/sat/sat_elim_vars.h | 61 ++++++++ src/sat/sat_simplifier.cpp | 14 +- src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.h | 1 + 8 files changed, 372 insertions(+), 3 deletions(-) create mode 100644 src/sat/sat_elim_vars.cpp create mode 100644 src/sat/sat_elim_vars.h diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index 7be6ffb45..88f4f3dd6 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -11,6 +11,7 @@ z3_add_component(sat sat_config.cpp sat_drat.cpp sat_elim_eqs.cpp + sat_elim_vars.cpp sat_iff3_finder.cpp sat_integrity_checker.cpp sat_local_search.cpp diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 216eec32f..4835b8580 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -506,6 +506,7 @@ namespace sat { bdd bdd::operator!() { return m->mk_not(*this); } bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); } bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); } + bdd& bdd::operator=(bdd const& other) { int r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 04aa1e8d7..da26c0b36 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -34,6 +34,7 @@ namespace sat { bdd(int root, bdd_manager* m); public: bdd(bdd & other); + bdd& operator=(bdd const& other); ~bdd(); bdd lo() const; bdd hi() const; @@ -44,6 +45,8 @@ namespace sat { bdd operator!(); bdd operator&&(bdd const& other); bdd operator||(bdd const& other); + bdd operator|=(bdd const& other) { return *this = *this || other; } + bdd operator&=(bdd const& other) { return *this = *this && other; } std::ostream& display(std::ostream& out) const; bool operator==(bdd const& other) const { return root == other.root; } bool operator!=(bdd const& other) const { return root != other.root; } @@ -190,9 +193,13 @@ namespace sat { bdd mk_var(unsigned i); bdd mk_nvar(unsigned i); + bdd mk_true() { return bdd(true_bdd, this); } + bdd mk_false() { return bdd(false_bdd, this); } bdd mk_not(bdd b); bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b); bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); } + bdd mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); } bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } bdd mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp new file mode 100644 index 000000000..4fb92c261 --- /dev/null +++ b/src/sat/sat_elim_vars.cpp @@ -0,0 +1,289 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_elim_vars.cpp + +Abstract: + + Helper class for eliminating variables + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-14 + +Revision History: + +--*/ + +#include "sat/sat_simplifier.h" +#include "sat/sat_elim_vars.h" +#include "sat/sat_solver.h" + +namespace sat{ + + elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20,10000) { + m_mark_lim = 0; + m_max_literals = 11; // p.resolution_occ_cutoff(); + } + + bool elim_vars::operator()(bool_var v) { + if (s.value(v) != l_undef) + return false; + + literal pos_l(v, false); + literal neg_l(v, true); + unsigned num_bin_pos = simp.get_num_non_learned_bin(pos_l); + if (num_bin_pos > m_max_literals) return false; + unsigned num_bin_neg = simp.get_num_non_learned_bin(neg_l); + if (num_bin_neg > m_max_literals) return false; + clause_use_list & pos_occs = simp.m_use_list.get(pos_l); + clause_use_list & neg_occs = simp.m_use_list.get(neg_l); + unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.size() + neg_occs.size(); + reset_mark(); + mark_var(v); + if (!mark_literals(pos_occs)) return false; + if (!mark_literals(neg_occs)) return false; + if (!mark_literals(pos_l)) return false; + if (!mark_literals(neg_l)) return false; + + // associate index with each variable. + unsigned index = 0; + for (bool_var w : m_vars) { + m_var2index[w] = index++; + } + bdd b1 = make_clauses(pos_l); + bdd b2 = make_clauses(neg_l); + bdd b3 = make_clauses(pos_occs); + bdd b4 = make_clauses(neg_occs); + bdd b0 = b1 && b2 && b3 && b4; + bdd b = m.mk_exists(m_var2index[v], b0); + TRACE("elim_vars", + tout << "eliminate " << v << "\n"; + tout << "clauses : " << clause_size << "\n"; + for (watched const& w : simp.get_wlist(~pos_l)) { + if (w.is_binary_non_learned_clause()) { + tout << pos_l << " " << w.get_literal() << "\n"; + } + } + m.display(tout, b1); + for (watched const& w : simp.get_wlist(~neg_l)) { + if (w.is_binary_non_learned_clause()) { + tout << neg_l << " " << w.get_literal() << "\n"; + } + } + m.display(tout, b2); + clause_use_list::iterator itp = pos_occs.mk_iterator(); + while (!itp.at_end()) { + clause const& c = itp.curr(); + tout << c << "\n"; + itp.next(); + } + m.display(tout, b3); + clause_use_list::iterator itn = neg_occs.mk_iterator(); + while (!itn.at_end()) { + clause const& c = itn.curr(); + tout << c << "\n"; + itn.next(); + } + m.display(tout, b4); + tout << "eliminated:\n"; + tout << b << "\n"; + tout << m.cnf_size(b) << "\n"; + ); + std::cout << "num clauses: " << clause_size << " cnf size: " << m.cnf_size(b) << "\n"; + if (clause_size < m.cnf_size(b)) + return false; + + + literal_vector lits; + TRACE("elim_vars", + clause_vector clauses; + literal_vector units; + get_clauses(b0, lits, clauses, units); + for (clause* c : clauses) + tout << *c << "\n"; + for (literal l : units) + tout << l << "\n"; + for (clause* c : clauses) + s.m_cls_allocator.del_clause(c); + SASSERT(lits.empty()); + clauses.reset(); + units.reset(); + tout << "after elim:\n"; + get_clauses(b, lits, clauses, units); + for (clause* c : clauses) + tout << *c << "\n"; + for (literal l : units) + tout << l << "\n"; + for (clause* c : clauses) + s.m_cls_allocator.del_clause(c); + SASSERT(lits.empty()); + clauses.reset(); + ); + + return false; + + // eliminate variable + simp.m_pos_cls.reset(); + simp.m_neg_cls.reset(); + simp.collect_clauses(pos_l, simp.m_pos_cls); + simp.collect_clauses(neg_l, simp.m_neg_cls); + model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); + simp.save_clauses(mc_entry, simp.m_pos_cls); + simp.save_clauses(mc_entry, simp.m_neg_cls); + s.m_eliminated[v] = true; + simp.remove_bin_clauses(pos_l); + simp.remove_bin_clauses(neg_l); + simp.remove_clauses(pos_occs, pos_l); + simp.remove_clauses(neg_occs, neg_l); + pos_occs.reset(); + neg_occs.reset(); + add_clauses(b, lits); + return true; + } + + void elim_vars::add_clauses(bdd const& b, literal_vector& lits) { + if (b.is_true()) { + // no-op + } + else if (b.is_false()) { + SASSERT(lits.size() > 0); + std::cout << lits << "\n"; + literal_vector c(lits); + if (simp.cleanup_clause(c)) + return; + + std::cout << c << "\n"; + + switch (c.size()) { + case 0: + UNREACHABLE(); + break; + case 1: + simp.propagate_unit(c[0]); + break; + case 2: + simp.add_non_learned_binary_clause(c[0],c[1]); + break; + default: { + clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false); + s.m_clauses.push_back(cp); + simp.m_use_list.insert(*cp); + break; + } + } + } + else { + unsigned v = m_vars[b.var()]; + lits.push_back(literal(v, false)); + add_clauses(b.lo(), lits); + lits.pop_back(); + lits.push_back(literal(v, true)); + add_clauses(b.hi(), lits); + lits.pop_back(); + } + } + + + void elim_vars::get_clauses(bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) { + if (b.is_true()) { + return; + } + if (b.is_false()) { + if (lits.size() > 1) { + clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), false); + clauses.push_back(c); + } + else { + units.push_back(lits.back()); + } + return; + } + + // if (v hi lo) + // (v | lo) & (!v | hi) + // if (v T lo) -> (v | lo) + unsigned v = m_vars[b.var()]; + lits.push_back(literal(v, false)); + get_clauses(b.lo(), lits, clauses, units); + lits.pop_back(); + lits.push_back(literal(v, true)); + get_clauses(b.hi(), lits, clauses, units); + lits.pop_back(); + } + + void elim_vars::reset_mark() { + m_vars.reset(); + m_mark.resize(s.num_vars()); + m_var2index.resize(s.num_vars()); + ++m_mark_lim; + if (m_mark_lim == 0) { + ++m_mark_lim; + m_mark.fill(0); + } + } + + void elim_vars::mark_var(bool_var v) { + if (m_mark[v] != m_mark_lim) { + m_mark[v] = m_mark_lim; + m_vars.push_back(v); + } + } + + bool elim_vars::mark_literals(clause_use_list & occs) { + clause_use_list::iterator it = occs.mk_iterator(); + while (!it.at_end()) { + clause const& c = it.curr(); + for (literal l : c) { + mark_var(l.var()); + } + if (num_vars() > m_max_literals) return false; + it.next(); + } + return true; + } + + bool elim_vars::mark_literals(literal lit) { + watch_list& wl = simp.get_wlist(lit); + for (watched const& w : wl) { + if (w.is_binary_non_learned_clause()) { + mark_var(w.get_literal().var()); + } + } + return num_vars() <= m_max_literals; + } + + bdd elim_vars::make_clauses(clause_use_list & occs) { + bdd result = m.mk_true(); + clause_use_list::iterator it = occs.mk_iterator(); + while (!it.at_end()) { + clause const& c = it.curr(); + bdd cl = m.mk_false(); + for (literal l : c) { + cl |= mk_literal(l); + } + it.next(); + result &= cl; + } + return result; + } + + bdd elim_vars::make_clauses(literal lit) { + bdd result = m.mk_true(); + watch_list& wl = simp.get_wlist(~lit); + for (watched const& w : wl) { + if (w.is_binary_non_learned_clause()) { + result &= (mk_literal(lit) || mk_literal(w.get_literal())); + } + } + return result; + } + + bdd elim_vars::mk_literal(literal l) { + return l.sign() ? m.mk_nvar(m_var2index[l.var()]) : m.mk_var(m_var2index[l.var()]); + } + +}; + diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h new file mode 100644 index 000000000..f9d3b374c --- /dev/null +++ b/src/sat/sat_elim_vars.h @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_elim_vars.h + +Abstract: + + Helper class for eliminating variables + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-14 + +Revision History: + +--*/ +#ifndef SAT_ELIM_VARS_H_ +#define SAT_ELIM_VARS_H_ + +#include "sat/sat_types.h" +#include "sat/sat_bdd.h" + +namespace sat { + class solver; + class simplifier; + + class elim_vars { + friend class simplifier; + + simplifier& simp; + solver& s; + bdd_manager m; + + svector m_vars; + unsigned_vector m_mark; + unsigned m_mark_lim; + unsigned_vector m_var2index; + + unsigned m_max_literals; + + unsigned num_vars() const { return m_vars.size(); } + void reset_mark(); + void mark_var(bool_var v); + bool mark_literals(clause_use_list & occs); + bool mark_literals(literal lit); + bdd make_clauses(clause_use_list & occs); + bdd make_clauses(literal lit); + bdd mk_literal(literal l); + void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units); + void add_clauses(bdd const& b, literal_vector& lits); + + public: + elim_vars(simplifier& s); + bool operator()(bool_var v); + }; + +}; + +#endif diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 4d5946795..12923e0d0 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -21,6 +21,7 @@ Revision History: #include "sat/sat_simplifier.h" #include "sat/sat_simplifier_params.hpp" #include "sat/sat_solver.h" +#include "sat/sat_elim_vars.h" #include "util/stopwatch.h" #include "util/trace.h" @@ -1308,7 +1309,6 @@ namespace sat { clause_use_list & neg_occs = m_use_list.get(neg_l); unsigned num_pos = pos_occs.size() + num_bin_pos; unsigned num_neg = neg_occs.size() + num_bin_neg; - m_elim_counter -= num_pos + num_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); @@ -1349,7 +1349,6 @@ namespace sat { collect_clauses(pos_l, m_pos_cls); collect_clauses(neg_l, m_neg_cls); - m_elim_counter -= num_pos * num_neg + before_lits; TRACE("resolution_detail", tout << "collecting number of after_clauses\n";); unsigned before_clauses = num_pos + num_neg; @@ -1371,6 +1370,8 @@ namespace sat { TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); + m_elim_counter -= num_pos * num_neg + before_lits; + // eliminate variable model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); @@ -1454,14 +1455,21 @@ namespace sat { elim_var_report rpt(*this); bool_var_vector vars; order_vars_for_elim(vars); + // sat::elim_vars elim_bdd(*this); + std::cout << "vars to elim: " << vars.size() << "\n"; for (bool_var v : vars) { checkpoint(); - if (m_elim_counter < 0) + if (m_elim_counter < 0) break; if (try_eliminate(v)) { m_num_elim_vars++; } +#if 0 + else if (elim_bdd(v)) { + m_num_elim_vars++; + } +#endif } m_pos_cls.finalize(); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index a38df3d3c..6ef0f8f18 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -49,6 +49,7 @@ namespace sat { class simplifier { friend class ba_solver; + friend class elim_vars; solver & s; unsigned m_num_calls; use_list m_use_list; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 020c1dc42..56071182b 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -179,6 +179,7 @@ namespace sat { friend class local_search; friend struct mk_stat; friend class ccc; + friend class elim_vars; public: solver(params_ref const & p, reslimit& l); ~solver(); From 11093166215845bf870cbd1f62a1d9f18b9f0504 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 15:53:25 -0700 Subject: [PATCH 07/21] fixing projection Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 33 +++++++++++++++++++-------------- src/sat/sat_bdd.h | 14 +++++++------- src/test/bdd.cpp | 25 +++++++++++++++++++++++++ 3 files changed, 51 insertions(+), 21 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 4835b8580..36900760e 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -94,8 +94,8 @@ namespace sat { bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { if (e1 != e2) { + push_entry(e1); if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) { - push_entry(e1); return true; } e1 = const_cast(e2); @@ -343,12 +343,15 @@ namespace sat { bdd_manager::BDD bdd_manager::mk_quant_rec(unsigned l, BDD b, bdd_op op) { unsigned lvl = level(b); - - if (lvl == l) { - return apply(lo(b), hi(b), op); + BDD r; + if (is_const(b)) { + r = b; + } + else if (lvl == l) { + r = apply(lo(b), hi(b), op); } else if (lvl < l) { - return b; + r = b; } else { BDD a = level2bdd(l); @@ -356,14 +359,16 @@ namespace sat { op_entry * e1 = pop_entry(a, b, q_op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); if (check_result(e1, e2, a, b, q_op)) - return e2->m_result; - push(mk_quant_rec(l, lo(b), op)); - push(mk_quant_rec(l, hi(b), op)); - BDD r = make_node(lvl, read(2), read(1)); - pop(2); - e1->m_result = r; - return r; + r = e2->m_result; + else { + push(mk_quant_rec(l, lo(b), op)); + push(mk_quant_rec(l, hi(b), op)); + r = make_node(lvl, read(2), read(1)); + pop(2); + e1->m_result = r; + } } + return r; } double bdd_manager::count(bdd const& b, unsigned z) { @@ -495,7 +500,7 @@ namespace sat { return out; } - bdd::bdd(int root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } + bdd::bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } bdd::~bdd() { m->dec_ref(root); } bdd bdd::lo() const { return bdd(m->lo(root), m); } @@ -506,7 +511,7 @@ namespace sat { bdd bdd::operator!() { return m->mk_not(*this); } bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); } bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); } - bdd& bdd::operator=(bdd const& other) { int r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } + bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index da26c0b36..29d91446e 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -29,9 +29,9 @@ namespace sat { class bdd { friend class bdd_manager; - int root; + unsigned root; bdd_manager* m; - bdd(int root, bdd_manager* m); + bdd(unsigned root, bdd_manager* m); public: bdd(bdd & other); bdd& operator=(bdd const& other); @@ -57,7 +57,7 @@ namespace sat { class bdd_manager { friend bdd; - typedef int BDD; + typedef unsigned BDD; enum bdd_op { bdd_and_op = 2, @@ -70,7 +70,7 @@ namespace sat { }; struct bdd_node { - bdd_node(unsigned level, int lo, int hi): + bdd_node(unsigned level, BDD lo, BDD hi): m_refcount(0), m_level(level), m_lo(lo), @@ -80,8 +80,8 @@ namespace sat { bdd_node(): m_level(0), m_lo(0), m_hi(0), m_index(0) {} unsigned m_refcount : 10; unsigned m_level : 22; - int m_lo; - int m_hi; + BDD m_lo; + BDD m_hi; unsigned m_index; unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } }; @@ -176,7 +176,7 @@ namespace sat { inline bool is_true(BDD b) const { return b == true_bdd; } inline bool is_false(BDD b) const { return b == false_bdd; } - inline bool is_const(BDD b) const { return 0 <= b && b <= 1; } + inline bool is_const(BDD b) const { return b <= 1; } inline unsigned level(BDD b) const { return m_nodes[b].m_level; } inline unsigned var(BDD b) const { return m_level2var[level(b)]; } inline BDD lo(BDD b) const { return m_nodes[b].m_lo; } diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 319f05bf8..f3f6e6b8d 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -33,9 +33,34 @@ namespace sat { SASSERT(!(v0 && v1) == (!v0 || !v1)); SASSERT(!(v0 || v1) == (!v0 && !v1)); } + + static void test3() { + bdd_manager m(20, 1000); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + bdd c1 = (v0 && v1) || v2; + bdd c2 = m.mk_exists(0, c1); + std::cout << c1 << "\n"; + std::cout << c2 << "\n"; + SASSERT(c2 == (v1 || v2)); + c2 = m.mk_exists(1, c1); + SASSERT(c2 == (v0 || v2)); + c2 = m.mk_exists(2, c1); + SASSERT(c2.is_true()); + SASSERT(m.mk_exists(3, c1) == c1); + c1 = (v0 && v1) || (v1 && v2) || (!v0 && !v2); + c2 = m.mk_exists(0, c1); + SASSERT(c2 == (v1 || (v1 && v2) || !v2)); + c2 = m.mk_exists(1, c1); + SASSERT(c2 == (v0 || v2 || (!v0 && !v2))); + c2 = m.mk_exists(2, c1); + SASSERT(c2 == ((v0 && v1) || v1 || !v0)); + } } void tst_bdd() { sat::test1(); sat::test2(); + sat::test3(); } From 46fa24532439afcb38f26561c066ff4da9e4a5c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 18:33:38 -0700 Subject: [PATCH 08/21] more agressive variable elimination Signed-off-by: Nikolaj Bjorner --- src/sat/sat_elim_vars.cpp | 131 +++++++++++++++++++++++++++++-------- src/sat/sat_elim_vars.h | 8 +++ src/sat/sat_simplifier.cpp | 10 ++- 3 files changed, 118 insertions(+), 31 deletions(-) diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 4fb92c261..764c193b3 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -25,7 +25,7 @@ namespace sat{ elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20,10000) { m_mark_lim = 0; - m_max_literals = 11; // p.resolution_occ_cutoff(); + m_max_literals = 13; // p.resolution_occ_cutoff(); } bool elim_vars::operator()(bool_var v) { @@ -41,6 +41,9 @@ namespace sat{ clause_use_list & pos_occs = simp.m_use_list.get(pos_l); clause_use_list & neg_occs = simp.m_use_list.get(neg_l); unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.size() + neg_occs.size(); + if (clause_size == 0) { + return false; + } reset_mark(); mark_var(v); if (!mark_literals(pos_occs)) return false; @@ -49,16 +52,72 @@ namespace sat{ if (!mark_literals(neg_l)) return false; // associate index with each variable. + sort_marked(); + bdd b1 = elim_var(v); + double sz1 = m.cnf_size(b1); + if (sz1 > 2*clause_size) { + return false; + } + if (sz1 <= clause_size) { + return elim_var(v, b1); + } + m_vars.reverse(); + bdd b2 = elim_var(v); + double sz2 = m.cnf_size(b2); + if (sz2 <= clause_size) { + return elim_var(v, b2); + } + shuffle_vars(); + bdd b3 = elim_var(v); + double sz3 = m.cnf_size(b3); + if (sz3 <= clause_size) { + return elim_var(v, b3); + } + return false; + } + + bool elim_vars::elim_var(bool_var v, bdd const& b) { + literal pos_l(v, false); + literal neg_l(v, true); + clause_use_list & pos_occs = simp.m_use_list.get(pos_l); + clause_use_list & neg_occs = simp.m_use_list.get(neg_l); + + // eliminate variable + simp.m_pos_cls.reset(); + simp.m_neg_cls.reset(); + simp.collect_clauses(pos_l, simp.m_pos_cls); + simp.collect_clauses(neg_l, simp.m_neg_cls); + model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); + simp.save_clauses(mc_entry, simp.m_pos_cls); + simp.save_clauses(mc_entry, simp.m_neg_cls); + s.m_eliminated[v] = true; + simp.remove_bin_clauses(pos_l); + simp.remove_bin_clauses(neg_l); + simp.remove_clauses(pos_occs, pos_l); + simp.remove_clauses(neg_occs, neg_l); + pos_occs.reset(); + neg_occs.reset(); + literal_vector lits; + add_clauses(b, lits); + return true; + } + + bdd elim_vars::elim_var(bool_var v) { unsigned index = 0; for (bool_var w : m_vars) { m_var2index[w] = index++; } + literal pos_l(v, false); + literal neg_l(v, true); + clause_use_list & pos_occs = simp.m_use_list.get(pos_l); + clause_use_list & neg_occs = simp.m_use_list.get(neg_l); + bdd b1 = make_clauses(pos_l); bdd b2 = make_clauses(neg_l); bdd b3 = make_clauses(pos_occs); bdd b4 = make_clauses(neg_occs); bdd b0 = b1 && b2 && b3 && b4; - bdd b = m.mk_exists(m_var2index[v], b0); + bdd b = m.mk_exists(m_var2index[v], b0); TRACE("elim_vars", tout << "eliminate " << v << "\n"; tout << "clauses : " << clause_size << "\n"; @@ -92,12 +151,8 @@ namespace sat{ tout << b << "\n"; tout << m.cnf_size(b) << "\n"; ); - std::cout << "num clauses: " << clause_size << " cnf size: " << m.cnf_size(b) << "\n"; - if (clause_size < m.cnf_size(b)) - return false; - - literal_vector lits; +#if 0 TRACE("elim_vars", clause_vector clauses; literal_vector units; @@ -122,26 +177,9 @@ namespace sat{ SASSERT(lits.empty()); clauses.reset(); ); +#endif - return false; - - // eliminate variable - simp.m_pos_cls.reset(); - simp.m_neg_cls.reset(); - simp.collect_clauses(pos_l, simp.m_pos_cls); - simp.collect_clauses(neg_l, simp.m_neg_cls); - model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); - simp.save_clauses(mc_entry, simp.m_pos_cls); - simp.save_clauses(mc_entry, simp.m_neg_cls); - s.m_eliminated[v] = true; - simp.remove_bin_clauses(pos_l); - simp.remove_bin_clauses(neg_l); - simp.remove_clauses(pos_occs, pos_l); - simp.remove_clauses(neg_occs, neg_l); - pos_occs.reset(); - neg_occs.reset(); - add_clauses(b, lits); - return true; + return b; } void elim_vars::add_clauses(bdd const& b, literal_vector& lits) { @@ -150,12 +188,9 @@ namespace sat{ } else if (b.is_false()) { SASSERT(lits.size() > 0); - std::cout << lits << "\n"; literal_vector c(lits); if (simp.cleanup_clause(c)) return; - - std::cout << c << "\n"; switch (c.size()) { case 0: @@ -165,12 +200,22 @@ namespace sat{ simp.propagate_unit(c[0]); break; case 2: + s.m_stats.m_mk_bin_clause++; simp.add_non_learned_binary_clause(c[0],c[1]); + simp.back_subsumption1(c[0],c[1], false); break; default: { + if (c.size() == 3) + s.m_stats.m_mk_ter_clause++; + else + s.m_stats.m_mk_clause++; clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false); s.m_clauses.push_back(cp); simp.m_use_list.insert(*cp); + if (simp.m_sub_counter > 0) + simp.back_subsumption1(*cp); + else + simp.back_subsumption0(*cp); break; } } @@ -218,6 +263,7 @@ namespace sat{ m_vars.reset(); m_mark.resize(s.num_vars()); m_var2index.resize(s.num_vars()); + m_occ.resize(s.num_vars()); ++m_mark_lim; if (m_mark_lim == 0) { ++m_mark_lim; @@ -225,10 +271,37 @@ namespace sat{ } } + class elim_vars::compare_occ { + elim_vars& ev; + public: + compare_occ(elim_vars& ev):ev(ev) {} + + bool operator()(bool_var v1, bool_var v2) const { + return ev.m_occ[v1] < ev.m_occ[v2]; + } + }; + + void elim_vars::sort_marked() { + std::sort(m_vars.begin(), m_vars.end(), compare_occ(*this)); + } + + void elim_vars::shuffle_vars() { + unsigned sz = m_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + unsigned x = m_rand(sz); + unsigned y = m_rand(sz); + std::swap(m_vars[x], m_vars[y]); + } + } + void elim_vars::mark_var(bool_var v) { if (m_mark[v] != m_mark_lim) { m_mark[v] = m_mark_lim; m_vars.push_back(v); + m_occ[v] = 1; + } + else { + ++m_occ[v]; } } diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index f9d3b374c..8f7ec1bb4 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -28,21 +28,27 @@ namespace sat { class elim_vars { friend class simplifier; + class compare_occ; simplifier& simp; solver& s; bdd_manager m; + random_gen m_rand; + svector m_vars; unsigned_vector m_mark; unsigned m_mark_lim; unsigned_vector m_var2index; + unsigned_vector m_occ; unsigned m_max_literals; unsigned num_vars() const { return m_vars.size(); } void reset_mark(); void mark_var(bool_var v); + void sort_marked(); + void shuffle_vars(); bool mark_literals(clause_use_list & occs); bool mark_literals(literal lit); bdd make_clauses(clause_use_list & occs); @@ -50,6 +56,8 @@ namespace sat { bdd mk_literal(literal l); void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units); void add_clauses(bdd const& b, literal_vector& lits); + bool elim_var(bool_var v, bdd const& b); + bdd elim_var(bool_var v); public: elim_vars(simplifier& s); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 12923e0d0..688510153 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -191,6 +191,12 @@ namespace sat { // scoped_finalize _scoped_finalize(*this); + for (bool_var v = 0; v < s.num_vars(); ++v) { + if (!s.m_eliminated[v] && !is_external(v)) { + insert_elim_todo(v); + } + } + do { if (m_subsumption) subsume(); @@ -1455,7 +1461,7 @@ namespace sat { elim_var_report rpt(*this); bool_var_vector vars; order_vars_for_elim(vars); - // sat::elim_vars elim_bdd(*this); + sat::elim_vars elim_bdd(*this); std::cout << "vars to elim: " << vars.size() << "\n"; for (bool_var v : vars) { @@ -1465,7 +1471,7 @@ namespace sat { if (try_eliminate(v)) { m_num_elim_vars++; } -#if 0 +#if 1 else if (elim_bdd(v)) { m_num_elim_vars++; } From 9f9ae4427de529643b9f18d2c0e77040a02c01fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Oct 2017 15:13:43 -0700 Subject: [PATCH 09/21] add cce Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 35 ++++-- src/sat/sat_bdd.h | 108 ++++++++++--------- src/sat/sat_elim_vars.cpp | 44 ++------ src/sat/sat_elim_vars.h | 1 - src/sat/sat_model_converter.cpp | 9 +- src/sat/sat_simplifier.cpp | 186 ++++++++++++++++++++++++++------ src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.cpp | 2 + src/sat/sat_solver.h | 2 + src/test/bdd.cpp | 10 +- 10 files changed, 259 insertions(+), 139 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 36900760e..edc8ad2a8 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -21,7 +21,7 @@ Revision History: namespace sat { - bdd_manager::bdd_manager(unsigned num_vars, unsigned cache_size) { + bdd_manager::bdd_manager(unsigned num_vars) { for (BDD a = 0; a < 2; ++a) { for (BDD b = 0; b < 2; ++b) { for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) { @@ -84,7 +84,7 @@ namespace sat { try { return apply_rec(arg1, arg2, op); } - catch (bdd_exception) { + catch (mem_out) { try_reorder(); if (!first) throw; first = false; @@ -92,6 +92,16 @@ namespace sat { } } + + bdd bdd_manager::mk_true() { return bdd(true_bdd, this); } + bdd bdd_manager::mk_false() { return bdd(false_bdd, this); } + bdd bdd_manager::mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } + bdd bdd_manager::mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } + bdd bdd_manager::mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } + bdd bdd_manager::mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); } + bdd bdd_manager::mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); } + + bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { if (e1 != e2) { push_entry(e1); @@ -203,14 +213,15 @@ namespace sat { return e->get_data().m_index; } e->get_data().m_refcount = 0; - if (m_free_nodes.empty()) { + bool do_gc = m_free_nodes.empty(); + if (do_gc) { gc(); e = m_node_table.insert_if_not_there2(n); e->get_data().m_refcount = 0; } - if (m_free_nodes.empty()) { + if (do_gc && m_free_nodes.size()*3 < m_nodes.size()) { if (m_nodes.size() > m_max_num_bdd_nodes) { - throw bdd_exception(); + throw mem_out(); } e->get_data().m_index = m_nodes.size(); m_nodes.push_back(e->get_data()); @@ -228,6 +239,11 @@ namespace sat { // TBD } + void bdd_manager::sift_up(unsigned level) { + // exchange level and level + 1. + + } + bdd bdd_manager::mk_var(unsigned i) { return bdd(m_var2bdd[2*i], this); } @@ -242,7 +258,7 @@ namespace sat { try { return bdd(mk_not_rec(b.root), this); } - catch (bdd_exception) { + catch (mem_out) { try_reorder(); if (!first) throw; first = false; @@ -271,7 +287,7 @@ namespace sat { try { return bdd(mk_ite_rec(c.root, t.root, e.root), this); } - catch (bdd_exception) { + catch (mem_out) { try_reorder(); if (!first) throw; first = false; @@ -409,7 +425,7 @@ namespace sat { } void bdd_manager::gc() { - IF_VERBOSE(1, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";); + IF_VERBOSE(3, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";); SASSERT(m_free_nodes.empty()); svector reachable(m_nodes.size(), false); for (unsigned i = m_bdd_stack.size(); i-- > 0; ) { @@ -502,6 +518,7 @@ namespace sat { bdd::bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } + bdd::bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); } bdd::~bdd() { m->dec_ref(root); } bdd bdd::lo() const { return bdd(m->lo(root), m); } bdd bdd::hi() const { return bdd(m->hi(root), m); } @@ -514,5 +531,7 @@ namespace sat { bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } + double bdd::cnf_size() const { return m->cnf_size(*this); } + double bdd::dnf_size() const { return m->dnf_size(*this); } } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 29d91446e..c0f1fc9b2 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -25,34 +25,7 @@ Revision History: namespace sat { - class bdd_manager; - - class bdd { - friend class bdd_manager; - unsigned root; - bdd_manager* m; - bdd(unsigned root, bdd_manager* m); - public: - bdd(bdd & other); - bdd& operator=(bdd const& other); - ~bdd(); - bdd lo() const; - bdd hi() const; - unsigned var() const; - bool is_true() const; - bool is_false() const; - - bdd operator!(); - bdd operator&&(bdd const& other); - bdd operator||(bdd const& other); - bdd operator|=(bdd const& other) { return *this = *this || other; } - bdd operator&=(bdd const& other) { return *this = *this && other; } - std::ostream& display(std::ostream& out) const; - bool operator==(bdd const& other) const { return root == other.root; } - bool operator!=(bdd const& other) const { return root != other.root; } - }; - - std::ostream& operator<<(std::ostream& out, bdd const& b); + class bdd; class bdd_manager { friend bdd; @@ -169,6 +142,7 @@ namespace sat { bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; } void try_reorder(); + void sift_up(unsigned level); static const BDD false_bdd = 0; static const BDD true_bdd = 1; @@ -185,32 +159,70 @@ namespace sat { inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; } inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; } - struct bdd_exception {}; - public: - bdd_manager(unsigned nodes, unsigned cache_size); - ~bdd_manager(); - - bdd mk_var(unsigned i); - bdd mk_nvar(unsigned i); - - bdd mk_true() { return bdd(true_bdd, this); } - bdd mk_false() { return bdd(false_bdd, this); } - bdd mk_not(bdd b); - bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b); - bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); - bdd mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); } - bdd mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); } - bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } - bdd mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } - bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } - bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); - double dnf_size(bdd const& b) { return count(b, 0); } double cnf_size(bdd const& b) { return count(b, 1); } + bdd mk_not(bdd b); + bdd mk_and(bdd const& a, bdd const& b); + bdd mk_or(bdd const& a, bdd const& b); + std::ostream& display(std::ostream& out, bdd const& b); + + public: + struct mem_out {}; + + bdd_manager(unsigned nodes); + ~bdd_manager(); + + void set_max_num_nodes(unsigned n) { m_max_num_bdd_nodes = n; } + + bdd mk_var(unsigned i); + bdd mk_nvar(unsigned i); + + bdd mk_true(); + bdd mk_false(); + + bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_exists(unsigned v, bdd const& b); + bdd mk_forall(unsigned v, bdd const& b); + bdd mk_iff(bdd const& a, bdd const& b); + bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); + std::ostream& display(std::ostream& out); }; + + class bdd { + friend class bdd_manager; + unsigned root; + bdd_manager* m; + bdd(unsigned root, bdd_manager* m); + public: + bdd(bdd & other); + bdd(bdd && other); + bdd& operator=(bdd const& other); + ~bdd(); + bdd lo() const; + bdd hi() const; + unsigned var() const; + bool is_true() const; + bool is_false() const; + + bdd operator!(); + bdd operator&&(bdd const& other); + bdd operator||(bdd const& other); + bdd operator|=(bdd const& other) { return *this = *this || other; } + bdd operator&=(bdd const& other) { return *this = *this && other; } + std::ostream& display(std::ostream& out) const; + bool operator==(bdd const& other) const { return root == other.root; } + bool operator!=(bdd const& other) const { return root != other.root; } + double cnf_size() const; + double dnf_size() const; + }; + + std::ostream& operator<<(std::ostream& out, bdd const& b); + } + #endif diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 764c193b3..a5ca80a32 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -23,9 +23,9 @@ Revision History: namespace sat{ - elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20,10000) { + elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) { m_mark_lim = 0; - m_max_literals = 13; // p.resolution_occ_cutoff(); + m_max_literals = 11; } bool elim_vars::operator()(bool_var v) { @@ -54,7 +54,7 @@ namespace sat{ // associate index with each variable. sort_marked(); bdd b1 = elim_var(v); - double sz1 = m.cnf_size(b1); + double sz1 = b1.cnf_size(); if (sz1 > 2*clause_size) { return false; } @@ -63,13 +63,13 @@ namespace sat{ } m_vars.reverse(); bdd b2 = elim_var(v); - double sz2 = m.cnf_size(b2); + double sz2 = b2.cnf_size(); if (sz2 <= clause_size) { return elim_var(v, b2); } shuffle_vars(); bdd b3 = elim_var(v); - double sz3 = m.cnf_size(b3); + double sz3 = b3.cnf_size(); if (sz3 <= clause_size) { return elim_var(v, b3); } @@ -91,6 +91,7 @@ namespace sat{ simp.save_clauses(mc_entry, simp.m_pos_cls); simp.save_clauses(mc_entry, simp.m_neg_cls); s.m_eliminated[v] = true; + ++s.m_stats.m_elim_var_bdd; simp.remove_bin_clauses(pos_l); simp.remove_bin_clauses(neg_l); simp.remove_clauses(pos_occs, pos_l); @@ -152,33 +153,6 @@ namespace sat{ tout << m.cnf_size(b) << "\n"; ); -#if 0 - TRACE("elim_vars", - clause_vector clauses; - literal_vector units; - get_clauses(b0, lits, clauses, units); - for (clause* c : clauses) - tout << *c << "\n"; - for (literal l : units) - tout << l << "\n"; - for (clause* c : clauses) - s.m_cls_allocator.del_clause(c); - SASSERT(lits.empty()); - clauses.reset(); - units.reset(); - tout << "after elim:\n"; - get_clauses(b, lits, clauses, units); - for (clause* c : clauses) - tout << *c << "\n"; - for (literal l : units) - tout << l << "\n"; - for (clause* c : clauses) - s.m_cls_allocator.del_clause(c); - SASSERT(lits.empty()); - clauses.reset(); - ); -#endif - return b; } @@ -194,15 +168,15 @@ namespace sat{ switch (c.size()) { case 0: - UNREACHABLE(); + s.set_conflict(justification()); break; case 1: simp.propagate_unit(c[0]); break; case 2: s.m_stats.m_mk_bin_clause++; - simp.add_non_learned_binary_clause(c[0],c[1]); - simp.back_subsumption1(c[0],c[1], false); + simp.add_non_learned_binary_clause(c[0], c[1]); + simp.back_subsumption1(c[0], c[1], false); break; default: { if (c.size() == 3) diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index 8f7ec1bb4..8893bbc40 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -27,7 +27,6 @@ namespace sat { class simplifier; class elim_vars { - friend class simplifier; class compare_occ; simplifier& simp; diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index e9d047086..d4a994d0f 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -226,13 +226,8 @@ namespace sat { unsigned model_converter::max_var(unsigned min) const { unsigned result = min; - vector::const_iterator it = m_entries.begin(); - vector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - literal_vector::const_iterator lvit = it->m_clauses.begin(); - literal_vector::const_iterator lvend = it->m_clauses.end(); - for (; lvit != lvend; ++lvit) { - literal l = *lvit; + for (entry const& e : m_entries) { + for (literal l : e.m_clauses) { if (l != null_literal) { if (l.var() > result) result = l.var(); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 688510153..6ad88a31b 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -330,19 +330,15 @@ namespace sat { cs.set_end(it2); } - void simplifier::mark_all_but(clause const & c, literal l) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - if (c[i] == l) - continue; - mark_visited(c[i]); - } + void simplifier::mark_all_but(clause const & c, literal l1) { + for (literal l2 : c) + if (l2 != l1) + mark_visited(l2); } void simplifier::unmark_all(clause const & c) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) - unmark_visited(c[i]); + for (literal l : c) + unmark_visited(l); } /** @@ -952,7 +948,7 @@ namespace sat { } bool process_var(bool_var v) { - return !s.s.is_assumption(v) && !s.was_eliminated(v); + return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v); } void operator()(unsigned num_vars) { @@ -971,6 +967,108 @@ namespace sat { } } + // + // Resolve intersection + // Find literals that are in the intersection of all resolvents with l. + // + void ri(literal l, literal_vector& inter) { + if (!process_var(l.var())) return; + bool first = true; + for (watched & w : s.get_wlist(~l)) { + if (w.is_binary_non_learned_clause()) { + literal lit = w.get_literal(); + if (s.is_marked(~lit)) continue; + if (!first) { + inter.reset(); + return; + } + first = false; + inter.push_back(lit); + } + } + clause_use_list & neg_occs = s.m_use_list.get(~l); + clause_use_list::iterator it = neg_occs.mk_iterator(); + while (!it.at_end()) { + bool tautology = false; + clause & c = it.curr(); + for (literal lit : c) { + if (s.is_marked(~lit)) { + tautology = true; + break; + } + } + if (!tautology) { + if (first) { + for (literal lit : c) { + if (lit != ~l) inter.push_back(lit); + } + first = false; + } + else { + unsigned j = 0; + unsigned sz = inter.size(); + for (unsigned i = 0; i < sz; ++i) { + literal lit1 = inter[i]; + for (literal lit2 : c) { + if (lit1 == lit2) { + inter[j++] = lit1; + break; + } + } + } + inter.shrink(j); + if (j == 0) return; + } + } + it.next(); + } + } + + // perform covered clause elimination. + // first extract the covered literal addition (CLA). + // then check whether the CLA is blocked. + bool cce(clause& c, literal lit) { + for (literal l : c) s.mark_visited(l); + literal_vector added, lits; + for (literal l : c) added.push_back(l); + for (unsigned i = 0; i < added.size(); ++i) { + ri(added[i], lits); + for (literal l : lits) { + if (!s.is_marked(l)) { + s.mark_visited(l); + added.push_back(l); + } + } + lits.reset(); + } + s.unmark_visited(lit); + bool is_tautology = (added.size() > c.size()) && all_tautology(lit); + for (literal l : added) s.unmark_visited(l); + return is_tautology; + } + + bool cce(literal lit, literal l2) { + literal_vector added, lits; + s.mark_visited(lit); + s.mark_visited(l2); + added.push_back(lit); + added.push_back(l2); + for (unsigned i = 0; i < added.size(); ++i) { + ri(added[i], lits); + for (literal l : lits) { + if (!s.is_marked(l)) { + s.mark_visited(l); + added.push_back(l); + } + } + lits.reset(); + } + s.unmark_visited(lit); + bool is_tautology = added.size() > 2 && all_tautology(lit); + for (literal l : added) s.unmark_visited(l); + return is_tautology; + } + void process(literal l) { TRACE("blocked_clause", tout << "processing: " << l << "\n";); model_converter::entry * new_entry = 0; @@ -988,21 +1086,14 @@ namespace sat { SASSERT(c.contains(l)); s.mark_all_but(c, l); if (all_tautology(l)) { - 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); + block_clause(c, l, new_entry); s.m_num_blocked_clauses++; - mc.insert(*new_entry, c); - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - literal lit = c[i]; - if (lit != l && process_var(lit.var())) { - m_queue.decreased(~lit); - } - } + s.unmark_all(c); + } + else if (cce(c, l)) { + block_clause(c, l, new_entry); + s.m_num_covered_clauses++; } - s.unmark_all(c); it.next(); } } @@ -1024,13 +1115,12 @@ namespace sat { literal l2 = it->get_literal(); s.mark_visited(l2); if (all_tautology(l)) { - if (new_entry == 0) - new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); - TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";); - s.remove_bin_clause_half(l2, l, it->is_learned()); + block_binary(it, l, new_entry); s.m_num_blocked_clauses++; - m_queue.decreased(~l2); - mc.insert(*new_entry, l, l2); + } + else if (cce(l, l2)) { + block_binary(it, l, new_entry); + s.m_num_covered_clauses++; } else { *it2 = *it; @@ -1042,6 +1132,29 @@ namespace sat { } } + void 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); + } + } + } + + void 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())); + TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";); + literal l2 = it->get_literal(); + s.remove_bin_clause_half(l2, l, it->is_learned()); + m_queue.decreased(~l2); + mc.insert(*new_entry, l, l2); + } + bool all_tautology(literal l) { watch_list & wlist = s.get_wlist(l); m_counter -= wlist.size(); @@ -1083,9 +1196,11 @@ namespace sat { simplifier & m_simplifier; stopwatch m_watch; unsigned m_num_blocked_clauses; + unsigned m_num_covered_clauses; blocked_cls_report(simplifier & s): m_simplifier(s), - m_num_blocked_clauses(s.m_num_blocked_clauses) { + m_num_blocked_clauses(s.m_num_blocked_clauses), + m_num_covered_clauses(s.m_num_covered_clauses) { m_watch.start(); } @@ -1094,6 +1209,8 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses " << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) + << " :elim-covered-clauses " + << (m_simplifier.m_num_covered_clauses - m_num_covered_clauses) << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } @@ -1379,6 +1496,7 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; // eliminate variable + ++s.m_stats.m_elim_var_res; model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); save_clauses(mc_entry, m_neg_cls); @@ -1463,7 +1581,6 @@ namespace sat { order_vars_for_elim(vars); sat::elim_vars elim_bdd(*this); - std::cout << "vars to elim: " << vars.size() << "\n"; for (bool_var v : vars) { checkpoint(); if (m_elim_counter < 0) @@ -1471,11 +1588,9 @@ namespace sat { if (try_eliminate(v)) { m_num_elim_vars++; } -#if 1 else if (elim_bdd(v)) { m_num_elim_vars++; } -#endif } m_pos_cls.finalize(); @@ -1512,12 +1627,13 @@ namespace sat { st.update("subsumed", m_num_subsumed); st.update("subsumption resolution", m_num_sub_res); st.update("elim literals", m_num_elim_lits); - st.update("elim bool vars", m_num_elim_vars); st.update("elim blocked clauses", m_num_blocked_clauses); + st.update("elim covered clauses", m_num_covered_clauses); } void simplifier::reset_statistics() { m_num_blocked_clauses = 0; + m_num_covered_clauses = 0; m_num_subsumed = 0; m_num_sub_res = 0; m_num_elim_lits = 0; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 6ef0f8f18..fdfabb513 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -90,6 +90,7 @@ namespace sat { // stats unsigned m_num_blocked_clauses; + unsigned m_num_covered_clauses; unsigned m_num_subsumed; unsigned m_num_elim_vars; unsigned m_num_sub_res; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8004c9635..ca1fc7801 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -4038,6 +4038,8 @@ namespace sat { st.update("dyn subsumption resolution", m_dyn_sub_res); st.update("blocked correction sets", m_blocked_corr_sets); st.update("units", m_units); + st.update("elim bool vars", m_elim_var_res); + st.update("elim bool vars bdd", m_elim_var_bdd); } void stats::reset() { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 56071182b..58d2824c7 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -67,6 +67,8 @@ namespace sat { unsigned m_dyn_sub_res; unsigned m_non_learned_generation; unsigned m_blocked_corr_sets; + unsigned m_elim_var_res; + unsigned m_elim_var_bdd; unsigned m_units; stats() { reset(); } void reset(); diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index f3f6e6b8d..6826df35e 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -2,7 +2,7 @@ namespace sat { static void test1() { - bdd_manager m(20, 1000); + bdd_manager m(20); bdd v0 = m.mk_var(0); bdd v1 = m.mk_var(1); bdd v2 = m.mk_var(2); @@ -10,17 +10,17 @@ namespace sat { bdd c2 = v2 && v0 && v1; std::cout << c1 << "\n"; SASSERT(c1 == c2); - std::cout << "cnf size: " << m.cnf_size(c1) << "\n"; + std::cout << "cnf size: " << c1.cnf_size() << "\n"; c1 = v0 || v1 || v2; c2 = v2 || v1 || v0; std::cout << c1 << "\n"; SASSERT(c1 == c2); - std::cout << "cnf size: " << m.cnf_size(c1) << "\n"; + std::cout << "cnf size: " << c1.cnf_size() << "\n"; } static void test2() { - bdd_manager m(20, 1000); + bdd_manager m(20); bdd v0 = m.mk_var(0); bdd v1 = m.mk_var(1); bdd v2 = m.mk_var(2); @@ -35,7 +35,7 @@ namespace sat { } static void test3() { - bdd_manager m(20, 1000); + bdd_manager m(20); bdd v0 = m.mk_var(0); bdd v1 = m.mk_var(1); bdd v2 = m.mk_var(2); From 00a401260e65557ceb7c6b410963a49c4365e376 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Oct 2017 21:19:02 -0700 Subject: [PATCH 10/21] fixing cce Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 90 +++++++++++++++++++------------------- 1 file changed, 46 insertions(+), 44 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 6ad88a31b..4bc42e76c 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -971,16 +971,16 @@ namespace sat { // Resolve intersection // Find literals that are in the intersection of all resolvents with l. // - void ri(literal l, literal_vector& inter) { - if (!process_var(l.var())) return; + bool ri(literal l, literal_vector& inter) { + if (!process_var(l.var())) return false; bool first = true; - for (watched & w : s.get_wlist(~l)) { + for (watched & w : s.get_wlist(l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); - if (s.is_marked(~lit)) continue; + if (s.is_marked(~lit) && lit != ~l) continue; if (!first) { inter.reset(); - return; + return false; } first = false; inter.push_back(lit); @@ -992,7 +992,7 @@ namespace sat { bool tautology = false; clause & c = it.curr(); for (literal lit : c) { - if (s.is_marked(~lit)) { + if (s.is_marked(~lit) && lit != ~l) { tautology = true; break; } @@ -1017,56 +1017,58 @@ namespace sat { } } inter.shrink(j); - if (j == 0) return; + if (j == 0) return false; } } it.next(); } + return first; + } + + literal_vector m_added; + literal_vector m_intersection; + + bool cla(literal lit) { + bool is_tautology = false; + for (literal l : m_added) s.mark_visited(l); + unsigned num_iterations = 0, sz; + 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) { + is_tautology = true; + break; + } + for (literal l : m_intersection) { + if (!s.is_marked(l)) { + s.mark_visited(l); + m_added.push_back(l); + } + } + m_intersection.reset(); + } + } + while (m_added.size() > sz && !is_tautology); + for (literal l : m_added) s.unmark_visited(l); + m_intersection.reset(); + m_added.reset(); + if (is_tautology) std::cout << "taut: " << num_iterations << "\n"; + return is_tautology; } // perform covered clause elimination. // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. bool cce(clause& c, literal lit) { - for (literal l : c) s.mark_visited(l); - literal_vector added, lits; - for (literal l : c) added.push_back(l); - for (unsigned i = 0; i < added.size(); ++i) { - ri(added[i], lits); - for (literal l : lits) { - if (!s.is_marked(l)) { - s.mark_visited(l); - added.push_back(l); - } - } - lits.reset(); - } - s.unmark_visited(lit); - bool is_tautology = (added.size() > c.size()) && all_tautology(lit); - for (literal l : added) s.unmark_visited(l); - return is_tautology; + for (literal l : c) m_added.push_back(l); + return cla(lit); } bool cce(literal lit, literal l2) { - literal_vector added, lits; - s.mark_visited(lit); - s.mark_visited(l2); - added.push_back(lit); - added.push_back(l2); - for (unsigned i = 0; i < added.size(); ++i) { - ri(added[i], lits); - for (literal l : lits) { - if (!s.is_marked(l)) { - s.mark_visited(l); - added.push_back(l); - } - } - lits.reset(); - } - s.unmark_visited(lit); - bool is_tautology = added.size() > 2 && all_tautology(lit); - for (literal l : added) s.unmark_visited(l); - return is_tautology; + m_added.push_back(lit); + m_added.push_back(l2); + return cla(lit); } void process(literal l) { @@ -1086,9 +1088,9 @@ namespace sat { SASSERT(c.contains(l)); s.mark_all_but(c, l); if (all_tautology(l)) { + s.unmark_all(c); block_clause(c, l, new_entry); s.m_num_blocked_clauses++; - s.unmark_all(c); } else if (cce(c, l)) { block_clause(c, l, new_entry); From d9ccb3928ec67b4d0bca29847053d822173172b4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Oct 2017 09:05:25 -0700 Subject: [PATCH 11/21] fix debug build Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.h | 3 +-- src/sat/sat_elim_vars.cpp | 3 +-- src/sat/sat_simplifier.cpp | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index c0f1fc9b2..10caa0125 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -166,8 +166,6 @@ namespace sat { bdd mk_and(bdd const& a, bdd const& b); bdd mk_or(bdd const& a, bdd const& b); - std::ostream& display(std::ostream& out, bdd const& b); - public: struct mem_out {}; @@ -190,6 +188,7 @@ namespace sat { bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); std::ostream& display(std::ostream& out); + std::ostream& display(std::ostream& out, bdd const& b); }; class bdd { diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index a5ca80a32..6edc125ea 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -121,7 +121,6 @@ namespace sat{ bdd b = m.mk_exists(m_var2index[v], b0); TRACE("elim_vars", tout << "eliminate " << v << "\n"; - tout << "clauses : " << clause_size << "\n"; for (watched const& w : simp.get_wlist(~pos_l)) { if (w.is_binary_non_learned_clause()) { tout << pos_l << " " << w.get_literal() << "\n"; @@ -150,7 +149,7 @@ namespace sat{ m.display(tout, b4); tout << "eliminated:\n"; tout << b << "\n"; - tout << m.cnf_size(b) << "\n"; + tout << b.cnf_size() << "\n"; ); return b; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 4bc42e76c..3bd5cefb9 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1150,8 +1150,8 @@ namespace sat { void 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())); - TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";); 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); From da4e8118b2220d81662116d182c2cb11846f5fc6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Oct 2017 17:58:56 -0700 Subject: [PATCH 12/21] adding elim sequences Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 25 ++++++++++++++++++++++++- src/sat/sat_model_converter.h | 26 ++++++++++++++++++++++++-- 2 files changed, 48 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index d4a994d0f..471d314c1 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -49,16 +49,35 @@ namespace sat { // and the following procedure flips its value. 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; } sat = false; + ++index; continue; } + prev = l; if (sat) continue; @@ -136,15 +155,17 @@ namespace sat { return e; } - void model_converter::insert(entry & e, clause const & c) { + void model_converter::insert(entry & e, clause const & c, elim_sequence* s) { 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); 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); @@ -152,6 +173,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); TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";); } @@ -163,6 +185,7 @@ 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); // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index aae3ad479..c5cefe84e 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -20,6 +20,7 @@ Revision History: #define SAT_MODEL_CONVERTER_H_ #include "sat/sat_types.h" +#include "util/ref_vector.h" namespace sat { /** @@ -36,19 +37,40 @@ namespace sat { it can be converted into a general Z3 model_converter */ class model_converter { + public: + class elim_sequence { + unsigned m_refcount; + elim_sequence* m_next; + literal m_literal; + literal_vector m_clause; + public: + elim_sequence(literal l, literal_vector const& clause, elim_sequence* next): + m_refcount(0), + m_next(next), + m_literal(l), + m_clause(clause) { + if (m_next) m_next->inc_ref(); + } + ~elim_sequence() { if (m_next) m_next->dec_ref(); } + void inc_ref() { ++m_refcount; } + void dec_ref() { if (0 == --m_refcount) dealloc(this); } + }; + enum kind { ELIM_VAR = 0, BLOCK_LIT }; class entry { friend class model_converter; 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; 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_clauses(src.m_clauses), + m_elim_sequence(src.m_elim_sequence) { } bool_var var() const { return m_var; } kind get_kind() const { return static_cast(m_kind); } @@ -62,7 +84,7 @@ namespace sat { model_converter& operator=(model_converter const& other); entry & mk(kind k, bool_var v); - void insert(entry & e, clause const & c); + void insert(entry & e, clause const & c, elim_sequence* s = nullptr); void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); From 42e9a0156b6a383f6ec5c9161026f38be6d0a18e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Oct 2017 04:52:06 -0700 Subject: [PATCH 13/21] add elimination stack for model reconstruction Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 53 ++++++++++++++++++++++++++- src/sat/sat_model_converter.cpp | 60 ++++++++++++++++++------------ src/sat/sat_model_converter.h | 26 ++++++------- src/sat/sat_simplifier.cpp | 65 +++++++++++++++++++++++---------- 4 files changed, 145 insertions(+), 59 deletions(-) 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) { From 43f82144536ed14f362b8daa7dd46f73938316a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Oct 2017 13:25:08 -0700 Subject: [PATCH 14/21] local Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 105 ++++++++++++++++++++++++++++++++------------ src/sat/sat_bdd.h | 9 ++++ src/util/vector.h | 2 +- 3 files changed, 88 insertions(+), 28 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index d88b28e74..52a362728 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -43,6 +43,8 @@ namespace sat { m_max_num_bdd_nodes = 1 << 24; // up to 16M nodes m_mark_level = 0; alloc_free_nodes(1024 + num_vars); + m_disable_gc = false; + m_is_new_node = false; // add variables for (unsigned i = 0; i < num_vars; ++i) { @@ -203,6 +205,7 @@ namespace sat { } bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) { + m_is_new_node = false; if (l == r) { return l; } @@ -214,7 +217,7 @@ namespace sat { } e->get_data().m_refcount = 0; bool do_gc = m_free_nodes.empty(); - if (do_gc) { + if (do_gc && !m_disable_gc) { gc(); e = m_node_table.insert_if_not_there2(n); e->get_data().m_refcount = 0; @@ -223,15 +226,14 @@ namespace sat { if (m_nodes.size() > m_max_num_bdd_nodes) { throw mem_out(); } - e->get_data().m_index = m_nodes.size(); - m_nodes.push_back(e->get_data()); alloc_free_nodes(m_nodes.size()/2); } - else { - e->get_data().m_index = m_free_nodes.back(); - m_nodes[e->get_data().m_index] = e->get_data(); - m_free_nodes.pop_back(); - } + + SASSERT(!m_free_nodes.empty()); + e->get_data().m_index = m_free_nodes.back(); + m_nodes[e->get_data().m_index] = e->get_data(); + m_free_nodes.pop_back(); + m_is_new_node = true; return e->get_data().m_index; } @@ -241,10 +243,45 @@ namespace sat { void bdd_manager::sift_up(unsigned lvl) { // exchange level and level + 1. -#if 0 - m_relevel.reset(); // nodes to be re-leveled. + m_S.reset(); + m_T.reset(); + m_disable_gc = true; for (unsigned n : m_level2nodes[lvl + 1]) { + BDD l = lo(n); + BDD h = hi(n); + if (l == 0 && h == 0) continue; + if ((is_const(l) || level(l) != lvl) && + (is_const(h) || level(h) != lvl)) { + m_S.push_back(n); + } + else { + m_T.push_back(n); + } + m_node_table.remove(m_nodes[n]); + } + + for (unsigned n : m_level2nodes[lvl]) { + bdd_node& node = m_nodes[n]; + m_node_table.remove(node); + if (m_max_parent[n] == lvl + 1 && node.m_refcount == 0) { + node.set_internal(); + m_free_nodes.push_back(n); + } + else { + node.m_level = lvl + 1; + m_node_table.insert(node); + } + } + + for (unsigned n : m_S) { + m_nodes[n].m_level = lvl; + m_node_table.insert(m_nodes[n]); + } + + std::swap(m_level2nodes[lvl], m_level2nodes[lvl + 1]); + + for (unsigned n : m_T) { BDD l = lo(n); BDD h = hi(n); if (l == 0 && h == 0) continue; @@ -264,28 +301,42 @@ namespace sat { 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); + unsigned ac = make_node(lvl, a, c); + if (is_new_node()) { + m_level2nodes[lvl].push_back(ac); + m_max_parent.setx(ac, lvl + 1, 0); + } + unsigned bd = make_node(lvl, b, d); + if (is_new_node()) { + m_level2nodes[lvl].push_back(bd); + m_max_parent.setx(bd, lvl + 1, 0); + } + m_nodes[n].m_lo = ac; + m_nodes[n].m_hi = bd; 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]]; - } + m_disable_gc = false; + } + + void bdd_manager::init_reorder() { + m_level2nodes.reset(); + unsigned sz = m_nodes.size(); + m_max_parent.fill(sz, 0); + for (unsigned i = 0; i < m_level2var.size(); ++i) { + m_level2nodes.push_back(unsigned_vector()); + } + for (unsigned i = 0; i < sz; ++i) { + bdd_node const& n = m_nodes[i]; + if (n.is_internal()) continue; + SASSERT(i == m_nodes[i].m_index); + m_level2nodes[n.m_level].push_back(i); + m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], n.m_level); + m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], n.m_level); } -#endif } bdd bdd_manager::mk_var(unsigned i) { @@ -498,7 +549,7 @@ 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_nodes[i].set_internal(); m_free_nodes.push_back(i); } } @@ -559,7 +610,7 @@ namespace sat { std::ostream& bdd_manager::display(std::ostream& out) { for (unsigned i = 0; i < m_nodes.size(); ++i) { bdd_node const& n = m_nodes[i]; - if (n.m_lo == 0 && n.m_hi == 0) continue; + if (n.is_internal()) continue; out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; } return out; diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 10caa0125..f38c26d21 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -57,6 +57,8 @@ namespace sat { BDD m_hi; unsigned m_index; unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } + bool is_internal() const { return m_lo == 0 && m_hi == 0; } + void set_internal() { m_lo = m_hi = 0; } }; struct hash_node { @@ -112,9 +114,15 @@ namespace sat { mutable unsigned m_mark_level; mutable svector m_count; mutable svector m_todo; + bool m_disable_gc; + bool m_is_new_node; unsigned m_max_num_bdd_nodes; + unsigned_vector m_S, m_T; // used for reordering + vector m_level2nodes; + unsigned_vector m_max_parent; BDD make_node(unsigned level, BDD l, BDD r); + bool is_new_node() const { return m_is_new_node; } BDD apply_const(BDD a, BDD b, bdd_op op); BDD apply(BDD arg1, BDD arg2, bdd_op op); @@ -142,6 +150,7 @@ namespace sat { bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; } void try_reorder(); + void init_reorder(); void sift_up(unsigned level); static const BDD false_bdd = 0; diff --git a/src/util/vector.h b/src/util/vector.h index 2e2640de3..c60585512 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -410,7 +410,7 @@ public: void fill(unsigned sz, T const & elem) { resize(sz); - fill(sz, elem); + fill(elem); } bool contains(T const & elem) const { From e0e7836c121c3daa587d716767cc4bff575a4abc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Oct 2017 14:20:49 -0700 Subject: [PATCH 15/21] working on BDD reordering Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 85 +++++++++++++++++++++++++++++++++++---- src/sat/sat_bdd.h | 3 ++ src/sat/sat_lookahead.cpp | 30 +------------- 3 files changed, 82 insertions(+), 36 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 52a362728..1073f482e 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -238,10 +238,82 @@ namespace sat { } void bdd_manager::try_reorder() { - // TBD + init_reorder(); + for (unsigned i = 0; i < m_var2level.size(); ++i) { + sift_var(i); + } + } + + double bdd_manager::current_cost() { +#if 0 + +#endif + return m_nodes.size() - m_free_nodes.size(); + } + + bool bdd_manager::is_bad_cost(double current_cost, double best_cost) const { + return current_cost > 1.1 * best_cost; + } + + void bdd_manager::sift_var(unsigned v) { + unsigned lvl = m_var2level[v]; + unsigned start = lvl; + double best_cost = current_cost(); + bool first = true; + unsigned max_lvl = m_level2nodes.size()-1; + if (lvl*2 < max_lvl) { + goto go_down; + } + go_up: + while (lvl < max_lvl) { + sift_up(lvl); + ++lvl; + double cost = current_cost(); + if (is_bad_cost(cost, best_cost)) break; + best_cost = std::min(cost, best_cost); + } + if (first) { + first = false; + while (lvl != start) { + sift_up(lvl-1); + --lvl; + } + goto go_down; + } + else { + while (current_cost() != best_cost) { + sift_up(lvl-1); + --lvl; + } + return; + } + go_down: + while (lvl > 0) { + sift_up(lvl-1); + --lvl; + double cost = current_cost(); + if (is_bad_cost(cost, best_cost)) break; + best_cost = std::min(cost, best_cost); + } + if (first) { + first = false; + while (lvl != start) { + sift_up(lvl); + ++lvl; + } + goto go_up; + } + else { + while (current_cost() != best_cost) { + sift_up(lvl); + ++lvl; + } + return; + } } void bdd_manager::sift_up(unsigned lvl) { + if (m_level2nodes[lvl].empty()) return; // exchange level and level + 1. m_S.reset(); m_T.reset(); @@ -326,16 +398,15 @@ namespace sat { m_level2nodes.reset(); unsigned sz = m_nodes.size(); m_max_parent.fill(sz, 0); - for (unsigned i = 0; i < m_level2var.size(); ++i) { - m_level2nodes.push_back(unsigned_vector()); - } for (unsigned i = 0; i < sz; ++i) { bdd_node const& n = m_nodes[i]; if (n.is_internal()) continue; + unsigned lvl = n.m_level; SASSERT(i == m_nodes[i].m_index); - m_level2nodes[n.m_level].push_back(i); - m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], n.m_level); - m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], n.m_level); + while (m_level2nodes.size() <= lvl) m_level2nodes.push_back(unsigned_vector()); + m_level2nodes[lvl].push_back(i); + m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], lvl); + m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], lvl); } } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index f38c26d21..dbd19ec61 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -152,6 +152,9 @@ namespace sat { void try_reorder(); void init_reorder(); void sift_up(unsigned level); + void sift_var(unsigned v); + double current_cost(); + bool is_bad_cost(double new_cost, double best_cost) const; static const BDD false_bdd = 0; static const BDD true_bdd = 1; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index edb881aa4..f607d53ad 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1445,35 +1445,7 @@ namespace sat { m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2); break; case ternary_reward: - if (nonfixed == 2) { - literal l1 = null_literal; - literal l2 = null_literal; - for (literal lit : *n) { - if (!is_fixed(lit)) { - if (l1 == null_literal) { - l1 = lit; - } - else { - SASSERT(l2 != null_literal); - l2 = lit; - break; - } - } - } - if (l1 == null_literal) { - set_conflict(); - continue; - } - else if (l2 == null_literal) { - propagated(l1); - } - else { - m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()]; - } - } - else { - m_lookahead_reward += (double)0.001; - } + UNREACHABLE(); break; case unit_literal_reward: break; From 8811d784154b0eaf64aa72137d097d66123df4ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Oct 2017 21:28:48 -0700 Subject: [PATCH 16/21] compress elimination stack representation Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 22 +++--- src/sat/sat_model_converter.h | 12 +-- src/sat/sat_simplifier.cpp | 128 ++++++++++++++++++++++---------- 3 files changed, 108 insertions(+), 54 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c79cd2944..14443a2f7 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -38,16 +38,15 @@ namespace sat { return *this; } - void model_converter::process_stack(model & m, literal_vector const& stack) const { + void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv 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 + for (unsigned i = sz; i-- > 0; ) { + unsigned csz = stack[i].first; + literal lit = stack[i].second; bool sat = false; - for (; i > 0 && stack[--i] != null_literal;) { - if (sat) continue; - sat = value_at(stack[i], m) == l_true; + for (unsigned j = 0; !sat && j < csz; ++j) { + sat = value_at(c[j], m) == l_true; } if (!sat) { m[lit.var()] = lit.sign() ? l_false : l_true; @@ -66,6 +65,7 @@ namespace sat { bool sat = false; bool var_sign = false; unsigned index = 0; + literal_vector clause; for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause @@ -74,13 +74,15 @@ namespace sat { } elim_stack* s = it->m_elim_stack[index]; if (s) { - process_stack(m, s->stack()); + process_stack(m, clause, s->stack()); } sat = false; ++index; + clause.reset(); continue; } + clause.push_back(l); if (sat) continue; bool sign = l.sign(); @@ -190,13 +192,13 @@ namespace sat { // 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) { + void model_converter::insert(entry & e, literal_vector const& c, elim_stackv 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)); + e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims)); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 00fd637b7..dcbe450a8 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -39,18 +39,20 @@ namespace sat { class model_converter { public: + typedef svector> elim_stackv; + class elim_stack { unsigned m_refcount; - literal_vector m_stack; + elim_stackv m_stack; public: - elim_stack(literal_vector const& stack): + elim_stack(elim_stackv const& stack): m_refcount(0), m_stack(stack) { } ~elim_stack() { } void inc_ref() { ++m_refcount; } void dec_ref() { if (0 == --m_refcount) dealloc(this); } - literal_vector const& stack() const { return m_stack; } + elim_stackv const& stack() const { return m_stack; } }; enum kind { ELIM_VAR = 0, BLOCK_LIT }; @@ -74,7 +76,7 @@ namespace sat { private: vector m_entries; - void process_stack(model & m, literal_vector const& stack) const; + void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const; public: model_converter(); @@ -86,7 +88,7 @@ namespace sat { 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); + void insert(entry & c, literal_vector const& covered_clause, elim_stackv 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 b09d180c0..b967ade06 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -965,6 +965,7 @@ namespace sat { literal l = m_queue.next(); process(l); } + cce(); } // @@ -1027,55 +1028,106 @@ namespace sat { literal_vector m_covered_clause; literal_vector m_intersection; - literal_vector m_elim_stack; + sat::model_converter::elim_stackv m_elim_stack; + unsigned m_ala_qhead; - bool cla(literal lit) { + /* + * C \/ l l \/ lit + * ------------------- + * C \/ l \/ ~lit + */ + void add_ala() { + for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) { + literal l = m_covered_clause[m_ala_qhead]; + for (watched & w : s.get_wlist(~l)) { + if (w.is_binary_clause()) { + literal lit = w.get_literal(); + if (!s.is_marked(lit) && !s.is_marked(~lit)) { + //std::cout << "ALA " << ~lit << "\n"; + m_covered_clause.push_back(~lit); + s.mark_visited(~lit); + } + } + } + } + } + + bool add_cla(literal& blocked) { + for (unsigned i = 0; i < m_covered_clause.size(); ++i) { + m_intersection.reset(); + if (ri(m_covered_clause[i], m_intersection)) { + blocked = m_covered_clause[i]; + return true; + } + for (literal l : m_intersection) { + if (!s.is_marked(l)) { + s.mark_visited(l); + m_covered_clause.push_back(l); + } + } + if (!m_intersection.empty()) { + m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i])); + } + } + return false; + } + + bool cla(literal& blocked) { bool is_tautology = false; for (literal l : m_covered_clause) s.mark_visited(l); unsigned num_iterations = 0, sz; m_elim_stack.reset(); + m_ala_qhead = 0; do { - ++num_iterations; - 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_covered_clause.push_back(l); - } - } - 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 - } + do { + ++num_iterations; + sz = m_covered_clause.size(); + is_tautology = add_cla(blocked); } + while (m_covered_clause.size() > sz && !is_tautology); + break; + //if (is_tautology) break; + //sz = m_covered_clause.size(); + // unsound? add_ala(); } - while (m_covered_clause.size() > sz && !is_tautology); + while (m_covered_clause.size() > sz); for (literal l : m_covered_clause) s.unmark_visited(l); - if (is_tautology) std::cout << "taut: " << num_iterations << "\n"; + // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n"; return is_tautology; } // perform covered clause elimination. // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. - bool cce(clause& c, literal lit) { + bool cce(clause& c, literal& blocked) { m_covered_clause.reset(); for (literal l : c) m_covered_clause.push_back(l); - return cla(lit); + return cla(blocked); } - bool cce(literal lit, literal l2) { + bool cce(literal lit, literal l2, literal& blocked) { m_covered_clause.reset(); m_covered_clause.push_back(lit); m_covered_clause.push_back(l2); - return cla(lit); + return cla(blocked); + } + + void cce() { + m_to_remove.reset(); + literal blocked; + for (clause* cp : s.s.m_clauses) { + clause& c = *cp; + if (c.was_removed()) continue; + if (cce(c, blocked)) { + model_converter::entry * new_entry = 0; + block_covered_clause(c, blocked, new_entry); + s.m_num_covered_clauses++; + } + } + for (clause* c : m_to_remove) { + s.remove_clause(*c); + } + m_to_remove.reset(); } void process(literal l) { @@ -1085,6 +1137,7 @@ namespace sat { return; } + literal blocked = null_literal; m_to_remove.reset(); { clause_use_list & occs = s.m_use_list.get(l); @@ -1095,14 +1148,10 @@ namespace sat { SASSERT(c.contains(l)); s.mark_all_but(c, l); if (all_tautology(l)) { - s.unmark_all(c); block_clause(c, l, new_entry); s.m_num_blocked_clauses++; } - else if (cce(c, l)) { - block_covered_clause(c, l, new_entry); - s.m_num_covered_clauses++; - } + s.unmark_all(c); it.next(); } } @@ -1127,8 +1176,9 @@ namespace sat { block_binary(it, l, new_entry); s.m_num_blocked_clauses++; } - else if (cce(l, l2)) { - block_covered_binary(it, l, new_entry); + else if (cce(l, l2, blocked)) { + model_converter::entry * blocked_entry = 0; + block_covered_binary(it, l, blocked, blocked_entry); s.m_num_covered_clauses++; } else { @@ -1163,9 +1213,9 @@ namespace sat { 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) { + void prepare_block_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { if (new_entry == 0) - new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); + new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.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()); @@ -1173,12 +1223,12 @@ namespace sat { } void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { - prepare_block_binary(it, l, new_entry); + prepare_block_binary(it, l, 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); + void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { + prepare_block_binary(it, l, blocked, new_entry); mc.insert(*new_entry, m_covered_clause, m_elim_stack); } From 80f24c29ab2831576b18d8bea4ac75f03b808ad9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 08:52:03 -0700 Subject: [PATCH 17/21] debugging reordering Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 145 ++++++++++++++++++++++++++++++-------------- src/sat/sat_bdd.h | 46 ++++++++------ src/test/bdd.cpp | 16 +++++ 3 files changed, 144 insertions(+), 63 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 1073f482e..3125b2a3a 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "sat/sat_bdd.h" +#include "util/trace.h" namespace sat { @@ -48,12 +49,7 @@ namespace sat { // add variables for (unsigned i = 0; i < num_vars; ++i) { - m_var2bdd.push_back(make_node(i, false_bdd, true_bdd)); - m_var2bdd.push_back(make_node(i, true_bdd, false_bdd)); - m_nodes[m_var2bdd[2*i]].m_refcount = max_rc; - m_nodes[m_var2bdd[2*i+1]].m_refcount = max_rc; - m_var2level.push_back(i); - m_level2var.push_back(i); + reserve_var(i); } } @@ -73,8 +69,8 @@ namespace sat { return (a == true_bdd && b == true_bdd) ? true_bdd : false_bdd; case bdd_or_op: return (a == true_bdd || b == true_bdd) ? true_bdd : false_bdd; - case bdd_iff_op: - return (a == b) ? true_bdd : false_bdd; + case bdd_xor_op: + return (a == b) ? false_bdd : true_bdd; default: return false_bdd; } @@ -99,7 +95,7 @@ namespace sat { bdd bdd_manager::mk_false() { return bdd(false_bdd, this); } bdd bdd_manager::mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } bdd bdd_manager::mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } - bdd bdd_manager::mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } + bdd bdd_manager::mk_xor(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_xor_op), this); } bdd bdd_manager::mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); } bdd bdd_manager::mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); } @@ -132,10 +128,10 @@ namespace sat { if (is_false(b)) return a; if (is_true(a) || is_true(b)) return true_bdd; break; - case bdd_iff_op: - if (a == b) return true_bdd; - if (is_true(a)) return b; - if (is_true(b)) return a; + case bdd_xor_op: + if (a == b) return false_bdd; + if (is_false(a)) return b; + if (is_false(b)) return a; break; default: UNREACHABLE(); @@ -265,9 +261,9 @@ namespace sat { goto go_down; } go_up: + TRACE("bdd", tout << "sift up " << lvl << "\n";); while (lvl < max_lvl) { - sift_up(lvl); - ++lvl; + sift_up(lvl++); double cost = current_cost(); if (is_bad_cost(cost, best_cost)) break; best_cost = std::min(cost, best_cost); @@ -275,22 +271,20 @@ namespace sat { if (first) { first = false; while (lvl != start) { - sift_up(lvl-1); - --lvl; + sift_up(--lvl); } goto go_down; } else { while (current_cost() != best_cost) { - sift_up(lvl-1); - --lvl; + sift_up(--lvl); } return; } go_down: + TRACE("bdd", tout << "sift down " << lvl << "\n";); while (lvl > 0) { - sift_up(lvl-1); - --lvl; + sift_up(--lvl); double cost = current_cost(); if (is_bad_cost(cost, best_cost)) break; best_cost = std::min(cost, best_cost); @@ -298,15 +292,13 @@ namespace sat { if (first) { first = false; while (lvl != start) { - sift_up(lvl); - ++lvl; + sift_up(lvl++); } goto go_up; } else { while (current_cost() != best_cost) { - sift_up(lvl); - ++lvl; + sift_up(lvl++); } return; } @@ -330,30 +322,37 @@ namespace sat { else { m_T.push_back(n); } + TRACE("bdd", tout << "remove " << n << "\n";); m_node_table.remove(m_nodes[n]); } + m_level2nodes[lvl + 1].reset(); + m_level2nodes[lvl + 1].append(m_T); for (unsigned n : m_level2nodes[lvl]) { bdd_node& node = m_nodes[n]; m_node_table.remove(node); if (m_max_parent[n] == lvl + 1 && node.m_refcount == 0) { + TRACE("bdd", tout << "free " << n << "\n";); node.set_internal(); m_free_nodes.push_back(n); } else { + TRACE("bdd", tout << "set level " << n << " to " << lvl + 1 << "\n";); node.m_level = lvl + 1; m_node_table.insert(node); + m_level2nodes[lvl + 1].push_back(n); } } - + m_level2nodes[lvl].reset(); + m_level2nodes[lvl].append(m_S); + for (unsigned n : m_S) { m_nodes[n].m_level = lvl; m_node_table.insert(m_nodes[n]); } - std::swap(m_level2nodes[lvl], m_level2nodes[lvl + 1]); - for (unsigned n : m_T) { + TRACE("bdd", tout << "transform " << n << "\n";); BDD l = lo(n); BDD h = hi(n); if (l == 0 && h == 0) continue; @@ -392,6 +391,14 @@ namespace sat { std::swap(m_level2var[lvl], m_level2var[lvl+1]); std::swap(m_var2level[v], m_var2level[w]); m_disable_gc = false; + TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); ); + DEBUG_CODE( + for (unsigned i = 0; i < m_level2nodes.size(); ++i) { + for (unsigned n : m_level2nodes[i]) { + bdd_node const& node = m_nodes[n]; + SASSERT(node.m_level == i); + } + }); } void bdd_manager::init_reorder() { @@ -403,18 +410,41 @@ namespace sat { if (n.is_internal()) continue; unsigned lvl = n.m_level; SASSERT(i == m_nodes[i].m_index); - while (m_level2nodes.size() <= lvl) m_level2nodes.push_back(unsigned_vector()); + m_level2nodes.reserve(lvl + 1); m_level2nodes[lvl].push_back(i); m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], lvl); m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], lvl); } + TRACE("bdd", + display(tout); + for (unsigned i = 0; i < sz; ++i) { + bdd_node const& n = m_nodes[i]; + if (n.is_internal()) continue; + unsigned lvl = n.m_level; + tout << "lvl: " << lvl << " parent: " << m_max_parent[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n"; + } + ); + } + + void bdd_manager::reserve_var(unsigned i) { + while (m_var2level.size() <= i) { + unsigned v = m_var2level.size(); + m_var2bdd.push_back(make_node(v, false_bdd, true_bdd)); + m_var2bdd.push_back(make_node(v, true_bdd, false_bdd)); + m_nodes[m_var2bdd[2*v]].m_refcount = max_rc; + m_nodes[m_var2bdd[2*v+1]].m_refcount = max_rc; + m_var2level.push_back(v); + m_level2var.push_back(v); + } } bdd bdd_manager::mk_var(unsigned i) { + reserve_var(i); return bdd(m_var2bdd[2*i], this); } bdd bdd_manager::mk_nvar(unsigned i) { + reserve_var(i); return bdd(m_var2bdd[2*i+1], this); } @@ -581,6 +611,29 @@ namespace sat { return m_count[b.root]; } + unsigned bdd_manager::bdd_size(bdd const& b) { + init_mark(); + set_mark(0); + set_mark(1); + unsigned sz = 0; + m_todo.push_back(b.root); + while (!m_todo.empty()) { + BDD r = m_todo.back(); + m_todo.pop_back(); + if (!is_marked(r)) { + ++sz; + set_mark(r); + if (!is_marked(lo(r))) { + m_todo.push_back(lo(r)); + } + if (!is_marked(hi(r))) { + m_todo.push_back(hi(r)); + } + } + } + return sz; + } + void bdd_manager::alloc_free_nodes(unsigned n) { for (unsigned i = 0; i < n; ++i) { m_free_nodes.push_back(m_nodes.size()); @@ -678,31 +731,35 @@ namespace sat { return out; } + void bdd_manager::well_formed() { + for (unsigned n : m_free_nodes) { + VERIFY(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0); + } + for (bdd_node const& n : m_nodes) { + if (n.is_internal()) continue; + unsigned lvl = n.m_level; + BDD lo = n.m_lo; + BDD hi = n.m_hi; + VERIFY(is_const(lo) || level(lo) < lvl); + VERIFY(is_const(hi) || level(hi) < lvl); + } + } + std::ostream& bdd_manager::display(std::ostream& out) { for (unsigned i = 0; i < m_nodes.size(); ++i) { bdd_node const& n = m_nodes[i]; if (n.is_internal()) continue; out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; } + for (unsigned i = 0; i < m_level2nodes.size(); ++i) { + out << i << " : "; + for (unsigned l : m_level2nodes[i]) out << l << " "; + out << "\n"; + } return out; } - bdd::bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } - bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } - bdd::bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); } - bdd::~bdd() { m->dec_ref(root); } - bdd bdd::lo() const { return bdd(m->lo(root), m); } - bdd bdd::hi() const { return bdd(m->hi(root), m); } - unsigned bdd::var() const { return m->var(root); } - bool bdd::is_true() const { return root == bdd_manager::true_bdd; } - bool bdd::is_false() const { return root == bdd_manager::false_bdd; } - bdd bdd::operator!() { return m->mk_not(*this); } - bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); } - bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); } bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } - std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } - double bdd::cnf_size() const { return m->cnf_size(*this); } - double bdd::dnf_size() const { return m->dnf_size(*this); } } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index dbd19ec61..41e45c822 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -35,7 +35,7 @@ namespace sat { enum bdd_op { bdd_and_op = 2, bdd_or_op = 3, - bdd_iff_op = 4, + bdd_xor_op = 4, bdd_not_op = 5, bdd_and_proj_op = 6, bdd_or_proj_op = 7, @@ -149,7 +149,6 @@ namespace sat { void set_mark(unsigned i) { m_mark[i] = m_mark_level; } bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; } - void try_reorder(); void init_reorder(); void sift_up(unsigned level); void sift_var(unsigned v); @@ -173,10 +172,15 @@ namespace sat { double dnf_size(bdd const& b) { return count(b, 0); } double cnf_size(bdd const& b) { return count(b, 1); } + unsigned bdd_size(bdd const& b); bdd mk_not(bdd b); bdd mk_and(bdd const& a, bdd const& b); bdd mk_or(bdd const& a, bdd const& b); + bdd mk_xor(bdd const& a, bdd const& b); + + void reserve_var(unsigned v); + void well_formed(); public: struct mem_out {}; @@ -196,39 +200,43 @@ namespace sat { bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); bdd mk_exists(unsigned v, bdd const& b); bdd mk_forall(unsigned v, bdd const& b); - bdd mk_iff(bdd const& a, bdd const& b); bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, bdd const& b); + + void try_reorder(); }; class bdd { friend class bdd_manager; unsigned root; bdd_manager* m; - bdd(unsigned root, bdd_manager* m); + bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } public: - bdd(bdd & other); - bdd(bdd && other); + bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } + bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); } bdd& operator=(bdd const& other); - ~bdd(); - bdd lo() const; - bdd hi() const; - unsigned var() const; - bool is_true() const; - bool is_false() const; - - bdd operator!(); - bdd operator&&(bdd const& other); - bdd operator||(bdd const& other); + ~bdd() { m->dec_ref(root); } + bdd lo() const { return bdd(m->lo(root), m); } + bdd hi() const { return bdd(m->hi(root), m); } + unsigned var() const { return m->var(root); } + + bool is_true() const { return root == bdd_manager::true_bdd; } + bool is_false() const { return root == bdd_manager::false_bdd; } + + bdd operator!() { return m->mk_not(*this); } + bdd operator&&(bdd const& other) { return m->mk_and(*this, other); } + bdd operator||(bdd const& other) { return m->mk_or(*this, other); } + bdd operator^(bdd const& other) { return m->mk_xor(*this, other); } bdd operator|=(bdd const& other) { return *this = *this || other; } bdd operator&=(bdd const& other) { return *this = *this && other; } - std::ostream& display(std::ostream& out) const; + std::ostream& display(std::ostream& out) const { return m->display(out, *this); } bool operator==(bdd const& other) const { return root == other.root; } bool operator!=(bdd const& other) const { return root != other.root; } - double cnf_size() const; - double dnf_size() const; + double cnf_size() const { return m->cnf_size(*this); } + double dnf_size() const { return m->dnf_size(*this); } + unsigned bdd_size() const { return m->bdd_size(*this); } }; std::ostream& operator<<(std::ostream& out, bdd const& b); diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 6826df35e..b60522740 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -57,10 +57,26 @@ namespace sat { c2 = m.mk_exists(2, c1); SASSERT(c2 == ((v0 && v1) || v1 || !v0)); } + + void test4() { + bdd_manager m(3); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + bdd c1 = (v0 && v2) || v1; + std::cout << "before reorder:\n"; + std::cout << c1 << "\n"; + std::cout << c1.bdd_size() << "\n"; + m.try_reorder(); + std::cout << "after reorder:\n"; + std::cout << c1 << "\n"; + std::cout << c1.bdd_size() << "\n"; + } } void tst_bdd() { sat::test1(); sat::test2(); sat::test3(); + sat::test4(); } From edea8798641477e3de17863179c9a80be136915d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 08:57:32 -0700 Subject: [PATCH 18/21] expose missed propagations Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 2 +- src/sat/ba_solver.h | 4 ++-- src/sat/sat_lookahead.cpp | 4 +++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index faa9b639e..ab2352253 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1556,7 +1556,7 @@ namespace sat { m_learned.push_back(c); } else { - SASSERT(s().at_base_lvl()); + SASSERT(!m_solver || s().at_base_lvl()); m_constraints.push_back(c); } literal lit = c->lit(); diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 3e02d49dc..09903f889 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -362,8 +362,8 @@ namespace sat { // access solver inline lbool value(bool_var v) const { return value(literal(v, false)); } inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } - inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); } - inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); } + inline unsigned lvl(literal lit) const { return m_lookahead ? 0 : m_solver->lvl(lit); } + inline unsigned lvl(bool_var v) const { return m_lookahead ? 0 : m_solver->lvl(v); } inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); } inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); } inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index f607d53ad..5c039f664 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -408,6 +408,7 @@ namespace sat { } bool lookahead::missed_propagation() const { + if (inconsistent()) return false; for (literal l1 : m_trail) { SASSERT(is_true(l1)); for (literal l2 : m_binary[l1.index()]) { @@ -1614,7 +1615,7 @@ namespace sat { } SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size())); //SASSERT(!missed_conflict()); - //SASSERT(inconsistent() || !missed_propagation()); + VERIFY(!missed_propagation()); TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); } @@ -1656,6 +1657,7 @@ namespace sat { unsat = inconsistent(); pop_lookahead1(lit, num_units); } + // VERIFY(!missed_propagation()); if (unsat) { TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); lookahead_backtrack(); From dc6ed64da1a534fae2cd83a96a63be9776a890f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 17:37:38 -0700 Subject: [PATCH 19/21] testing bdd for elim-vars Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 248 +++++++++++++++++++++++++++++-------- src/sat/sat_bdd.h | 39 +++--- src/sat/sat_elim_vars.cpp | 9 +- src/sat/sat_elim_vars.h | 2 + src/sat/sat_lookahead.cpp | 76 ++---------- src/sat/sat_lookahead.h | 1 + src/sat/sat_simplifier.cpp | 6 +- src/test/bdd.cpp | 1 + src/util/vector.h | 5 + 9 files changed, 254 insertions(+), 133 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 3125b2a3a..e44bf7944 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -23,6 +23,8 @@ Revision History: namespace sat { bdd_manager::bdd_manager(unsigned num_vars) { + m_cost_metric = bdd_cost; + m_cost_bdd = 0; for (BDD a = 0; a < 2; ++a) { for (BDD b = 0; b < 2; ++b) { for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) { @@ -58,6 +60,7 @@ namespace sat { m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry); } for (auto* e : m_op_cache) { + VERIFY(e != m_spare_entry); m_alloc.deallocate(sizeof(*e), e); } } @@ -78,16 +81,21 @@ namespace sat { bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) { bool first = true; + SASSERT(well_formed()); while (true) { try { return apply_rec(arg1, arg2, op); } catch (mem_out) { + throw; +#if 0 try_reorder(); if (!first) throw; first = false; +#endif } } + SASSERT(well_formed()); } @@ -101,17 +109,20 @@ namespace sat { bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { + // std::cout << a << " " << b << " " << c << " " << e1 << " " << e2 << "\n"; if (e1 != e2) { + VERIFY(e2->m_result != -1); push_entry(e1); - if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) { - return true; - } - e1 = const_cast(e2); + e1 = nullptr; + return true; + } + else { + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = c; + VERIFY(e1->m_result == -1); + return false; } - e1->m_bdd1 = a; - e1->m_bdd2 = b; - e1->m_op = c; - return false; } bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) { @@ -143,8 +154,10 @@ namespace sat { op_entry * e1 = pop_entry(a, b, op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); if (check_result(e1, e2, a, b, op)) { + SASSERT(!m_free_nodes.contains(e2->m_result)); return e2->m_result; } + // VERIFY(well_formed()); BDD r; if (level(a) == level(b)) { push(apply_rec(lo(a), lo(b), op)); @@ -163,6 +176,8 @@ namespace sat { } pop(2); e1->m_result = r; + // VERIFY(well_formed()); + SASSERT(!m_free_nodes.contains(r)); return r; } @@ -190,6 +205,7 @@ namespace sat { else { void * mem = m_alloc.allocate(sizeof(op_entry)); result = new (mem) op_entry(l, r, op); + // std::cout << "alloc: " << result << "\n"; } result->m_result = -1; return result; @@ -200,16 +216,22 @@ namespace sat { m_spare_entry = e; } - bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) { + bdd_manager::BDD bdd_manager::make_node(unsigned lvl, BDD l, BDD h) { m_is_new_node = false; - if (l == r) { + if (l == h) { return l; } + if (!is_const(l) && level(l) >= lvl) { + display(std::cout << l << " level: " << level(l) << " lvl: " << lvl << "\n"); + } + VERIFY(is_const(l) || level(l) < lvl); + VERIFY(is_const(h) || level(h) < lvl); - bdd_node n(level, l, r); + bdd_node n(lvl, l, h); node_table::entry* e = m_node_table.insert_if_not_there2(n); if (e->get_data().m_index != 0) { - return e->get_data().m_index; + unsigned result = e->get_data().m_index; + return result; } e->get_data().m_refcount = 0; bool do_gc = m_free_nodes.empty(); @@ -226,25 +248,50 @@ namespace sat { } SASSERT(!m_free_nodes.empty()); - e->get_data().m_index = m_free_nodes.back(); - m_nodes[e->get_data().m_index] = e->get_data(); - m_free_nodes.pop_back(); - m_is_new_node = true; - return e->get_data().m_index; + unsigned result = m_free_nodes.back(); + m_free_nodes.pop_back(); + e->get_data().m_index = result; + m_nodes[result] = e->get_data(); + m_is_new_node = true; + SASSERT(!m_free_nodes.contains(result)); + SASSERT(m_nodes[result].m_index == result); + return result; } + void bdd_manager::try_cnf_reorder(bdd const& b) { + m_cost_bdd = b.root; + m_cost_metric = cnf_cost; + try_reorder(); + m_cost_metric = bdd_cost; + m_cost_bdd = 0; + } + void bdd_manager::try_reorder() { + gc(); + for (auto* e : m_op_cache) { + m_alloc.deallocate(sizeof(*e), e); + } + m_op_cache.reset(); init_reorder(); for (unsigned i = 0; i < m_var2level.size(); ++i) { sift_var(i); } + SASSERT(m_op_cache.empty()); + SASSERT(well_formed()); } double bdd_manager::current_cost() { -#if 0 - -#endif - return m_nodes.size() - m_free_nodes.size(); + switch (m_cost_metric) { + case bdd_cost: + return m_nodes.size() - m_free_nodes.size(); + case cnf_cost: + return cnf_size(m_cost_bdd); + case dnf_cost: + return dnf_size(m_cost_bdd); + default: + UNREACHABLE(); + return 0; + } } bool bdd_manager::is_bad_cost(double current_cost, double best_cost) const { @@ -306,9 +353,11 @@ namespace sat { void bdd_manager::sift_up(unsigned lvl) { if (m_level2nodes[lvl].empty()) return; + // VERIFY(well_formed()); // exchange level and level + 1. m_S.reset(); m_T.reset(); + m_to_free.reset(); m_disable_gc = true; for (unsigned n : m_level2nodes[lvl + 1]) { @@ -320,6 +369,8 @@ namespace sat { m_S.push_back(n); } else { + reorder_decref(l); + reorder_decref(h); m_T.push_back(n); } TRACE("bdd", tout << "remove " << n << "\n";); @@ -331,14 +382,12 @@ namespace sat { for (unsigned n : m_level2nodes[lvl]) { bdd_node& node = m_nodes[n]; m_node_table.remove(node); - if (m_max_parent[n] == lvl + 1 && node.m_refcount == 0) { - TRACE("bdd", tout << "free " << n << "\n";); - node.set_internal(); - m_free_nodes.push_back(n); + node.m_level = lvl + 1; + if (m_reorder_rc[n] == 0) { + m_to_free.push_back(n); } else { TRACE("bdd", tout << "set level " << n << " to " << lvl + 1 << "\n";); - node.m_level = lvl + 1; m_node_table.insert(node); m_level2nodes[lvl + 1].push_back(n); } @@ -352,19 +401,18 @@ namespace sat { } for (unsigned n : m_T) { - TRACE("bdd", tout << "transform " << n << "\n";); BDD l = lo(n); BDD h = hi(n); if (l == 0 && h == 0) continue; BDD a, b, c, d; - if (level(l) == lvl) { + if (level(l) == lvl + 1) { a = lo(l); b = hi(l); } else { a = b = l; } - if (level(h) == lvl) { + if (level(h) == lvl + 1) { c = lo(h); d = hi(h); } @@ -375,15 +423,22 @@ namespace sat { unsigned ac = make_node(lvl, a, c); if (is_new_node()) { m_level2nodes[lvl].push_back(ac); - m_max_parent.setx(ac, lvl + 1, 0); + m_reorder_rc.reserve(ac+1); + reorder_incref(a); + reorder_incref(c); } unsigned bd = make_node(lvl, b, d); if (is_new_node()) { m_level2nodes[lvl].push_back(bd); - m_max_parent.setx(bd, lvl + 1, 0); + m_reorder_rc.reserve(bd+1); + reorder_incref(b); + reorder_incref(d); } m_nodes[n].m_lo = ac; m_nodes[n].m_hi = bd; + reorder_incref(ac); + reorder_incref(bd); + TRACE("bdd", tout << "transform " << n << " " << " " << a << " " << b << " " << c << " " << d << " " << ac << " " << bd << "\n";); m_node_table.insert(m_nodes[n]); } unsigned v = m_level2var[lvl]; @@ -391,6 +446,30 @@ namespace sat { std::swap(m_level2var[lvl], m_level2var[lvl+1]); std::swap(m_var2level[v], m_var2level[w]); m_disable_gc = false; + + // add orphaned nodes to free-list + for (unsigned i = 0; i < m_to_free.size(); ++i) { + unsigned n = m_to_free[i]; + bdd_node& node = m_nodes[n]; + if (!node.is_internal()) { + VERIFY(!m_free_nodes.contains(n)); + VERIFY(node.m_refcount == 0); + m_free_nodes.push_back(n); + m_node_table.remove(node); + BDD l = lo(n); + BDD h = hi(n); + node.set_internal(); + + reorder_decref(l); + if (!m_nodes[l].is_internal() && m_reorder_rc[l] == 0) { + m_to_free.push_back(l); + } + reorder_decref(h); + if (!m_nodes[h].is_internal() && m_reorder_rc[h] == 0) { + m_to_free.push_back(h); + } + } + } TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); ); DEBUG_CODE( for (unsigned i = 0; i < m_level2nodes.size(); ++i) { @@ -399,12 +478,24 @@ namespace sat { SASSERT(node.m_level == i); } }); + + TRACE("bdd", + for (unsigned i = 0; i < m_nodes.size(); ++i) { + if (m_reorder_rc[i] != 0) { + tout << i << " " << m_reorder_rc[i] << "\n"; + }}); + + // VERIFY(well_formed()); } void bdd_manager::init_reorder() { m_level2nodes.reset(); unsigned sz = m_nodes.size(); - m_max_parent.fill(sz, 0); + m_reorder_rc.fill(sz, 0); + for (unsigned i = 0; i < sz; ++i) { + if (m_nodes[i].m_refcount > 0) + m_reorder_rc[i] = UINT_MAX; + } for (unsigned i = 0; i < sz; ++i) { bdd_node const& n = m_nodes[i]; if (n.is_internal()) continue; @@ -412,8 +503,8 @@ namespace sat { SASSERT(i == m_nodes[i].m_index); m_level2nodes.reserve(lvl + 1); m_level2nodes[lvl].push_back(i); - m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], lvl); - m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], lvl); + reorder_incref(n.m_lo); + reorder_incref(n.m_hi); } TRACE("bdd", display(tout); @@ -421,11 +512,19 @@ namespace sat { bdd_node const& n = m_nodes[i]; if (n.is_internal()) continue; unsigned lvl = n.m_level; - tout << "lvl: " << lvl << " parent: " << m_max_parent[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n"; + tout << i << " lvl: " << lvl << " rc: " << m_reorder_rc[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n"; } ); } + void bdd_manager::reorder_incref(unsigned n) { + if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]++; + } + + void bdd_manager::reorder_decref(unsigned n) { + if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]--; + } + void bdd_manager::reserve_var(unsigned i) { while (m_var2level.size() <= i) { unsigned v = m_var2level.size(); @@ -455,9 +554,12 @@ namespace sat { return bdd(mk_not_rec(b.root), this); } catch (mem_out) { + throw; +#if 0 try_reorder(); if (!first) throw; first = false; +#endif } } } @@ -532,12 +634,13 @@ namespace sat { push(mk_ite_rec(a1, b1, c1)); push(mk_ite_rec(a2, b2, c2)); r = make_node(lvl, read(2), read(1)); - pop(2); + pop(2); e1->m_result = r; return r; } bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) { + // VERIFY(well_formed()); return bdd(mk_quant(n, vars, b.root, bdd_or_op), this); } @@ -570,9 +673,11 @@ namespace sat { bdd_op q_op = op == bdd_and_op ? bdd_and_proj_op : bdd_or_proj_op; op_entry * e1 = pop_entry(a, b, q_op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); - if (check_result(e1, e2, a, b, q_op)) + if (check_result(e1, e2, a, b, q_op)) { r = e2->m_result; + } else { + VERIFY(e1->m_result == -1); push(mk_quant_rec(l, lo(b), op)); push(mk_quant_rec(l, hi(b), op)); r = make_node(lvl, read(2), read(1)); @@ -580,26 +685,29 @@ namespace sat { e1->m_result = r; } } + VERIFY(r != UINT_MAX); return r; } - double bdd_manager::count(bdd const& b, unsigned z) { + double bdd_manager::count(BDD b, unsigned z) { init_mark(); m_count.resize(m_nodes.size()); m_count[0] = z; m_count[1] = 1-z; set_mark(0); set_mark(1); - m_todo.push_back(b.root); + m_todo.push_back(b); while (!m_todo.empty()) { BDD r = m_todo.back(); if (is_marked(r)) { m_todo.pop_back(); } else if (!is_marked(lo(r))) { + VERIFY (is_const(r) || r != lo(r)); m_todo.push_back(lo(r)); } else if (!is_marked(hi(r))) { + VERIFY (is_const(r) || r != hi(r)); m_todo.push_back(hi(r)); } else { @@ -608,7 +716,7 @@ namespace sat { m_todo.pop_back(); } } - return m_count[b.root]; + return m_count[b]; } unsigned bdd_manager::bdd_size(bdd const& b) { @@ -644,8 +752,8 @@ namespace sat { } void bdd_manager::gc() { + m_free_nodes.reset(); IF_VERBOSE(3, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";); - SASSERT(m_free_nodes.empty()); svector reachable(m_nodes.size(), false); for (unsigned i = m_bdd_stack.size(); i-- > 0; ) { reachable[m_bdd_stack[i]] = true; @@ -674,6 +782,7 @@ namespace sat { for (unsigned i = m_nodes.size(); i-- > 2; ) { if (!reachable[i]) { m_nodes[i].set_internal(); + VERIFY(m_nodes[i].m_refcount == 0); m_free_nodes.push_back(i); } } @@ -681,10 +790,25 @@ namespace sat { 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); + ptr_vector to_delete, to_keep; + for (auto* e : m_op_cache) { + // std::cout << "check: " << e << "\n"; + if (!reachable[e->m_bdd1] || !reachable[e->m_bdd2] || !reachable[e->m_op] || (e->m_result != -1 && !reachable[e->m_result])) { + to_delete.push_back(e); + } + else { + to_keep.push_back(e); + } } m_op_cache.reset(); + for (op_entry* e : to_delete) { + // std::cout << "erase: " << e << "\n"; + m_alloc.deallocate(sizeof(*e), e); + } + for (op_entry* e : to_keep) { + m_op_cache.insert(e); + } + m_node_table.reset(); // re-populate node cache for (unsigned i = m_nodes.size(); i-- > 2; ) { @@ -693,6 +817,7 @@ namespace sat { m_node_table.insert(m_nodes[i]); } } + SASSERT(well_formed()); } void bdd_manager::init_mark() { @@ -707,6 +832,7 @@ namespace sat { std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) { init_mark(); m_todo.push_back(b.root); + m_reorder_rc.reserve(m_nodes.size()); while (!m_todo.empty()) { BDD r = m_todo.back(); if (is_marked(r)) { @@ -723,7 +849,7 @@ namespace sat { m_todo.push_back(hi(r)); } else { - out << r << " : " << var(r) << " " << lo(r) << " " << hi(r) << "\n"; + out << r << " : " << var(r) << " @ " << level(r) << " " << lo(r) << " " << hi(r) << " " << m_reorder_rc[r] << "\n"; set_mark(r); m_todo.pop_back(); } @@ -731,30 +857,52 @@ namespace sat { return out; } - void bdd_manager::well_formed() { + bool bdd_manager::well_formed() { for (unsigned n : m_free_nodes) { - VERIFY(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0); + if (!(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0)) { + std::cout << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n"; + display(std::cout); + UNREACHABLE(); + } } for (bdd_node const& n : m_nodes) { if (n.is_internal()) continue; unsigned lvl = n.m_level; BDD lo = n.m_lo; BDD hi = n.m_hi; + if (!is_const(lo) && level(lo) >= lvl) { + std::cout << n.m_index << " lo: " << lo << "\n"; + display(std::cout); + } VERIFY(is_const(lo) || level(lo) < lvl); + if (!is_const(hi) && level(hi) >= lvl) { + std::cout << n.m_index << " hi: " << hi << "\n"; + display(std::cout); + } VERIFY(is_const(hi) || level(hi) < lvl); + if (!is_const(lo) && m_nodes[lo].is_internal()) { + std::cout << n.m_index << " lo: " << lo << "\n"; + display(std::cout); + } + if (!is_const(hi) && m_nodes[hi].is_internal()) { + std::cout << n.m_index << " hi: " << hi << "\n"; + display(std::cout); + } + VERIFY(is_const(lo) || !m_nodes[lo].is_internal()); + VERIFY(is_const(hi) || !m_nodes[hi].is_internal()); } + return true; } std::ostream& bdd_manager::display(std::ostream& out) { + m_reorder_rc.reserve(m_nodes.size()); for (unsigned i = 0; i < m_nodes.size(); ++i) { bdd_node const& n = m_nodes[i]; if (n.is_internal()) continue; - out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; + out << i << " : v" << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << " rc " << m_reorder_rc[i] << "\n"; } for (unsigned i = 0; i < m_level2nodes.size(); ++i) { - out << i << " : "; - for (unsigned l : m_level2nodes[i]) out << l << " "; - out << "\n"; + out << "level: " << i << " : " << m_level2nodes[i] << "\n"; } return out; } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 41e45c822..41d1115b9 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -50,7 +50,7 @@ namespace sat { m_hi(hi), m_index(0) {} - bdd_node(): m_level(0), m_lo(0), m_hi(0), m_index(0) {} + bdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {} unsigned m_refcount : 10; unsigned m_level : 22; BDD m_lo; @@ -58,7 +58,13 @@ namespace sat { unsigned m_index; unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } bool is_internal() const { return m_lo == 0 && m_hi == 0; } - void set_internal() { m_lo = m_hi = 0; } + void set_internal() { m_lo = 0; m_hi = 0; } + }; + + enum cost_metric { + cnf_cost, + dnf_cost, + bdd_cost }; struct hash_node { @@ -94,7 +100,7 @@ namespace sat { struct eq_entry { bool operator()(op_entry * a, op_entry * b) const { - return a->hash() == b->hash(); + return a->m_bdd1 == b->m_bdd2 && a->m_bdd2 == b->m_bdd2 && a->m_op == b->m_op; } }; @@ -117,9 +123,11 @@ namespace sat { bool m_disable_gc; bool m_is_new_node; unsigned m_max_num_bdd_nodes; - unsigned_vector m_S, m_T; // used for reordering + unsigned_vector m_S, m_T, m_to_free; // used for reordering vector m_level2nodes; - unsigned_vector m_max_parent; + unsigned_vector m_reorder_rc; + cost_metric m_cost_metric; + BDD m_cost_bdd; BDD make_node(unsigned level, BDD l, BDD r); bool is_new_node() const { return m_is_new_node; } @@ -141,15 +149,16 @@ namespace sat { void push_entry(op_entry* e); bool check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c); - double count(bdd const& b, unsigned z); + double count(BDD b, unsigned z); - void gc(); void alloc_free_nodes(unsigned n); void init_mark(); void set_mark(unsigned i) { m_mark[i] = m_mark_level; } bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; } void init_reorder(); + void reorder_incref(unsigned n); + void reorder_decref(unsigned n); void sift_up(unsigned level); void sift_var(unsigned v); double current_cost(); @@ -166,12 +175,12 @@ namespace sat { inline unsigned var(BDD b) const { return m_level2var[level(b)]; } inline BDD lo(BDD b) const { return m_nodes[b].m_lo; } inline BDD hi(BDD b) const { return m_nodes[b].m_hi; } - inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; } - inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; } + inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; VERIFY(!m_free_nodes.contains(b)); } + inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; VERIFY(!m_free_nodes.contains(b)); } inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; } - double dnf_size(bdd const& b) { return count(b, 0); } - double cnf_size(bdd const& b) { return count(b, 1); } + double dnf_size(BDD b) { return count(b, 0); } + double cnf_size(BDD b) { return count(b, 1); } unsigned bdd_size(bdd const& b); bdd mk_not(bdd b); @@ -180,7 +189,7 @@ namespace sat { bdd mk_xor(bdd const& a, bdd const& b); void reserve_var(unsigned v); - void well_formed(); + bool well_formed(); public: struct mem_out {}; @@ -205,7 +214,9 @@ namespace sat { std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, bdd const& b); + void gc(); void try_reorder(); + void try_cnf_reorder(bdd const& b); }; class bdd { @@ -234,8 +245,8 @@ namespace sat { std::ostream& display(std::ostream& out) const { return m->display(out, *this); } bool operator==(bdd const& other) const { return root == other.root; } bool operator!=(bdd const& other) const { return root != other.root; } - double cnf_size() const { return m->cnf_size(*this); } - double dnf_size() const { return m->dnf_size(*this); } + double cnf_size() const { return m->cnf_size(root); } + double dnf_size() const { return m->dnf_size(root); } unsigned bdd_size() const { return m->bdd_size(*this); } }; diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 6edc125ea..99c15c247 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -26,6 +26,7 @@ namespace sat{ elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) { m_mark_lim = 0; m_max_literals = 11; + m_miss = 0; } bool elim_vars::operator()(bool_var v) { @@ -57,10 +58,11 @@ namespace sat{ double sz1 = b1.cnf_size(); if (sz1 > 2*clause_size) { return false; - } + } if (sz1 <= clause_size) { return elim_var(v, b1); } + m_vars.reverse(); bdd b2 = elim_var(v); double sz2 = b2.cnf_size(); @@ -73,6 +75,11 @@ namespace sat{ if (sz3 <= clause_size) { return elim_var(v, b3); } +#if 0 + m.try_cnf_reorder(b3); + sz3 = b3.cnf_size(); + if (sz3 <= clause_size) ++m_miss; +#endif return false; } diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index 8893bbc40..e4843c41c 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -40,6 +40,7 @@ namespace sat { unsigned m_mark_lim; unsigned_vector m_var2index; unsigned_vector m_occ; + unsigned m_miss; unsigned m_max_literals; @@ -61,6 +62,7 @@ namespace sat { public: elim_vars(simplifier& s); bool operator()(bool_var v); + unsigned miss() const { return m_miss; } }; }; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 5c039f664..be698fc46 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -412,11 +412,17 @@ namespace sat { for (literal l1 : m_trail) { SASSERT(is_true(l1)); for (literal l2 : m_binary[l1.index()]) { + VERIFY(is_true(l2)); if (is_undef(l2)) return true; } unsigned sz = m_ternary_count[(~l1).index()]; for (binary b : m_ternary[(~l1).index()]) { if (sz-- == 0) break; + if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) { + std::cout << b.m_u << " " << b.m_v << "\n"; + std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n"; + UNREACHABLE(); + } if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u))) return true; } @@ -424,6 +430,7 @@ namespace sat { for (nary * n : m_nary_clauses) { if (n->size() == 1 && !is_true(n->get_head())) { for (literal lit : *n) { + VERIFY(!is_undef(lit)); if (is_undef(lit)) return true; } } @@ -1743,74 +1750,10 @@ namespace sat { bool lookahead::check_autarky(literal l, unsigned level) { return false; -#if 0 - // no propagations are allowed to reduce clauses. - for (nary * cp : m_nary[(~l).index()]) { - clause& c = *cp; - unsigned sz = c.size(); - bool found = false; - for (unsigned i = 0; !found && i < sz; ++i) { - found = is_true(c[i]); - if (found) { - TRACE("sat", tout << c[i] << " is true in " << c << "\n";); - } - } - IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";); - if (!found) return false; - } - // - // bail out if there is a pending binary propagation. - // In general, we would have to check, recursively that - // a binary propagation does not create reduced clauses. - // - literal_vector const& lits = m_binary[l.index()]; - TRACE("sat", tout << l << ": " << lits << "\n";); - for (unsigned i = 0; i < lits.size(); ++i) { - literal l2 = lits[i]; - if (is_true(l2)) continue; - SASSERT(!is_false(l2)); - return false; - } - - return true; -#endif } - - void lookahead::update_lookahead_reward(literal l, unsigned level) { - if (m_lookahead_reward == 0) { - if (!check_autarky(l, level)) { - // skip - } - else if (get_lookahead_reward(l) == 0) { - ++m_stats.m_autarky_propagations; - IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";); - - TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] - << " " - << (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";); - lookahead_backtrack(); - assign(l); - propagate(); - } - else { - ++m_stats.m_autarky_equivalences; - // l => p is known, but p => l is possibly not. - // add p => l. - // justification: any consequence of l - // that is not a consequence of p does not - // reduce the clauses. - literal p = get_parent(l); - SASSERT(p != null_literal); - if (m_stamp[p.var()] > m_stamp[l.var()]) { - TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout);); - IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";); - add_binary(~l, p); - set_level(l, p); - } - } - } - else { + void lookahead::update_lookahead_reward(literal l, unsigned level) { + if (m_lookahead_reward != 0) { inc_lookahead_reward(l, m_lookahead_reward); } } @@ -1852,7 +1795,6 @@ namespace sat { literal last_changed = null_literal; unsigned num_iterations = 0; while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { - change = false; num_iterations++; for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { literal lit = m_lookahead[i].m_lit; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index d30485254..64a4ef63e 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -247,6 +247,7 @@ namespace sat { inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); } inline void set_undef(literal l) { m_stamp[l.var()] = 0; } void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); } + unsigned get_level(literal d) const { return m_stamp[d.var()]; } lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; } // set the level within a scope of the search. diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b967ade06..b1f0431cc 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1657,6 +1657,7 @@ namespace sat { bool_var_vector vars; order_vars_for_elim(vars); sat::elim_vars elim_bdd(*this); + unsigned bdd_vars = 0; for (bool_var v : vars) { checkpoint(); @@ -1665,10 +1666,13 @@ namespace sat { if (try_eliminate(v)) { m_num_elim_vars++; } - else if (elim_bdd(v)) { + else if (false && elim_bdd(v)) { m_num_elim_vars++; + ++bdd_vars; } } + std::cout << "bdd elim: " << bdd_vars << "\n"; + std::cout << "bdd miss: " << elim_bdd.miss() << "\n"; m_pos_cls.finalize(); m_neg_cls.finalize(); diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index b60522740..ea5a0bc34 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -67,6 +67,7 @@ namespace sat { std::cout << "before reorder:\n"; std::cout << c1 << "\n"; std::cout << c1.bdd_size() << "\n"; + m.gc(); m.try_reorder(); std::cout << "after reorder:\n"; std::cout << c1 << "\n"; diff --git a/src/util/vector.h b/src/util/vector.h index c60585512..f068481db 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -472,6 +472,11 @@ typedef svector char_vector; typedef svector signed_char_vector; typedef svector double_vector; +inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) { + for (unsigned u : v) out << u << " "; + return out; +} + template struct vector_hash_tpl { Hash m_hash; From 553bf74f47f04fab0c55b97e1d64ab1626c29763 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 17:38:39 -0700 Subject: [PATCH 20/21] testing bdd for elim-vars Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index be698fc46..4bb7ba180 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1622,7 +1622,7 @@ namespace sat { } SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size())); //SASSERT(!missed_conflict()); - VERIFY(!missed_propagation()); + //VERIFY(!missed_propagation()); TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); } From 636f740b1afcaa4fcb2c8af91784d4fe0948b852 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 19:32:49 -0700 Subject: [PATCH 21/21] fixup bdd reordering, assertions and perf Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 89 +++++++++++++++----------------------- src/sat/sat_elim_vars.cpp | 29 +++++-------- src/sat/sat_elim_vars.h | 6 ++- src/sat/sat_simplifier.cpp | 7 +-- 4 files changed, 52 insertions(+), 79 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index e44bf7944..52714eae6 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -19,6 +19,7 @@ Revision History: #include "sat/sat_bdd.h" #include "util/trace.h" +#include "util/stopwatch.h" namespace sat { @@ -60,7 +61,7 @@ namespace sat { m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry); } for (auto* e : m_op_cache) { - VERIFY(e != m_spare_entry); + SASSERT(e != m_spare_entry); m_alloc.deallocate(sizeof(*e), e); } } @@ -87,12 +88,9 @@ namespace sat { return apply_rec(arg1, arg2, op); } catch (mem_out) { - throw; -#if 0 try_reorder(); if (!first) throw; first = false; -#endif } } SASSERT(well_formed()); @@ -109,9 +107,8 @@ namespace sat { bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { - // std::cout << a << " " << b << " " << c << " " << e1 << " " << e2 << "\n"; if (e1 != e2) { - VERIFY(e2->m_result != -1); + SASSERT(e2->m_result != -1); push_entry(e1); e1 = nullptr; return true; @@ -120,7 +117,7 @@ namespace sat { e1->m_bdd1 = a; e1->m_bdd2 = b; e1->m_op = c; - VERIFY(e1->m_result == -1); + SASSERT(e1->m_result == -1); return false; } } @@ -157,7 +154,7 @@ namespace sat { SASSERT(!m_free_nodes.contains(e2->m_result)); return e2->m_result; } - // VERIFY(well_formed()); + // SASSERT(well_formed()); BDD r; if (level(a) == level(b)) { push(apply_rec(lo(a), lo(b), op)); @@ -176,7 +173,7 @@ namespace sat { } pop(2); e1->m_result = r; - // VERIFY(well_formed()); + // SASSERT(well_formed()); SASSERT(!m_free_nodes.contains(r)); return r; } @@ -205,7 +202,6 @@ namespace sat { else { void * mem = m_alloc.allocate(sizeof(op_entry)); result = new (mem) op_entry(l, r, op); - // std::cout << "alloc: " << result << "\n"; } result->m_result = -1; return result; @@ -221,11 +217,8 @@ namespace sat { if (l == h) { return l; } - if (!is_const(l) && level(l) >= lvl) { - display(std::cout << l << " level: " << level(l) << " lvl: " << lvl << "\n"); - } - VERIFY(is_const(l) || level(l) < lvl); - VERIFY(is_const(h) || level(h) < lvl); + SASSERT(is_const(l) || level(l) < lvl); + SASSERT(is_const(h) || level(h) < lvl); bdd_node n(lvl, l, h); node_table::entry* e = m_node_table.insert_if_not_there2(n); @@ -353,7 +346,7 @@ namespace sat { void bdd_manager::sift_up(unsigned lvl) { if (m_level2nodes[lvl].empty()) return; - // VERIFY(well_formed()); + // SASSERT(well_formed()); // exchange level and level + 1. m_S.reset(); m_T.reset(); @@ -452,8 +445,8 @@ namespace sat { unsigned n = m_to_free[i]; bdd_node& node = m_nodes[n]; if (!node.is_internal()) { - VERIFY(!m_free_nodes.contains(n)); - VERIFY(node.m_refcount == 0); + SASSERT(!m_free_nodes.contains(n)); + SASSERT(node.m_refcount == 0); m_free_nodes.push_back(n); m_node_table.remove(node); BDD l = lo(n); @@ -485,7 +478,7 @@ namespace sat { tout << i << " " << m_reorder_rc[i] << "\n"; }}); - // VERIFY(well_formed()); + // SASSERT(well_formed()); } void bdd_manager::init_reorder() { @@ -554,12 +547,9 @@ namespace sat { return bdd(mk_not_rec(b.root), this); } catch (mem_out) { - throw; -#if 0 try_reorder(); if (!first) throw; first = false; -#endif } } } @@ -640,7 +630,7 @@ namespace sat { } bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) { - // VERIFY(well_formed()); + // SASSERT(well_formed()); return bdd(mk_quant(n, vars, b.root, bdd_or_op), this); } @@ -677,7 +667,7 @@ namespace sat { r = e2->m_result; } else { - VERIFY(e1->m_result == -1); + SASSERT(e1->m_result == -1); push(mk_quant_rec(l, lo(b), op)); push(mk_quant_rec(l, hi(b), op)); r = make_node(lvl, read(2), read(1)); @@ -685,7 +675,7 @@ namespace sat { e1->m_result = r; } } - VERIFY(r != UINT_MAX); + SASSERT(r != UINT_MAX); return r; } @@ -703,11 +693,11 @@ namespace sat { m_todo.pop_back(); } else if (!is_marked(lo(r))) { - VERIFY (is_const(r) || r != lo(r)); + SASSERT (is_const(r) || r != lo(r)); m_todo.push_back(lo(r)); } else if (!is_marked(hi(r))) { - VERIFY (is_const(r) || r != hi(r)); + SASSERT (is_const(r) || r != hi(r)); m_todo.push_back(hi(r)); } else { @@ -782,7 +772,7 @@ namespace sat { for (unsigned i = m_nodes.size(); i-- > 2; ) { if (!reachable[i]) { m_nodes[i].set_internal(); - VERIFY(m_nodes[i].m_refcount == 0); + SASSERT(m_nodes[i].m_refcount == 0); m_free_nodes.push_back(i); } } @@ -792,8 +782,7 @@ namespace sat { ptr_vector to_delete, to_keep; for (auto* e : m_op_cache) { - // std::cout << "check: " << e << "\n"; - if (!reachable[e->m_bdd1] || !reachable[e->m_bdd2] || !reachable[e->m_op] || (e->m_result != -1 && !reachable[e->m_result])) { + if (e->m_result != -1) { to_delete.push_back(e); } else { @@ -802,7 +791,6 @@ namespace sat { } m_op_cache.reset(); for (op_entry* e : to_delete) { - // std::cout << "erase: " << e << "\n"; m_alloc.deallocate(sizeof(*e), e); } for (op_entry* e : to_keep) { @@ -858,11 +846,15 @@ namespace sat { } bool bdd_manager::well_formed() { + bool ok = true; for (unsigned n : m_free_nodes) { - if (!(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0)) { - std::cout << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n"; - display(std::cout); + ok &= (lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0); + if (!ok) { + IF_VERBOSE(0, + verbose_stream() << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n"; + display(verbose_stream());); UNREACHABLE(); + return false; } } for (bdd_node const& n : m_nodes) { @@ -870,28 +862,17 @@ namespace sat { unsigned lvl = n.m_level; BDD lo = n.m_lo; BDD hi = n.m_hi; - if (!is_const(lo) && level(lo) >= lvl) { - std::cout << n.m_index << " lo: " << lo << "\n"; - display(std::cout); + ok &= is_const(lo) || level(lo) < lvl; + ok &= is_const(hi) || level(hi) < lvl; + ok &= is_const(lo) || !m_nodes[lo].is_internal(); + ok &= is_const(hi) || !m_nodes[hi].is_internal(); + if (!ok) { + IF_VERBOSE(0, display(verbose_stream() << n.m_index << " lo " << lo << " hi " << hi << "\n");); + UNREACHABLE(); + return false; } - VERIFY(is_const(lo) || level(lo) < lvl); - if (!is_const(hi) && level(hi) >= lvl) { - std::cout << n.m_index << " hi: " << hi << "\n"; - display(std::cout); - } - VERIFY(is_const(hi) || level(hi) < lvl); - if (!is_const(lo) && m_nodes[lo].is_internal()) { - std::cout << n.m_index << " lo: " << lo << "\n"; - display(std::cout); - } - if (!is_const(hi) && m_nodes[hi].is_internal()) { - std::cout << n.m_index << " hi: " << hi << "\n"; - display(std::cout); - } - VERIFY(is_const(lo) || !m_nodes[lo].is_internal()); - VERIFY(is_const(hi) || !m_nodes[hi].is_internal()); } - return true; + return ok; } std::ostream& bdd_manager::display(std::ostream& out) { diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 99c15c247..86954d037 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -27,6 +27,8 @@ namespace sat{ m_mark_lim = 0; m_max_literals = 11; m_miss = 0; + m_hit1 = 0; + m_hit2 = 0; } bool elim_vars::operator()(bool_var v) { @@ -57,29 +59,20 @@ namespace sat{ bdd b1 = elim_var(v); double sz1 = b1.cnf_size(); if (sz1 > 2*clause_size) { + ++m_miss; return false; } if (sz1 <= clause_size) { + ++m_hit1; return elim_var(v, b1); } - - m_vars.reverse(); - bdd b2 = elim_var(v); - double sz2 = b2.cnf_size(); - if (sz2 <= clause_size) { - return elim_var(v, b2); - } - shuffle_vars(); - bdd b3 = elim_var(v); - double sz3 = b3.cnf_size(); - if (sz3 <= clause_size) { - return elim_var(v, b3); - } -#if 0 - m.try_cnf_reorder(b3); - sz3 = b3.cnf_size(); - if (sz3 <= clause_size) ++m_miss; -#endif + m.try_cnf_reorder(b1); + sz1 = b1.cnf_size(); + if (sz1 <= clause_size) { + ++m_hit2; + return elim_var(v, b1); + } + ++m_miss; return false; } diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index e4843c41c..ba5a02d67 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -41,6 +41,8 @@ namespace sat { unsigned_vector m_var2index; unsigned_vector m_occ; unsigned m_miss; + unsigned m_hit1; + unsigned m_hit2; unsigned m_max_literals; @@ -62,7 +64,9 @@ namespace sat { public: elim_vars(simplifier& s); bool operator()(bool_var v); - unsigned miss() const { return m_miss; } + unsigned hit2() const { return m_hit1; } // first round bdd construction is minimal + unsigned hit1() const { return m_hit2; } // minimal after reshufling + unsigned miss() const { return m_miss; } // not-minimal }; }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b1f0431cc..cd46f1916 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1657,8 +1657,6 @@ namespace sat { bool_var_vector vars; order_vars_for_elim(vars); sat::elim_vars elim_bdd(*this); - unsigned bdd_vars = 0; - for (bool_var v : vars) { checkpoint(); if (m_elim_counter < 0) @@ -1666,13 +1664,10 @@ namespace sat { if (try_eliminate(v)) { m_num_elim_vars++; } - else if (false && elim_bdd(v)) { + else if (elim_bdd(v)) { m_num_elim_vars++; - ++bdd_vars; } } - std::cout << "bdd elim: " << bdd_vars << "\n"; - std::cout << "bdd miss: " << elim_bdd.miss() << "\n"; m_pos_cls.finalize(); m_neg_cls.finalize();