mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

sketch possible AC functionality

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-15 13:49:13 -07:00
parent f932d480a0
commit 20ddfc7795
1 changed files with 98 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

111
src/ast/euf/euf_mam.cpp
View file

@ -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,14 +632,14 @@ 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<typename OP>
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;
#ifdef _PROFILE_MAM
@ -642,8 +648,18 @@ namespace euf {
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<initn>(INITAC, sizeof(initn));
r->m_num_args = n;
return r;
}
opcode op = n <= 6 ? static_cast<opcode>(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;
}
@ -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<enode_vector> m_pool;
ptr_buffer<enode> 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<const initn*>(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<initn const*>(m_pc)))
goto backtrack;
m_pc = m_pc->m_next;
goto main_loop;
}
case COMPARE:
m_n1 = m_registers[static_cast<const compare *>(m_pc)->m_reg1];
m_n2 = m_registers[static_cast<const compare *>(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) {