diff --git a/src/muz/pdr/pdr_smt_context_manager.h b/src/muz/pdr/pdr_smt_context_manager.h index 4775dc58f..ea8947ea1 100644 --- a/src/muz/pdr/pdr_smt_context_manager.h +++ b/src/muz/pdr/pdr_smt_context_manager.h @@ -71,23 +71,6 @@ namespace pdr { virtual expr* get_unsat_core_expr(unsigned i) { return m_context.get_unsat_core_expr(i); } }; - // TBD: - class sat_context : public smt_context { - sat::solver m_solver; - public: - sat_context(smt::kernel & ctx, smt_context_manager& p, app* pred); - virtual ~sat_context() {} - virtual void assert_expr(expr* e); - virtual lbool check(expr_ref_vector& assumptions); - virtual void get_model(model_ref& model); - virtual proof* get_proof(); - virtual void pop() { m_solver.pop(1); } - virtual void push() { m_solver.push(); } - // TBD: add unsat core extraction with sat::solver. - virtual unsigned get_unsat_core_size(); - virtual expr* get_unsat_core_expr(unsigned i); - }; - class smt_context_manager { smt_params& m_fparams; ast_manager& m; diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp index 62b36961b..6cad9a8c2 100644 --- a/src/opt/hitting_sets.cpp +++ b/src/opt/hitting_sets.cpp @@ -110,7 +110,8 @@ namespace opt { lbool compute_lower() { m_lower.reset(); - if (L1() && L2() && L3()) { + // L3() disabled: mostly a waste of time. + if (L1() && L2()) { return l_true; } else { @@ -238,7 +239,9 @@ namespace opt { lbool U1() { scoped_select _sc(*this); while (true) { - if (!compute_U1()) return l_undef; + if (!compute_U1()) { + return l_undef; + } unsigned i = 0, j = 0; set_undef_to_false(); if (values_satisfy_Ts(i)) { @@ -251,7 +254,7 @@ namespace opt { // literal to true. // - IF_VERBOSE(1, verbose_stream() << "(hs.refining exclusion set " << i << "\n";); + IF_VERBOSE(1, verbose_stream() << "(hs.refining exclusion set " << i << ")\n";); set const& T = m_T[i]; rational max_value(0); j = 0; @@ -270,7 +273,7 @@ namespace opt { if (l_false != selected(S[j])) break; } if (j == S.size()) { - IF_VERBOSE(1, verbose_stream() << "approximation failed, fall back to SAT\n";); + IF_VERBOSE(1, verbose_stream() << "(hs.fallback-to-SAT)\n";); return compute_U2(); } } @@ -327,7 +330,7 @@ namespace opt { m_value_saved.reset(); m_value_saved.append(m_value); if (m_upper > m_max_weight) { - IF_VERBOSE(0, verbose_stream() << "got worse upper bound\n";); + IF_VERBOSE(1, verbose_stream() << "(hs.bound_degradation " << m_upper << " )\n";); } return !m_cancel; } diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index bdac382f9..cd7540317 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -686,8 +686,9 @@ namespace opt { case l_true: seed2hs(false, hs); break; - case l_false: + case l_false: TRACE("opt", tout << "no more seeds\n";); + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.maxhs.no-more-seeds)\n";); m_lower = m_upper; return l_true; case l_undef: @@ -696,6 +697,7 @@ namespace opt { break; } case l_false: + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.maxhs.no-more-cores)\n";); TRACE("opt", tout << "no more cores\n";); m_lower = m_upper; return l_true; @@ -825,7 +827,7 @@ namespace opt { // Auxiliary Algorithm 10 for producing cores. // lbool generate_cores(ptr_vector& hs) { - bool core = false; + bool core = !m_at_lower_bound; while (true) { hs2seed(hs); lbool is_sat = check_subset(); @@ -869,25 +871,6 @@ namespace opt { } } - lbool next_seed(ptr_vector& hs, lbool core_found) { - - if (core_found == l_false && m_at_lower_bound) { - return l_true; - } - lbool is_sat = next_seed(); - switch(is_sat) { - case l_true: - seed2hs(false, hs); - return m_at_lower_bound?l_true:l_false; - case l_false: - TRACE("opt", tout << "no more seeds\n";); - return l_true; - case l_undef: - return l_undef; - } - return l_undef; - } - // // retrieve the next seed that satisfies state of hs. // state of hs must be satisfiable before optimization is called. @@ -922,9 +905,6 @@ namespace opt { // // check assignment returned by HS with the original // hard constraints. - // If the assignment is consistent with the hard constraints - // update the current model, otherwise, update the current lower - // bound. // lbool check_subset() { TRACE("opt", tout << "\n";); @@ -935,19 +915,7 @@ namespace opt { ensure_active(i); } } - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - switch (is_sat) { - case l_true: - update_model(); - break; - case l_false: - break; - default: - break; - } - TRACE("opt", tout << is_sat << "\n";); - - return is_sat; + return s().check_sat(m_asms.size(), m_asms.c_ptr()); } // @@ -957,18 +925,17 @@ namespace opt { // bool grow() { scoped_stopwatch _sw(m_stats.m_model_expansion_time); + model_ref mdl; + s().get_model(mdl); for (unsigned i = 0; i < num_soft(); ++i) { if (!m_seed[i]) { - if (is_true(m_model, m_soft[i].get())) { + if (is_true(mdl, m_soft[i].get())) { m_seed[i] = true; } else { ensure_active(i); m_asms.push_back(m_aux[i].get()); lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - IF_VERBOSE(3, verbose_stream() - << "check: " << mk_pp(m_asms.back(), m) - << ":" << is_sat << "\n";); TRACE("opt", tout << "check: " << mk_pp(m_asms.back(), m) << ":" << is_sat << "\n";); @@ -981,9 +948,7 @@ namespace opt { break; case l_true: ++m_stats.m_num_model_expansions_success; - update_model(); - TRACE("opt", model_smt2_pp(tout << mk_pp(m_aux[i].get(), m) << "\n", - m, *(m_model.get()), 0);); + s().get_model(mdl); m_seed[i] = true; break; } @@ -999,7 +964,12 @@ namespace opt { if (upper < m_upper) { m_upper = upper; m_hs.set_upper(upper); - TRACE("opt", tout << "new upper: " << m_upper << "\n";); + m_model = mdl; + m_assignment.reset(); + m_assignment.append(m_seed); + TRACE("opt", + tout << "new upper: " << m_upper << "\n"; + model_smt2_pp(tout, m, *(mdl.get()), 0);); } return true; } @@ -1049,13 +1019,6 @@ namespace opt { return true; } - void update_model() { - s().get_model(m_model); - for (unsigned i = 0; i < num_soft(); ++i) { - m_assignment[i] = is_true(m_model, m_soft[i].get()); - } - } - void print_asms(std::ostream& out, ptr_vector const& asms) { for (unsigned j = 0; j < asms.size(); ++j) { out << mk_pp(asms[j], m) << " "; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 0738f0118..b18bae06a 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -339,8 +339,8 @@ namespace sat { // Backtracking // // ----------------------- - public: void push(); + public: void pop(unsigned num_scopes); protected: