mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
https://github.com/Z3Prover/z3/issues/5417#issuecomment-882050602
This commit is contained in:
parent
750c06e258
commit
e8bc9f3469
|
@ -326,6 +326,7 @@ namespace euf {
|
|||
void collect_statistics(statistics& st) const;
|
||||
|
||||
unsigned num_scopes() const { return m_scopes.size() + m_num_scopes; }
|
||||
unsigned num_nodes() const { return m_nodes.size(); }
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); }
|
||||
|
|
|
@ -427,9 +427,11 @@ namespace array {
|
|||
app_ref sel1(m), sel2(m);
|
||||
sel1 = a.mk_select(args1);
|
||||
sel2 = a.mk_select(args2);
|
||||
prop |= !ctx.get_enode(sel1) || !ctx.get_enode(sel2);
|
||||
if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom()))
|
||||
prop = true;
|
||||
}
|
||||
prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
|
||||
if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()))
|
||||
prop = true;
|
||||
return prop;
|
||||
|
|
|
@ -714,6 +714,7 @@ namespace dt {
|
|||
if (v == euf::null_theory_var)
|
||||
return false;
|
||||
euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
|
||||
CTRACE("dt", !con, display(tout) << ctx.bpp(n) << "\n";);
|
||||
if (con->num_args() == 0)
|
||||
dep.insert(n, nullptr);
|
||||
for (enode* arg : euf::enode_args(con))
|
||||
|
|
|
@ -449,8 +449,8 @@ namespace euf {
|
|||
|
||||
if (!init_relevancy())
|
||||
give_up = true;
|
||||
|
||||
|
||||
|
||||
unsigned num_nodes = m_egraph.num_nodes();
|
||||
for (auto* e : m_solvers) {
|
||||
if (!m.inc())
|
||||
return sat::check_result::CR_GIVEUP;
|
||||
|
@ -468,6 +468,10 @@ namespace euf {
|
|||
return sat::check_result::CR_CONTINUE;
|
||||
if (give_up)
|
||||
return sat::check_result::CR_GIVEUP;
|
||||
if (num_nodes < m_egraph.num_nodes()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
}
|
||||
if (m_qsolver)
|
||||
return m_qsolver->check();
|
||||
TRACE("after_search", s().display(tout););
|
||||
|
|
Loading…
Reference in a new issue