mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
parent
5c67c9d907
commit
8da1b024b7
|
@ -1875,7 +1875,6 @@ void ast_manager::delete_node(ast * n) {
|
|||
|
||||
while ((n = m_ast_table.pop_erase())) {
|
||||
|
||||
TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";);
|
||||
CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
|
||||
TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";);
|
||||
TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
|
||||
|
|
|
@ -454,23 +454,24 @@ namespace datatype {
|
|||
}
|
||||
|
||||
void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) {
|
||||
std::ostream& out = m_manager->trace_stream();
|
||||
symbol const& family_name = m_manager->get_family_name(get_family_id());
|
||||
for (constructor const* c : *m_defs[s]) {
|
||||
func_decl_ref f = c->instantiate(new_sort);
|
||||
const unsigned num_args = f->get_arity();
|
||||
if (num_args == 0) continue;
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
|
||||
out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
|
||||
++m_id_counter;
|
||||
}
|
||||
const unsigned constructor_id = m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name();
|
||||
out << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i;
|
||||
out << " " << family_name << "#" << constructor_id - num_args + i;
|
||||
}
|
||||
m_manager->trace_stream() << "\n";
|
||||
out << "\n";
|
||||
++m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
|
||||
out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
|
||||
++m_id_counter;
|
||||
m_axiom_bases.insert(f->get_name(), constructor_id + 4);
|
||||
std::ostringstream var_sorts;
|
||||
|
@ -481,14 +482,14 @@ namespace datatype {
|
|||
unsigned i = 0;
|
||||
for (accessor const* a : *c) {
|
||||
func_decl_ref acc = a->instantiate(new_sort);
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n";
|
||||
out << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n";
|
||||
++m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i
|
||||
out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i
|
||||
<< " " << family_name << "#" << m_id_counter - 1 << "\n";
|
||||
++m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
|
||||
out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
|
||||
<< " " << family_name << "#" << m_id_counter - 1 << "\n";
|
||||
m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
|
||||
out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
|
||||
++m_id_counter;
|
||||
++i;
|
||||
}
|
||||
|
|
|
@ -583,6 +583,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
|
||||
m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
|
||||
m().trace_stream() << "[end-of-instance]\n";
|
||||
m().trace_stream().flush();
|
||||
}
|
||||
|
||||
if (st != BR_DONE && st != BR_FAILED) {
|
||||
|
|
|
@ -137,5 +137,56 @@ namespace smt {
|
|||
theory::~theory() {
|
||||
}
|
||||
|
||||
|
||||
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
|
||||
ast_manager & m = get_manager();
|
||||
std::ostream& out = m.trace_stream();
|
||||
symbol const & family_name = m.get_family_name(get_family_id());
|
||||
if (pattern_id == UINT_MAX) {
|
||||
out << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << family_name << "#";
|
||||
if (axiom_id != UINT_MAX)
|
||||
out << axiom_id;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
out << " #" << bindings[i]->get_id();
|
||||
}
|
||||
if (used_enodes.size() > 0) {
|
||||
out << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *substituted = std::get<1>(n);
|
||||
SASSERT(std::get<0>(n) == nullptr);
|
||||
out << " #" << substituted->get_owner_id();
|
||||
}
|
||||
}
|
||||
} else {
|
||||
SASSERT(axiom_id != UINT_MAX);
|
||||
obj_hashtable<enode> already_visited;
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
quantifier_manager::log_justification_to_root(out, orig, already_visited, get_context(), get_manager());
|
||||
quantifier_manager::log_justification_to_root(out, substituted, already_visited, get_context(), get_manager());
|
||||
}
|
||||
}
|
||||
out << "[new-match] " << static_cast<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
out << " #" << bindings[i]->get_id();
|
||||
}
|
||||
out << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig == nullptr) {
|
||||
out << " #" << substituted->get_owner_id();
|
||||
} else {
|
||||
out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
out << "\n";
|
||||
out << "[instance] " << static_cast<void *>(nullptr) << " #" << r->get_id() << "\n";
|
||||
out.flush();
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -360,55 +360,15 @@ namespace smt {
|
|||
std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_owner()); }
|
||||
|
||||
protected:
|
||||
void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
|
||||
ast_manager & m = get_manager();
|
||||
symbol const & family_name = m.get_family_name(get_family_id());
|
||||
if (pattern_id == UINT_MAX) {
|
||||
m.trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << family_name << "#";
|
||||
if (axiom_id != UINT_MAX)
|
||||
m.trace_stream() << axiom_id;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
m.trace_stream() << " #" << bindings[i]->get_id();
|
||||
}
|
||||
if (used_enodes.size() > 0) {
|
||||
m.trace_stream() << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *substituted = std::get<1>(n);
|
||||
SASSERT(std::get<0>(n) == nullptr);
|
||||
m.trace_stream() << " #" << substituted->get_owner_id();
|
||||
}
|
||||
}
|
||||
} else {
|
||||
SASSERT(axiom_id != UINT_MAX);
|
||||
obj_hashtable<enode> already_visited;
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
quantifier_manager::log_justification_to_root(m.trace_stream(), orig, already_visited, get_context(), get_manager());
|
||||
quantifier_manager::log_justification_to_root(m.trace_stream(), substituted, already_visited, get_context(), get_manager());
|
||||
}
|
||||
}
|
||||
m.trace_stream() << "[new-match] " << static_cast<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
m.trace_stream() << " #" << bindings[i]->get_id();
|
||||
}
|
||||
m.trace_stream() << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig == nullptr) {
|
||||
m.trace_stream() << " #" << substituted->get_owner_id();
|
||||
} else {
|
||||
m.trace_stream() << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
m.trace_stream() << "\n";
|
||||
m.trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << r->get_id() << "\n";
|
||||
}
|
||||
void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
|
||||
app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
|
||||
const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>());
|
||||
|
||||
void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); }
|
||||
void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
|
||||
app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX,
|
||||
const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
|
||||
log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes);
|
||||
}
|
||||
|
||||
void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) {
|
||||
vector<std::tuple<enode *, enode *>> used_enodes;
|
||||
|
|
|
@ -139,7 +139,7 @@ namespace smt {
|
|||
expr * acc = m.mk_app(d, n->get_owner());
|
||||
args.push_back(acc);
|
||||
}
|
||||
expr * mk = m.mk_app(c, args.size(), args.c_ptr());
|
||||
expr_ref mk(m.mk_app(c, args.size(), args.c_ptr()), m);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(n->get_owner(), mk);
|
||||
|
|
Loading…
Reference in a new issue