mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fixing incremental

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-11 16:50:31 -07:00
parent 46252b669c
commit 2af713e4db
2 changed files with 21 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/sls/sls_euf_plugin.cpp
View file

@ -86,6 +86,7 @@ namespace sls {
if (!g.inconsistent())
return;
++m_stats.m_num_conflicts;
unsigned n = 1;
sat::literal_vector lits;
sat::literal flit = sat::null_literal, slit;
@ -111,7 +112,7 @@ namespace sls {
}
while (slit != flit);
// flip the last literal on the replay stack
IF_VERBOSE(2, verbose_stream() << "sls.euf - flip " << flit << "\n");
IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
ctx.flip(flit.var());
m_replay_stack.back().neg();
}
@ -142,6 +143,7 @@ namespace sls {
auto a = g.find(x);
auto b = g.find(y);
g.merge(a, b, to_ptr(lit));
g.merge(g.find(e), g.find(m.mk_true()), to_ptr(lit));
}
else if (!lit.sign() && m.is_distinct(e)) {
auto n = to_app(e)->get_num_args();
@ -206,6 +208,7 @@ namespace sls {
flit = l;
}
ctx.add_clause(lits);
++m_stats.m_num_conflicts;
if (flit != sat::null_literal)
ctx.flip(flit.var());
};
@ -406,4 +409,12 @@ namespace sls {
}
}
}
void euf_plugin::collect_statistics(statistics& st) const {
st.update("sls.euf-conflict", m_stats.m_num_conflicts);
}
void euf_plugin::reset_statistics() {
m_stats.reset();
}
}

11
src/ast/sls/sls_euf_plugin.h
View file

@ -23,6 +23,10 @@ Author:
namespace sls {
class euf_plugin : public plugin {
struct stats {
unsigned m_num_conflicts = 0;
void reset() { memset(this, 0, sizeof(*this)); }
};
obj_map<func_decl, ptr_vector<app>> m_app;
struct value_hash {
euf_plugin& cc;
@ -36,7 +40,10 @@ namespace sls {
};
hashtable<app*, value_hash, value_eq> m_values;
bool m_incremental = false;
stats m_stats;
scoped_ptr<euf::egraph> m_g;
scoped_ptr<obj_map<sort, unsigned>> m_num_elems;
@ -75,8 +82,8 @@ namespace sls {
bool repair_down(app* e) override { return false; }
void repair_literal(sat::literal lit) override {}
void collect_statistics(statistics& st) const override {}
void reset_statistics() override {}
void collect_statistics(statistics& st) const override;
void reset_statistics() override;
};
}