From c870b77366a141e60e4fe3ecb48156fb49cad6a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Jun 2017 17:25:06 -0700 Subject: [PATCH] fixes to lookahead Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.h | 1 + src/sat/sat_lookahead.cpp | 15 +++++++++------ src/sat/sat_solver/inc_sat_solver.cpp | 8 +++++++- src/smt/smt_solver.cpp | 5 +++++ src/solver/combined_solver.cpp | 4 ++++ src/solver/solver.cpp | 4 ++++ src/solver/solver.h | 2 +- src/solver/tactic2solver.cpp | 6 ++++++ src/tactic/portfolio/bounded_int2bv_solver.cpp | 2 +- src/tactic/portfolio/enum2bv_solver.cpp | 2 +- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- 11 files changed, 40 insertions(+), 11 deletions(-) diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 27168e2ca..24d0408fc 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -107,6 +107,7 @@ namespace opt { virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + virtual expr_ref lookahead(expr_ref_vector const& candidates) { return expr_ref(m.mk_true(), m); } void set_logic(symbol const& logic); smt::theory_var add_objective(app* term); diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index fd6860ff3..347228b79 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -151,7 +151,7 @@ namespace sat { } if (m_num_tc1 < m_config.m_tc1_limit) { ++m_num_tc1; - IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";); + IF_VERBOSE(30, verbose_stream() << "tc1: " << u << " " << w << "\n";); add_binary(u, w); } } @@ -285,9 +285,11 @@ namespace sat { for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { SASSERT(is_undef(*it)); bool_var x = *it; - if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) { - m_candidates.push_back(candidate(x, m_rating[x])); - sum += m_rating[x]; + if (!m_select_lookahead_vars.empty()) { + if (m_select_lookahead_vars.contains(x)) { + m_candidates.push_back(candidate(x, m_rating[x])); + sum += m_rating[x]; + } } else if (newbies || active_prefix(x)) { m_candidates.push_back(candidate(x, m_rating[x])); @@ -1214,7 +1216,7 @@ namespace sat { continue; } if (scope_lvl() == 1) { - IF_VERBOSE(3, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";); + IF_VERBOSE(30, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";); } TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";); reset_wnb(lit); @@ -1602,12 +1604,13 @@ namespace sat { literal lookahead::select_lookahead(bool_var_vector const& vars) { + IF_VERBOSE(1, verbose_stream() << "(sat-select " << vars.size() << ")\n";); scoped_ext _sext(*this); m_search_mode = lookahead_mode::searching; scoped_level _sl(*this, c_fixed_truth); init(); if (inconsistent()) return null_literal; - inc_istamp(); + inc_istamp(); for (auto v : vars) { m_select_lookahead_vars.insert(v); } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index eb931d428..3fa9f4c81 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -281,8 +281,10 @@ public: } virtual expr_ref lookahead(expr_ref_vector const& candidates) { + IF_VERBOSE(1, verbose_stream() << "(sat-lookahead " << candidates.size() << ")\n";); sat::bool_var_vector vars; expr_ref_vector lit2expr(m); + lit2expr.resize(m_solver.num_vars() * 2); m_map.mk_inv(lit2expr); for (auto c : candidates) { sat::bool_var v = m_map.to_bool_var(c); @@ -290,17 +292,21 @@ public: vars.push_back(v); } } + IF_VERBOSE(1, verbose_stream() << "vars: " << vars.size() << "\n";); if (vars.empty()) { return expr_ref(m.mk_true(), m); } sat::literal l = m_solver.select_lookahead(vars); if (m_solver.inconsistent()) { + IF_VERBOSE(1, verbose_stream() << "(sat-lookahead inconsistent)\n";); return expr_ref(m.mk_false(), m); } if (l == sat::null_literal) { return expr_ref(m.mk_true(), m); } - return expr_ref(lit2expr[l.index()].get(), m); + expr_ref result(lit2expr[l.index()].get(), m); + IF_VERBOSE(1, verbose_stream() << "solution: " << l << " " << result << "\n";); + return result; } virtual void get_lemmas(expr_ref_vector & lemmas) { IF_VERBOSE(1, verbose_stream() << "(sat-get-lemmas " << lemmas.size() << ")\n";); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index cd912b72e..2ca5a11c3 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -219,6 +219,11 @@ namespace smt { return m_context.get_formulas()[idx]; } + virtual expr_ref lookahead(expr_ref_vector const& candidates) { + ast_manager& m = get_manager(); + return expr_ref(m.mk_true(), m); + } + struct collect_fds_proc { ast_manager & m; func_decl_set & m_fds; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index d67643edf..5d6cd232f 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -274,6 +274,10 @@ public: return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions(); } + virtual expr_ref lookahead(expr_ref_vector const& candidates) { + return m_solver1->lookahead(candidates); + } + virtual expr * get_assumption(unsigned idx) const { unsigned c1 = m_solver1->get_num_assumptions(); if (idx < c1) return m_solver1->get_assumption(idx); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 59b950972..7175eacbf 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -162,9 +162,13 @@ bool solver::is_literal(ast_manager& m, expr* e) { return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } +#if 0 expr_ref solver::lookahead(expr_ref_vector const& candidates) { + std::cout << "lookahead: " << candidates.size() << "\n"; + INVOKE_DEBUGGER(); ast_manager& m = candidates.get_manager(); return expr_ref(m.mk_true(), m); } +#endif diff --git a/src/solver/solver.h b/src/solver/solver.h index 51bff08ad..56890f7c0 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -176,7 +176,7 @@ public: \brief extract a lookahead candidates for branching. */ - virtual expr_ref lookahead(expr_ref_vector const& candidates); + virtual expr_ref lookahead(expr_ref_vector const& candidates) = 0; /** \brief extract learned lemmas. diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index e451f57d4..f9d5a4b0f 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -75,6 +75,12 @@ public: virtual expr * get_assertion(unsigned idx) const; virtual ast_manager& get_manager() const; + + virtual expr_ref lookahead(expr_ref_vector const& candidates) { + ast_manager& m = get_manager(); + std::cout << "tactic2solver\n"; + return expr_ref(m.mk_true(), m); + } }; ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); } diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 3645ba97a..aeaa88bc2 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -149,7 +149,7 @@ public: virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } - virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); } + virtual expr_ref lookahead(expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(candidates); } virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index a40f2988a..d50dee57c 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -97,7 +97,7 @@ public: virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } - virtual expr_ref lookahead(expr_ref_vector& candidates) { return m_solver->lookahead(candidates); } + virtual expr_ref lookahead(expr_ref_vector const& candidates) { return m_solver->lookahead(candidates); } virtual void get_lemmas(expr_ref_vector & lemmas) { m_solver->get_lemmas(lemmas); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 8bf6b7e39..46a5912b0 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -93,7 +93,7 @@ public: virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } - virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); } + virtual expr_ref lookahead(expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(candidates); } virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {