mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

make rule processing fully incremental

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-06 20:45:10 +02:00
parent 590b79dc54
commit 1cd162203d
2 changed files with 19 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/ast/simplifiers/euf_completion.cpp
View file

@ -51,10 +51,6 @@ Delayed solver invocation
Mam optimization?
match(p, t, S) = suppose all variables in p are bound in S, check equality using canonization of p[S], otherwise prune instances from S.
--*/
#include "ast/ast_pp.h"
@ -94,13 +90,6 @@ namespace euf {
}
completion::~completion() {
reset_rules();
}
void completion::reset_rules() {
for (auto r : m_rules)
dealloc(r);
m_rules.reset();
}
void completion::reduce() {
@ -113,7 +102,6 @@ namespace euf {
read_egraph();
IF_VERBOSE(11, verbose_stream() << "(euf.completion :rounds " << rounds << ")\n");
}
reset_rules();
}
void completion::add_egraph() {
@ -229,33 +217,34 @@ namespace euf {
}
}
body.shrink(j);
if (body.empty()) {
add_constraint(head, d);
return;
if (body.empty())
add_constraint(head, d);
else {
m_rules.push_back(alloc(ground_rule, body, head, d));
get_trail().push(push_back_vector(m_rules));
}
m_rules.push_back(alloc(ground_rule, body, head, d));
}
void completion::check_rules() {
unsigned j = 0;
for (auto& r : m_rules) {
if (!r->m_active)
continue;
switch (check_rule(*r)) {
case l_true:
dealloc(r);
get_trail().push(value_trail(r->m_active));
r->m_active = false;
break; // remove rule, it is activated
case l_false:
dealloc(r);
get_trail().push(value_trail(r->m_active));
r->m_active = false;
break; // remove rule, premise is false
case l_undef:
m_rules[j++] = r;
break;
}
}
m_rules.shrink(j);
}
lbool completion::check_rule(ground_rule& r) {
unsigned j = 0;
for (auto* f : r.m_body) {
switch (eval_cond(f, r.m_dep)) {
case l_true:
@ -263,11 +252,9 @@ namespace euf {
case l_false:
return l_false;
default:
r.m_body[j++] = f;
break;
}
}
r.m_body.shrink(j);
if (r.m_body.empty()) {
add_constraint(r.m_head, r.m_dep);
return l_true;
@ -650,6 +637,4 @@ namespace euf {
}
}
}
}

11
src/ast/simplifiers/euf_completion.h
View file

@ -30,6 +30,8 @@ namespace euf {
virtual ~side_condition_solver() = default;
virtual void add_constraint(expr* f, expr_dependency* d) = 0;
virtual bool is_true(expr* f, expr_dependency*& d) = 0;
virtual void push() = 0;
virtual void pop(unsigned n) = 0;
};
class completion : public dependent_expr_simplifier, public on_binding_callback, public mam_solver {
@ -44,6 +46,7 @@ namespace euf {
expr_ref_vector m_body;
expr_ref m_head;
expr_dependency* m_dep;
bool m_active = true;
ground_rule(expr_ref_vector& b, expr_ref& h, expr_dependency* d) :
m_body(b), m_head(h), m_dep(d) {}
};
@ -87,15 +90,15 @@ namespace euf {
lbool check_rule(ground_rule& rule);
void check_rules();
void add_rule(expr* f, expr_dependency* d);
void reset_rules();
bool is_gt(expr* a, expr* b) const;
public:
completion(ast_manager& m, dependent_expr_state& fmls);
~completion() override;
char const* name() const override { return "euf-reduce"; }
void push() override { m_egraph.push(); dependent_expr_simplifier::push(); }
void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); }
char const* name() const override { return "euf-completion"; }
void push() override { if (m_side_condition_solver) m_side_condition_solver->push(); m_egraph.push(); dependent_expr_simplifier::push(); }
void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); if (m_side_condition_solver) m_side_condition_solver->pop(1);
}
void reduce() override;
void collect_statistics(statistics& st) const override;
void reset_statistics() override { m_stats.reset(); }