From 6f4c873b296327d12e6c7b0eb126a18a3b569b72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Jun 2017 13:18:20 -0700 Subject: [PATCH] debugging Signed-off-by: Nikolaj Bjorner --- src/sat/card_extension.cpp | 186 +++++++++--------- src/sat/sat_lookahead.cpp | 5 +- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_solver.cpp | 16 +- src/tactic/arith/bound_manager.cpp | 13 ++ src/tactic/arith/bound_manager.h | 2 + .../portfolio/bounded_int2bv_solver.cpp | 13 +- src/tactic/portfolio/enum2bv_solver.cpp | 2 +- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- 9 files changed, 139 insertions(+), 102 deletions(-) diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index d6f23ad3d..690ed042d 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -281,106 +281,109 @@ namespace sat { for (unsigned i = 0; i < num_watch; ++i) { watch_literal(p, p[i]); } - p.set_slack(slack); - p.set_num_watch(num_watch); - } - TRACE("sat", display(tout << "init watch: ", p, true);); - } +p.set_slack(slack); +p.set_num_watch(num_watch); + } + TRACE("sat", display(tout << "init watch: ", p, true);); + } - /* - Chai Kuhlmann: - Lw - set of watched literals - Lu - set of unwatched literals that are not false - - Lw = Lw \ { alit } - Sw -= value - a_max = max { a | l in Lw u Lu, l = undef } - while (Sw < k + a_max & Lu != 0) { - a_s = max { a | l in Lu } - Sw += a_s - Lw = Lw u {l_s} - Lu = Lu \ {l_s} - } - if (Sw < k) conflict - while (Sw < k + a_max) { - assign (l_max) - a_max = max { ai | li in Lw, li = undef } - } - ASSERT(Sw >= bound) - return no-conflict + /* + Chai Kuhlmann: + Lw - set of watched literals + Lu - set of unwatched literals that are not false - a_max index: index of non-false literal with maximal weight. - - - */ - void card_extension::add_index(pb& p, unsigned index, literal lit) { - if (value(lit) == l_undef) { - m_pb_undef.push_back(index); - if (p[index].first > m_a_max) { - m_a_max = p[index].first; - } - } - } + Lw = Lw \ { alit } + Sw -= value + a_max = max { a | l in Lw u Lu, l = undef } + while (Sw < k + a_max & Lu != 0) { + a_s = max { a | l in Lu } + Sw += a_s + Lw = Lw u {l_s} + Lu = Lu \ {l_s} + } + if (Sw < k) conflict + while (Sw < k + a_max) { + assign (l_max) + a_max = max { ai | li in Lw, li = undef } + } + ASSERT(Sw >= bound) + return no-conflict - lbool card_extension::add_assign(pb& p, literal alit) { + a_max index: index of non-false literal with maximal weight. - TRACE("sat", display(tout << "assign: " << alit << "\n", p, true);); - SASSERT(!inconsistent()); - unsigned sz = p.size(); - unsigned bound = p.k(); - unsigned num_watch = p.num_watch(); - unsigned slack = p.slack(); - SASSERT(value(alit) == l_false); - SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); - SASSERT(num_watch <= sz); - SASSERT(num_watch > 0); - unsigned index = 0; - m_a_max = 0; - m_pb_undef.reset(); - for (; index < num_watch; ++index) { - literal lit = p[index].second; - if (lit == alit) { - break; - } - add_index(p, index, lit); - } - SASSERT(index < num_watch); - unsigned index1 = index + 1; - for (; m_a_max == 0 && index1 < num_watch; ++index1) { - add_index(p, index1, p[index1].second); - } + */ + void card_extension::add_index(pb& p, unsigned index, literal lit) { + if (value(lit) == l_undef) { + m_pb_undef.push_back(index); + if (p[index].first > m_a_max) { + m_a_max = p[index].first; + } + } + } - unsigned val = p[index].first; - SASSERT(value(p[index].second) == l_false); - SASSERT(val <= slack); - slack -= val; - // find literals to swap with: - for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) { - literal lit = p[j].second; - if (value(lit) != l_false) { - slack += p[j].first; - watch_literal(p, p[j]); - p.swap(num_watch, j); - add_index(p, num_watch, lit); - ++num_watch; - } - } + lbool card_extension::add_assign(pb& p, literal alit) { - SASSERT(!inconsistent()); - DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); }); + TRACE("sat", display(tout << "assign: " << alit << "\n", p, true);); + SASSERT(!inconsistent()); + unsigned sz = p.size(); + unsigned bound = p.k(); + unsigned num_watch = p.num_watch(); + unsigned slack = p.slack(); + SASSERT(value(alit) == l_false); + SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); + SASSERT(num_watch <= sz); + SASSERT(num_watch > 0); + unsigned index = 0; + m_a_max = 0; + m_pb_undef.reset(); + for (; index < num_watch; ++index) { + literal lit = p[index].second; + if (lit == alit) { + break; + } + add_index(p, index, lit); + } + SASSERT(index < num_watch); - if (slack < bound) { - // maintain watching the literal - slack += val; - p.set_slack(slack); - p.set_num_watch(num_watch); - SASSERT(bound <= slack); - TRACE("sat", tout << "conflict " << alit << "\n";); - set_conflict(p, alit); - return l_false; - } + unsigned index1 = index + 1; + for (; m_a_max == 0 && index1 < num_watch; ++index1) { + add_index(p, index1, p[index1].second); + } + unsigned val = p[index].first; + SASSERT(value(p[index].second) == l_false); + SASSERT(val <= slack); + slack -= val; + // find literals to swap with: + for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) { + literal lit = p[j].second; + if (value(lit) != l_false) { + slack += p[j].first; + watch_literal(p, p[j]); + p.swap(num_watch, j); + add_index(p, num_watch, lit); + ++num_watch; + } + } + + SASSERT(!inconsistent()); + DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); }); + + if (slack < bound) { + // maintain watching the literal + slack += val; + p.set_slack(slack); + p.set_num_watch(num_watch); + SASSERT(bound <= slack); + TRACE("sat", tout << "conflict " << alit << "\n";); + set_conflict(p, alit); + return l_false; + } + + if (index > p.size() || num_watch > p.size()) { + std::cout << "size: " << p.size() << "index: " << index << " num watch: " << num_watch << "\n"; + } // swap out the watched literal. --num_watch; SASSERT(num_watch > 0); @@ -1711,6 +1714,7 @@ namespace sat { } void card_extension::simplify() { + return; s().pop_to_base_level(); unsigned trail_sz; do { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 95b11fa15..2a1837e20 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1734,11 +1734,14 @@ namespace sat { } IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << ")\n";); - if (num_units > 0 && !m_s.inconsistent()) { + if (m_s.inconsistent()) return; + + if (num_units > 0) { m_s.propagate_core(false); m_s.m_simplifier(false); } m_lookahead.reset(); + } // diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c6f340f2e..45429805c 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -162,7 +162,7 @@ namespace sat { for (unsigned i = 0; i < sz; ++i) e.m_clauses.push_back(c[i]); e.m_clauses.push_back(null_literal); - TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); + // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } bool model_converter::check_invariant(unsigned num_vars) const { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4e34579a7..13f0246af 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1415,10 +1415,16 @@ namespace sat { } if (m_config.m_lookahead_simplify) { - lookahead lh(*this); - lh.simplify(); - lh.scc(); - lh.collect_statistics(m_aux_stats); + { + lookahead lh(*this); + lh.simplify(); + lh.collect_statistics(m_aux_stats); + } + { + lookahead lh(*this); + lh.scc(); + lh.collect_statistics(m_aux_stats); + } } sort_watch_lits(); @@ -1450,7 +1456,7 @@ namespace sat { m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max; } -#if 1 +#if 0 static unsigned file_no = 0; #pragma omp critical (print_sat) { diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp index 97d93658c..02671ee15 100644 --- a/src/tactic/arith/bound_manager.cpp +++ b/src/tactic/arith/bound_manager.cpp @@ -28,6 +28,19 @@ bound_manager::~bound_manager() { reset(); } +bound_manager* bound_manager::translate(ast_manager& dst_m) { + bound_manager* result = alloc(bound_manager, dst_m); + ast_translation tr(m(), dst_m); + expr_dependency_translation edtr(tr); + for (auto& kv : m_lowers) result->m_lowers.insert(tr(kv.m_key), kv.m_value); + for (auto& kv : m_uppers) result->m_uppers.insert(tr(kv.m_key), kv.m_value); + for (auto& kv : m_lower_deps) result->m_lower_deps.insert(tr(kv.m_key), edtr(kv.m_value)); + for (auto& kv : m_upper_deps) result->m_upper_deps.insert(tr(kv.m_key), edtr(kv.m_value)); + for (expr* e : m_bounded_vars) result->m_bounded_vars.push_back(tr(e)); + return result; +} + + static decl_kind swap_decl(decl_kind k) { switch (k) { case OP_LE: return OP_GE; diff --git a/src/tactic/arith/bound_manager.h b/src/tactic/arith/bound_manager.h index 6a4dc2c96..4e1922bf5 100644 --- a/src/tactic/arith/bound_manager.h +++ b/src/tactic/arith/bound_manager.h @@ -47,6 +47,8 @@ public: bound_manager(ast_manager & m); ~bound_manager(); + bound_manager* translate(ast_manager& dst_m); + ast_manager & m() const { return m_util.get_manager(); } void operator()(goal const & g); diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 4ef909234..c8d5d1eb3 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -73,8 +73,17 @@ public: } } - virtual solver* translate(ast_manager& m, params_ref const& p) { - return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p)); + virtual solver* translate(ast_manager& dst_m, params_ref const& p) { + flush_assertions(); + bounded_int2bv_solver* result = alloc(bounded_int2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); + ast_translation tr(m, dst_m); + for (auto& kv : m_int2bv) result->m_int2bv.insert(tr(kv.m_key), tr(kv.m_value)); + for (auto& kv : m_bv2int) result->m_bv2int.insert(tr(kv.m_key), tr(kv.m_value)); + for (auto& kv : m_bv2offset) result->m_bv2offset.insert(tr(kv.m_key), kv.m_value); + for (func_decl* f : m_bv_fns) result->m_bv_fns.push_back(tr(f)); + for (func_decl* f : m_int_fns) result->m_int_fns.push_back(tr(f)); + for (bound_manager* b : m_bounds) result->m_bounds.push_back(b->translate(dst_m)); + return result; } virtual void assert_expr(expr * t) { diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 39519af4e..353ea4441 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -50,7 +50,7 @@ public: virtual ~enum2bv_solver() {} - virtual solver* translate(ast_manager& m, params_ref const& p) { + virtual solver* translate(ast_manager& m, params_ref const& p) { return alloc(enum2bv_solver, m, p, m_solver->translate(m, p)); } diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index d0e5598c7..b151b9bb3 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -49,7 +49,7 @@ public: virtual ~pb2bv_solver() {} virtual solver* translate(ast_manager& m, params_ref const& p) { - + flush_assertions(); return alloc(pb2bv_solver, m, p, m_solver->translate(m, p)); }