From 3714e520bed8e95696bfe9e2e51032eece1a2c73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Oct 2016 08:27:11 -0700 Subject: [PATCH] fix performance bottlnecks: gc of literals walk through potentially huge watch-lists, avoid user-push/pop around calls to solver2tactic Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 17 ++++++++++------- src/solver/solver2tactic.cpp | 21 +++++++++++---------- 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e70a30a5a..e0bb0f2a3 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -745,7 +745,7 @@ namespace sat { if (m_config.m_max_conflicts == 0) { - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";); + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";); return l_undef; } @@ -757,7 +757,7 @@ namespace sat { return r; if (m_conflicts > m_config.m_max_conflicts) { - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = " << m_conflicts << "\"\n";); + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";); return l_undef; } @@ -1016,7 +1016,7 @@ namespace sat { set_conflict(justification(), ~lit); m_conflict_lvl = scope_lvl(); resolve_conflict_for_unsat_core(); - IF_VERBOSE(3, verbose_stream() << "core: " << m_core << "\n";); + IF_VERBOSE(3, verbose_stream() << "(sat.core: " << m_core << ")\n";); update_min_core(); SASSERT(m_min_core_valid); m_weight += weights[i]; @@ -1029,7 +1029,7 @@ namespace sat { if (m_core.size() <= 3) { m_inconsistent = true; TRACE("opt", tout << "found small core: " << m_core << "\n";); - IF_VERBOSE(11, verbose_stream() << "small core: " << m_core << "\n";); + IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";); return true; } pop_assumption(); @@ -1042,7 +1042,7 @@ namespace sat { } } TRACE("sat", tout << "initialized\n";); - IF_VERBOSE(11, verbose_stream() << "Blocker: " << m_blocker << "\nCore: " << m_min_core << "\n";); + IF_VERBOSE(11, verbose_stream() << "(sat.blocker: " << m_blocker << "\nCore: " << m_min_core << ")\n";); if (m_weight >= max_weight) { // block the current correction set candidate. ++m_stats.m_blocked_corr_sets; @@ -2584,7 +2584,7 @@ namespace sat { // void solver::user_push() { - literal lit; + literal lit; bool_var new_v = mk_var(true, false); lit = literal(new_v, false); m_user_scope_literals.push_back(lit); @@ -2683,6 +2683,9 @@ namespace sat { while (num_scopes > 0) { literal lit = m_user_scope_literals.back(); m_user_scope_literals.pop_back(); + get_wlist(lit).reset(); + get_wlist(~lit).reset(); + gc_lit(m_learned, lit); gc_lit(m_clauses, lit); gc_bin(true, lit); @@ -3218,7 +3221,7 @@ namespace sat { delete_unfixed(vars); } extract_fixed_consequences(num_units, assumptions, vars, conseq); - IF_VERBOSE(1, verbose_stream() << "(get-consequences" + IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences" << " iterations: " << num_iterations << " variables: " << vars.size() << " fixed: " << conseq.size() diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 8646d4813..76ebf73dd 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -84,6 +84,7 @@ class solver2tactic : public tactic { ast_manager& m; ref m_solver; params_ref m_params; + statistics m_st; public: solver2tactic(solver* s): @@ -109,14 +110,14 @@ public: ptr_vector assumptions; ref fmc; extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc); - m_solver->push(); - m_solver->assert_expr(clauses); - lbool r = m_solver->check_sat(assumptions.size(), assumptions.c_ptr()); + ref local_solver = m_solver->translate(m, m_params); + local_solver->assert_expr(clauses); + lbool r = local_solver->check_sat(assumptions.size(), assumptions.c_ptr()); switch (r) { case l_true: if (in->models_enabled()) { model_ref mdl; - m_solver->get_model(mdl); + local_solver->get_model(mdl); mc = model2model_converter(mdl.get()); mc = concat(fmc.get(), mc.get()); } @@ -130,11 +131,11 @@ public: proof* pr = 0; expr_dependency* lcore = 0; if (in->proofs_enabled()) { - pr = m_solver->get_proof(); + pr = local_solver->get_proof(); } if (in->unsat_core_enabled()) { ptr_vector core; - m_solver->get_unsat_core(core); + local_solver->get_unsat_core(core); for (unsigned i = 0; i < core.size(); ++i) { lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(core[i]))); } @@ -150,15 +151,15 @@ public: if (m.canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } - throw tactic_exception(m_solver->reason_unknown().c_str()); + throw tactic_exception(local_solver->reason_unknown().c_str()); } - m_solver->pop(1); + local_solver->collect_statistics(m_st); } virtual void collect_statistics(statistics & st) const { - m_solver->collect_statistics(st); + st.copy(m_st); } - virtual void reset_statistics() {} + virtual void reset_statistics() { m_st.reset(); } virtual void cleanup() { } virtual void reset() { cleanup(); }