From cedb13d045c63cc245fa4827c95fddd839d1f719 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 22 May 2026 14:38:07 +0200 Subject: [PATCH] First check for conflict and then sat --- src/smt/seq/seq_nielsen.cpp | 119 +++++---------------------------- src/smt/seq/seq_nielsen.h | 8 --- src/smt/seq/seq_nielsen_pp.cpp | 3 +- src/smt/theory_nseq.cpp | 5 +- 4 files changed, 20 insertions(+), 115 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 3b47ae516..ef8552ce5 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1770,14 +1770,6 @@ namespace seq { if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes) return search_result::unknown; - if (node->is_satisfied()) { - m_sat_node = node; - m_sat_path = cur_path; - return search_result::sat; - } - if (node->is_currently_conflict()) - return search_result::unsat; - // we might need to tell the SAT solver about the new integer inequalities // that might have been added by an extension step assert_node_side_constraints(node); @@ -1787,6 +1779,12 @@ namespace seq { return search_result::unsat; } + if (node->is_satisfied()) { + m_sat_node = node; + m_sat_path = cur_path; + return search_result::sat; + } + // simplify constraints (idempotent after first call) const simplify_result sr = node->simplify_and_init(cur_path); @@ -1900,9 +1898,7 @@ namespace seq { m_length_solver.push(); // Lazily compute substitution length constraints (|x| = |u|) on first - // traversal. This must happen before asserting side_constraints and before - // bumping mod counts, so that LHS uses the parent's counts and RHS - // uses the temporarily-bumped counts. + // traversal. This must happen before asserting side_constraints if (!e->len_constraints_computed()) { add_subst_length_constraints(e); e->set_len_constraints_computed(true); @@ -1910,18 +1906,11 @@ namespace seq { for (const auto& sc : e->side_constraints()) { e->tgt()->add_constraint(sc); } - } - // Bump modification counts for the child's context. - inc_edge_mod_counts(e); - const auto new_depth = depth + (e->is_progress() ? 0 : 1); const search_result r = search_dfs(e->tgt(), cur_path, new_depth); - // Restore modification counts on backtrack. - dec_edge_mod_counts(e); - m_length_solver.pop(1); if (r == search_result::sat) return search_result::sat; @@ -1986,10 +1975,8 @@ namespace seq { } else if (t->is_power()) { expr* expr_node = t->get_expr(); expr* pow_base = nullptr, *pow_exp = nullptr; - if (seq().str.is_power(expr_node, pow_base, pow_exp) && pow_exp) { - e->add_side_constraint(mk_constraint(a.mk_ge(pow_exp, a.mk_int(0)), eq.m_dep)); - e->add_side_constraint(mk_constraint(a.mk_le(pow_exp, a.mk_int(0)), eq.m_dep)); - } + if (seq().str.is_power(expr_node, pow_base, pow_exp) && pow_exp) + e->add_side_constraint(mk_constraint(a.mk_eq(pow_exp, a.mk_int(0)), eq.m_dep)); nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), nullptr, eq.m_dep); e->add_subst(s); child->apply_subst(m_sg, s); @@ -2104,8 +2091,7 @@ namespace seq { expr* pow_exp = get_power_exp_expr(pow_head, m_seq); if (pow_exp) { expr* zero = a.mk_int(0); - e->add_side_constraint(mk_constraint(a.mk_ge(pow_exp, zero), eq.m_dep)); - e->add_side_constraint(mk_constraint(a.mk_le(pow_exp, zero), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_eq(pow_exp, zero), eq.m_dep)); } return true; } @@ -3089,10 +3075,8 @@ namespace seq { const nielsen_subst s1(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, eq->m_dep); e->add_subst(s1); child->apply_subst(m_sg, s1); - if (exp_n) { - e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, zero), eq->m_dep)); - e->add_side_constraint(mk_constraint(a.mk_le(exp_n, zero), eq->m_dep)); - } + if (exp_n) + e->add_side_constraint(mk_constraint(a.mk_eq(exp_n, zero), eq->m_dep)); // Branch 2 (explored second): n >= 1 → peel one u: replace u^n with u · u^(n-1) // Side constraint: n >= 1 @@ -4239,8 +4223,7 @@ namespace seq { const nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, mem->m_dep); e->add_subst(s); child->apply_subst(m_sg, s); - e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, zero), mem->m_dep)); - e->add_side_constraint(mk_constraint(a.mk_le(exp_n, zero), mem->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_eq(exp_n, zero), mem->m_dep)); } // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1) @@ -4455,12 +4438,7 @@ namespace seq { void nielsen_graph::add_subst_length_constraints(nielsen_edge* e) { auto const& substs = e->subst(); - bool has_non_elim = false; - - - // Step 1: Compute LHS (|x|) for each non-eliminating substitution - // using current m_mod_cnt (before bumping). - // Also assert |x|_k >= 0 (mirrors ZIPT's NielsenNode constructor line 172). + // Compute LHS (|x|) for each non-eliminating substitution vector> lhs_exprs; for (unsigned i = 0; i < substs.size(); ++i) { auto const& s = substs[i]; @@ -4469,72 +4447,8 @@ namespace seq { if (!m_seq.is_seq(s.m_var->get_expr())) continue; expr_ref lhs = compute_length_expr(s.m_var); - lhs_exprs.push_back({i, lhs}); - if (s.is_eliminating()) - continue; - has_non_elim = true; - // Assert LHS >= 0 - e->add_side_constraint(mk_constraint(a.mk_ge(lhs, a.mk_int(0)), s.m_dep)); - } - - // Step 2: Bump mod counts for all non-eliminating variables at once. - if (has_non_elim) - inc_edge_mod_counts(e); - - - // Step 3: Compute RHS (|u|) with bumped mod counts and add |x| = |u|. - for (auto const &[idx, lhs] : lhs_exprs) { - auto const& s = substs[idx]; expr_ref rhs = compute_length_expr(s.m_replacement); - e->add_side_constraint(mk_constraint(a.mk_ge(lhs, rhs), s.m_dep)); - e->add_side_constraint(mk_constraint(a.mk_le(lhs, rhs), s.m_dep)); - // otw. we have equality as a side-constraint in the Nielsen node - // and adding the Nielsen assumption will force the phase of the equality to true - // however the arith.-solver will axiomatize it as <= && >= which do not have a phase - // hence it might get assigned false by decision which is a performance problem - // e->add_side_constraint(mk_constraint(a.mk_le(lhs, rhs), s.m_dep)); - // e->add_side_constraint(mk_constraint(a.mk_ge(lhs, rhs), s.m_dep)); - } - - // Step 4: Restore mod counts (temporary bump for computing RHS only). - if (has_non_elim) - dec_edge_mod_counts(e); - } - - void nielsen_graph::inc_edge_mod_counts(nielsen_edge* e) { - auto const &sub = e->subst(); - for (unsigned i = 0; i < sub.size(); ++i) { - auto const &s = sub[i]; - unsigned id = s.m_var->id(); - //if (s.m_length) { - // euf::snode *old_length = nullptr; - // m_length_info.find(id, old_length); - // m_length_trail.push_back(old_length); - // m_length_info.insert(id, s.m_length); - //} - //unsigned prev = 0; - //m_mod_cnt.find(id, prev); - //m_mod_cnt.insert(id, prev + 1); - } - } - - void nielsen_graph::dec_edge_mod_counts(nielsen_edge* e) { - auto const &sub = e->subst(); - for (unsigned i = sub.size(); i-- > 0; ) { - auto const &s = sub[i]; - unsigned id = s.m_var->id(); - //if (s.m_length) { - // auto old_length = m_length_trail.back(); - // m_length_trail.pop_back(); - // m_length_info.insert(id, old_length); - //} - //unsigned prev = 0; - //VERIFY(m_mod_cnt.find(id, prev)); - //SASSERT(prev >= 1); - //if (prev <= 1) - // m_mod_cnt.remove(id); - //else - // m_mod_cnt.insert(id, prev - 1); + e->add_side_constraint(mk_constraint(a.mk_eq(lhs, rhs), s.m_dep)); } } @@ -4586,8 +4500,7 @@ namespace seq { expr_ref len_lhs = compute_length_expr(eq.m_lhs); expr_ref len_rhs = compute_length_expr(eq.m_rhs); //node->add_constraint(mk_constraint(m.mk_eq(len_lhs, len_rhs), eq.m_dep)); - node->add_constraint(mk_constraint(a.mk_ge(len_lhs, len_rhs), eq.m_dep)); - node->add_constraint(mk_constraint(a.mk_le(len_lhs, len_rhs), eq.m_dep)); + node->add_constraint(mk_constraint(a.mk_eq(len_lhs, len_rhs), eq.m_dep)); // non-negativity for each variable (mod-count-aware) euf::snode_vector tokens; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index d216ec259..c0dc90ba0 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -1329,14 +1329,6 @@ namespace seq { // Temporarily bumps m_mod_cnt for RHS computation, then restores. // Called lazily on first edge traversal in search_dfs. void add_subst_length_constraints(nielsen_edge* e); - - // Bump modification counts for an edge's non-eliminating substitutions. - // Called when entering an edge during DFS. - void inc_edge_mod_counts(nielsen_edge* e); - - // Restore modification counts for an edge's non-eliminating substitutions. - // Called when backtracking from an edge during DFS. - void dec_edge_mod_counts(nielsen_edge* e); }; } diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 137fc5ed7..65cceed49 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -548,6 +548,7 @@ namespace seq { std::vector int_constraints; for (auto const& ic : m_constraints) { int_constraints.push_back(constraint_html(ic, names, next_id, m)); + SASSERT(!int_constraints.empty()); } if (!int_constraints.empty()) { // eliminate duplicates @@ -557,7 +558,7 @@ namespace seq { if (int_constraints[i] != int_constraints[prev]) int_constraints[++prev] = int_constraints[i]; } - int_constraints.resize(prev); + int_constraints.resize(prev + 1); if (!any) { out << "Cnstr:
"; any = true; } out << "Int:
"; for (const auto& s : int_constraints) { diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index adef5b26d..8aba2fe45 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -850,8 +850,7 @@ namespace smt { //std::cout << "Nielsen assumptions:\n"; bool all_sat = true; ctx.push_trail(reset_vector(m_nielsen_literals)); - for (auto it = m_nielsen.sat_node()->constraints().rbegin(); it != m_nielsen.sat_node()->constraints().rend(); ++it) { - const auto& c = *it; + for (const auto& c : m_nielsen.sat_node()->constraints()) { std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; auto lit = mk_literal(c.fml); m_nielsen_literals.push_back(lit); @@ -876,7 +875,7 @@ namespace smt { // this should not happen because nielsen checks for this before returning a satisfying path. TRACE(seq, tout << "nseq final_check: nielsen assumption " << c.fml << " is false; internalized - " << ctx.e_internalized(c.fml) << "\n"); all_sat = false; - // std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl; + std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl; ctx.push_trail(value_trail(m_context_solver.m_should_internalize)); m_context_solver.m_should_internalize = true; break;