From 20ddfc7795d2bc995311d6cf94897b78a1f09cab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Jun 2025 13:49:13 -0700 Subject: [PATCH] sketch possible AC functionality --- src/ast/euf/euf_mam.cpp | 117 +++++++++++++++++++++++++++++++++------- 1 file changed, 98 insertions(+), 19 deletions(-) diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index d9e9a8378..c87cd4197 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -134,7 +134,7 @@ namespace euf { // // ------------------------------------ typedef enum { - INIT1=0, INIT2, INIT3, INIT4, INIT5, INIT6, INITN, + INIT1=0, INIT2, INIT3, INIT4, INIT5, INIT6, INITN, INITAC, BIND1, BIND2, BIND3, BIND4, BIND5, BIND6, BINDN, YIELD1, YIELD2, YIELD3, YIELD4, YIELD5, YIELD6, YIELDN, COMPARE, CHECK, FILTER, CFILTER, PFILTER, CHOOSE, NOOP, CONTINUE, @@ -150,7 +150,7 @@ namespace euf { unsigned m_counter; // how often it was executed #endif bool is_init() const { - return m_opcode >= INIT1 && m_opcode <= INITN; + return m_opcode >= INIT1 && m_opcode <= INITAC; } }; @@ -332,12 +332,14 @@ namespace euf { std::ostream & operator<<(std::ostream & out, const instruction & instr) { switch (instr.m_opcode) { - case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: + case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: case INITAC: out << "(INIT"; if (instr.m_opcode <= INIT6) out << (instr.m_opcode - INIT1 + 1); - else + else if (instr.m_opcode == INITN) out << "N"; + else + out << "AC"; out << ")"; break; case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: @@ -519,6 +521,10 @@ namespace euf { } #endif + bool arg_compatible(app* f) const { + return expected_num_args() == f->get_num_args(); + } + unsigned expected_num_args() const { return m_num_args; } @@ -626,24 +632,34 @@ namespace euf { // ------------------------------------ class code_tree_manager { - euf::mam_solver & ctx; - label_hasher & m_lbl_hasher; - region & m_region; + euf::mam_solver& ctx; + label_hasher& m_lbl_hasher; + region& m_region; template - OP * mk_instr(opcode op, unsigned size) { - void * mem = m_region.allocate(size); - OP * r = new (mem) OP; + OP* mk_instr(opcode op, unsigned size) { + void* mem = m_region.allocate(size); + OP* r = new (mem) OP; r->m_opcode = op; - r->m_next = nullptr; + r->m_next = nullptr; #ifdef _PROFILE_MAM r->m_counter = 0; #endif return r; } - - instruction * mk_init(unsigned n) { + + bool is_ac(func_decl* f) const { + return false && f->is_associative() && f->is_commutative(); + } + + instruction * mk_init(func_decl* f, unsigned n) { SASSERT(n >= 1); + if (is_ac(f)) { + auto* r = mk_instr(INITAC, sizeof(initn)); + r->m_num_args = n; + return r; + } + opcode op = n <= 6 ? static_cast(INIT1 + n - 1) : INITN; if (op == INITN) { // We store the actual number of arguments for INITN. @@ -668,7 +684,7 @@ namespace euf { code_tree * mk_code_tree(func_decl * lbl, unsigned short num_args, bool filter_candidates) { code_tree * r = alloc(code_tree,m_lbl_hasher, lbl, num_args, filter_candidates); - r->m_root = mk_init(num_args); + r->m_root = mk_init(lbl, num_args); return r; } @@ -1238,7 +1254,7 @@ namespace euf { m_matched_exprs.reset(); while (!m_todo.empty()) linearise_core(); - + if (m_mp->get_num_args() > 1) { m_mp_already_processed.reset(); m_mp_already_processed.resize(m_mp->get_num_args()); @@ -1786,7 +1802,7 @@ namespace euf { - is_tmp_tree: trail for update operations is created if is_tmp_tree = false. */ void insert(code_tree * tree, quantifier * qa, app * mp, unsigned first_idx, bool is_tmp_tree) { - if (tree->expected_num_args() != to_app(mp->get_arg(first_idx))->get_num_args()) { + if (!tree->arg_compatible(to_app(mp->get_arg(first_idx)))) { // We have to check the number of arguments because of nary + and * operators. // The E-matching engine that was built when all + and * applications were binary. // We ignore the pattern if it does not have the expected number of arguments. @@ -1845,6 +1861,9 @@ namespace euf { unsigned m_old_max_generation; union { enode * m_curr; + struct { + unsigned m_next_pattern; + }; struct { enode_vector * m_to_recycle; enode * const * m_it; @@ -1883,6 +1902,9 @@ namespace euf { unsigned_vector m_min_top_generation, m_max_top_generation; pool m_pool; + ptr_buffer m_acargs; + bool_vector m_acbitset; + unsigned_vector m_acpatarg; enode_vector * mk_enode_vector() { enode_vector * r = m_pool.mk(); @@ -1987,6 +2009,8 @@ namespace euf { void display_pc_info(std::ostream & out); + bool match_ac(initn const* pc); + #define INIT_ARGS_SIZE 16 public: @@ -2219,7 +2243,7 @@ namespace euf { void interpreter::display_instr_input_reg(std::ostream & out, const instruction * instr) { switch (instr->m_opcode) { - case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: + case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: case INITAC: display_reg(out, 0); break; case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN: @@ -2254,6 +2278,25 @@ namespace euf { display_instr_input_reg(out, m_pc); } + // + // plan: + // - bit-set of matched elements in m_acargs (m_acbitset) + // - for each pattern index an index into m_acargs that it matches (m_acpatarg) + // when backtracking, take previous pattern index and clear bit-set at position + // of pattern_index: try binding the next available position not in the bit-index + // + // If pattern argument is a variable it can bind to multiple m_acargs + // Initially: simply punt. Dont consider these as matches + // Naive: iterate over all subsets not in current bitset and use a sequence binding. + // Established: use Diophantine equations to capture matchability. + // + + bool interpreter::match_ac(initn const* pc) { + unsigned f_args = pc->m_num_args; + SASSERT(f_args <= m_acargs.size()); + return false; + } + 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_expr(), m) << "\n";); unsigned since_last_check = 0; @@ -2364,6 +2407,37 @@ namespace euf { m_pc = m_pc->m_next; goto main_loop; + case INITAC: { + m_app = m_registers[0]; + m_acargs.reset(); + m_acargs.push_back(m_app); + auto* f = m_app->get_decl(); + for (unsigned i = 0; i < m_acargs.size(); ++i) { + auto* arg = m_acargs[i]; + if (is_app(arg->get_expr()) && f == arg->get_decl()) { + m_acargs.append(arg->num_args(), arg->args()); + m_acargs[i] = m_acargs.back(); + m_acargs.pop_back(); + --i; + } + } + if (static_cast(m_pc)->m_num_args > m_acargs.size()) + goto backtrack; + m_acbitset.reset(); + m_acbitset.reserve(m_acargs.size(), false); + m_acpatarg.reset(); + m_acpatarg.reserve(m_acargs.size(), 0); + 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_next_pattern = 0; + ++m_top; + // perform the match relative index + if (!match_ac(static_cast(m_pc))) + goto backtrack; + m_pc = m_pc->m_next; + goto main_loop; + } + case COMPARE: m_n1 = m_registers[static_cast(m_pc)->m_reg1]; m_n2 = m_registers[static_cast(m_pc)->m_reg2]; @@ -2756,6 +2830,11 @@ namespace euf { m_pc = m_b->m_next; goto main_loop; + case INITAC: + // this is a backtracking point. + NOT_IMPLEMENTED_YET(); + goto main_loop; + case CONTINUE: ++bp.m_it; for (; bp.m_it != bp.m_end; ++bp.m_it) { @@ -2867,7 +2946,7 @@ namespace euf { m_trees.reserve(lbl_id+1, nullptr); if (m_trees[lbl_id] == nullptr) { m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); - SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args()); + SASSERT(m_trees[lbl_id]->arg_compatible(p)); DEBUG_CODE(m_trees[lbl_id]->set_egraph(m_egraph);); ctx.get_trail().push(mk_tree_trail(m_trees, lbl_id)); } @@ -2877,7 +2956,7 @@ namespace euf { // The E-matching engine that was built when all + and * applications were binary. // We ignore the pattern if it does not have the expected number of arguments. // This is not the ideal solution, but it avoids possible crashes. - if (tree->expected_num_args() == p->get_num_args()) + if (tree->arg_compatible(p)) m_compiler.insert(tree, qa, mp, first_idx, false); } DEBUG_CODE(if (first_idx == 0) {