diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 4ed0e4583..43407df41 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -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()) { diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 00a753cd8..dbda2edab 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -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; } diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 7fa5ac06a..3517ebbe7 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -66,6 +66,8 @@ namespace smt { obj_hashtable 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;