mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix performance bottlnecks: gc of literals walk through potentially huge watch-lists, avoid user-push/pop around calls to solver2tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-28 08:27:11 -07:00
parent ca309341c3
commit 3714e520be
2 changed files with 21 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/sat/sat_solver.cpp
View file

@ -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()

21
src/solver/solver2tactic.cpp
View file

@ -84,6 +84,7 @@ class solver2tactic : public tactic {
ast_manager& m;
ref<solver> m_solver;
params_ref m_params;
statistics m_st;
public:
solver2tactic(solver* s):
@ -109,14 +110,14 @@ public:
ptr_vector<expr> assumptions;
ref<filter_model_converter> 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<solver> 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<expr> 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(); }