diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index ac4b818b4..f5d6e3dca 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2990,6 +2990,8 @@ namespace seq { if (mem.is_primitive() || !mem.m_regex->is_classical()) continue; + std::cout << "Factoring " << mk_pp(mem.m_str->get_expr(), m) << " ∈ " << mk_pp(mem.m_regex->get_expr(), m) << std::endl; + euf::snode* first = mem.m_str->first(); SASSERT(first); euf::snode* tail = m_sg.drop_first(mem.m_str); @@ -2998,6 +3000,9 @@ namespace seq { tau_pairs pairs; compute_tau(m, m_seq, m_sg, mem.m_regex->get_expr(), pairs); + bool any_child = false; + dep_tracker conflict_dep = mem.m_dep; + for (auto const& pair : pairs) { euf::snode* sn_p = m_sg.mk(pair.m_p); euf::snode* sn_q = m_sg.mk(pair.m_q); @@ -3012,13 +3017,19 @@ namespace seq { // Also check intersection with other primitive constraints on `first` ptr_vector regexes_p; regexes_p.push_back(sn_p); + dep_tracker local_dep = nullptr; for (auto const& prev_mem : node->str_mems()) { - if (prev_mem.m_str == first) + if (prev_mem.m_str == first) { regexes_p.push_back(prev_mem.m_regex); + local_dep = m_dep_mgr.mk_join(local_dep, prev_mem.m_dep); + } } - if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) + if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { + conflict_dep = m_dep_mgr.mk_join(conflict_dep, local_dep); continue; + } + any_child = true; nielsen_node* child = mk_child(node); mk_edge(node, child, true); @@ -3036,6 +3047,11 @@ namespace seq { child->add_str_mem(str_mem(tail, sn_q, mem.m_history, next_mem_id(), mem.m_dep)); } + if (!any_child) { + node->set_conflict(backtrack_reason::regex, conflict_dep); + node->set_general_conflict(); + } + return true; } return false; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index c4be3d4d5..fe3e7768b 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -202,21 +202,29 @@ namespace smt { // ----------------------------------------------------------------------- void theory_nseq::new_eq_eh(theory_var v1, theory_var v2) { - expr* e1 = get_enode(v1)->get_expr(); - expr* e2 = get_enode(v2)->get_expr(); - TRACE(seq, tout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << "\n"); - if (m_seq.is_re(e1)) { - push_unhandled_pred(); - return; + try { + expr* e1 = get_enode(v1)->get_expr(); + expr* e2 = get_enode(v2)->get_expr(); + TRACE(seq, tout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << "\n"); + if (m_seq.is_re(e1)) { + push_unhandled_pred(); + return; + } + if (!m_seq.is_seq(e1) || !m_seq.is_seq(e2)) + return; + euf::snode* s1 = get_snode(e1); + euf::snode* s2 = get_snode(e2); + if (s1 && s2) { + seq::dep_tracker dep = nullptr; + ctx.push_trail(restore_vector(m_prop_queue)); + m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); + } } - if (!m_seq.is_seq(e1) || !m_seq.is_seq(e2)) - return; - euf::snode* s1 = get_snode(e1); - euf::snode* s2 = get_snode(e2); - if (s1 && s2) { - seq::dep_tracker dep = nullptr; - ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); + catch(const std::exception&) { +#ifdef Z3DEBUG + std::string dot = m_nielsen.to_dot(); +#endif + throw; } } @@ -238,79 +246,87 @@ namespace smt { // ----------------------------------------------------------------------- void theory_nseq::assign_eh(bool_var v, bool is_true) { - expr* e = ctx.bool_var2expr(v); - // std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl; - expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr; - TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";); - if (m_seq.str.is_in_re(e, s, re)) { - euf::snode* sn_str = get_snode(s); - euf::snode* sn_re = get_snode(re); - if (!sn_str || !sn_re) - return; - literal lit(v, !is_true); - seq::dep_tracker dep = nullptr; - if (is_true) { - ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, nullptr, m_next_mem_id++, dep)); + try { + expr* e = ctx.bool_var2expr(v); + std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl; + expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr; + TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";); + if (m_seq.str.is_in_re(e, s, re)) { + euf::snode* sn_str = get_snode(s); + euf::snode* sn_re = get_snode(re); + if (!sn_str || !sn_re) + return; + literal lit(v, !is_true); + seq::dep_tracker dep = nullptr; + if (is_true) { + ctx.push_trail(restore_vector(m_prop_queue)); + m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, nullptr, m_next_mem_id++, dep)); + } + else { + // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership + // so the Nielsen graph sees it uniformly; the original negative literal + // is kept in mem_source for conflict reporting. + expr_ref re_compl(m_seq.re.mk_complement(re), m); + euf::snode* sn_re_compl = get_snode(re_compl.get()); + ctx.push_trail(restore_vector(m_prop_queue)); + m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, nullptr, m_next_mem_id++, dep)); + } } - else { - // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership - // so the Nielsen graph sees it uniformly; the original negative literal - // is kept in mem_source for conflict reporting. - expr_ref re_compl(m_seq.re.mk_complement(re), m); - euf::snode* sn_re_compl = get_snode(re_compl.get()); - ctx.push_trail(restore_vector(m_prop_queue)); - m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, nullptr, m_next_mem_id++, dep)); + else if (m_seq.str.is_prefix(e)) { + if (is_true) + m_axioms.prefix_true_axiom(e); + else + m_axioms.prefix_axiom(e); } - } - else if (m_seq.str.is_prefix(e)) { - if (is_true) - m_axioms.prefix_true_axiom(e); - else - m_axioms.prefix_axiom(e); - } - else if (m_seq.str.is_suffix(e)) { - if (is_true) - m_axioms.suffix_true_axiom(e); - else - m_axioms.suffix_axiom(e); - } - else if (m_seq.str.is_contains(e)) { - if (is_true) - m_axioms.contains_true_axiom(e); - else - m_axioms.not_contains_axiom(e); - } - else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { - // axioms added via relevant_eh → dequeue_axiom - } - else if (m_axioms.sk().is_eq(e, a, b) && is_true) { - enode* n1 = ensure_enode(a); - enode* n2 = ensure_enode(b); - auto v1 = mk_var(n1); - auto v2 = mk_var(n2); - if (n1->get_root() != n2->get_root()) { - literal lit(v, false); - ctx.mark_as_relevant(n1); - ctx.mark_as_relevant(n2); - TRACE(seq, tout << "is-eq " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n"); - justification* js = ctx.mk_justification( - ext_theory_eq_propagation_justification( - get_id(), ctx, 1, &lit, 0, nullptr, n1, n2)); - ctx.assign_eq(n1, n2, eq_justification(js)); - new_eq_eh(v1, v2); + else if (m_seq.str.is_suffix(e)) { + if (is_true) + m_axioms.suffix_true_axiom(e); + else + m_axioms.suffix_axiom(e); } + else if (m_seq.str.is_contains(e)) { + if (is_true) + m_axioms.contains_true_axiom(e); + else + m_axioms.not_contains_axiom(e); + } + else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { + // axioms added via relevant_eh → dequeue_axiom + } + else if (m_axioms.sk().is_eq(e, a, b) && is_true) { + enode* n1 = ensure_enode(a); + enode* n2 = ensure_enode(b); + auto v1 = mk_var(n1); + auto v2 = mk_var(n2); + if (n1->get_root() != n2->get_root()) { + literal lit(v, false); + ctx.mark_as_relevant(n1); + ctx.mark_as_relevant(n2); + TRACE(seq, tout << "is-eq " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n"); + justification* js = ctx.mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx, 1, &lit, 0, nullptr, n1, n2)); + ctx.assign_eq(n1, n2, eq_justification(js)); + new_eq_eh(v1, v2); + } + } + else if (m_seq.is_skolem(e) || + m_seq.str.is_nth_i(e) || + m_seq.str.is_nth_u(e) || + m_seq.str.is_is_digit(e) || + m_seq.str.is_foldl(e) || + m_seq.str.is_foldli(e)) { + // no-op: handled by other mechanisms + } + else if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id()) + push_unhandled_pred(); } - else if (m_seq.is_skolem(e) || - m_seq.str.is_nth_i(e) || - m_seq.str.is_nth_u(e) || - m_seq.str.is_is_digit(e) || - m_seq.str.is_foldl(e) || - m_seq.str.is_foldli(e)) { - // no-op: handled by other mechanisms + catch(const std::exception&) { +#ifdef Z3DEBUG + std::string dot = m_nielsen.to_dot(); +#endif + throw; } - else if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id()) - push_unhandled_pred(); } // ----------------------------------------------------------------------- @@ -324,8 +340,16 @@ namespace smt { } void theory_nseq::pop_scope_eh(unsigned num_scopes) { - theory::pop_scope_eh(num_scopes); - m_sgraph.pop(num_scopes); + try { + theory::pop_scope_eh(num_scopes); + m_sgraph.pop(num_scopes); + } + catch(const std::exception&) { +#ifdef Z3DEBUG + std::string dot = m_nielsen.to_dot(); +#endif + throw; + } } void theory_nseq::push_unhandled_pred() { @@ -342,21 +366,29 @@ namespace smt { } void theory_nseq::propagate() { - if (m_prop_qhead == m_prop_queue.size()) - return; - ctx.push_trail(value_trail(m_prop_qhead)); - while (m_prop_qhead < m_prop_queue.size() && !ctx.inconsistent()) { - auto const& item = m_prop_queue[m_prop_qhead++]; - if (std::holds_alternative(item)) - propagate_eq(std::get(item)); - else if (std::holds_alternative(item)) - propagate_pos_mem(std::get(item)); - else if (std::holds_alternative(item)) - dequeue_axiom(std::get(item).e); - else { - UNREACHABLE(); + try { + if (m_prop_qhead == m_prop_queue.size()) + return; + ctx.push_trail(value_trail(m_prop_qhead)); + while (m_prop_qhead < m_prop_queue.size() && !ctx.inconsistent()) { + auto const& item = m_prop_queue[m_prop_qhead++]; + if (std::holds_alternative(item)) + propagate_eq(std::get(item)); + else if (std::holds_alternative(item)) + propagate_pos_mem(std::get(item)); + else if (std::holds_alternative(item)) + dequeue_axiom(std::get(item).e); + else { + UNREACHABLE(); + } } } + catch(const std::exception&) { +#ifdef Z3DEBUG + std::string dot = m_nielsen.to_dot(); +#endif + throw; + } } void theory_nseq::propagate_eq(tracked_str_eq const& eq) { @@ -553,127 +585,135 @@ namespace smt { } final_check_status theory_nseq::final_check_eh(unsigned /*final_check_round*/) { - // Always assert non-negativity for all string theory vars, - // even when there are no string equations/memberships. - if (assert_nonneg_for_all_vars()) { - IF_VERBOSE(1, verbose_stream() << "nseq final_check: nonneg assertions added, FC_CONTINUE\n";); - return FC_CONTINUE; - } - - // Check if there are any eq/mem items in the propagation queue. - bool has_eq_or_mem = any_of(m_prop_queue, [](auto const &item) { - return std::holds_alternative(item) || std::holds_alternative(item); - }); - - // there is nothing to do for the string solver, as there are no string constraints - if (!has_eq_or_mem && m_ho_terms.empty() && !has_unhandled_preds()) { - IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state+ho, FC_DONE (no solve)\n";); - m_nielsen.reset(); - m_nielsen.create_root(); - m_nielsen.set_sat_node(m_nielsen.root()); - TRACE(seq, display(tout << "empty nielsen\n")); - 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() && m_nielsen.sat_node() != nullptr && - 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";); - return FC_CONTINUE; - } - - if (!has_eq_or_mem && !has_unhandled_preds()) { - IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state (after ho), FC_DONE (no solve)\n";); - m_nielsen.reset(); - m_nielsen.create_root(); - m_nielsen.set_sat_node(m_nielsen.root()); - TRACE(seq, display(tout << "empty nielsen\n")); - return FC_DONE; - } - - populate_nielsen_graph(); - - // assert length constraints derived from string equalities - if (assert_length_constraints()) { - IF_VERBOSE(1, verbose_stream() << "nseq final_check: length constraints asserted, FC_CONTINUE\n";); - return FC_CONTINUE; - } - - ++m_num_final_checks; - - m_nielsen.set_max_search_depth(get_fparams().m_nseq_max_depth); - m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes); - m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); - m_nielsen.set_signature_split(get_fparams().m_nseq_signature); - m_nielsen.set_regex_factorization(get_fparams().m_nseq_regex_factorization); - - // Regex membership pre-check: before running DFS, check intersection - // emptiness for each variable's regex constraints. This handles - // regex-only problems that the DFS cannot efficiently solve. - if (get_fparams().m_nseq_regex_precheck) { - switch (check_regex_memberships_precheck()) { - case l_true: - // conflict was asserted inside check_regex_memberships_precheck - IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck UNSAT\n";); + try { + // Always assert non-negativity for all string theory vars, + // even when there are no string equations/memberships. + if (assert_nonneg_for_all_vars()) { + IF_VERBOSE(1, verbose_stream() << "nseq final_check: nonneg assertions added, FC_CONTINUE\n";); return FC_CONTINUE; - case l_false: - // all regex constraints satisfiable, no word eqs → SAT - IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";); - m_nielsen.set_sat_node(m_nielsen.root()); - if (!check_length_coherence()) - return FC_CONTINUE; - TRACE(seq, display(tout << "pre-check done\n")); - return FC_DONE; - default: - break; } - } - IF_VERBOSE(1, verbose_stream() << "nseq final_check: calling solve()\n";); + // Check if there are any eq/mem items in the propagation queue. + bool has_eq_or_mem = any_of(m_prop_queue, [](auto const &item) { + return std::holds_alternative(item) || std::holds_alternative(item); + }); - // here the actual Nielsen solving happens - auto result = m_nielsen.solve(); + // there is nothing to do for the string solver, as there are no string constraints + if (!has_eq_or_mem && m_ho_terms.empty() && !has_unhandled_preds()) { + IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state+ho, FC_DONE (no solve)\n";); + m_nielsen.reset(); + m_nielsen.create_root(); + m_nielsen.set_sat_node(m_nielsen.root()); + TRACE(seq, display(tout << "empty nielsen\n")); + 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() && m_nielsen.sat_node() != nullptr && + 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";); + return FC_CONTINUE; + } + + if (!has_eq_or_mem && !has_unhandled_preds()) { + IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state (after ho), FC_DONE (no solve)\n";); + m_nielsen.reset(); + m_nielsen.create_root(); + m_nielsen.set_sat_node(m_nielsen.root()); + TRACE(seq, display(tout << "empty nielsen\n")); + return FC_DONE; + } + + populate_nielsen_graph(); + + // assert length constraints derived from string equalities + if (assert_length_constraints()) { + IF_VERBOSE(1, verbose_stream() << "nseq final_check: length constraints asserted, FC_CONTINUE\n";); + return FC_CONTINUE; + } + + ++m_num_final_checks; + + m_nielsen.set_max_search_depth(get_fparams().m_nseq_max_depth); + m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes); + m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); + m_nielsen.set_signature_split(get_fparams().m_nseq_signature); + m_nielsen.set_regex_factorization(get_fparams().m_nseq_regex_factorization); + + // Regex membership pre-check: before running DFS, check intersection + // emptiness for each variable's regex constraints. This handles + // regex-only problems that the DFS cannot efficiently solve. + if (get_fparams().m_nseq_regex_precheck) { + switch (check_regex_memberships_precheck()) { + case l_true: + // conflict was asserted inside check_regex_memberships_precheck + IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck UNSAT\n";); + return FC_CONTINUE; + case l_false: + // all regex constraints satisfiable, no word eqs → SAT + IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";); + m_nielsen.set_sat_node(m_nielsen.root()); + if (!check_length_coherence()) + return FC_CONTINUE; + TRACE(seq, display(tout << "pre-check done\n")); + return FC_DONE; + default: + break; + } + } + + IF_VERBOSE(1, verbose_stream() << "nseq final_check: calling solve()\n";); + + // here the actual Nielsen solving happens + auto result = m_nielsen.solve(); #ifdef Z3DEBUG - // Examining the Nielsen graph is probably the best way of debugging - std::string dot = m_nielsen.to_dot(); - IF_VERBOSE(1, verbose_stream() << dot << "\n";); - // std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl; + // Examining the Nielsen graph is probably the best way of debugging + std::string dot = m_nielsen.to_dot(); + IF_VERBOSE(1, verbose_stream() << dot << "\n";); + // std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl; #endif - if (result == seq::nielsen_graph::search_result::unsat) { - IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";); - explain_nielsen_conflict(); - return FC_CONTINUE; - } - - if (result == seq::nielsen_graph::search_result::sat) { - IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve SAT, sat_node=" - << (m_nielsen.sat_node() ? "set" : "null") << "\n";); - // Nielsen found a consistent assignment for positive constraints. - SASSERT(has_eq_or_mem); // we should have axiomatized them - - if (!add_nielsen_assumptions()) + if (result == seq::nielsen_graph::search_result::unsat) { + IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";); + explain_nielsen_conflict(); return FC_CONTINUE; + } - if (!check_length_coherence()) - return FC_CONTINUE; + if (result == seq::nielsen_graph::search_result::sat) { + IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve SAT, sat_node=" + << (m_nielsen.sat_node() ? "set" : "null") << "\n";); + // Nielsen found a consistent assignment for positive constraints. + SASSERT(has_eq_or_mem); // we should have axiomatized them - CTRACE(seq, !has_unhandled_preds(), display(tout << "done\n")); - if (!has_unhandled_preds()) - return FC_DONE; + if (!add_nielsen_assumptions()) + return FC_CONTINUE; + + if (!check_length_coherence()) + return FC_CONTINUE; + + CTRACE(seq, !has_unhandled_preds(), display(tout << "done\n")); + if (!has_unhandled_preds()) + return FC_DONE; + } + + TRACE(seq, display(tout << "unknown\n")); + IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNKNOWN, FC_GIVEUP\n";); + return FC_GIVEUP; + } + catch(const std::exception&) { +#ifdef Z3DEBUG + std::string dot = m_nielsen.to_dot(); +#endif + throw; } - - TRACE(seq, display(tout << "unknown\n")); - IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNKNOWN, FC_GIVEUP\n";); - return FC_GIVEUP; } @@ -839,6 +879,13 @@ namespace smt { } VERIFY(res != l_true); } +#else + for (auto& lit : lits) { + std::cout << mk_pp(ctx.literal2expr(lit), m) << "\n-----------\n"; + } + for (auto& eq : eqs) { + std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << "\n-----------\n"; + } #endif #endif