mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

fixes to occurs check

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-18 10:41:27 -07:00
parent 5864fcba6b
commit aa2292d5c4
3 changed files with 25 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sat_ddfw.cpp
View file

@ -572,8 +572,8 @@ namespace sat {
transfer_weight(from_idx, to_idx, w); transfer_weight(from_idx, to_idx, w);
} }
//verbose_stream() << m_shifts << " " << m_flips << " " << shifted << "\n"; //verbose_stream() << m_shifts << " " << m_flips << " " << shifted << "\n";
if (!shifted) if (!shifted && m_restart_next > m_flips)
m_reinit_next = m_flips; m_restart_next = m_flips + (m_restart_next - m_flips) / 2;
// DEBUG_CODE(invariant();); // DEBUG_CODE(invariant(););
} }

34
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -96,10 +96,10 @@ namespace sls {
expr* t = nullptr, *z = nullptr; expr* t = nullptr, *z = nullptr;
for (auto s : ctx.subterms()) { for (auto s : ctx.subterms()) {
if (dt.is_accessor(s, t) && dt.is_recursive(t) && dt.is_recursive(s)) if (dt.is_accessor(s, t) && dt.is_recursive(t) && dt.is_recursive(s))
add_edge(s, t, sat::null_literal); add_edge(s, t, m.mk_app(dt.get_constructor_is(dt.get_accessor_constructor(to_app(s)->get_decl())), t));
if (dt.is_constructor(s) && dt.is_recursive(s)) { if (dt.is_constructor(s) && dt.is_recursive(s)) {
for (auto arg : *to_app(s)) for (auto arg : *to_app(s))
add_edge(arg, s, sat::null_literal); add_edge(arg, s, nullptr);
} }
} }
expr* x = nullptr, *y = nullptr; expr* x = nullptr, *y = nullptr;
@ -114,27 +114,27 @@ namespace sls {
sat::literal lp(v, false), ln(v, true); sat::literal lp(v, false), ln(v, true);
if (dt.is_accessor(x, z) && dt.is_recursive(z)) { if (dt.is_accessor(x, z) && dt.is_recursive(z)) {
if (ctx.is_unit(lp)) if (ctx.is_unit(lp))
add_edge(y, z, sat::null_literal); add_edge(y, z, nullptr);
else if (ctx.is_unit(ln)) else if (ctx.is_unit(ln))
; ;
else else
add_edge(y, z, lp); add_edge(y, z, e);
} }
if (dt.is_accessor(y, z) && dt.is_recursive(z)) { if (dt.is_accessor(y, z) && dt.is_recursive(z)) {
if (ctx.is_unit(lp)) if (ctx.is_unit(lp))
add_edge(x, z, sat::null_literal); add_edge(x, z, m.mk_app(dt.get_constructor_is(dt.get_accessor_constructor(to_app(y)->get_decl())), z));
else if (ctx.is_unit(ln)) else if (ctx.is_unit(ln))
; ;
else else
add_edge(x, z, lp); add_edge(x, z, e);
} }
} }
add_path_axioms(); add_path_axioms();
} }
void datatype_plugin::add_edge(expr* child, expr* parent, sat::literal lit) { void datatype_plugin::add_edge(expr* child, expr* parent, expr* cond) {
TRACE("dt", tout << mk_bounded_pp(child, m) << " <- " << mk_bounded_pp(parent, m) << " " << lit << "\n"); m_parents.insert_if_not_there(child, vector<parent_t>()).push_back({parent, expr_ref(cond, m)});
m_parents.insert_if_not_there(child, svector<parent_t>()).push_back({parent, lit}); TRACE("dt", tout << mk_bounded_pp(child, m) << " <- " << mk_bounded_pp(parent, m) << " " << mk_bounded_pp(cond, m) << "\n");
} }
void datatype_plugin::add_path_axioms() { void datatype_plugin::add_path_axioms() {
@ -148,21 +148,21 @@ namespace sls {
} }
} }
void datatype_plugin::add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, svector<parent_t> const& parents) { void datatype_plugin::add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, vector<parent_t> const& parents) {
for (auto const& [parent, lit] : parents) { for (auto const& [parent, cond] : parents) {
if (lit != sat::null_literal) if (cond)
lits.push_back(~lit); lits.push_back(~ctx.mk_literal(cond));
if (children.contains(parent)) { if (children.contains(parent)) {
// only assert loop clauses for proper loops // only assert loop clauses for proper loops
if (parent == children[0]) if (parent == children[0])
ctx.add_clause(lits); ctx.add_clause(lits);
if (lit != sat::null_literal) if (cond)
lits.pop_back(); lits.pop_back();
continue; continue;
} }
if (children[0]->get_sort() == parent->get_sort()) { if (children[0]->get_sort() == parent->get_sort()) {
lits.push_back(~ctx.mk_literal(m.mk_eq(children[0], parent))); lits.push_back(~ctx.mk_literal(m.mk_eq(children[0], parent)));
TRACE("dt", tout << lits << "\n"); TRACE("dt", for (auto lit : lits) tout << (lit.sign() ? "~": "") << mk_pp(ctx.atom(lit.var()), m) << "\n";);
ctx.add_clause(lits); ctx.add_clause(lits);
lits.pop_back(); lits.pop_back();
} }
@ -173,7 +173,7 @@ namespace sls {
add_path_axioms(children, lits, parents2); add_path_axioms(children, lits, parents2);
children.pop_back(); children.pop_back();
} }
if (lit != sat::null_literal) if (cond)
lits.pop_back(); lits.pop_back();
} }
} }
@ -414,6 +414,7 @@ namespace sls {
} }
IF_VERBOSE(1, verbose_stream() << "cycle\n"; for (auto e : diseqs) verbose_stream() << mk_pp(e, m) << "\n";); IF_VERBOSE(1, verbose_stream() << "cycle\n"; for (auto e : diseqs) verbose_stream() << mk_pp(e, m) << "\n";);
ctx.add_constraint(m.mk_or(diseqs)); ctx.add_constraint(m.mk_or(diseqs));
++m_stats.m_num_occurs;
}; };
for (auto n : g->nodes()) { for (auto n : g->nodes()) {
@ -516,6 +517,7 @@ namespace sls {
void datatype_plugin::collect_statistics(statistics& st) const { void datatype_plugin::collect_statistics(statistics& st) const {
st.update("sls-dt-axioms", m_axioms.size()); st.update("sls-dt-axioms", m_axioms.size());
st.update("sls-dt-occurs-conflicts", m_stats.m_num_occurs);
} }
void datatype_plugin::reset_statistics() {} void datatype_plugin::reset_statistics() {}

10
src/ast/sls/sls_datatype_plugin.h
View file

@ -26,17 +26,17 @@ namespace sls {
class datatype_plugin : public plugin { class datatype_plugin : public plugin {
struct stats { struct stats {
unsigned m_num_axioms = 0; unsigned m_num_occurs = 0;
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
}; };
struct parent_t { struct parent_t {
expr* parent; expr* parent;
sat::literal lit; expr_ref condition;
}; };
euf_plugin& euf; euf_plugin& euf;
scoped_ptr<euf::egraph>& g; scoped_ptr<euf::egraph>& g;
obj_map<sort, ptr_vector<expr>> m_dts; obj_map<sort, ptr_vector<expr>> m_dts;
obj_map<expr, svector<parent_t>> m_parents; obj_map<expr, vector<parent_t>> m_parents;
mutable datatype_util dt; mutable datatype_util dt;
expr_ref_vector m_axioms, m_values; expr_ref_vector m_axioms, m_values;
@ -44,9 +44,9 @@ namespace sls {
stats m_stats; stats m_stats;
void collect_path_axioms(); void collect_path_axioms();
void add_edge(expr* child, expr* parent, sat::literal lit); void add_edge(expr* child, expr* parent, expr* cond);
void add_path_axioms(); void add_path_axioms();
void add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, svector<parent_t> const& parents); void add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, vector<parent_t> const& parents);
void add_axioms(); void add_axioms();
void init_values(); void init_values();