mirror of
https://github.com/Z3Prover/z3
synced 2026-05-21 09:29:35 +00:00
reviewing seq_nielsen, detect repeated final-check to avoid rebuilding nielsen graph
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
a79a48ed2a
commit
9aceaf3cac
3 changed files with 34 additions and 87 deletions
|
|
@ -88,10 +88,8 @@ namespace seq {
|
|||
toks.reset();
|
||||
if (!s) return;
|
||||
s->collect_tokens(toks);
|
||||
if (fwd || toks.size() < 2) return;
|
||||
unsigned n = toks.size();
|
||||
for (unsigned i = 0; i < n / 2; ++i)
|
||||
std::swap(toks[i], toks[n - 1 - i]);
|
||||
if (!fwd)
|
||||
toks.reverse();
|
||||
}
|
||||
|
||||
// Right-derivative helper used by backward str_mem simplification:
|
||||
|
|
@ -173,10 +171,7 @@ namespace seq {
|
|||
if (m_str) {
|
||||
euf::snode_vector tokens;
|
||||
m_str->collect_tokens(tokens);
|
||||
for (const euf::snode* t : tokens) {
|
||||
if (t == var)
|
||||
return true;
|
||||
}
|
||||
return any_of(tokens, [var](auto t) { return t == var; });
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
|
@ -190,11 +185,7 @@ namespace seq {
|
|||
// check if var appears in replacement
|
||||
euf::snode_vector tokens;
|
||||
m_replacement->collect_tokens(tokens);
|
||||
for (const euf::snode* t : tokens) {
|
||||
if (t == m_var)
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
return all_of(tokens, [this](auto t) { return t != m_var; });
|
||||
}
|
||||
|
||||
bool nielsen_subst::is_char_subst() const {
|
||||
|
|
@ -892,7 +883,7 @@ namespace seq {
|
|||
if (m.are_equal(lt->get_expr(), rt->get_expr())) {
|
||||
++prefix;
|
||||
}
|
||||
else if (lt->is_char() && rt->is_char() && m.are_distinct(lt->get_expr(), rt->get_expr())) {
|
||||
else if (lt->is_char_or_unit() && rt->is_char_or_unit() && m.are_distinct(lt->get_expr(), rt->get_expr())) {
|
||||
m_is_general_conflict = true;
|
||||
m_reason = backtrack_reason::symbol_clash;
|
||||
return simplify_result::conflict;
|
||||
|
|
@ -1221,61 +1212,13 @@ namespace seq {
|
|||
}
|
||||
|
||||
bool nielsen_node::is_satisfied() const {
|
||||
for (str_eq const& eq : m_str_eq) {
|
||||
if (!eq.is_trivial())
|
||||
return false;
|
||||
}
|
||||
for (str_mem const& mem : m_str_mem) {
|
||||
if (!mem.is_trivial() && !mem.is_primitive())
|
||||
return false;
|
||||
}
|
||||
if (any_of(m_str_eq, [](auto const &eq) { return !eq.is_trivial(); }))
|
||||
return false;
|
||||
if (any_of(m_str_mem, [](auto const &m) { return !m.is_trivial() && !m.is_primitive();}))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
bool nielsen_node::has_opaque_terms() const {
|
||||
return false;
|
||||
// needed only if there are terms that are not going to be supported at Nielsen level.
|
||||
// though, unsupported ops are already tracked (or supposed to be tracked) in theory_nseq.
|
||||
#if 0
|
||||
auto is_opaque = [](euf::snode* n) { return false; };
|
||||
for (str_eq const& eq : m_str_eq) {
|
||||
if (eq.is_trivial())
|
||||
continue;
|
||||
if (is_opaque(eq.m_lhs) || is_opaque(eq.m_rhs))
|
||||
return true;
|
||||
euf::snode_vector toks;
|
||||
if (eq.m_lhs) {
|
||||
eq.m_lhs->collect_tokens(toks);
|
||||
for (auto* t : toks) {
|
||||
if (is_opaque(t))
|
||||
return true;
|
||||
}
|
||||
toks.reset();
|
||||
}
|
||||
if (eq.m_rhs) {
|
||||
eq.m_rhs->collect_tokens(toks);
|
||||
for (auto* t : toks) {
|
||||
if (is_opaque(t))
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
for (str_mem const& mem : m_str_mem) {
|
||||
if (!mem.m_str)
|
||||
continue;
|
||||
if (is_opaque(mem.m_str))
|
||||
return true;
|
||||
euf::snode_vector toks;
|
||||
mem.m_str->collect_tokens(toks);
|
||||
for (auto* t : toks) {
|
||||
if (is_opaque(t))
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
#endif
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// nielsen_graph: search
|
||||
// -----------------------------------------------------------------------
|
||||
|
|
@ -1543,10 +1486,6 @@ namespace seq {
|
|||
any_unknown = true;
|
||||
}
|
||||
|
||||
// If no children exist and the node has opaque terms, report unknown
|
||||
if (node->outgoing().empty() && node->has_opaque_terms())
|
||||
return search_result::unknown;
|
||||
|
||||
if (!any_unknown) {
|
||||
node->set_reason(backtrack_reason::children_failed);
|
||||
return search_result::unsat;
|
||||
|
|
@ -1559,11 +1498,7 @@ namespace seq {
|
|||
SASSERT(n && var);
|
||||
euf::snode_vector tokens;
|
||||
n->collect_tokens(tokens);
|
||||
for (const euf::snode* t : tokens) {
|
||||
if (t == var)
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
return any_of(tokens, [var](auto const &t) { return t == var; });
|
||||
}
|
||||
|
||||
bool nielsen_graph::apply_det_modifier(nielsen_node* node) {
|
||||
|
|
@ -1597,7 +1532,7 @@ namespace seq {
|
|||
if (m.are_equal(lt->get_expr(), rt->get_expr())) {
|
||||
++prefix;
|
||||
}
|
||||
else if (lt->is_char() && rt->is_char() && m.are_distinct(lt->get_expr(), rt->get_expr())) {
|
||||
else if (lt->is_char_or_unit() && rt->is_char_or_unit() && m.are_distinct(lt->get_expr(), rt->get_expr())) {
|
||||
break;
|
||||
}
|
||||
else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
|
||||
|
|
@ -1637,7 +1572,7 @@ namespace seq {
|
|||
euf::snode* rt = rhs_toks[rsz - 1 - suffix];
|
||||
if (m.are_equal(lt->get_expr(), rt->get_expr())) {
|
||||
++suffix;
|
||||
} else if (lt->is_char() && rt->is_char() && m.are_distinct(lt->get_expr(), rt->get_expr())) {
|
||||
} else if (lt->is_char_or_unit() && rt->is_char_or_unit() && m.are_distinct(lt->get_expr(), rt->get_expr())) {
|
||||
break;
|
||||
}
|
||||
else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
|
||||
|
|
|
|||
|
|
@ -537,6 +537,14 @@ namespace smt {
|
|||
return FC_DONE;
|
||||
}
|
||||
|
||||
// All literals that were needed to build a model could be assigned to true.
|
||||
// There is an existing nielsen graph with a satisfying assignment.
|
||||
if (!m_nielsen_literals.empty() &&
|
||||
all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) {
|
||||
IF_VERBOSE(1, verbose_stream() << "nseq final_check: satifiable state revisited\n");
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
// unfold higher-order terms when sequence structure is known
|
||||
if (unfold_ho_terms()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "nseq final_check: unfolded ho_terms, FC_CONTINUE\n";);
|
||||
|
|
@ -625,12 +633,20 @@ namespace smt {
|
|||
}
|
||||
|
||||
|
||||
bool theory_nseq::add_nielsen_assumptions() {
|
||||
// return true;
|
||||
bool theory_nseq::add_nielsen_assumptions() {
|
||||
bool has_undef = false;
|
||||
bool has_false = false;
|
||||
m_nielsen_literals.reset();
|
||||
struct reset_vector : public trail {
|
||||
sat::literal_vector &v;
|
||||
reset_vector(sat::literal_vector &v) : v(v) {}
|
||||
void undo() override {
|
||||
v.reset();
|
||||
}
|
||||
};
|
||||
ctx.push_trail(reset_vector(m_nielsen_literals));
|
||||
for (auto const& c : m_nielsen.sat_node()->constraints()) {
|
||||
auto lit = mk_literal(c.fml);
|
||||
m_nielsen_literals.push_back(lit);
|
||||
switch (ctx.get_assignment(lit)) {
|
||||
case l_true:
|
||||
break;
|
||||
|
|
@ -642,8 +658,7 @@ namespace smt {
|
|||
TRACE(seq, tout << "assign: " << c.fml << "\n");
|
||||
break;
|
||||
case l_false:
|
||||
// do we really expect this to happen?
|
||||
has_false = true;
|
||||
// this should not happen because nielsen checks for this before returning a satisfying path.
|
||||
IF_VERBOSE(0, verbose_stream()
|
||||
<< "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
|
||||
ctx.force_phase(lit);
|
||||
|
|
@ -654,11 +669,6 @@ namespace smt {
|
|||
}
|
||||
if (has_undef)
|
||||
return false;
|
||||
if (has_false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "has false\n");
|
||||
// fishy case.
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -66,6 +66,8 @@ namespace smt {
|
|||
obj_hashtable<expr> m_no_diseq_set; // track expressions that should not trigger new disequality axioms
|
||||
expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant
|
||||
|
||||
sat::literal_vector m_nielsen_literals; // literals created by a Nilsen check
|
||||
|
||||
// statistics
|
||||
unsigned m_num_conflicts = 0;
|
||||
unsigned m_num_final_checks = 0;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue