mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

add debugging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-15 18:59:19 -07:00
parent d4977cb2db
commit cdf080061e
1 changed files with 28 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/sat/sat_lookahead.h
View file

@ -520,7 +520,7 @@ namespace sat {
struct arcs : public literal_vector {}; struct arcs : public literal_vector {};
// Knuth uses a shared pool of fixed size for arcs. // Knuth uses a shared pool of fixed size for arcs.
// Should it be useful we could use this approach tooo // Should it be useful we could use this approach too
// by changing the arcs abstraction and associated functions. // by changing the arcs abstraction and associated functions.
struct dfs_info { struct dfs_info {
@ -682,14 +682,16 @@ namespace sat {
std::ostream& display_dfs(std::ostream& out) const { std::ostream& display_dfs(std::ostream& out) const {
for (unsigned i = 0; i < m_candidates.size(); ++i) { for (unsigned i = 0; i < m_candidates.size(); ++i) {
literal l(m_candidates[i].m_var, false); literal l(m_candidates[i].m_var, false);
arcs const& a1 = get_arcs(l); display_dfs(out, l);
if (!a1.empty()) { display_dfs(out, ~l);
out << l << " -> " << a1 << "\n"; }
} return out;
arcs const& a2 = get_arcs(~l); }
if (!a2.empty()) {
out << ~l << " -> " << a2 << "\n"; std::ostream& display_dfs(std::ostream& out, literal l) const {
} arcs const& a1 = get_arcs(l);
if (!a1.empty()) {
out << l << " -> " << a1 << "\n";
} }
return out; return out;
} }
@ -698,12 +700,23 @@ namespace sat {
display_dfs(out); display_dfs(out);
for (unsigned i = 0; i < m_candidates.size(); ++i) { for (unsigned i = 0; i < m_candidates.size(); ++i) {
literal l(m_candidates[i].m_var, false); literal l(m_candidates[i].m_var, false);
out << l << " := " << get_parent(l) << "\n"; display_scc(out, l);
out << ~l << " := " << get_parent(~l) << "\n"; display_scc(out, ~l);
} }
return out; return out;
} }
std::ostream& display_scc(std::ostream& out, literal l) const {
out << l << " := " << get_parent(l)
<< " min: " << get_min(l)
<< " rank: " << get_rank(l)
<< " height: " << get_height(l)
<< " link: " << get_link(l)
<< " vcomp: " << get_vcomp(l) << "\n";
return out;
}
// ------------------------------------ // ------------------------------------
// lookahead forest // lookahead forest
// sat11.w 115-121 // sat11.w 115-121
@ -720,13 +733,13 @@ namespace sat {
} }
void find_heights() { void find_heights() {
TRACE("sat", tout << m_settled << "\n";); TRACE("sat", display_scc(tout << m_settled << "\n"););
literal pp = null_literal; literal pp = null_literal;
set_child(pp, null_literal); set_child(pp, null_literal);
unsigned h = 0; unsigned h = 0;
literal w; literal w;
for (unsigned i = 0; i < m_settled.size(); ++i) { for (unsigned i = m_settled.size(); i > 0; ) {
literal u = m_settled[i]; literal u = m_settled[--i];
literal p = get_parent(u); literal p = get_parent(u);
if (p != pp) { if (p != pp) {
h = 0; h = 0;
@ -751,6 +764,7 @@ namespace sat {
set_child(w, u); set_child(w, u);
} }
} }
TRACE("sat", display_scc(tout); );
} }
struct literal_offset { struct literal_offset {
literal m_lit; literal m_lit;