mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

fixing repair

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-27 10:39:15 -07:00
parent 6b0a10637c
commit 7699ce56db
3 changed files with 17 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/sls/sls_bv_plugin.cpp
View file

@ -39,13 +39,19 @@ namespace sls {
return expr_ref(bv.mk_numeral(val.get_value(), e->get_sort()), m);
}
bool bv_plugin::is_bv_predicate(expr* e) {
return e && is_app(e) && to_app(e)->get_family_id() == bv.get_family_id();
}
void bv_plugin::propagate_literal(sat::literal lit) {
SASSERT(ctx.is_true(lit));
auto a = ctx.atom(lit.var());
if (!a || !is_app(a))
auto e = ctx.atom(lit.var());
if (!is_bv_predicate(e))
return;
if (!m_eval.eval_is_correct(to_app(a)))
ctx.new_value_eh(a);
auto a = to_app(e);
if (!m_eval.eval_is_correct(a))
ctx.new_value_eh(e);
}
bool bv_plugin::propagate() {
@ -145,10 +151,11 @@ namespace sls {
void bv_plugin::repair_literal(sat::literal lit) {
SASSERT(ctx.is_true(lit));
auto a = ctx.atom(lit.var());
if (!a || !is_app(a))
auto e = ctx.atom(lit.var());
if (!is_bv_predicate(e))
return;
if (!m_eval.eval_is_correct(to_app(a)))
auto a = to_app(e);
if (!m_eval.eval_is_correct(a))
ctx.flip(lit.var());
}

1
src/ast/sls/sls_bv_plugin.h
View file

@ -34,6 +34,7 @@ namespace sls {
std::ostream& trace_repair(bool down, expr* e);
void trace();
bool can_propagate();
bool is_bv_predicate(expr* e);
public:
bv_plugin(context& ctx);

2
src/ast/sls/sls_context.cpp
View file

@ -401,6 +401,7 @@ namespace sls {
auto is_visited = [&](expr* e) {
return nullptr != m_allterms.get(e->get_id(), nullptr);
};
auto visit = [&](expr* e) {
m_allterms.setx(e->get_id(), e);
};
@ -451,6 +452,7 @@ namespace sls {
m_repair_down.reserve(e->get_id() + 1);
m_repair_up.reserve(e->get_id() + 1);
SASSERT(e == term(e->get_id()));
if (!m_repair_down.contains(e->get_id()))
m_repair_down.insert(e->get_id());
for (auto p : parents(e)) {