mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

display justifications compactly for tracing #4575

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-08 13:32:41 -07:00
parent ab7b8b6ec5
commit 80cc45c5c1
3 changed files with 38 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.h
View file

@ -1572,6 +1572,12 @@ public:
bool has_trace_stream() const { return m_trace_stream != nullptr; }
std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
struct suspend_trace {
ast_manager& m;
std::fstream* m_tr;
suspend_trace(ast_manager& m): m(m), m_tr(m.m_trace_stream) { m.m_trace_stream = nullptr; }
~suspend_trace() { m.m_trace_stream = m_tr; }
};
void enable_int_real_coercions(bool f) { m_int_real_coercions = f; }
bool int_real_coercions() const { return m_int_real_coercions; }

2
src/smt/smt_context.h
View file

@ -1406,6 +1406,8 @@ namespace smt {
std::ostream& display(std::ostream& out, b_justification j) const;
std::ostream& display_compact_j(std::ostream& out, b_justification j) const;
// -----------------------------------
//
// Debugging support

31
src/smt/smt_context_pp.cpp
View file

@ -618,15 +618,44 @@ namespace smt {
return out << "\n";
}
std::ostream& context::display_compact_j(std::ostream& out, b_justification j) const {
switch (j.get_kind()) {
case b_justification::AXIOM:
out << "axiom";
break;
case b_justification::BIN_CLAUSE:
out << "bin " << j.get_literal();
break;
case b_justification::CLAUSE: {
clause * cls = j.get_clause();
out << "clause ";
if (cls) out << literal_vector(cls->get_num_literals(), cls->begin());
break;
}
case b_justification::JUSTIFICATION: {
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
out << "justification " << j.get_justification()->get_from_theory() << ": ";
out << lits;
break;
}
default:
UNREACHABLE();
break;
}
return out << "\n";
}
void context::trace_assign(literal l, b_justification j, bool decision) const {
SASSERT(m.has_trace_stream());
std::ostream & out = m.trace_stream();
ast_manager::suspend_trace _st(m);
out << "[assign] ";
display_literal(out, l);
if (decision)
out << " decision";
out << " ";
display(out, j);
display_compact_j(out, j);
}
std::ostream& operator<<(std::ostream& out, enode_pp const& p) {