mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge pull request #1963 from Nils-Becker/master
Logging Improvements for the Axiom Profiler
This commit is contained in:
commit
abfb9989b6
|
@ -2376,6 +2376,13 @@ namespace smt {
|
|||
SASSERT(m_n2 != 0);
|
||||
if (m_n1->get_root() != m_n2->get_root())
|
||||
goto backtrack;
|
||||
|
||||
// We will use the common root when instantiating the quantifier => log the necessary equalities
|
||||
if (m_ast_manager.has_trace_stream()) {
|
||||
m_used_enodes.push_back(std::make_tuple(m_n1, m_n1->get_root()));
|
||||
m_used_enodes.push_back(std::make_tuple(m_n2, m_n2->get_root()));
|
||||
}
|
||||
|
||||
m_pc = m_pc->m_next;
|
||||
goto main_loop;
|
||||
|
||||
|
@ -2572,6 +2579,11 @@ namespace smt {
|
|||
if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \
|
||||
goto backtrack; \
|
||||
update_max_generation(m_n1, nullptr); \
|
||||
if (m_ast_manager.has_trace_stream()) { \
|
||||
for (unsigned i = 0; i < static_cast<const get_cgr *>(m_pc)->m_num_args; ++i) { \
|
||||
m_used_enodes.push_back(std::make_tuple(m_n1->get_arg(i), m_n1->get_arg(i)->get_root())); \
|
||||
} \
|
||||
} \
|
||||
m_registers[static_cast<const get_cgr *>(m_pc)->m_oreg] = m_n1; \
|
||||
m_pc = m_pc->m_next; \
|
||||
goto main_loop;
|
||||
|
|
|
@ -563,7 +563,7 @@ namespace smt {
|
|||
invert_trans(n1);
|
||||
n1->m_trans.m_target = n2;
|
||||
n1->m_trans.m_justification = js;
|
||||
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
n1->m_proof_is_logged = false;
|
||||
SASSERT(r1->trans_reaches(n1));
|
||||
// ---------------
|
||||
// r1 -> .. -> n1 -> n2 -> ... -> r2
|
||||
|
@ -743,14 +743,14 @@ namespace smt {
|
|||
eq_justification js = n->m_trans.m_justification;
|
||||
prev->m_trans.m_target = nullptr;
|
||||
prev->m_trans.m_justification = null_eq_justification;
|
||||
prev->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
prev->m_proof_is_logged = false;
|
||||
while (curr != nullptr) {
|
||||
SASSERT(prev->trans_reaches(n));
|
||||
enode * new_curr = curr->m_trans.m_target;
|
||||
eq_justification new_js = curr->m_trans.m_justification;
|
||||
curr->m_trans.m_target = prev;
|
||||
curr->m_trans.m_justification = js;
|
||||
curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
curr->m_proof_is_logged = false;
|
||||
prev = curr;
|
||||
js = new_js;
|
||||
curr = new_curr;
|
||||
|
@ -1044,7 +1044,7 @@ namespace smt {
|
|||
SASSERT(r1->trans_reaches(n1));
|
||||
n1->m_trans.m_target = nullptr;
|
||||
n1->m_trans.m_justification = null_eq_justification;
|
||||
n1->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
n1->m_proof_is_logged = false;
|
||||
invert_trans(r1);
|
||||
// ---------------
|
||||
// n1 -> ... -> r1
|
||||
|
|
|
@ -47,7 +47,7 @@ namespace smt {
|
|||
n->m_cgc_enabled = cgc_enabled;
|
||||
n->m_iscope_lvl = iscope_lvl;
|
||||
n->m_lbl_hash = -1;
|
||||
n->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
|
||||
n->m_proof_is_logged = false;
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
enode * arg = app2enode[owner->get_arg(i)->get_id()];
|
||||
|
|
|
@ -38,15 +38,6 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Indicates whether the proof for membership in an equivalence class is already logged.
|
||||
*/
|
||||
enum logged_status {
|
||||
NOT_LOGGED, //!< Proof is not logged or logged information is not up-to-date.
|
||||
BEING_LOGGED, //!< We are currently in the process of logging all relevant information. This is used to prevent looping when logging congruence steps.
|
||||
LOGGED //!< Proof is logged and logged information is still up-to-date.
|
||||
};
|
||||
|
||||
/** \ brief Use sparse maps in SMT solver.
|
||||
|
||||
Define this to use hash maps rather than vectors over ast
|
||||
|
@ -114,7 +105,7 @@ namespace smt {
|
|||
enode_vector m_parents; //!< Parent enodes of the equivalence class.
|
||||
theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode.
|
||||
trans_justification m_trans; //!< A justification for the enode being equal to its root.
|
||||
logged_status m_proof_logged_status; //!< Indicates that the proof for the enode being equal to its root is in the log.
|
||||
bool m_proof_is_logged; //!< Indicates that the proof for the enode being equal to its root is in the log.
|
||||
signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern
|
||||
approx_set m_lbls;
|
||||
approx_set m_plbls;
|
||||
|
|
|
@ -1018,8 +1018,17 @@ namespace smt {
|
|||
void context::apply_sort_cnstr(app * term, enode * e) {
|
||||
sort * s = term->get_decl()->get_range();
|
||||
theory * th = m_theories.get_plugin(s->get_family_id());
|
||||
if (th)
|
||||
if (th) {
|
||||
if (m_manager.has_trace_stream()) {
|
||||
m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n";
|
||||
}
|
||||
|
||||
th->apply_sort_cnstr(e, s);
|
||||
|
||||
if (m_manager.has_trace_stream()) {
|
||||
m_manager.trace_stream() << "[end-theory-constraints]\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
@ -26,6 +26,7 @@ Revision History:
|
|||
#include "smt/smt_quick_checker.h"
|
||||
#include "smt/mam.h"
|
||||
#include "smt/qi_queue.h"
|
||||
#include "util/obj_hashtable.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
@ -108,30 +109,31 @@ namespace smt {
|
|||
\brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
|
||||
equivalence class are in the log and up-to-date.
|
||||
*/
|
||||
void log_justification_to_root(std::ostream & log, enode *en) {
|
||||
void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited) {
|
||||
enode *root = en->get_root();
|
||||
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
|
||||
if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
|
||||
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
|
||||
log_single_justification(log, it);
|
||||
it->m_proof_logged_status = smt::logged_status::LOGGED;
|
||||
} else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
|
||||
if (already_visited.find(it) == already_visited.end()) already_visited.insert(it);
|
||||
else break;
|
||||
|
||||
// When the justification of an argument changes m_proof_logged_status is not reset => We need to check if the proofs of all arguments are logged.
|
||||
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
|
||||
if (!it->m_proof_is_logged) {
|
||||
log_single_justification(log, it, already_visited);
|
||||
it->m_proof_is_logged = true;
|
||||
} else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
|
||||
|
||||
// When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are logged.
|
||||
const unsigned num_args = it->get_num_args();
|
||||
enode *target = it->get_trans_justification().m_target;
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(log, it->get_arg(i));
|
||||
log_justification_to_root(log, target->get_arg(i));
|
||||
log_justification_to_root(log, it->get_arg(i), already_visited);
|
||||
log_justification_to_root(log, target->get_arg(i), already_visited);
|
||||
}
|
||||
it->m_proof_logged_status = smt::logged_status::LOGGED;
|
||||
it->m_proof_is_logged = true;
|
||||
}
|
||||
}
|
||||
if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
|
||||
if (!root->m_proof_is_logged) {
|
||||
log << "[eq-expl] #" << root->get_owner_id() << " root\n";
|
||||
root->m_proof_logged_status = smt::logged_status::LOGGED;
|
||||
root->m_proof_is_logged = true;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -139,7 +141,7 @@ namespace smt {
|
|||
\brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
|
||||
equalities needed by the step (e.g. argument equalities for congruence steps).
|
||||
*/
|
||||
void log_single_justification(std::ostream & out, enode *en) {
|
||||
void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited) {
|
||||
smt::literal lit;
|
||||
unsigned num_args;
|
||||
enode *target = en->get_trans_justification().m_target;
|
||||
|
@ -158,8 +160,8 @@ namespace smt {
|
|||
num_args = en->get_num_args();
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(out, en->get_arg(i));
|
||||
log_justification_to_root(out, target->get_arg(i));
|
||||
log_justification_to_root(out, en->get_arg(i), already_visited);
|
||||
log_justification_to_root(out, target->get_arg(i), already_visited);
|
||||
}
|
||||
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " cg";
|
||||
|
@ -206,18 +208,20 @@ namespace smt {
|
|||
if (has_trace_stream()) {
|
||||
std::ostream & out = trace_stream();
|
||||
|
||||
obj_hashtable<enode> already_visited;
|
||||
|
||||
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
|
||||
// is used. We need to make sure that all of these equalities appear in the log.
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
log_justification_to_root(out, bindings[i]);
|
||||
log_justification_to_root(out, bindings[i], already_visited);
|
||||
}
|
||||
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
log_justification_to_root(out, orig);
|
||||
log_justification_to_root(out, substituted);
|
||||
log_justification_to_root(out, orig, already_visited);
|
||||
log_justification_to_root(out, substituted, already_visited);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue