diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 77eb108a9..235fa4205 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -22,6 +22,7 @@ Notes: #include "tactic2solver.h" #include "goal.h" #include "probe.h" +#include "tactic.h" #include "smt_context.h" /** @@ -41,16 +42,16 @@ Notes: namespace opt { struct fu_malik::imp { - ast_manager& m; - ref m_s; + ast_manager& m; expr_ref_vector m_soft; expr_ref_vector m_orig_soft; expr_ref_vector m_aux; expr_ref_vector m_assignment; unsigned m_upper_size; + ref m_s; solver & m_original_solver; - bool m_use_new_bv_solver; + bool m_use_new_bv_solver; imp(ast_manager& m, solver& s, expr_ref_vector const& soft): m(m), @@ -82,6 +83,63 @@ namespace opt { * add at-most-one constraint with blocking */ + typedef obj_hashtable expr_set; + + void set2vector(expr_set const& set, expr_ref_vector & es) const { + es.reset(); + expr_set::iterator it = set.begin(), end = set.end(); + for (; it != end; ++it) { + es.push_back(*it); + } + } + + void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const { + set.reset(); + expr_set::iterator it = set1.begin(), end = set1.end(); + for (; it != end; ++it) { + set.insert(*it); + } + it = set2.begin(); + end = set2.end(); + for (; it != end; ++it) { + set.insert(*it); + } + } + + void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) { + if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { + core.reset(); + return; + } + + SASSERT(!literals.empty()); + if (literals.size() == 1) { + core.reset(); + core.insert(literals[0].get()); + return; + } + + unsigned mid = literals.size()/2; + expr_ref_vector ls1(m), ls2(m); + ls1.append(mid, literals.c_ptr()); + ls2.append(literals.size()-mid, literals.c_ptr() + mid); + + expr_ref_vector as1(m); + as1.append(assumptions); + as1.append(ls1); + expr_set core2; + quick_explain(as1, ls2, !ls1.empty(), core2); + + expr_ref_vector as2(m), cs2(m); + as2.append(assumptions); + set2vector(core2, cs2); + as2.append(cs2); + expr_set core1; + quick_explain(as2, ls1, !core2.empty(), core1); + + set_union(core1, core2, core); + } + lbool step() { IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";); expr_ref_vector assumptions(m), block_vars(m); @@ -95,12 +153,14 @@ namespace opt { ptr_vector core; if (m_use_new_bv_solver) { - unsigned i = 0; - while (s().check_sat(core.size(), core.c_ptr()) != l_false) { - IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";); - core.push_back(assumptions[i].get()); - ++i; + expr_set core_set; + expr_ref_vector empty(m); + quick_explain(empty, assumptions, true, core_set); + expr_set::iterator it = core_set.begin(), end = core_set.end(); + for (; it != end; ++it) { + core.push_back(*it); } + IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";); } else { s().get_unsat_core(core); @@ -164,11 +224,11 @@ namespace opt { probe *p = mk_is_qfbv_probe(); bool all_bv = (*p)(g).is_true(); if (all_bv) { - opt_solver & os = opt_solver::to_opt(m_original_solver); - smt::context & ctx = os.get_context(); - tactic* t = mk_qfbv_tactic(m, ctx.get_params()); + opt_solver & opt_s = opt_solver::to_opt(m_original_solver); + smt::context & ctx = opt_s.get_context(); + tactic_ref t = mk_qfbv_tactic(m, ctx.get_params()); // The new SAT solver hasn't supported unsat core yet - m_s = mk_tactic2solver(m, t); + m_s = mk_tactic2solver(m, t.get()); SASSERT(m_s != &m_original_solver); for (unsigned i = 0; i < num_assertions; ++i) { m_s->assert_expr(current_solver.get_assertion(i)); @@ -211,6 +271,11 @@ namespace opt { } } } + statistics st; + s().collect_statistics(st); + SASSERT(st.size() > 0); + opt_solver & opt_s = opt_solver::to_opt(m_original_solver); + opt_s.set_interim_stats(st); // We are done and soft_constraints has // been updated with the max-sat assignment. return is_sat; diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index fee4a8663..a8e7d8535 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -55,7 +55,13 @@ namespace opt { } void opt_solver::collect_statistics(statistics & st) const { - m_context.collect_statistics(st); + // Hack to display fu_malik statistics + if (m_stats.size() > 0) { + st.copy(m_stats); + } + else { + m_context.collect_statistics(st); + } } void opt_solver::assert_expr(expr * t) { @@ -213,6 +219,10 @@ namespace opt { } return dynamic_cast(s); } + + void opt_solver::set_interim_stats(statistics & st) { + m_stats.copy(st); + } void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, char const * status, char const * attributes) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index de7ef0b1d..e5af48a5c 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -46,7 +46,8 @@ namespace opt { bool m_objective_enabled; svector m_objective_vars; vector m_objective_values; - bool m_is_dump; + bool m_is_dump; + statistics m_stats; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); virtual ~opt_solver(); @@ -77,7 +78,8 @@ namespace opt { expr_ref block_upper_bound(unsigned obj_index, inf_eps const& val); static opt_solver& to_opt(solver& s); - + void set_interim_stats(statistics & st); + class toggle_objective { opt_solver& s; bool m_old_value; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3e9b60260..ec00be897 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -671,6 +671,7 @@ namespace sat { // // ----------------------- lbool solver::check() { + IF_VERBOSE(0, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";); SASSERT(scope_lvl() == 0); #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { @@ -1970,7 +1971,7 @@ namespace sat { m_cancel = f; } - void solver::collect_statistics(statistics & st) { + void solver::collect_statistics(statistics & st) { m_stats.collect_statistics(st); m_cleaner.collect_statistics(st); m_simplifier.collect_statistics(st); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 95b150a8c..0fdde612d 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -135,6 +135,7 @@ public: proof_converter_ref & pc, expr_dependency_ref & core) { try { + IF_VERBOSE(0, verbose_stream() << "(smt.smt-tactic using the old SAT solver)\n";); SASSERT(in->is_well_sorted()); ast_manager & m = in->m(); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 1268fbcea..dde03f962 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -40,6 +40,7 @@ class tactic2solver : public solver_na2as { bool m_produce_models; bool m_produce_proofs; bool m_produce_unsat_cores; + statistics m_stats; public: tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic); virtual ~tactic2solver(); @@ -161,6 +162,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass m_result->m_unknown = ex.msg(); } m_tactic->collect_statistics(m_result->m_stats); + m_tactic->collect_statistics(m_stats); m_result->m_model = md; m_result->m_proof = pr; if (m_produce_unsat_cores) { @@ -177,9 +179,9 @@ void tactic2solver::set_cancel(bool f) { m_tactic->set_cancel(f); } -void tactic2solver::collect_statistics(statistics & st) const { - if (m_result.get()) - m_result->collect_statistics(st); +void tactic2solver::collect_statistics(statistics & st) const { + st.copy(m_stats); + SASSERT(m_stats.size() > 0); } void tactic2solver::get_unsat_core(ptr_vector & r) { diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index cdbc6927e..51b040332 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -31,15 +31,6 @@ Notes: #define MEMLIMIT 300 -tactic * mk_new_sat_tactic(ast_manager & m) { - IF_VERBOSE(0, verbose_stream() << "Try to use the new SAT solver." << std::endl;); - tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), - and_then(mk_simplify_tactic(m), - mk_smt_tactic()), - mk_sat_tactic(m)); - return new_sat; -} - tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; main_p.set_bool("elim_and", true); @@ -94,7 +85,10 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * new_sat = and_then(mk_simplify_tactic(m), mk_smt_tactic()); #else - tactic * new_sat = mk_new_sat_tactic(m); + tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + and_then(mk_simplify_tactic(m), + mk_smt_tactic()), + mk_sat_tactic(m)); #endif tactic * st = using_params(and_then(preamble_st,