From 528dc8a3f8cbbd9f3d4fb017cf87d13fedb810af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Mar 2018 17:05:22 -0700 Subject: [PATCH] disable bdd variable elimination Signed-off-by: Nikolaj Bjorner --- src/sat/sat_clause_use_list.h | 9 +++++ src/sat/sat_elim_eqs.cpp | 2 +- src/sat/sat_elim_vars.cpp | 9 ++--- src/sat/sat_elim_vars.h | 2 +- src/sat/sat_model_converter.cpp | 5 --- src/sat/sat_simplifier.cpp | 12 +++++-- src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.cpp | 3 +- src/tactic/portfolio/parallel_tactic.cpp | 45 +++++++++++++++--------- src/tactic/smtlogics/qfbv_tactic.cpp | 2 ++ 10 files changed, 58 insertions(+), 32 deletions(-) diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index c028ad713..90c2d7779 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -124,6 +124,15 @@ namespace sat { }; iterator mk_iterator() const { return iterator(const_cast(this)->m_clauses); } + + std::ostream& display(std::ostream& out) const { + iterator it = mk_iterator(); + while (!it.at_end()) { + out << it.curr() << "\n"; + it.next(); + } + return out; + } }; }; diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 11c1d4780..870aa7fe2 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -199,7 +199,7 @@ namespace sat { literal r = roots[v]; SASSERT(v != r.var()); bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r); - if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) { + if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) { // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 34f871a8f..a80807450 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -101,7 +101,7 @@ namespace sat{ pos_occs.reset(); neg_occs.reset(); literal_vector lits; - add_clauses(b, lits); + add_clauses(v, b, lits); return true; } @@ -157,7 +157,7 @@ namespace sat{ return b; } - void elim_vars::add_clauses(bdd const& b, literal_vector& lits) { + void elim_vars::add_clauses(bool_var v0, bdd const& b, literal_vector& lits) { if (b.is_true()) { // no-op } @@ -167,6 +167,7 @@ namespace sat{ if (simp.cleanup_clause(c)) return; + if (v0 == 39063) IF_VERBOSE(0, verbose_stream() << "bdd: " << c << "\n"); switch (c.size()) { case 0: s.set_conflict(justification()); @@ -198,10 +199,10 @@ namespace sat{ else { unsigned v = m_vars[b.var()]; lits.push_back(literal(v, false)); - add_clauses(b.lo(), lits); + add_clauses(v0, b.lo(), lits); lits.pop_back(); lits.push_back(literal(v, true)); - add_clauses(b.hi(), lits); + add_clauses(v0, b.hi(), lits); lits.pop_back(); } } diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index ba5a02d67..b62fdc5db 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -57,7 +57,7 @@ namespace sat { 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); + void add_clauses(bool_var v, bdd const& b, literal_vector& lits); bool elim_var(bool_var v, bdd const& b); bdd elim_var(bool_var v); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c9d046197..c2a4858f7 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -91,11 +91,6 @@ namespace sat { for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause - if (v0 == 36858) - IF_VERBOSE(0, verbose_stream() << "clause: " << clause << "\n"; - for (literal lit : clause) verbose_stream() << m[lit.var()] << " "; - verbose_stream() << "\n";); - elim_stack* st = it->m_elim_stack[index]; if (!sat) { VERIFY(legal_to_flip(v0)); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 642fca348..bac790698 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1518,6 +1518,14 @@ namespace sat { } void block_covered_clause(clause& c, literal l, model_converter::kind k) { + if (false && l.var() == 39021) { + IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n"; + s.m_use_list.display(verbose_stream() << "use " << l << ":", l); + s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l); + /*s.s.display(verbose_stream());*/ + ); + + } TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); SASSERT(!s.is_external(l)); model_converter::entry& new_entry = mc.mk(k, l.var()); @@ -1563,7 +1571,6 @@ namespace sat { for (literal l2 : m_intersection) { watched* w = find_binary_watch(s.get_wlist(~l), ~l2); if (!w) { - IF_VERBOSE(10, verbose_stream() << "bca " << l << " " << ~l2 << "\n";); s.s.mk_bin_clause(l, ~l2, true); ++s.m_num_bca; } @@ -1934,6 +1941,7 @@ namespace sat { m_new_cls.reset(); if (!resolve(c1, c2, pos_l, m_new_cls)) continue; + // if (v == 39063) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";); if (cleanup_clause(m_new_cls)) continue; // clause is already satisfied. @@ -2045,7 +2053,7 @@ namespace sat { m_subsumption = p.subsumption(); m_subsumption_limit = p.subsumption_limit(); m_elim_vars = p.elim_vars(); - m_elim_vars_bdd = p.elim_vars_bdd(); + m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy m_elim_vars_bdd_delay = p.elim_vars_bdd_delay(); m_incremental_mode = s.get_config().m_incremental && !p.override_incremental(); } diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 086111f84..a777e07a4 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -47,6 +47,7 @@ namespace sat { clause_use_list & get(literal l) { return m_use_list[l.index()]; } clause_use_list const & get(literal l) const { return m_use_list[l.index()]; } void finalize() { m_use_list.finalize(); } + std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); } }; class simplifier { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7def379e0..299b1f704 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1654,11 +1654,10 @@ namespace sat { // m_mc.set_solver(nullptr); m_mc(m_model); - if (!check_clauses(m_model)) { IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); - IF_VERBOSE(10, m_mc.display(verbose_stream())); + // IF_VERBOSE(10, m_mc.display(verbose_stream())); throw solver_exception("check model failed"); } diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 4a5af3679..b19bab487 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -114,10 +114,10 @@ class parallel_tactic : public tactic { dec_wait(); return st; } - { - std::unique_lock lock(m_mutex); - m_cond.wait(lock); - } + { + std::unique_lock lock(m_mutex); + m_cond.wait(lock); + } dec_wait(); } return nullptr; @@ -233,7 +233,9 @@ class parallel_tactic : public tactic { void inc_depth(unsigned inc) { m_depth += inc; } - void inc_width(unsigned w) { m_width *= w; } + void inc_width(unsigned w) { + m_width *= w; + } double get_width() const { return m_width; } @@ -280,14 +282,14 @@ class parallel_tactic : public tactic { void set_cube_params() { unsigned cutoff = m_cube_cutoff; double fraction = m_cube_fraction; - if (m_depth == 1 && cutoff > 0) { - fraction = 0; // use fixed cubing at depth 1. + if (true || (m_depth == 1 && cutoff > 0)) { + m_params.set_sym("lookahead.cube.cutoff", symbol("depth")); + m_params.set_uint("lookahead.cube.depth", std::max(m_depth, 10u)); } else { - cutoff = 0; // use dynamic cubing beyond depth 1 + m_params.set_sym("lookahead.cube.cutoff", symbol("adaptive_psat")); + m_params.set_double("lookahead.cube.fraction", fraction); } - m_params.set_uint ("lookahead.cube.cutoff", cutoff); - m_params.set_double("lookahead.cube.fraction", fraction); get_solver().updt_params(m_params); } @@ -329,6 +331,7 @@ private: task_queue m_queue; std::mutex m_mutex; double m_progress; + unsigned m_branches; bool m_has_undef; bool m_allsat; unsigned m_num_unsat; @@ -341,20 +344,27 @@ private: m_has_undef = false; m_allsat = false; m_num_unsat = 0; + m_branches = 0; m_exn_code = 0; m_params.set_bool("override_incremental", true); } + void add_branches(unsigned b) { + std::lock_guard lock(m_mutex); + m_branches += b; + } + void close_branch(solver_state& s, lbool status) { double f = 100.0 / s.get_width(); { std::lock_guard lock(m_mutex); m_progress += f; + --m_branches; } - IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; + IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% "; if (status == l_true) verbose_stream() << ":status sat "; if (status == l_undef) verbose_stream() << ":status unknown "; - verbose_stream() << ":unsat " << m_num_unsat << ")\n";); + verbose_stream() << ":unsat " << m_num_unsat << " :branches " << m_branches << ")\n";); } void report_sat(solver_state& s) { @@ -401,7 +411,7 @@ private: cube.reset(); cube.append(s.split_cubes(1)); SASSERT(cube.size() <= 1); - IF_VERBOSE(2, verbose_stream() << "(sat.parallel :split-cube " << cube.size() << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); if (!s.cubes().empty()) m_queue.add_task(s.clone()); if (!cube.empty()) s.assert_cube(cube.get(0)); s.inc_depth(1); @@ -430,8 +440,8 @@ private: cubes.push_back(mk_and(c)); } - IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";); - IF_VERBOSE(10, verbose_stream() << "(parallel_tactic :cubes " << cubes << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << ")\n";); + IF_VERBOSE(12, verbose_stream() << "(tactic.parallel :cubes " << cubes << ")\n";); if (cubes.empty()) { report_unsat(s); @@ -439,6 +449,7 @@ private: } else { s.inc_width(cubes.size()); + add_branches(cubes.size()); s.set_cubes(cubes); s.set_type(conquer_task); goto conquer; @@ -462,7 +473,7 @@ private: } if (canceled(s)) return; } - IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";); if (hard_cubes.empty()) return; s.set_cubes(hard_cubes); @@ -534,7 +545,7 @@ private: m_stats.display(out); m_queue.display(out); std::lock_guard lock(m_mutex); - out << "(parallel_tactic :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n"; + out << "(tactic.parallel :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n"; return out; } diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index b69069864..f28129a52 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -28,6 +28,7 @@ Notes: #include "tactic/bv/bv_size_reduction_tactic.h" #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" +#include "tactic/portfolio/parallel_tactic.h" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300 @@ -130,6 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), + //mk_parallel_tactic(m, p)); mk_sat_tactic(m)); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());