From c91b485fcfcbe31ae84f3ab93f00ab1ad316c74d Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 25 Mar 2026 12:47:52 +0100 Subject: [PATCH] Int Bounds where not updated properly --- src/smt/seq/seq_nielsen.cpp | 137 +++++++++++++-------------------- src/smt/seq/seq_nielsen.h | 14 ++-- src/smt/seq/seq_nielsen_pp.cpp | 12 +-- src/test/seq_nielsen.cpp | 30 ++++---- src/test/seq_parikh.cpp | 16 ++-- 5 files changed, 87 insertions(+), 122 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index bb183ba96..10af489cf 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -241,8 +241,7 @@ namespace seq { } void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { - if (!s.m_var) - return; + SASSERT(s.m_var); for (auto &eq : m_str_eq) { auto new_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement); auto new_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_replacement); @@ -264,7 +263,7 @@ namespace seq { } } // VarBoundWatcher: propagate bounds on s.m_var to variables in s.m_replacement - watch_var_bounds(s); + update_var_bounds(s); } void nielsen_node::add_char_range(euf::snode* sym_char, char_set const& range) { @@ -317,13 +316,11 @@ namespace seq { return v; } - bool nielsen_node::add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep) { + bool nielsen_node::set_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep) { SASSERT(var && var->is_var()); - unsigned id = var->id(); + const unsigned id = var->id(); // check against existing lower bound unsigned cur_lb = 0; - m_var_lb.find(id, cur_lb); - if (lb <= cur_lb) return false; // no tightening m_var_lb.insert(id, lb); // conflict if lb > current upper bound unsigned cur_ub = UINT_MAX; @@ -343,13 +340,10 @@ namespace seq { return true; } - bool nielsen_node::add_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep) { - if (!var || !var->is_var()) return false; - unsigned id = var->id(); + bool nielsen_node::set_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep) { + SASSERT(var && var->is_var()); + const unsigned id = var->id(); // check against existing upper bound - unsigned cur_ub = UINT_MAX; - m_var_ub.find(id, cur_ub); - if (ub >= cur_ub) return false; // no tightening m_var_ub.insert(id, ub); // conflict if current lower bound > ub unsigned cur_lb = 0; @@ -376,8 +370,8 @@ namespace seq { // - for a single variable y: lo-const_len <= len(y) <= hi-const_len // - for multiple variables: each gets an upper bound hi-const_len // Mirrors ZIPT's VarBoundWatcher mechanism. - void nielsen_node::watch_var_bounds(nielsen_subst const& s) { - SASSERT(s.m_var); + void nielsen_node::update_var_bounds(nielsen_subst const& s) { + SASSERT(s.m_var && s.m_replacement); unsigned id = s.m_var->id(); unsigned lo = 0, hi = UINT_MAX; m_var_lb.find(id, lo); @@ -386,8 +380,6 @@ namespace seq { return; // no bounds to propagate // decompose replacement into constant length + variable tokens - if (!s.m_replacement) - return; euf::snode_vector tokens; s.m_replacement->collect_tokens(tokens); @@ -414,9 +406,11 @@ namespace seq { if (var_tokens.size() == 1) { euf::snode* y = var_tokens[0]; - // lo <= const_len + len(y) => len(y) >= lo - const_len (if lo > const_len) - if (lo > const_len) - add_lower_int_bound(y, lo - const_len, s.m_dep); + if ((signed)(lo - const_len) >= 0) + // lo <= const_len + len(y) => len(y) >= lo - const_len (if lo > const_len) + set_lower_int_bound(y, lo - const_len, s.m_dep); + else + set_lower_int_bound(y, 0, s.m_dep); // const_len + len(y) <= hi => len(y) <= hi - const_len if (hi != UINT_MAX) { if (const_len > hi) { @@ -424,7 +418,7 @@ namespace seq { m_reason = backtrack_reason::arithmetic; } else - add_upper_int_bound(y, hi - const_len, s.m_dep); + set_upper_int_bound(y, hi - const_len, s.m_dep); } } else { @@ -438,7 +432,7 @@ namespace seq { } unsigned each_ub = hi - const_len; for (euf::snode* y : var_tokens) { - add_upper_int_bound(y, each_ub, s.m_dep); + set_upper_int_bound(y, each_ub, s.m_dep); } } } @@ -458,9 +452,9 @@ namespace seq { // if str is a single variable, apply bounds directly if (mem.m_str->is_var()) { if (min_len > 0) - add_lower_int_bound(mem.m_str, min_len, mem.m_dep); + set_lower_int_bound(mem.m_str, min_len, mem.m_dep); if (max_len < UINT_MAX) - add_upper_int_bound(mem.m_str, max_len, mem.m_dep); + set_upper_int_bound(mem.m_str, max_len, mem.m_dep); } else { // str is a concatenation or other term: add as general constraints @@ -1536,7 +1530,7 @@ namespace seq { nielsen_graph::search_result nielsen_graph::search_dfs(nielsen_node* node, unsigned depth) { ++m_stats.m_num_dfs_nodes; - std::cout << m_stats.m_num_dfs_nodes << std::endl; + // std::cout << m_stats.m_num_dfs_nodes << std::endl; m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth); // check for external cancellation (timeout, user interrupt) @@ -1651,15 +1645,16 @@ namespace seq { if (!e->len_constraints_computed()) { add_subst_length_constraints(e); e->set_len_constraints_computed(true); - } - for (auto const &ic : e->side_constraints()) - m_solver.assert_expr(ic.fml); + 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); - search_result r = search_dfs(e->tgt(), e->is_progress() ? depth : depth + 1); + const search_result r = search_dfs(e->tgt(), e->is_progress() ? depth : depth + 1); // Restore modification counts on backtrack. dec_edge_mod_counts(e); @@ -2780,7 +2775,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_const_num_unwinding(nielsen_node* node) { - ast_manager &m = m_sg.get_manager(); arith_util arith(m); euf::snode *power = nullptr; @@ -3797,14 +3791,8 @@ namespace seq { void nielsen_graph::add_subst_length_constraints(nielsen_edge* e) { auto const& substs = e->subst(); - - // Quick check: any non-eliminating substitutions? bool has_non_elim = false; - for (auto const& s : substs) - if (!s.is_eliminating()) { has_non_elim = true; break; } - if (!has_non_elim) return; - ast_manager& m = m_sg.get_manager(); arith_util arith(m); // Step 1: Compute LHS (|x|) for each non-eliminating substitution @@ -3813,21 +3801,26 @@ namespace seq { svector> lhs_exprs; for (unsigned i = 0; i < substs.size(); ++i) { auto const& s = substs[i]; - if (s.is_eliminating()) continue; SASSERT(s.m_var && s.m_var->is_var()); expr_ref lhs = compute_length_expr(s.m_var); lhs_exprs.push_back({i, lhs.get()}); + if (s.is_eliminating()) + continue; + has_non_elim = true; // Assert LHS >= 0 e->add_side_constraint(mk_constraint(arith.mk_ge(lhs, arith.mk_int(0)), s.m_dep)); } - // Step 2: Bump mod counts for all non-eliminating variables at once. - for (auto const& s : substs) { - if (s.is_eliminating()) continue; - unsigned id = s.m_var->id(); - unsigned prev = 0; - m_mod_cnt.find(id, prev); - m_mod_cnt.insert(id, prev + 1); + if (has_non_elim) { + // Step 2: Bump mod counts for all non-eliminating variables at once. + for (auto const& s : substs) { + if (s.is_eliminating()) + continue; + unsigned id = s.m_var->id(); + unsigned prev = 0; + m_mod_cnt.find(id, prev); + m_mod_cnt.insert(id, prev + 1); + } } // Step 3: Compute RHS (|u|) with bumped mod counts and add |x| = |u|. @@ -3837,34 +3830,22 @@ namespace seq { auto const& s = substs[idx]; expr_ref rhs = compute_length_expr(s.m_replacement); e->add_side_constraint(mk_constraint(m.mk_eq(lhs_expr, rhs), s.m_dep)); - - // Assert non-negativity for any fresh length variables in the RHS - // (variables at mod_count > 0 that are newly created). - euf::snode_vector tokens; - s.m_replacement->collect_tokens(tokens); - for (euf::snode* tok : tokens) { - if (tok->is_var()) { - unsigned mc = 0; - m_mod_cnt.find(tok->id(), mc); - if (mc > 0) { - expr_ref len_var = get_or_create_len_var(tok, mc); - e->add_side_constraint(mk_constraint(arith.mk_ge(len_var, arith.mk_int(0)), s.m_dep)); - } - } - } } - // Step 4: Restore mod counts (temporary bump for computing RHS only). - for (auto const& s : substs) { - if (s.is_eliminating()) continue; - unsigned id = s.m_var->id(); - unsigned prev = 0; - 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); + if (has_non_elim) { + // Step 4: Restore mod counts (temporary bump for computing RHS only). + for (auto const& s : substs) { + if (s.is_eliminating()) + continue; + unsigned id = s.m_var->id(); + unsigned prev = 0; + 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); + } } } @@ -3898,8 +3879,9 @@ namespace seq { // already present in the enclosing solver scope; asserting them again would // be redundant (though harmless). This is called by search_dfs right after // simplify_and_init, which is where new constraints are produced. - for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) + for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) { m_solver.assert_expr(node->constraints()[i].fml); + } } void nielsen_graph::generate_node_length_constraints(nielsen_node* node) { @@ -3995,19 +3977,6 @@ namespace seq { return constraint(fml, dep, m_sg.get_manager()); } - vector nielsen_graph::get_path_leaf_side_constraints() const { - vector result; - for (nielsen_edge* e : m_cur_path) - for (constraint const& c : e->side_constraints()) - result.push_back(c); - nielsen_node* leaf = m_cur_path.empty() ? m_root - : m_cur_path.back()->tgt(); - if (leaf) - for (constraint const& c : leaf->constraints()) - result.push_back(c); - return result; - } - expr* nielsen_graph::get_power_exponent(euf::snode* power) { if (!power || !power->is_power()) return nullptr; if (power->num_args() < 2) return nullptr; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 1790d3109..e03db5a44 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -487,6 +487,8 @@ namespace seq { void set_tgt(nielsen_node* tgt) { m_tgt = tgt; } + // don't forget to add the substitution + // applying it only to the node is NOT sufficient (otw. length counters are not in sync) vector const& subst() const { return m_subst; } void add_subst(nielsen_subst const& s) { m_subst.push_back(s); } @@ -587,7 +589,7 @@ namespace seq { // and still returns true (the bound value changed). Check is_general_conflict() // separately to distinguish tightening-with-conflict from normal tightening. // Mirrors ZIPT's AddLowerIntBound(). - bool add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep); + bool set_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep); // IntBounds: tighten the upper bound for len(var). // Returns true if the bound was tightened (ub < current upper bound). @@ -596,7 +598,7 @@ namespace seq { // and still returns true (the bound value changed). Check is_general_conflict() // separately to distinguish tightening-with-conflict from normal tightening. // Mirrors ZIPT's AddHigherIntBound(). - bool add_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep); + bool set_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep); // Query current bounds for a variable (default: 0 / UINT_MAX if not set). unsigned var_lb(euf::snode* var) const; @@ -695,7 +697,7 @@ namespace seq { // When var has bounds [lo, hi], derives bounds for variables in replacement // using the known constant-length contribution of non-variable tokens. // Mirrors ZIPT's VarBoundWatcher re-check mechanism. - void watch_var_bounds(nielsen_subst const& s); + void update_var_bounds(nielsen_subst const& s); // Initialize per-variable Parikh bounds from this node's regex memberships. // For each str_mem constraint (str ∈ regex) where regex has length bounds @@ -856,12 +858,6 @@ namespace seq { // current DFS path (valid during and after solve()) svector const& cur_path() const { return m_cur_path; } - // Collect all side constraints along the current path and at the leaf node. - // Returns the edge side_constraints for every edge on m_cur_path plus the - // constraints() of the leaf node (last edge's target, or root if path is empty). - // Intended for theory_nseq to extract assertions implied by the SAT leaf. - vector get_path_leaf_side_constraints() const; - // add constraints to the root node from external solver void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r); void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l); diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 49b1b997c..04e4327ab 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -200,13 +200,13 @@ namespace seq { return r; } if (seq.str.is_length(e, x)) { - if (a->get_num_args() == 0) - return "|" + dot_html_escape(a->get_decl()->get_name().str()) + "|"; - if (names.contains(e)) { - return "|" + names[e] + "|"; + if (to_app(x)->get_num_args() == 0) + return "|" + dot_html_escape(to_app(x)->get_decl()->get_name().str()) + "|"; + if (names.contains(x)) { + return "|" + names[x] + "|"; } - std::string s = dot_html_escape(to_app(e)->get_decl()->get_name().str()) + std::to_string(next_id++); - names.insert(e, s); + std::string s = dot_html_escape(to_app(x)->get_decl()->get_name().str()) + std::to_string(next_id++); + names.insert(x, s); return "|" + s + "|"; } // named constant, fresh variable like n!0 diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index b1c881328..71fcd327d 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -3303,20 +3303,20 @@ static void test_add_lower_int_bound_basic() { SASSERT(node->constraints().empty()); // add lower bound lb=3: should tighten and add constraint - bool tightened = node->add_lower_int_bound(x, 3, dep); + bool tightened = node->set_lower_int_bound(x, 3, dep); SASSERT(tightened); SASSERT(node->var_lb(x) == 3); SASSERT(node->constraints().size() == 1); SASSERT(node->constraints()[0].fml); // add weaker lb=2: no tightening - tightened = node->add_lower_int_bound(x, 2, dep); + tightened = node->set_lower_int_bound(x, 2, dep); SASSERT(!tightened); SASSERT(node->var_lb(x) == 3); SASSERT(node->constraints().size() == 1); // add tighter lb=5: should tighten and add another constraint - tightened = node->add_lower_int_bound(x, 5, dep); + tightened = node->set_lower_int_bound(x, 5, dep); SASSERT(tightened); SASSERT(node->var_lb(x) == 5); SASSERT(node->constraints().size() == 2); @@ -3344,20 +3344,20 @@ static void test_add_upper_int_bound_basic() { SASSERT(node->var_ub(x) == UINT_MAX); // add upper bound ub=10: tightens - bool tightened = node->add_upper_int_bound(x, 10, dep); + bool tightened = node->set_upper_int_bound(x, 10, dep); SASSERT(tightened); SASSERT(node->var_ub(x) == 10); SASSERT(node->constraints().size() == 1); SASSERT(node->constraints()[0].fml); // add weaker ub=20: no tightening - tightened = node->add_upper_int_bound(x, 20, dep); + tightened = node->set_upper_int_bound(x, 20, dep); SASSERT(!tightened); SASSERT(node->var_ub(x) == 10); SASSERT(node->constraints().size() == 1); // add tighter ub=5: tightens - tightened = node->add_upper_int_bound(x, 5, dep); + tightened = node->set_upper_int_bound(x, 5, dep); SASSERT(tightened); SASSERT(node->var_ub(x) == 5); SASSERT(node->constraints().size() == 2); @@ -3383,11 +3383,11 @@ static void test_add_bound_lb_gt_ub_conflict() { seq::dep_tracker dep = nullptr; // set ub=3 first - node->add_upper_int_bound(x, 3, dep); + node->set_upper_int_bound(x, 3, dep); SASSERT(!node->is_general_conflict()); // now set lb=5 > ub=3: should trigger conflict - node->add_lower_int_bound(x, 5, dep); + node->set_lower_int_bound(x, 5, dep); SASSERT(node->is_general_conflict()); SASSERT(node->reason() == seq::backtrack_reason::arithmetic); @@ -3413,9 +3413,9 @@ static void test_bounds_cloned() { seq::dep_tracker dep = nullptr; // set bounds on parent - parent->add_lower_int_bound(x, 2, dep); - parent->add_upper_int_bound(x, 7, dep); - parent->add_lower_int_bound(y, 1, dep); + parent->set_lower_int_bound(x, 2, dep); + parent->set_upper_int_bound(x, 7, dep); + parent->set_lower_int_bound(y, 1, dep); // clone to child seq::nielsen_node* child = ng.mk_child(parent); @@ -3452,8 +3452,8 @@ static void test_var_bound_watcher_single_var() { seq::dep_tracker dep = nullptr; // set bounds: 3 <= len(x) <= 7 - node->add_lower_int_bound(x, 3, dep); - node->add_upper_int_bound(x, 7, dep); + node->set_lower_int_bound(x, 3, dep); + node->set_upper_int_bound(x, 7, dep); node->constraints().reset(); // clear for clean count // apply substitution x → a·y @@ -3489,7 +3489,7 @@ static void test_var_bound_watcher_conflict() { seq::dep_tracker dep = nullptr; // set bounds: 3 <= len(x) (so x must have at least 3 chars) - node->add_lower_int_bound(x, 3, dep); + node->set_lower_int_bound(x, 3, dep); node->constraints().reset(); // apply substitution x → a·b (const_len=2 < lb=3) @@ -3623,7 +3623,7 @@ static void test_var_bound_watcher_multi_var() { seq::dep_tracker dep = nullptr; // set upper bound: len(x) <= 5 - node->add_upper_int_bound(x, 5, dep); + node->set_upper_int_bound(x, 5, dep); node->constraints().reset(); // apply substitution x → y·z (two vars, no constants) diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp index 4d68feb0c..ec76a5238 100644 --- a/src/test/seq_parikh.cpp +++ b/src/test/seq_parikh.cpp @@ -580,8 +580,8 @@ static void test_check_conflict_valid_k_exists() { // lb=3, ub=5: length 4 is achievable (k=2) → no conflict seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); - ng.root()->add_lower_int_bound(x, 3, dep); - ng.root()->add_upper_int_bound(x, 5, dep); + ng.root()->set_lower_int_bound(x, 3, dep); + ng.root()->set_upper_int_bound(x, 5, dep); bool conflict = parikh.check_parikh_conflict(*ng.root()); std::cout << " conflict = " << conflict << " (expect 0)\n"; @@ -608,8 +608,8 @@ static void test_check_conflict_no_valid_k() { // lb=3, ub=3: only odd length 3 — never a multiple of 2 → conflict seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); - ng.root()->add_lower_int_bound(x, 3, dep); - ng.root()->add_upper_int_bound(x, 3, dep); + ng.root()->set_lower_int_bound(x, 3, dep); + ng.root()->set_upper_int_bound(x, 3, dep); bool conflict = parikh.check_parikh_conflict(*ng.root()); std::cout << " conflict = " << conflict << " (expect 1)\n"; @@ -636,8 +636,8 @@ static void test_check_conflict_abc_star() { // lb=5, ub=5 → no valid k (5 is not a multiple of 3) → conflict seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); - ng.root()->add_lower_int_bound(x, 5, dep); - ng.root()->add_upper_int_bound(x, 5, dep); + ng.root()->set_lower_int_bound(x, 5, dep); + ng.root()->set_upper_int_bound(x, 5, dep); bool conflict = parikh.check_parikh_conflict(*ng.root()); std::cout << " conflict = " << conflict << " (expect 1)\n"; @@ -663,8 +663,8 @@ static void test_check_conflict_stride_one_never_conflicts() { ng.add_str_mem(x, regex); seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); - ng.root()->add_lower_int_bound(x, 7, dep); - ng.root()->add_upper_int_bound(x, 7, dep); + ng.root()->set_lower_int_bound(x, 7, dep); + ng.root()->set_upper_int_bound(x, 7, dep); bool conflict = parikh.check_parikh_conflict(*ng.root()); std::cout << " conflict = " << conflict << " (expect 0: stride=1 skipped)\n";