mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
debugging unsat core generation...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
78f29416f1
commit
5f735d2f12
24
lib/goal.cpp
24
lib/goal.cpp
|
@ -284,6 +284,30 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons
|
|||
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
|
||||
}
|
||||
|
||||
void goal::display_with_dependencies(std::ostream & out) const {
|
||||
ptr_vector<expr> deps;
|
||||
out << "(goal";
|
||||
unsigned sz = size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
out << "\n |-";
|
||||
deps.reset();
|
||||
m().linearize(dep(i), deps);
|
||||
ptr_vector<expr>::iterator it = deps.begin();
|
||||
ptr_vector<expr>::iterator end = deps.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * d = *it;
|
||||
if (is_uninterp_const(d)) {
|
||||
out << " " << mk_ismt2_pp(d, m());
|
||||
}
|
||||
else {
|
||||
out << " #" << d->get_id();
|
||||
}
|
||||
}
|
||||
out << "\n " << mk_ismt2_pp(form(i), m(), 2);
|
||||
}
|
||||
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
|
||||
}
|
||||
|
||||
void goal::display(cmd_context & ctx) const {
|
||||
display(ctx, ctx.regular_stream());
|
||||
}
|
||||
|
|
|
@ -180,6 +180,7 @@ public:
|
|||
void display_dimacs(std::ostream & out) const;
|
||||
void display_with_dependencies(cmd_context & ctx, std::ostream & out) const;
|
||||
void display_with_dependencies(cmd_context & ctx) const;
|
||||
void display_with_dependencies(std::ostream & out) const;
|
||||
|
||||
bool sat_preserved() const {
|
||||
return prec() == PRECISE || prec() == UNDER;
|
||||
|
|
|
@ -67,6 +67,7 @@ struct simplify_tactic::imp {
|
|||
TRACE("after_simplifier_bug", g.display(tout););
|
||||
g.elim_redundancies();
|
||||
TRACE("after_simplifier", g.display(tout););
|
||||
TRACE("after_simplifier_detail", g.display_with_dependencies(tout););
|
||||
SASSERT(g.is_well_sorted());
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue