Skip to content

Commit 423930d

Browse files
NikolajBjornerNikolajBjorner
committed
missing files
1 parent e166175 commit 423930d

File tree

2 files changed

+42
-29
lines changed

2 files changed

+42
-29
lines changed

‎src/ast/simplifiers/euf_completion.cpp‎

Lines changed: 31 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -186,7 +186,7 @@ namespace euf {
186186

187187
for (unsigned i = qhead(); i < sz; ++i) {
188188
auto [f, p, d] = m_fmls[i]();
189-
add_constraint(f, d);
189+
add_constraint(f, p, d);
190190
}
191191
m_should_propagate = true;
192192
while (m_should_propagate && !should_stop()) {
@@ -200,7 +200,7 @@ namespace euf {
200200
}
201201
}
202202

203-
void completion::add_constraint(expr* f, expr_dependency* d) {
203+
void completion::add_constraint(expr* f, proof* pr, expr_dependency* d) {
204204
if (m_egraph.inconsistent())
205205
return;
206206
auto add_children = [&](enode* n) {
@@ -234,21 +234,21 @@ namespace euf {
234234
mk_enode(g);
235235
m_mam->add_pattern(q, p);
236236
}
237-
if (!get_dependency(q)) {
238-
m_q2dep.insert(q, d);
239-
get_trail().push(insert_obj_map(m_q2dep, q));
240-
}
237+
auto pq = get_dependency(q);
238+
m_q2dep.insert(q, pq);
239+
get_trail().push(insert_obj_map(m_q2dep, q));
241240
}
242-
add_rule(f, d);
241+
add_rule(f, pr, d);
243242
}
244243
if (m_side_condition_solver)
245-
m_side_condition_solver->add_constraint(f, d);
244+
m_side_condition_solver->add_constraint(f, pr, d);
246245
}
247246

248-
lbool completion::eval_cond(expr* f, expr_dependency*& d) {
247+
lbool completion::eval_cond(expr* f, proof_ref& pr, expr_dependency*& d) {
249248
auto n = mk_enode(f);
250249
if (m.is_true(n->get_root()->get_expr())) {
251250
d = m.mk_join(d, explain_eq(n, n->get_root()));
251+
// TODO update pr
252252
return l_true;
253253
}
254254
if (m.is_false(n->get_root()->get_expr()))
@@ -259,34 +259,39 @@ namespace euf {
259259
n = mk_enode(g);
260260
if (m.is_false(n->get_root()->get_expr())) {
261261
d = m.mk_join(d, explain_eq(n, n->get_root()));
262+
// TODO update pr
262263
return l_true;
263264
}
264265
if (m.is_true(n->get_root()->get_expr()))
265266
return l_false;
266267
}
267268
if (m_side_condition_solver) {
268269
expr_dependency* sd = nullptr;
269-
if (m_side_condition_solver->is_true(f, sd)) {
270-
add_constraint(f, sd);
270+
if (m_side_condition_solver->is_true(f, pr, sd)) {
271+
add_constraint(f, pr, sd);
271272
d = m.mk_join(d, sd);
272273
return l_true;
273274
}
274275
}
275276
return l_undef;
276277
}
277278

278-
void completion::add_rule(expr* f, expr_dependency* d) {
279+
void completion::add_rule(expr* f, proof* pr, expr_dependency* d) {
279280
expr* x = nullptr, * y = nullptr;
280281
if (!m.is_implies(f, x, y))
281282
return;
282283
expr_ref_vector body(m);
284+
proof_ref pr_i(m), pr0(m);
285+
proof_ref_vector prs(m);
283286
expr_ref head(y, m);
284287
body.push_back(x);
285288
flatten_and(body);
286289
unsigned j = 0;
287290
for (auto f : body) {
288-
switch (eval_cond(f, d)) {
291+
switch (eval_cond(f, pr_i, d)) {
289292
case l_true:
293+
if (m.proofs_enabled())
294+
prs.push_back(pr_i);
290295
break;
291296
case l_false:
292297
return;
@@ -296,13 +301,16 @@ namespace euf {
296301
}
297302
}
298303
body.shrink(j);
304+
if (m.proofs_enabled()) {
305+
// TODO
306+
}
299307
if (body.empty())
300-
add_constraint(head, d);
308+
add_constraint(head, pr0, d);
301309
else {
302310
euf::enode_vector _body;
303311
for (auto* f : body)
304312
_body.push_back(m_egraph.find(f)->get_root());
305-
auto r = alloc(conditional_rule, _body, head, d);
313+
auto r = alloc(conditional_rule, _body, head, pr0, d);
306314
m_rules.push_back(r);
307315
get_trail().push(new_obj_trail(r));
308316
get_trail().push(push_back_vector(m_rules));
@@ -340,11 +348,13 @@ namespace euf {
340348
if (!r.m_active)
341349
return;
342350
for (unsigned i = r.m_watch_index; i < r.m_body.size(); ++i) {
343-
auto* f = r.m_body.get(i);
344-
switch (eval_cond(f->get_expr(), r.m_dep)) {
351+
auto* f = r.m_body.get(i);
352+
proof_ref pr(m);
353+
switch (eval_cond(f->get_expr(), pr, r.m_dep)) {
345354
case l_true:
346355
get_trail().push(value_trail(r.m_watch_index));
347356
++r.m_watch_index;
357+
// TODO accumulate proof in r?
348358
break;
349359
case l_false:
350360
get_trail().push(value_trail(r.m_active));
@@ -356,7 +366,7 @@ namespace euf {
356366
}
357367
}
358368
if (r.m_body.empty()) {
359-
add_constraint(r.m_head, r.m_dep);
369+
add_constraint(r.m_head, r.m_proof, r.m_dep);
360370
get_trail().push(value_trail(r.m_active));
361371
r.m_active = false;
362372
}
@@ -375,9 +385,10 @@ namespace euf {
375385
}
376386
expr_ref r = subst(q->get_expr(), _binding);
377387
IF_VERBOSE(12, verbose_stream() << "add " << r << "\n");
378-
388+
IF_VERBOSE(1, verbose_stream() << max_generation << "\n");
379389
scoped_generation sg(*this, max_generation + 1);
380-
add_constraint(r, get_dependency(q));
390+
auto [pr, d] = get_dependency(q);
391+
add_constraint(r, pr, d);
381392
propagate_rules();
382393
m_should_propagate = true;
383394
++m_stats.m_num_instances;

‎src/ast/simplifiers/euf_completion.h‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,8 @@ namespace euf {
3636
expr_ref guard;
3737
};
3838
virtual ~side_condition_solver() = default;
39-
virtual void add_constraint(expr* f, expr_dependency* d) = 0;
40-
virtual bool is_true(expr* f, expr_dependency*& d) = 0;
39+
virtual void add_constraint(expr* f, proof*, expr_dependency* d) = 0;
40+
virtual bool is_true(expr* f, proof_ref& pr, expr_dependency*& d) = 0;
4141
virtual void push() = 0;
4242
virtual void pop(unsigned n) = 0;
4343
virtual void solve_for(vector<solution>& sol) = 0;
@@ -54,12 +54,13 @@ namespace euf {
5454
struct conditional_rule {
5555
euf::enode_vector m_body;
5656
expr_ref m_head;
57+
proof_ref m_proof;
5758
expr_dependency* m_dep;
5859
unsigned m_watch_index = 0;
5960
bool m_active = true;
6061
bool m_in_queue = false;
61-
conditional_rule(euf::enode_vector& b, expr_ref& h, expr_dependency* d) :
62-
m_body(b), m_head(h), m_dep(d) {}
62+
conditional_rule(euf::enode_vector& b, expr_ref& h, proof* pr, expr_dependency* d) :
63+
m_body(b), m_head(h), m_proof(pr, h.get_manager()), m_dep(d) {}
6364
};
6465

6566
egraph m_egraph;
@@ -69,7 +70,7 @@ namespace euf {
6970
enode_vector m_args, m_reps, m_nodes_to_canonize;
7071
expr_ref_vector m_canonical, m_eargs;
7172
expr_dependency_ref_vector m_deps;
72-
obj_map<quantifier, expr_dependency*> m_q2dep;
73+
obj_map<quantifier, std::pair<proof*, expr_dependency*>> m_q2dep;
7374
unsigned m_epoch = 0;
7475
unsigned_vector m_epochs;
7576
th_rewriter m_rewriter;
@@ -94,17 +95,18 @@ namespace euf {
9495
expr* get_canonical(expr* f, expr_dependency_ref& d);
9596
expr* get_canonical(enode* n);
9697
void set_canonical(enode* n, expr* e);
97-
void add_constraint(expr*f, expr_dependency* d);
98+
void add_constraint(expr*f, proof* pr, expr_dependency* d);
9899
expr_dependency* explain_eq(enode* a, enode* b);
100+
void prove_eq(enode* a, enode* b, proof_ref& pr);
99101
expr_dependency* explain_conflict();
100-
expr_dependency* get_dependency(quantifier* q) { return m_q2dep.contains(q) ? m_q2dep[q] : nullptr; }
102+
std::pair<proof*, expr_dependency*> get_dependency(quantifier* q) { return m_q2dep.contains(q) ? m_q2dep[q] : std::pair(nullptr, nullptr); }
101103

102-
lbool eval_cond(expr* f, expr_dependency*& d);
104+
lbool eval_cond(expr* f, proof_ref& pr, expr_dependency*& d);
103105

104106

105107
bool should_stop();
106108

107-
void add_rule(expr* f, expr_dependency* d);
109+
void add_rule(expr* f, proof* pr, expr_dependency* d);
108110
void watch_rule(enode* root, enode* other);
109111
void insert_watch(enode* n, conditional_rule* r);
110112
void propagate_rule(conditional_rule& r);

0 commit comments

Comments
 (0)