mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Adding comments

Browse source
This commit is contained in:
nilsbecker 2018-07-06 12:43:46 +02:00
parent 4f64f069ab
commit a405742037
4 changed files with 14 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/mam.cpp
View file

@ -1847,6 +1847,9 @@ namespace smt {
enode * m_n2;
enode * m_app;
const bind * m_b;
// equalities used for pattern match. The first element of the tuple gives the argument (or null) of some term that was matched against some higher level
// structure of the trigger, the second element gives the term that argument is replaced with in order to match the trigger. Used for logging purposes only.
vector<std::tuple<enode *, enode *>> m_used_enodes;
unsigned m_curr_used_enodes_size;
ptr_vector<enode> m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
@ -2275,7 +2278,7 @@ namespace smt {
if (m_ast_manager.has_trace_stream()) {
m_used_enodes.reset();
m_used_enodes.push_back(std::make_tuple(nullptr, n));
m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
}
m_pc = t->get_root();
@ -2381,6 +2384,7 @@ namespace smt {
if (m_n1->get_root() != m_n2->get_root())
goto backtrack;
// we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
m_pc = m_pc->m_next;
@ -2777,7 +2781,7 @@ namespace smt {
m_pattern_instances.pop_back();
m_pattern_instances.push_back(m_app);
// continue succeeded
update_max_generation(m_app, nullptr);
update_max_generation(m_app, nullptr); // null indicates a top-level match
TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
m_num_args = c->m_num_args;
m_oreg = c->m_oreg;

2
src/smt/smt_context.h
View file

@ -959,7 +959,7 @@ namespace smt {
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes);
unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
void set_global_generation(unsigned generation) { m_generation = generation; }

6
src/smt/smt_quantifier.cpp
View file

@ -204,9 +204,13 @@ namespace smt {
if (f) {
if (has_trace_stream()) {
std::ostream & out = trace_stream();
// 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]);
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
@ -215,6 +219,8 @@ namespace smt {
log_justification_to_root(out, substituted);
}
}
// At this point all relevant equalities for the match are logged.
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing.

2
src/smt/smt_quantifier.h
View file

@ -58,7 +58,7 @@ namespace smt {
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
vector<std::tuple<enode *, enode *>> & used_enodes);
vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
void init_search_eh();