mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

neatify logging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-14 16:42:13 -08:00
parent b11ec3bfbf
commit ed7cac8cc0
4 changed files with 109 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_asymm_branch.cpp
View file

@ -84,11 +84,11 @@ namespace sat {
if (s.m_inconsistent) if (s.m_inconsistent)
break; break;
unsigned num_elim = m_elim_literals + m_tr - elim; unsigned num_elim = m_elim_literals + m_tr - elim;
IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";); IF_VERBOSE(2, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
if (num_elim == 0) if (num_elim == 0)
break; break;
} }
IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) IF_VERBOSE(2, if (m_elim_learned_literals > eliml0)
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";); verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
return m_elim_literals > elim0; return m_elim_literals > elim0;
} }
@ -98,7 +98,7 @@ namespace sat {
unsigned elim = m_elim_literals; unsigned elim = m_elim_literals;
process(nullptr, s.m_clauses); process(nullptr, s.m_clauses);
s.propagate(false); s.propagate(false);
IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) IF_VERBOSE(2, if (m_elim_learned_literals > eliml0)
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";); verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
return m_elim_literals > elim; return m_elim_literals > elim;
} }

124
src/sat/sat_solver.cpp
View file

@ -534,7 +534,7 @@ namespace sat {
void solver::defrag_clauses() { void solver::defrag_clauses() {
if (memory_pressure()) return; if (memory_pressure()) return;
pop(scope_lvl()); pop(scope_lvl());
IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n"); IF_VERBOSE(2, verbose_stream() << "(sat-defrag)\n");
clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx]; clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx];
ptr_vector<clause> new_clauses, new_learned; ptr_vector<clause> new_clauses, new_learned;
for (clause* c : m_clauses) c->unmark_used(); for (clause* c : m_clauses) c->unmark_used();
@ -1626,6 +1626,8 @@ namespace sat {
m_gc_threshold = m_config.m_gc_initial; m_gc_threshold = m_config.m_gc_initial;
m_defrag_threshold = 2; m_defrag_threshold = 2;
m_restarts = 0; m_restarts = 0;
m_last_position_log = 0;
m_restart_logs = 0;
m_simplifications = 0; m_simplifications = 0;
m_conflicts_since_init = 0; m_conflicts_since_init = 0;
m_next_simplify = m_config.m_simplify_delay; m_next_simplify = m_config.m_simplify_delay;
@ -1879,12 +1881,72 @@ namespace sat {
void solver::restart(bool to_base) { void solver::restart(bool to_base) {
m_stats.m_restart++; m_stats.m_restart++;
m_restarts++; m_restarts++;
if (m_conflicts_since_init > m_restart_next_out + 500) { if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) {
m_restart_next_out = m_conflicts_since_init; m_restart_logs++;
IF_VERBOSE(1, if (0 == m_restart_next_out) {
verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision m_restart_next_out = 1;
<< " :restarts " << m_stats.m_restart << mk_stat(*this) }
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); else {
m_restart_next_out = (3*m_restart_next_out)/2 + 1;
}
std::stringstream strm;
strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " "
<< std::setw(6) << m_stats.m_decision << " "
<< std::setw(4) << m_stats.m_restart
<< mk_stat(*this)
<< " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
std::string str(strm.str());
svector<size_t> nums;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;
while (i < str.size() && str[i] == ' ') ++i;
// position of first character after space
if (i < str.size()) {
nums.push_back(i);
}
}
bool same = m_last_positions.size() == nums.size();
size_t diff = 0;
for (unsigned i = 0; i < nums.size() && same; ++i) {
if (m_last_positions[i] > nums[i]) diff += m_last_positions[i] - nums[i];
if (m_last_positions[i] < nums[i]) diff += nums[i] - m_last_positions[i];
}
if (m_last_positions.empty() || m_restart_logs >= 20 + m_last_position_log || (m_restart_logs >= 6 + m_last_position_log && (!same || diff > 3))) {
m_last_position_log = m_restart_logs;
// conflicts restarts learned gc time
// decisions clauses units memory
int adjust[9] = { -3, -3, -3, -1, -3, -2, -1, -2, -1 };
char* tag[9] = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" };
std::stringstream l1, l2;
l1 << "(sat.stats ";
l2 << "(sat.stats ";
size_t p1 = 11, p2 = 11;
SASSERT(nums.size() == 9);
for (unsigned i = 0; i < 9 && i < nums.size(); ++i) {
size_t p = nums[i];
if (i & 0x1) {
// odd positions
for (; p2 < p + adjust[i]; ++p2) l2 << " ";
p2 += strlen(tag[i]);
l2 << tag[i];
}
else {
// even positions
for (; p1 < p + adjust[i]; ++p1) l1 << " ";
p1 += strlen(tag[i]);
l1 << tag[i];
}
}
for (; p1 + 2 < str.size(); ++p1) l1 << " ";
for (; p2 + 2 < str.size(); ++p2) l2 << " ";
l1 << ")\n";
l2 << ")\n";
IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str());
m_last_positions.reset();
m_last_positions.append(nums);
}
IF_VERBOSE(1, verbose_stream() << str);
} }
IF_VERBOSE(30, display_status(verbose_stream());); IF_VERBOSE(30, display_status(verbose_stream()););
pop_reinit(restart_level(to_base)); pop_reinit(restart_level(to_base));
@ -3503,16 +3565,39 @@ namespace sat {
} }
std::ostream& solver::display_justification(std::ostream & out, justification const& js) const { std::ostream& solver::display_justification(std::ostream & out, justification const& js) const {
out << js; switch (js.get_kind()) {
if (js.is_clause()) { case justification::NONE:
out << get_clause(js); out << "none "; // << js.level();
break;
case justification::BINARY:
out << "binary " << js.get_literal() << "@" << lvl(js.get_literal());
break;
case justification::TERNARY:
out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " ";
out << js.get_literal2() << "@" << lvl(js.get_literal2());
break;
case justification::CLAUSE: {
out << "(";
bool first = true;
for (literal l : get_clause(js)) {
if (first) first = false; else out << " ";
out << l << "@" << lvl(l);
}
out << ")";
break;
} }
else if (js.is_ext_justification() && m_ext) { case justification::EXT_JUSTIFICATION:
m_ext->display_justification(out << " ", js.get_ext_justification_idx()); if (m_ext) {
m_ext->display_justification(out << " ", js.get_ext_justification_idx());
}
break;
default:
break;
} }
return out; return out;
} }
unsigned solver::num_clauses() const { unsigned solver::num_clauses() const {
unsigned num_cls = m_trail.size(); // units; unsigned num_cls = m_trail.size(); // units;
unsigned l_idx = 0; unsigned l_idx = 0;
@ -4329,16 +4414,11 @@ namespace sat {
void mk_stat::display(std::ostream & out) const { void mk_stat::display(std::ostream & out) const {
unsigned given, learned; unsigned given, learned;
m_solver.num_binary(given, learned); m_solver.num_binary(given, learned);
if (!m_solver.m_clauses.empty()) out << " " << std::setw(5) << m_solver.m_clauses.size() + given << "/" << given;
out << " :clauses " << m_solver.m_clauses.size() + given << "/" << given; out << " " << std::setw(5) << (m_solver.m_learned.size() + learned - m_solver.m_num_frozen) << "/" << learned;
if (!m_solver.m_learned.empty()) { out << " " << std::setw(3) << m_solver.init_trail_size();
out << " :learned " << (m_solver.m_learned.size() + learned - m_solver.m_num_frozen) << "/" << learned; out << " " << std::setw(7) << m_solver.m_stats.m_gc_clause << " ";
if (m_solver.m_num_frozen > 0) out << " " << std::setw(7) << mem_stat();
out << " :frozen " << m_solver.m_num_frozen;
}
out << " :units " << m_solver.init_trail_size();
out << " :gc-clause " << m_solver.m_stats.m_gc_clause;
out << mem_stat();
} }
std::ostream & operator<<(std::ostream & out, mk_stat const & stat) { std::ostream & operator<<(std::ostream & out, mk_stat const & stat) {

3
src/sat/sat_solver.h
View file

@ -421,6 +421,9 @@ namespace sat {
void mk_model(); void mk_model();
bool check_model(model const & m) const; bool check_model(model const & m) const;
void restart(bool to_base); void restart(bool to_base);
svector<size_t> m_last_positions;
unsigned m_last_position_log;
unsigned m_restart_logs;
unsigned restart_level(bool to_base); unsigned restart_level(bool to_base);
bool should_restart() const; bool should_restart() const;
void set_next_restart(); void set_next_restart();

3
src/sat/sat_types.h
View file

@ -220,8 +220,7 @@ namespace sat {
inline std::ostream & operator<<(std::ostream & out, mem_stat const & m) { inline std::ostream & operator<<(std::ostream & out, mem_stat const & m) {
double mem = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024); double mem = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
out << " :memory " << std::fixed << std::setprecision(2) << mem; return out << std::fixed << std::setprecision(2) << mem;
return out;
} }
struct dimacs_lit { struct dimacs_lit {