mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 21:31:22 +00:00
Code Activity

avoid rechecking whether equality explanations are already logged

Browse source
This commit is contained in:
nilsbecker 2018-10-09 16:42:10 +02:00
parent a0f6447a33
commit 547fbd4764
4 changed files with 29 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_context.cpp
View file

@ -562,7 +562,7 @@ namespace smt {
invert_trans(n1); invert_trans(n1);
n1->m_trans.m_target = n2; n1->m_trans.m_target = n2;
n1->m_trans.m_justification = js; 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)); SASSERT(r1->trans_reaches(n1));
// --------------- // ---------------
// r1 -> .. -> n1 -> n2 -> ... -> r2 // r1 -> .. -> n1 -> n2 -> ... -> r2
@ -742,14 +742,14 @@ namespace smt {
eq_justification js = n->m_trans.m_justification; eq_justification js = n->m_trans.m_justification;
prev->m_trans.m_target = nullptr; prev->m_trans.m_target = nullptr;
prev->m_trans.m_justification = null_eq_justification; 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) { while (curr != nullptr) {
SASSERT(prev->trans_reaches(n)); SASSERT(prev->trans_reaches(n));
enode * new_curr = curr->m_trans.m_target; enode * new_curr = curr->m_trans.m_target;
eq_justification new_js = curr->m_trans.m_justification; eq_justification new_js = curr->m_trans.m_justification;
curr->m_trans.m_target = prev; curr->m_trans.m_target = prev;
curr->m_trans.m_justification = js; curr->m_trans.m_justification = js;
curr->m_proof_logged_status = smt::logged_status::NOT_LOGGED; curr->m_proof_is_logged = false;
prev = curr; prev = curr;
js = new_js; js = new_js;
curr = new_curr; curr = new_curr;
@ -1043,7 +1043,7 @@ namespace smt {
SASSERT(r1->trans_reaches(n1)); SASSERT(r1->trans_reaches(n1));
n1->m_trans.m_target = nullptr; n1->m_trans.m_target = nullptr;
n1->m_trans.m_justification = null_eq_justification; 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); invert_trans(r1);
// --------------- // ---------------
// n1 -> ... -> r1 // n1 -> ... -> r1

2
src/smt/smt_enode.cpp
View file

@ -47,7 +47,7 @@ namespace smt {
n->m_cgc_enabled = cgc_enabled; n->m_cgc_enabled = cgc_enabled;
n->m_iscope_lvl = iscope_lvl; n->m_iscope_lvl = iscope_lvl;
n->m_lbl_hash = -1; 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(); unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
enode * arg = app2enode[owner->get_arg(i)->get_id()]; enode * arg = app2enode[owner->get_arg(i)->get_id()];

11
src/smt/smt_enode.h
View file

@ -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. /** \ brief Use sparse maps in SMT solver.
Define this to use hash maps rather than vectors over ast 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. 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. 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. 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 signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern
approx_set m_lbls; approx_set m_lbls;
approx_set m_plbls; approx_set m_plbls;

42
src/smt/smt_quantifier.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "smt/smt_quick_checker.h" #include "smt/smt_quick_checker.h"
#include "smt/mam.h" #include "smt/mam.h"
#include "smt/qi_queue.h" #include "smt/qi_queue.h"
#include <unordered_set>
namespace smt { 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 \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. 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, std::unordered_set<enode *> &already_visited) {
enode *root = en->get_root(); enode *root = en->get_root();
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) { if (already_visited.find(it) == already_visited.end()) already_visited.insert(it);
it->m_proof_logged_status = smt::logged_status::BEING_LOGGED; else break;
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) {
// 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. if (!it->m_proof_is_logged) {
it->m_proof_logged_status = smt::logged_status::BEING_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(); const unsigned num_args = it->get_num_args();
enode *target = it->get_trans_justification().m_target; enode *target = it->get_trans_justification().m_target;
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(log, it->get_arg(i)); log_justification_to_root(log, it->get_arg(i), already_visited);
log_justification_to_root(log, target->get_arg(i)); 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"; 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 \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). 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, std::unordered_set<enode *> &already_visited) {
smt::literal lit; smt::literal lit;
unsigned num_args; unsigned num_args;
enode *target = en->get_trans_justification().m_target; enode *target = en->get_trans_justification().m_target;
@ -158,8 +160,8 @@ namespace smt {
num_args = en->get_num_args(); num_args = en->get_num_args();
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
log_justification_to_root(out, en->get_arg(i)); log_justification_to_root(out, en->get_arg(i), already_visited);
log_justification_to_root(out, target->get_arg(i)); log_justification_to_root(out, target->get_arg(i), already_visited);
} }
out << "[eq-expl] #" << en->get_owner_id() << " cg"; out << "[eq-expl] #" << en->get_owner_id() << " cg";
@ -206,18 +208,20 @@ namespace smt {
if (has_trace_stream()) { if (has_trace_stream()) {
std::ostream & out = trace_stream(); std::ostream & out = trace_stream();
std::unordered_set<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 // 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. // is used. We need to make sure that all of these equalities appear in the log.
for (unsigned i = 0; i < num_bindings; ++i) { 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) { for (auto n : used_enodes) {
enode *orig = std::get<0>(n); enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n); enode *substituted = std::get<1>(n);
if (orig != nullptr) { if (orig != nullptr) {
log_justification_to_root(out, orig); log_justification_to_root(out, orig, already_visited);
log_justification_to_root(out, substituted); log_justification_to_root(out, substituted, already_visited);
} }
} }