From 5f735d2f12a24158a66e3a92dc2fd8910160b9b2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Oct 2012 01:10:19 -0700
Subject: [PATCH] debugging unsat core generation...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
lib/goal.cpp | 24 ++++++++++++++++++++++++
lib/goal.h | 1 +
lib/simplify_tactic.cpp | 1 +
3 files changed, 26 insertions(+)
diff --git a/lib/goal.cpp b/lib/goal.cpp
index 0146ac252..71f3a097c 100644
--- a/lib/goal.cpp
+++ b/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());
}
diff --git a/lib/goal.h b/lib/goal.h
index 9beb9421e..61c7e2081 100644
--- a/lib/goal.h
+++ b/lib/goal.h
@@ -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;
diff --git a/lib/simplify_tactic.cpp b/lib/simplify_tactic.cpp
index 2a912822b..a7ce0b39f 100644
--- a/lib/simplify_tactic.cpp
+++ b/lib/simplify_tactic.cpp
@@ -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());
}