mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-08 08:15:47 +00:00
Code Activity

disable fixes for #2128 and related as it breaks model evaluation time in regressions, set longer delay for inprocessing in sat solver, report stats

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-09 16:06:02 -08:00
parent c7bd985fac
commit 24dfdfe9bc
9 changed files with 44 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/sat/sat_asymm_branch.cpp
View file

@ -44,26 +44,32 @@ namespace sat {
unsigned m_elim_literals;
unsigned m_elim_learned_literals;
unsigned m_tr;
unsigned m_units;
report(asymm_branch & a):
m_asymm_branch(a),
m_elim_literals(a.m_elim_literals),
m_elim_learned_literals(a.m_elim_learned_literals),
m_tr(a.m_tr) {
m_elim_learned_literals(a.m_elim_learned_literals),
m_tr(a.m_tr),
m_units(a.s.init_trail_size()) {
m_watch.start();
}
~report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(2,
unsigned num_learned = (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals);
unsigned num_total = (m_asymm_branch.m_elim_literals - m_elim_literals);
verbose_stream()
<< " (sat-asymm-branch :elim-literals " << (num_total - num_learned)
<< " :elim-learned-literals " << num_learned
<< " :hte " << (m_asymm_branch.m_tr - m_tr)
<< " :cost " << m_asymm_branch.m_counter
<< mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
unsigned num_units = (m_asymm_branch.s.init_trail_size() - m_units);
unsigned elim_lits = (num_total - num_learned);
unsigned tr = (m_asymm_branch.m_tr - m_tr);
verbose_stream() << " (sat-asymm-branch";
if (elim_lits > 0) verbose_stream() << " :elim-literals " << elim_lits;
if (num_learned > 0) verbose_stream() << " :elim-learned-literals " << num_learned;
if (num_units > 0) verbose_stream() << " :units " << num_units;
if (tr > 0) verbose_stream() << " :hte " << tr;
verbose_stream() << " :cost " << m_asymm_branch.m_counter;
verbose_stream() << mem_stat();
verbose_stream() << m_watch << ")\n";);
}
};
@ -84,11 +90,11 @@ namespace sat {
if (s.m_inconsistent)
break;
unsigned num_elim = m_elim_literals + m_tr - elim;
IF_VERBOSE(2, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
IF_VERBOSE(4, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
if (num_elim == 0)
break;
}
IF_VERBOSE(2, if (m_elim_learned_literals > eliml0)
IF_VERBOSE(4, if (m_elim_learned_literals > eliml0)
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
return m_elim_literals > elim0;
}
@ -98,7 +104,7 @@ namespace sat {
unsigned elim = m_elim_literals;
process(nullptr, s.m_clauses);
s.propagate(false);
IF_VERBOSE(2, if (m_elim_learned_literals > eliml0)
IF_VERBOSE(4, if (m_elim_learned_literals > eliml0)
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
return m_elim_literals > elim;
}