Skip to content

Commit 20ddfc7

Browse files
NikolajBjornerNikolajBjorner
committed
sketch possible AC functionality
1 parent f932d48 commit 20ddfc7

File tree

1 file changed

+98
-19
lines changed

1 file changed

+98
-19
lines changed

‎src/ast/euf/euf_mam.cpp

Lines changed: 98 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ namespace euf {
134134
//
135135
// ------------------------------------
136136
typedef enum {
137-
INIT1=0, INIT2, INIT3, INIT4, INIT5, INIT6, INITN,
137+
INIT1=0, INIT2, INIT3, INIT4, INIT5, INIT6, INITN, INITAC,
138138
BIND1, BIND2, BIND3, BIND4, BIND5, BIND6, BINDN,
139139
YIELD1, YIELD2, YIELD3, YIELD4, YIELD5, YIELD6, YIELDN,
140140
COMPARE, CHECK, FILTER, CFILTER, PFILTER, CHOOSE, NOOP, CONTINUE,
@@ -150,7 +150,7 @@ namespace euf {
150150
unsigned m_counter; // how often it was executed
151151
#endif
152152
bool is_init() const {
153-
return m_opcode >= INIT1 && m_opcode <= INITN;
153+
return m_opcode >= INIT1 && m_opcode <= INITAC;
154154
}
155155
};
156156

@@ -332,12 +332,14 @@ namespace euf {
332332

333333
std::ostream & operator<<(std::ostream & out, const instruction & instr) {
334334
switch (instr.m_opcode) {
335-
case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN:
335+
case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: case INITAC:
336336
out << "(INIT";
337337
if (instr.m_opcode <= INIT6)
338338
out << (instr.m_opcode - INIT1 + 1);
339-
else
339+
else if (instr.m_opcode == INITN)
340340
out << "N";
341+
else
342+
out << "AC";
341343
out << ")";
342344
break;
343345
case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN:
@@ -519,6 +521,10 @@ namespace euf {
519521
}
520522
#endif
521523

524+
bool arg_compatible(app* f) const {
525+
return expected_num_args() == f->get_num_args();
526+
}
527+
522528
unsigned expected_num_args() const {
523529
return m_num_args;
524530
}
@@ -626,24 +632,34 @@ namespace euf {
626632
// ------------------------------------
627633

628634
class code_tree_manager {
629-
euf::mam_solver & ctx;
630-
label_hasher & m_lbl_hasher;
631-
region & m_region;
635+
euf::mam_solver& ctx;
636+
label_hasher& m_lbl_hasher;
637+
region& m_region;
632638

633639
template<typename OP>
634-
OP * mk_instr(opcode op, unsigned size) {
635-
void * mem = m_region.allocate(size);
636-
OP * r = new (mem) OP;
640+
OP* mk_instr(opcode op, unsigned size) {
641+
void* mem = m_region.allocate(size);
642+
OP* r = new (mem) OP;
637643
r->m_opcode = op;
638-
r->m_next = nullptr;
644+
r->m_next = nullptr;
639645
#ifdef _PROFILE_MAM
640646
r->m_counter = 0;
641647
#endif
642648
return r;
643649
}
644-
645-
instruction * mk_init(unsigned n) {
650+
651+
bool is_ac(func_decl* f) const {
652+
return false && f->is_associative() && f->is_commutative();
653+
}
654+
655+
instruction * mk_init(func_decl* f, unsigned n) {
646656
SASSERT(n >= 1);
657+
if (is_ac(f)) {
658+
auto* r = mk_instr<initn>(INITAC, sizeof(initn));
659+
r->m_num_args = n;
660+
return r;
661+
}
662+
647663
opcode op = n <= 6 ? static_cast<opcode>(INIT1 + n - 1) : INITN;
648664
if (op == INITN) {
649665
// We store the actual number of arguments for INITN.
@@ -668,7 +684,7 @@ namespace euf {
668684

669685
code_tree * mk_code_tree(func_decl * lbl, unsigned short num_args, bool filter_candidates) {
670686
code_tree * r = alloc(code_tree,m_lbl_hasher, lbl, num_args, filter_candidates);
671-
r->m_root = mk_init(num_args);
687+
r->m_root = mk_init(lbl, num_args);
672688
return r;
673689
}
674690

@@ -1238,7 +1254,7 @@ namespace euf {
12381254
m_matched_exprs.reset();
12391255
while (!m_todo.empty())
12401256
linearise_core();
1241-
1257+
12421258
if (m_mp->get_num_args() > 1) {
12431259
m_mp_already_processed.reset();
12441260
m_mp_already_processed.resize(m_mp->get_num_args());
@@ -1786,7 +1802,7 @@ namespace euf {
17861802
- is_tmp_tree: trail for update operations is created if is_tmp_tree = false.
17871803
*/
17881804
void insert(code_tree * tree, quantifier * qa, app * mp, unsigned first_idx, bool is_tmp_tree) {
1789-
if (tree->expected_num_args() != to_app(mp->get_arg(first_idx))->get_num_args()) {
1805+
if (!tree->arg_compatible(to_app(mp->get_arg(first_idx)))) {
17901806
// We have to check the number of arguments because of nary + and * operators.
17911807
// The E-matching engine that was built when all + and * applications were binary.
17921808
// We ignore the pattern if it does not have the expected number of arguments.
@@ -1845,6 +1861,9 @@ namespace euf {
18451861
unsigned m_old_max_generation;
18461862
union {
18471863
enode * m_curr;
1864+
struct {
1865+
unsigned m_next_pattern;
1866+
};
18481867
struct {
18491868
enode_vector * m_to_recycle;
18501869
enode * const * m_it;
@@ -1883,6 +1902,9 @@ namespace euf {
18831902
unsigned_vector m_min_top_generation, m_max_top_generation;
18841903

18851904
pool<enode_vector> m_pool;
1905+
ptr_buffer<enode> m_acargs;
1906+
bool_vector m_acbitset;
1907+
unsigned_vector m_acpatarg;
18861908

18871909
enode_vector * mk_enode_vector() {
18881910
enode_vector * r = m_pool.mk();
@@ -1987,6 +2009,8 @@ namespace euf {
19872009

19882010
void display_pc_info(std::ostream & out);
19892011

2012+
bool match_ac(initn const* pc);
2013+
19902014
#define INIT_ARGS_SIZE 16
19912015

19922016
public:
@@ -2219,7 +2243,7 @@ namespace euf {
22192243

22202244
void interpreter::display_instr_input_reg(std::ostream & out, const instruction * instr) {
22212245
switch (instr->m_opcode) {
2222-
case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN:
2246+
case INIT1: case INIT2: case INIT3: case INIT4: case INIT5: case INIT6: case INITN: case INITAC:
22232247
display_reg(out, 0);
22242248
break;
22252249
case BIND1: case BIND2: case BIND3: case BIND4: case BIND5: case BIND6: case BINDN:
@@ -2254,6 +2278,25 @@ namespace euf {
22542278
display_instr_input_reg(out, m_pc);
22552279
}
22562280

2281+
//
2282+
// plan:
2283+
// - bit-set of matched elements in m_acargs (m_acbitset)
2284+
// - for each pattern index an index into m_acargs that it matches (m_acpatarg)
2285+
// when backtracking, take previous pattern index and clear bit-set at position
2286+
// of pattern_index: try binding the next available position not in the bit-index
2287+
//
2288+
// If pattern argument is a variable it can bind to multiple m_acargs
2289+
// Initially: simply punt. Dont consider these as matches
2290+
// Naive: iterate over all subsets not in current bitset and use a sequence binding.
2291+
// Established: use Diophantine equations to capture matchability.
2292+
//
2293+
2294+
bool interpreter::match_ac(initn const* pc) {
2295+
unsigned f_args = pc->m_num_args;
2296+
SASSERT(f_args <= m_acargs.size());
2297+
return false;
2298+
}
2299+
22572300
bool interpreter::execute_core(code_tree * t, enode * n) {
22582301
TRACE(trigger_bug, tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_expr(), m) << "\n";);
22592302
unsigned since_last_check = 0;
@@ -2364,6 +2407,37 @@ namespace euf {
23642407
m_pc = m_pc->m_next;
23652408
goto main_loop;
23662409

2410+
case INITAC: {
2411+
m_app = m_registers[0];
2412+
m_acargs.reset();
2413+
m_acargs.push_back(m_app);
2414+
auto* f = m_app->get_decl();
2415+
for (unsigned i = 0; i < m_acargs.size(); ++i) {
2416+
auto* arg = m_acargs[i];
2417+
if (is_app(arg->get_expr()) && f == arg->get_decl()) {
2418+
m_acargs.append(arg->num_args(), arg->args());
2419+
m_acargs[i] = m_acargs.back();
2420+
m_acargs.pop_back();
2421+
--i;
2422+
}
2423+
}
2424+
if (static_cast<const initn*>(m_pc)->m_num_args > m_acargs.size())
2425+
goto backtrack;
2426+
m_acbitset.reset();
2427+
m_acbitset.reserve(m_acargs.size(), false);
2428+
m_acpatarg.reset();
2429+
m_acpatarg.reserve(m_acargs.size(), 0);
2430+
m_backtrack_stack[m_top].m_instr = m_pc;
2431+
m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation;
2432+
m_backtrack_stack[m_top].m_next_pattern = 0;
2433+
++m_top;
2434+
// perform the match relative index
2435+
if (!match_ac(static_cast<initn const*>(m_pc)))
2436+
goto backtrack;
2437+
m_pc = m_pc->m_next;
2438+
goto main_loop;
2439+
}
2440+
23672441
case COMPARE:
23682442
m_n1 = m_registers[static_cast<const compare *>(m_pc)->m_reg1];
23692443
m_n2 = m_registers[static_cast<const compare *>(m_pc)->m_reg2];
@@ -2756,6 +2830,11 @@ namespace euf {
27562830
m_pc = m_b->m_next;
27572831
goto main_loop;
27582832

2833+
case INITAC:
2834+
// this is a backtracking point.
2835+
NOT_IMPLEMENTED_YET();
2836+
goto main_loop;
2837+
27592838
case CONTINUE:
27602839
++bp.m_it;
27612840
for (; bp.m_it != bp.m_end; ++bp.m_it) {
@@ -2867,7 +2946,7 @@ namespace euf {
28672946
m_trees.reserve(lbl_id+1, nullptr);
28682947
if (m_trees[lbl_id] == nullptr) {
28692948
m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false);
2870-
SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args());
2949+
SASSERT(m_trees[lbl_id]->arg_compatible(p));
28712950
DEBUG_CODE(m_trees[lbl_id]->set_egraph(m_egraph););
28722951
ctx.get_trail().push(mk_tree_trail(m_trees, lbl_id));
28732952
}
@@ -2877,7 +2956,7 @@ namespace euf {
28772956
// The E-matching engine that was built when all + and * applications were binary.
28782957
// We ignore the pattern if it does not have the expected number of arguments.
28792958
// This is not the ideal solution, but it avoids possible crashes.
2880-
if (tree->expected_num_args() == p->get_num_args())
2959+
if (tree->arg_compatible(p))
28812960
m_compiler.insert(tree, qa, mp, first_idx, false);
28822961
}
28832962
DEBUG_CODE(if (first_idx == 0) {

0 commit comments

Comments
 (0)