mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Nikolaj Bjorner
parent
a90529e3dc
commit
a1b690032a
1 changed files with 111 additions and 94 deletions
205
src/smt/mam.cpp
205
src/smt/mam.cpp
|
|
@ -782,7 +782,7 @@ namespace smt {
|
|||
|
||||
class compiler {
|
||||
context & m_context;
|
||||
ast_manager & m_ast_manager;
|
||||
ast_manager & m;
|
||||
code_tree_manager & m_ct_manager;
|
||||
label_hasher & m_lbl_hasher;
|
||||
bool m_use_filters;
|
||||
|
|
@ -812,23 +812,22 @@ namespace smt {
|
|||
unsigned_vector m_to_reset;
|
||||
ptr_vector<instruction> m_compatible;
|
||||
ptr_vector<instruction> m_incompatible;
|
||||
|
||||
ptr_vector<instruction> m_seq;
|
||||
|
||||
void set_register(unsigned reg, expr * p) {
|
||||
m_registers.setx(reg, p, 0);
|
||||
m_registers.setx(reg, p, nullptr);
|
||||
}
|
||||
|
||||
check_mark get_check_mark(unsigned reg) const {
|
||||
return m_mark.get(reg, NOT_CHECKED);
|
||||
}
|
||||
|
||||
void set_check_mark(unsigned reg, check_mark m) {
|
||||
m_mark.setx(reg, m, NOT_CHECKED);
|
||||
void set_check_mark(unsigned reg, check_mark cm) {
|
||||
m_mark.setx(reg, cm, NOT_CHECKED);
|
||||
}
|
||||
|
||||
void init(code_tree * t, quantifier * qa, app * mp, unsigned first_idx) {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
#ifdef Z3DEBUG
|
||||
for (auto cm : m_mark) {
|
||||
SASSERT(cm == NOT_CHECKED);
|
||||
|
|
@ -924,6 +923,7 @@ namespace smt {
|
|||
for (unsigned reg : m_todo) {
|
||||
expr * p = m_registers[reg];
|
||||
SASSERT(!is_quantifier(p));
|
||||
TRACE("mam", tout << "lin: " << reg << " " << get_check_mark(reg) << " " << is_var(p) << "\n";);
|
||||
if (is_var(p)) {
|
||||
unsigned var_id = to_var(p)->get_idx();
|
||||
if (m_vars[var_id] != -1)
|
||||
|
|
@ -933,6 +933,7 @@ namespace smt {
|
|||
continue;
|
||||
}
|
||||
|
||||
|
||||
SASSERT(is_app(p));
|
||||
|
||||
if (to_app(p)->is_ground()) {
|
||||
|
|
@ -1229,8 +1230,8 @@ namespace smt {
|
|||
|
||||
#ifdef Z3DEBUG
|
||||
for (unsigned i = 0; i < m_qa->get_num_decls(); i++) {
|
||||
CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m_ast_manager) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n";
|
||||
tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m_ast_manager) << "\n";
|
||||
CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n";
|
||||
tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n";
|
||||
tout << "tree:\n" << *m_tree << "\n";
|
||||
);
|
||||
SASSERT(m_vars[i] >= 0);
|
||||
|
|
@ -1285,6 +1286,7 @@ namespace smt {
|
|||
return nullptr; // it is unlikely we will find a compatible node
|
||||
}
|
||||
if (curr_compatibility > max_compatibility) {
|
||||
TRACE("mam", tout << "better child " << best_child << " -> " << curr_child << "\n";);
|
||||
best_child = curr_child;
|
||||
max_compatibility = curr_compatibility;
|
||||
}
|
||||
|
|
@ -1406,7 +1408,7 @@ namespace smt {
|
|||
bool is_semi_compatible(filter * instr) const {
|
||||
unsigned reg = instr->m_reg;
|
||||
return
|
||||
m_registers[reg] != 0 &&
|
||||
m_registers[reg] != nullptr &&
|
||||
get_check_mark(reg) == NOT_CHECKED &&
|
||||
is_app(m_registers[reg]) &&
|
||||
!is_ground(m_registers[reg]);
|
||||
|
|
@ -1497,17 +1499,18 @@ namespace smt {
|
|||
while (curr != nullptr && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) {
|
||||
TRACE("mam_compiler_detail", tout << "processing instr: " << *curr << "\n";);
|
||||
switch (curr->m_opcode) {
|
||||
case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN:
|
||||
if (is_compatible(static_cast<bind*>(curr))) {
|
||||
case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: {
|
||||
bind* bnd = static_cast<bind*>(curr);
|
||||
if (is_compatible(bnd)) {
|
||||
TRACE("mam_compiler_detail", tout << "compatible\n";);
|
||||
unsigned ireg = static_cast<bind*>(curr)->m_ireg;
|
||||
unsigned ireg = bnd->m_ireg;
|
||||
SASSERT(m_todo.contains(ireg));
|
||||
m_todo.erase(ireg);
|
||||
set_check_mark(ireg, NOT_CHECKED);
|
||||
m_compatible.push_back(curr);
|
||||
app * app = to_app(m_registers[ireg]);
|
||||
unsigned oreg = static_cast<bind*>(curr)->m_oreg;
|
||||
unsigned num_args = static_cast<bind*>(curr)->m_num_args;
|
||||
unsigned oreg = bnd->m_oreg;
|
||||
unsigned num_args = bnd->m_num_args;
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
set_register(oreg + i, app->get_arg(i));
|
||||
m_todo.push_back(oreg + i);
|
||||
|
|
@ -1518,19 +1521,21 @@ namespace smt {
|
|||
m_incompatible.push_back(curr);
|
||||
}
|
||||
break;
|
||||
case CHECK:
|
||||
if (is_compatible(static_cast<check*>(curr))) {
|
||||
}
|
||||
case CHECK: {
|
||||
check* chk = static_cast<check*>(curr);
|
||||
if (is_compatible(chk)) {
|
||||
TRACE("mam_compiler_detail", tout << "compatible\n";);
|
||||
unsigned reg = static_cast<check*>(curr)->m_reg;
|
||||
unsigned reg = chk->m_reg;
|
||||
SASSERT(m_todo.contains(reg));
|
||||
m_todo.erase(reg);
|
||||
set_check_mark(reg, NOT_CHECKED);
|
||||
m_compatible.push_back(curr);
|
||||
}
|
||||
else if (m_use_filters && is_semi_compatible(static_cast<check*>(curr))) {
|
||||
else if (m_use_filters && is_semi_compatible(chk)) {
|
||||
TRACE("mam_compiler_detail", tout << "semi compatible\n";);
|
||||
unsigned reg = static_cast<check*>(curr)->m_reg;
|
||||
enode * n1 = static_cast<check*>(curr)->m_enode;
|
||||
unsigned reg = chk->m_reg;
|
||||
enode * n1 = chk->m_enode;
|
||||
// n1->has_lbl_hash may be false, even
|
||||
// when update_filters is invoked before
|
||||
// executing this method.
|
||||
|
|
@ -1556,10 +1561,11 @@ namespace smt {
|
|||
m_incompatible.push_back(curr);
|
||||
}
|
||||
else {
|
||||
TRACE("mam_compiler_detail", tout << "incompatible\n";);
|
||||
TRACE("mam_compiler_detail", tout << "incompatible " << chk->m_reg << "\n";);
|
||||
m_incompatible.push_back(curr);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case COMPARE:
|
||||
if (is_compatible(static_cast<compare*>(curr))) {
|
||||
TRACE("mam_compiler_detail", tout << "compatible\n";);
|
||||
|
|
@ -1567,8 +1573,10 @@ namespace smt {
|
|||
unsigned reg2 = static_cast<compare*>(curr)->m_reg2;
|
||||
SASSERT(m_todo.contains(reg2));
|
||||
m_todo.erase(reg2);
|
||||
set_check_mark(reg2, NOT_CHECKED);
|
||||
if (is_var(m_registers[reg1])) {
|
||||
m_todo.erase(reg1);
|
||||
set_check_mark(reg1, NOT_CHECKED);
|
||||
unsigned var_id = to_var(m_registers[reg1])->get_idx();
|
||||
if (m_vars[var_id] == -1)
|
||||
m_vars[var_id] = reg1;
|
||||
|
|
@ -1592,44 +1600,47 @@ namespace smt {
|
|||
m_incompatible.push_back(curr);
|
||||
}
|
||||
break;
|
||||
case FILTER:
|
||||
case FILTER: {
|
||||
filter *flt = static_cast<filter*>(curr);
|
||||
SASSERT(m_use_filters);
|
||||
if (is_compatible(static_cast<filter*>(curr))) {
|
||||
TRACE("mam_compiler_detail", tout << "compatible\n";);
|
||||
unsigned reg = static_cast<filter*>(curr)->m_reg;
|
||||
if (is_compatible(flt)) {
|
||||
unsigned reg = flt->m_reg;
|
||||
TRACE("mam_compiler_detail", tout << "compatible " << reg << "\n";);
|
||||
CTRACE("mam_compiler_bug", !m_todo.contains(reg), {
|
||||
for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; }
|
||||
tout << "\nregisters:\n";
|
||||
for (unsigned i = 0; i < m_registers.size(); i++) { if (m_registers[i]) { tout << i << ":\n" << mk_pp(m_registers[i], m_ast_manager) << "\n"; } }
|
||||
tout << "quantifier:\n" << mk_pp(m_qa, m_ast_manager) << "\n";
|
||||
tout << "pattern:\n" << mk_pp(m_mp, m_ast_manager) << "\n";
|
||||
});
|
||||
for (unsigned t : m_todo) { tout << t << " "; }
|
||||
tout << "\nregisters:\n";
|
||||
unsigned i = 0;
|
||||
for (expr* r : m_registers) { if (r) { tout << i++ << ":\n" << mk_pp(r, m) << "\n"; } }
|
||||
tout << "quantifier:\n" << mk_pp(m_qa, m) << "\n";
|
||||
tout << "pattern:\n" << mk_pp(m_mp, m) << "\n";
|
||||
});
|
||||
SASSERT(m_todo.contains(reg));
|
||||
if (static_cast<filter*>(curr)->m_lbl_set.size() == 1)
|
||||
if (flt->m_lbl_set.size() == 1)
|
||||
set_check_mark(reg, CHECK_SINGLETON);
|
||||
else
|
||||
set_check_mark(reg, CHECK_SET);
|
||||
m_compatible.push_back(curr);
|
||||
}
|
||||
else if (is_semi_compatible(static_cast<filter*>(curr))) {
|
||||
TRACE("mam_compiler_detail", tout << "semi compatible\n";);
|
||||
unsigned reg = static_cast<filter*>(curr)->m_reg;
|
||||
else if (is_semi_compatible(flt)) {
|
||||
unsigned reg = flt->m_reg;
|
||||
TRACE("mam_compiler_detail", tout << "semi compatible " << reg << "\n";);
|
||||
CTRACE("mam_compiler_bug", !m_todo.contains(reg), {
|
||||
for (unsigned i = 0; i < m_todo.size(); i++) { tout << m_todo[i] << " "; }
|
||||
tout << "\nregisters:\n";
|
||||
for (unsigned i = 0; i < m_registers.size(); i++) { if (m_registers[i]) { tout << i << ":\n" << mk_pp(m_registers[i], m_ast_manager) << "\n"; } }
|
||||
tout << "quantifier:\n" << mk_pp(m_qa, m_ast_manager) << "\n";
|
||||
tout << "pattern:\n" << mk_pp(m_mp, m_ast_manager) << "\n";
|
||||
});
|
||||
for (unsigned t : m_todo) { tout << t << " "; }
|
||||
tout << "\nregisters:\n";
|
||||
unsigned i = 0;
|
||||
for (expr* r : m_registers) { if (r) { tout << i++ << ":\n" << mk_pp(r, m) << "\n"; } }
|
||||
tout << "quantifier:\n" << mk_pp(m_qa, m) << "\n";
|
||||
tout << "pattern:\n" << mk_pp(m_mp, m) << "\n";
|
||||
});
|
||||
SASSERT(m_todo.contains(reg));
|
||||
unsigned h = get_pat_lbl_hash(reg);
|
||||
TRACE("mam_lbl_bug",
|
||||
tout << "curr_set: " << static_cast<filter*>(curr)->m_lbl_set << "\n";
|
||||
tout << "curr_set: " << flt->m_lbl_set << "\n";
|
||||
tout << "new hash: " << h << "\n";);
|
||||
set_check_mark(reg, CHECK_SET);
|
||||
approx_set const & s = static_cast<filter*>(curr)->m_lbl_set;
|
||||
approx_set const & s = flt->m_lbl_set;
|
||||
if (s.size() > 1) {
|
||||
m_ct_manager.insert_new_lbl_hash(static_cast<filter*>(curr), h);
|
||||
m_ct_manager.insert_new_lbl_hash(flt, h);
|
||||
m_compatible.push_back(curr);
|
||||
}
|
||||
else {
|
||||
|
|
@ -1646,6 +1657,7 @@ namespace smt {
|
|||
m_incompatible.push_back(curr);
|
||||
}
|
||||
break;
|
||||
}
|
||||
default:
|
||||
TRACE("mam_compiler_detail", tout << "incompatible\n";);
|
||||
m_incompatible.push_back(curr);
|
||||
|
|
@ -1665,6 +1677,7 @@ namespace smt {
|
|||
SASSERT(curr->m_opcode == CHOOSE);
|
||||
choose * first_child = static_cast<choose *>(curr);
|
||||
choose * best_child = find_best_child(first_child);
|
||||
TRACE("mam", tout << "best child " << best_child << "\n";);
|
||||
if (best_child == nullptr) {
|
||||
// There is no compatible child
|
||||
// Suppose the sequence is:
|
||||
|
|
@ -1728,7 +1741,7 @@ namespace smt {
|
|||
public:
|
||||
compiler(context & ctx, code_tree_manager & ct_mg, label_hasher & h, bool use_filters = true):
|
||||
m_context(ctx),
|
||||
m_ast_manager(ctx.get_manager()),
|
||||
m(ctx.get_manager()),
|
||||
m_ct_manager(ct_mg),
|
||||
m_lbl_hasher(h),
|
||||
m_use_filters(use_filters) {
|
||||
|
|
@ -1742,14 +1755,14 @@ namespace smt {
|
|||
- first_idx: index of mp that will be the "head" (first to be processed) of the multi-pattern.
|
||||
*/
|
||||
code_tree * mk_tree(quantifier * qa, app * mp, unsigned first_idx, bool filter_candidates) {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
app * p = to_app(mp->get_arg(first_idx));
|
||||
unsigned num_args = p->get_num_args();
|
||||
code_tree * r = m_ct_manager.mk_code_tree(p->get_decl(), num_args, filter_candidates);
|
||||
init(r, qa, mp, first_idx);
|
||||
linearise(r->m_root, first_idx);
|
||||
r->m_num_choices = m_num_choices;
|
||||
TRACE("mam_compiler", tout << "new tree for:\n" << mk_pp(mp, m_ast_manager) << "\n" << *r;);
|
||||
TRACE("mam_compiler", tout << "new tree for:\n" << mk_pp(mp, m) << "\n" << *r;);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
@ -1767,7 +1780,7 @@ namespace smt {
|
|||
return;
|
||||
}
|
||||
m_is_tmp_tree = is_tmp_tree;
|
||||
TRACE("mam_compiler", tout << "updating tree with:\n" << mk_pp(mp, m_ast_manager) << "\n";);
|
||||
TRACE("mam_compiler", tout << "updating tree with:\n" << mk_pp(mp, m) << "\n";);
|
||||
TRACE("mam_bug", tout << "before insertion\n" << *tree << "\n";);
|
||||
if (!is_tmp_tree)
|
||||
m_ct_manager.save_num_regs(tree);
|
||||
|
|
@ -1783,7 +1796,10 @@ namespace smt {
|
|||
}
|
||||
TRACE("mam_bug",
|
||||
tout << "m_num_choices: " << m_num_choices << "\n";
|
||||
tout << "new tree:\n" << *tree;);
|
||||
tout << "new tree:\n" << *tree;
|
||||
tout << "todo ";
|
||||
for (auto t : m_todo) tout << t << " ";
|
||||
tout << "\n";);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -1828,7 +1844,7 @@ namespace smt {
|
|||
|
||||
class interpreter {
|
||||
context & m_context;
|
||||
ast_manager & m_ast_manager;
|
||||
ast_manager & m;
|
||||
mam & m_mam;
|
||||
bool m_use_filters;
|
||||
enode_vector m_registers;
|
||||
|
|
@ -1870,7 +1886,7 @@ namespace smt {
|
|||
void update_max_generation(enode * n, enode * prev) {
|
||||
m_max_generation = std::max(m_max_generation, n->get_generation());
|
||||
|
||||
if (m_ast_manager.has_trace_stream())
|
||||
if (m.has_trace_stream())
|
||||
m_used_enodes.push_back(std::make_tuple(prev, n));
|
||||
}
|
||||
|
||||
|
|
@ -1980,7 +1996,7 @@ namespace smt {
|
|||
public:
|
||||
interpreter(context & ctx, mam & ma, bool use_filters):
|
||||
m_context(ctx),
|
||||
m_ast_manager(ctx.get_manager()),
|
||||
m(ctx.get_manager()),
|
||||
m_mam(ma),
|
||||
m_use_filters(use_filters) {
|
||||
m_args.resize(INIT_ARGS_SIZE);
|
||||
|
|
@ -1991,8 +2007,8 @@ namespace smt {
|
|||
|
||||
void init(code_tree * t) {
|
||||
TRACE("mam_bug", tout << "preparing to match tree:\n" << *t << "\n";);
|
||||
m_registers.reserve(t->get_num_regs(), 0);
|
||||
m_bindings.reserve(t->get_num_regs(), 0);
|
||||
m_registers.reserve(t->get_num_regs(), nullptr);
|
||||
m_bindings.reserve(t->get_num_regs(), nullptr);
|
||||
if (m_backtrack_stack.size() < t->get_num_choices())
|
||||
m_backtrack_stack.resize(t->get_num_choices());
|
||||
}
|
||||
|
|
@ -2002,7 +2018,7 @@ namespace smt {
|
|||
init(t);
|
||||
if (t->filter_candidates()) {
|
||||
for (enode* app : t->get_candidates()) {
|
||||
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
|
||||
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m) << "\n";);
|
||||
if (!app->is_marked() && app->is_cgr()) {
|
||||
if (m_context.resource_limits_exceeded() || !execute_core(t, app))
|
||||
return;
|
||||
|
|
@ -2016,7 +2032,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
for (enode* app : t->get_candidates()) {
|
||||
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
|
||||
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m) << "\n";);
|
||||
if (app->is_cgr()) {
|
||||
TRACE("trigger_bug", tout << "is_cgr\n";);
|
||||
if (m_context.resource_limits_exceeded() || !execute_core(t, app))
|
||||
|
|
@ -2215,7 +2231,7 @@ namespace smt {
|
|||
if (m_use_filters)
|
||||
out << ", lbls: " << n->get_root()->get_lbls() << " ";
|
||||
out << "\n";
|
||||
out << mk_pp(n->get_owner(), m_ast_manager) << "\n";
|
||||
out << mk_pp(n->get_owner(), m) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -2257,7 +2273,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool interpreter::execute_core(code_tree * t, enode * n) {
|
||||
TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";);
|
||||
TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m) << "\n";);
|
||||
unsigned since_last_check = 0;
|
||||
|
||||
#ifdef _PROFILE_MAM
|
||||
|
|
@ -2279,7 +2295,7 @@ namespace smt {
|
|||
m_pattern_instances.push_back(n);
|
||||
m_max_generation = n->get_generation();
|
||||
|
||||
if (m_ast_manager.has_trace_stream()) {
|
||||
if (m.has_trace_stream()) {
|
||||
m_used_enodes.reset();
|
||||
m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
|
||||
}
|
||||
|
|
@ -2378,7 +2394,7 @@ namespace smt {
|
|||
goto backtrack;
|
||||
|
||||
// We will use the common root when instantiating the quantifier => log the necessary equalities
|
||||
if (m_ast_manager.has_trace_stream()) {
|
||||
if (m.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()));
|
||||
}
|
||||
|
|
@ -2395,7 +2411,7 @@ namespace smt {
|
|||
goto backtrack;
|
||||
|
||||
// we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
|
||||
if (m_ast_manager.has_trace_stream()) {
|
||||
if (m.has_trace_stream()) {
|
||||
m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
|
||||
}
|
||||
|
||||
|
|
@ -2443,7 +2459,7 @@ namespace smt {
|
|||
m_app = get_first_f_app(static_cast<const bind *>(m_pc)->m_label, static_cast<const bind *>(m_pc)->m_num_args, m_n1); \
|
||||
if (!m_app) \
|
||||
goto backtrack; \
|
||||
TRACE("mam_int", tout << "bind candidate: " << mk_pp(m_app->get_owner(), m_ast_manager) << "\n";); \
|
||||
TRACE("mam_int", tout << "bind candidate: " << mk_pp(m_app->get_owner(), m) << "\n";); \
|
||||
m_backtrack_stack[m_top].m_instr = m_pc; \
|
||||
m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation; \
|
||||
m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size; \
|
||||
|
|
@ -2581,7 +2597,7 @@ 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()) { \
|
||||
if (m.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())); \
|
||||
} \
|
||||
|
|
@ -2593,7 +2609,7 @@ namespace smt {
|
|||
#define SET_VAR(IDX) \
|
||||
m_args[IDX] = m_registers[static_cast<const get_cgr *>(m_pc)->m_iregs[IDX]]; \
|
||||
if (m_use_filters && static_cast<const get_cgr *>(m_pc)->m_lbl_set.empty_intersection(m_args[IDX]->get_root()->get_plbls())) { \
|
||||
TRACE("trigger_bug", tout << "m_args[IDX]->get_root():\n" << mk_ismt2_pp(m_args[IDX]->get_root()->get_owner(), m_ast_manager) << "\n"; \
|
||||
TRACE("trigger_bug", tout << "m_args[IDX]->get_root():\n" << mk_ismt2_pp(m_args[IDX]->get_root()->get_owner(), m) << "\n"; \
|
||||
tout << "cgr set: "; static_cast<const get_cgr *>(m_pc)->m_lbl_set.display(tout); tout << "\n"; \
|
||||
tout << "node set: "; m_args[IDX]->get_root()->get_plbls().display(tout); tout << "\n";); \
|
||||
goto backtrack; \
|
||||
|
|
@ -2657,7 +2673,7 @@ namespace smt {
|
|||
if (m_app == nullptr)
|
||||
goto backtrack;
|
||||
m_pattern_instances.push_back(m_app);
|
||||
TRACE("mam_int", tout << "continue candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
|
||||
TRACE("mam_int", tout << "continue candidate:\n" << mk_ll_pp(m_app->get_owner(), m););
|
||||
for (unsigned i = 0; i < m_num_args; i++)
|
||||
m_registers[m_oreg+i] = m_app->get_arg(i);
|
||||
m_pc = m_pc->m_next;
|
||||
|
|
@ -2677,7 +2693,7 @@ namespace smt {
|
|||
backtrack_point & bp = m_backtrack_stack[m_top - 1];
|
||||
m_max_generation = bp.m_old_max_generation;
|
||||
|
||||
if (m_ast_manager.has_trace_stream())
|
||||
if (m.has_trace_stream())
|
||||
m_used_enodes.shrink(bp.m_old_used_enodes_size);
|
||||
|
||||
TRACE("mam_int", tout << "backtrack top: " << bp.m_instr << " " << *(bp.m_instr) << "\n";);
|
||||
|
|
@ -2720,7 +2736,7 @@ namespace smt {
|
|||
goto backtrack; \
|
||||
} \
|
||||
bp.m_curr = m_app; \
|
||||
TRACE("mam_int", tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager);); \
|
||||
TRACE("mam_int", tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_owner(), m);); \
|
||||
m_oreg = m_b->m_oreg
|
||||
|
||||
BBIND_COMMON();
|
||||
|
|
@ -2800,7 +2816,7 @@ namespace smt {
|
|||
m_pattern_instances.push_back(m_app);
|
||||
// continue succeeded
|
||||
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););
|
||||
TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m););
|
||||
m_num_args = c->m_num_args;
|
||||
m_oreg = c->m_oreg;
|
||||
for (unsigned i = 0; i < m_num_args; i++)
|
||||
|
|
@ -2838,7 +2854,7 @@ namespace smt {
|
|||
//
|
||||
// ------------------------------------
|
||||
class code_tree_map {
|
||||
ast_manager & m_ast_manager;
|
||||
ast_manager & m;
|
||||
compiler & m_compiler;
|
||||
ptr_vector<code_tree> m_trees; // mapping: func_label -> tree
|
||||
mam_trail_stack & m_trail_stack;
|
||||
|
|
@ -2859,7 +2875,7 @@ namespace smt {
|
|||
|
||||
public:
|
||||
code_tree_map(ast_manager & m, compiler & c, mam_trail_stack & s):
|
||||
m_ast_manager(m),
|
||||
m(m),
|
||||
m_compiler(c),
|
||||
m_trail_stack(s) {
|
||||
}
|
||||
|
|
@ -2880,8 +2896,8 @@ namespace smt {
|
|||
- first_idx: index to be used as head of the multi-pattern mp
|
||||
*/
|
||||
void add_pattern(quantifier * qa, app * mp, unsigned first_idx) {
|
||||
(void)m_ast_manager;
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
(void)m;
|
||||
SASSERT(m.is_pattern(mp));
|
||||
SASSERT(first_idx < mp->get_num_args());
|
||||
app * p = to_app(mp->get_arg(first_idx));
|
||||
func_decl * lbl = p->get_decl();
|
||||
|
|
@ -3062,7 +3078,7 @@ namespace smt {
|
|||
// ------------------------------------
|
||||
class mam_impl : public mam {
|
||||
protected:
|
||||
ast_manager & m_ast_manager;
|
||||
ast_manager & m;
|
||||
bool m_use_filters;
|
||||
mam_trail_stack m_trail_stack;
|
||||
label_hasher m_lbl_hasher;
|
||||
|
|
@ -3130,7 +3146,7 @@ namespace smt {
|
|||
|
||||
void add_candidate(code_tree * t, enode * app) {
|
||||
if (t != nullptr) {
|
||||
TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_owner(), m_ast_manager););
|
||||
TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_owner(), m););
|
||||
if (!t->has_candidates())
|
||||
m_to_match.push_back(t);
|
||||
t->add_candidate(app);
|
||||
|
|
@ -3188,7 +3204,7 @@ namespace smt {
|
|||
if (!r_plbls.may_contain(elem)) {
|
||||
m_trail_stack.push(mam_value_trail<approx_set>(r_plbls));
|
||||
r_plbls.insert(elem);
|
||||
TRACE("trigger_bug", tout << "updating plabels of:\n" << mk_ismt2_pp(c->get_root()->get_owner(), m_ast_manager) << "\n";
|
||||
TRACE("trigger_bug", tout << "updating plabels of:\n" << mk_ismt2_pp(c->get_root()->get_owner(), m) << "\n";
|
||||
tout << "new_elem: " << static_cast<unsigned>(elem) << "\n";
|
||||
tout << "plbls: " << c->get_root()->get_plbls() << "\n";);
|
||||
TRACE("mam_bug", tout << "updating plabels of: #" << c->get_root()->get_owner_id() << "\n";
|
||||
|
|
@ -3228,17 +3244,17 @@ namespace smt {
|
|||
}
|
||||
|
||||
code_tree * mk_code(quantifier * qa, app * mp, unsigned pat_idx) {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
return m_compiler.mk_tree(qa, mp, pat_idx, true);
|
||||
}
|
||||
|
||||
void insert_code(path_tree * t, quantifier * qa, app * mp, unsigned pat_idx) {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
m_compiler.insert(t->m_code, qa, mp, pat_idx, false);
|
||||
}
|
||||
|
||||
path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
SASSERT(p != nullptr);
|
||||
unsigned pat_idx = p->m_pattern_idx;
|
||||
path_tree * head = nullptr;
|
||||
|
|
@ -3259,7 +3275,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void insert(path_tree * t, path * p, quantifier * qa, app * mp) {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
path_tree * head = t;
|
||||
path_tree * prev_sibling = nullptr;
|
||||
bool found_label = false;
|
||||
|
|
@ -3442,7 +3458,7 @@ namespace smt {
|
|||
\brief Update inverted path index.
|
||||
*/
|
||||
void update_filters(quantifier * qa, app * mp) {
|
||||
TRACE("mam_bug", tout << "updating filters using:\n" << mk_pp(mp, m_ast_manager) << "\n";);
|
||||
TRACE("mam_bug", tout << "updating filters using:\n" << mk_pp(mp, m) << "\n";);
|
||||
unsigned num_vars = qa->get_num_decls();
|
||||
if (num_vars >= m_var_paths.size())
|
||||
m_var_paths.resize(num_vars+1);
|
||||
|
|
@ -3499,6 +3515,7 @@ namespace smt {
|
|||
#ifdef _PROFILE_PATH_TREE
|
||||
t->m_watch.start();
|
||||
#endif
|
||||
|
||||
m_todo.reset();
|
||||
enode_vector * to_unmark = mk_tmp_vector();
|
||||
enode_vector * to_unmark2 = mk_tmp_vector();
|
||||
|
|
@ -3576,7 +3593,7 @@ namespace smt {
|
|||
bool is_flat_assoc = lbl->is_flat_associative();
|
||||
enode * curr_parent_root = curr_parent->get_root();
|
||||
enode * curr_parent_cg = curr_parent->get_cg();
|
||||
TRACE("mam_path_tree", tout << "processing parent:\n" << mk_pp(curr_parent->get_owner(), m_ast_manager) << "\n";);
|
||||
TRACE("mam_path_tree", tout << "processing parent:\n" << mk_pp(curr_parent->get_owner(), m) << "\n";);
|
||||
TRACE("mam_path_tree", tout << "parent is marked: " << curr_parent->is_marked() << "\n";);
|
||||
if (filter.may_contain(m_lbl_hasher(lbl)) &&
|
||||
!curr_parent->is_marked() &&
|
||||
|
|
@ -3605,7 +3622,7 @@ namespace smt {
|
|||
is_eq(curr_tree->m_ground_arg, curr_parent->get_arg(curr_tree->m_ground_arg_idx))
|
||||
)) {
|
||||
if (curr_tree->m_code) {
|
||||
TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m_ast_manager) << "\n";);
|
||||
TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m) << "\n";);
|
||||
add_candidate(curr_tree->m_code, curr_parent);
|
||||
}
|
||||
if (curr_tree->m_first_child) {
|
||||
|
|
@ -3717,7 +3734,7 @@ namespace smt {
|
|||
}
|
||||
quantifier * qa = kv.first;
|
||||
app * mp = kv.second;
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(m.is_pattern(mp));
|
||||
app * p = to_app(mp->get_arg(0));
|
||||
func_decl * lbl = p->get_decl();
|
||||
if (m_context.get_num_enodes_of(lbl) > 0) {
|
||||
|
|
@ -3754,7 +3771,7 @@ namespace smt {
|
|||
unsigned num_patterns = mp->get_num_args();
|
||||
for (unsigned i = 0; i < num_patterns; i++) {
|
||||
app * pat = to_app(mp->get_arg(i));
|
||||
TRACE("mam_pat", tout << mk_ismt2_pp(qa, m_ast_manager) << "\npat:\n" << mk_ismt2_pp(pat, m_ast_manager) << "\n";);
|
||||
TRACE("mam_pat", tout << mk_ismt2_pp(qa, m) << "\npat:\n" << mk_ismt2_pp(pat, m) << "\n";);
|
||||
SASSERT(!pat->is_ground());
|
||||
todo.push_back(pat);
|
||||
}
|
||||
|
|
@ -3780,13 +3797,13 @@ namespace smt {
|
|||
public:
|
||||
mam_impl(context & ctx, bool use_filters):
|
||||
mam(ctx),
|
||||
m_ast_manager(ctx.get_manager()),
|
||||
m(ctx.get_manager()),
|
||||
m_use_filters(use_filters),
|
||||
m_trail_stack(*this),
|
||||
m_ct_manager(m_lbl_hasher, m_trail_stack),
|
||||
m_compiler(ctx, m_ct_manager, m_lbl_hasher, use_filters),
|
||||
m_interpreter(ctx, *this, use_filters),
|
||||
m_trees(m_ast_manager, m_compiler, m_trail_stack),
|
||||
m_trees(m, m_compiler, m_trail_stack),
|
||||
m_region(m_trail_stack.get_region()),
|
||||
m_r1(nullptr),
|
||||
m_r2(nullptr) {
|
||||
|
|
@ -3800,9 +3817,9 @@ namespace smt {
|
|||
}
|
||||
|
||||
void add_pattern(quantifier * qa, app * mp) override {
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m_ast_manager) << "\n" << mk_ismt2_pp(mp, m_ast_manager) << "\n";);
|
||||
TRACE("mam_bug", tout << "adding pattern\n" << mk_pp(qa, m_ast_manager) << "\n" << mk_pp(mp, m_ast_manager) << "\n";);
|
||||
SASSERT(m.is_pattern(mp));
|
||||
TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m) << "\n" << mk_ismt2_pp(mp, m) << "\n";);
|
||||
TRACE("mam_bug", tout << "adding pattern\n" << mk_pp(qa, m) << "\n" << mk_pp(mp, m) << "\n";);
|
||||
// Z3 checks if a pattern is ground or not before solving.
|
||||
// Ground patterns are discarded.
|
||||
// However, the simplifier may turn a non-ground pattern into a ground one.
|
||||
|
|
@ -3900,14 +3917,14 @@ namespace smt {
|
|||
#endif
|
||||
|
||||
void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) override {
|
||||
TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
|
||||
TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m) << "\n";);
|
||||
#ifdef Z3DEBUG
|
||||
if (m_check_missing_instances) {
|
||||
if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) {
|
||||
TRACE("missing_instance",
|
||||
tout << "qa:\n" << mk_ll_pp(qa, m_ast_manager) << "\npat:\n" << mk_ll_pp(pat, m_ast_manager);
|
||||
tout << "qa:\n" << mk_ll_pp(qa, m) << "\npat:\n" << mk_ll_pp(pat, m);
|
||||
for (unsigned i = 0; i < num_bindings; i++)
|
||||
tout << "#" << bindings[i]->get_owner_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m_ast_manager) << "\n";
|
||||
tout << "#" << bindings[i]->get_owner_id() << "\n" << mk_ll_pp(bindings[i]->get_owner(), m) << "\n";
|
||||
);
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
@ -3929,7 +3946,7 @@ namespace smt {
|
|||
// This method is invoked when n becomes relevant.
|
||||
// If lazy == true, then n is not added to the list of candidate enodes for matching. That is, the method just updates the lbls.
|
||||
void relevant_eh(enode * n, bool lazy) override {
|
||||
TRACE("trigger_bug", tout << "relevant_eh:\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";
|
||||
TRACE("trigger_bug", tout << "relevant_eh:\n" << mk_ismt2_pp(n->get_owner(), m) << "\n";
|
||||
tout << "mam: " << this << "\n";);
|
||||
TRACE("mam", tout << "relevant_eh: #" << n->get_owner_id() << "\n";);
|
||||
if (n->has_lbl_hash())
|
||||
|
|
@ -3945,7 +3962,7 @@ namespace smt {
|
|||
update_lbls(n, h);
|
||||
if (is_plbl(lbl))
|
||||
update_children_plbls(n, h);
|
||||
TRACE("mam_bug", tout << "adding relevant candidate:\n" << mk_ll_pp(n->get_owner(), m_ast_manager) << "\n";);
|
||||
TRACE("mam_bug", tout << "adding relevant candidate:\n" << mk_ll_pp(n->get_owner(), m) << "\n";);
|
||||
if (!lazy)
|
||||
add_candidate(n);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue