From 367ae39a509e57cb972f48c4259115b81d9bd210 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 31 Mar 2026 21:05:44 +0000 Subject: [PATCH] fix CI: add set_lower/upper_int_bound to nielsen_node, fix nseq_basic simplify_and_init call Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/68ff7081-aa79-475d-9b6c-181c32e8c983 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/seq_nielsen.cpp | 19 +++++++++++++++++++ src/smt/seq/seq_nielsen.h | 11 +++++++++++ src/test/nseq_basic.cpp | 2 +- 3 files changed, 31 insertions(+), 1 deletion(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index abfae8e8a..48f8dddfe 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -315,6 +315,11 @@ namespace seq { bool nielsen_node::lower_bound(expr* e, rational& lo) const { SASSERT(e); + rational stored; + if (m_lower_int_bounds.contains(e->get_id())) { + lo = m_lower_int_bounds.find(e->get_id()); + return true; + } return m_graph.m_solver.lower_bound(e, lo); } @@ -327,9 +332,23 @@ namespace seq { up = v; return true; } + if (m_upper_int_bounds.contains(e->get_id())) { + up = m_upper_int_bounds.find(e->get_id()); + return true; + } return m_graph.m_solver.upper_bound(e, up); } + void nielsen_node::set_lower_int_bound(euf::snode* x, unsigned n, dep_tracker) { + SASSERT(x && x->get_expr()); + m_lower_int_bounds.insert(x->get_expr()->get_id(), rational(n)); + } + + void nielsen_node::set_upper_int_bound(euf::snode* x, unsigned n, dep_tracker) { + SASSERT(x && x->get_expr()); + m_upper_int_bounds.insert(x->get_expr()->get_id(), rational(n)); + } + void nielsen_node::apply_char_subst(euf::sgraph& sg, char_subst const& s) { if (!s.m_var) return; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 00801c78d..33c180d5d 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -530,6 +530,12 @@ namespace seq { u_map> m_char_diseqs; // ?c != {?d, ?e, ...} u_map m_char_ranges; // ?c in [lo, hi) + // direct integer bounds on string length expressions, keyed by expr id. + // used by lower_bound/upper_bound when the solver has no information, + // e.g. in tests that inject bounds without a backing solver. + u_map m_lower_int_bounds; + u_map m_upper_int_bounds; + // edges ptr_vector m_outgoing; nielsen_node* m_backedge = nullptr; @@ -586,6 +592,11 @@ namespace seq { bool lower_bound(expr* e, rational& lo) const; bool upper_bound(expr* e, rational& up) const; + // Directly inject integer bounds on a string snode's expression. + // Used in tests and anywhere bounds are known without a backing solver. + void set_lower_int_bound(euf::snode* x, unsigned n, dep_tracker dep); + void set_upper_int_bound(euf::snode* x, unsigned n, dep_tracker dep); + // character constraint access (mirrors ZIPT's DisEqualities / CharRanges) u_map> const& char_diseqs() const { return m_char_diseqs; } u_map const& char_ranges() const { return m_char_ranges; } diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 6ebcdc018..cf6e4f0e9 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -133,7 +133,7 @@ static void test_nseq_node_satisfied() { SASSERT(node->str_eqs().size() == 1); SASSERT(!node->str_eqs()[0].is_trivial() || node->str_eqs()[0].m_lhs == node->str_eqs()[0].m_rhs); // After simplification, trivial equalities should be removed - seq::simplify_result sr = node->simplify_and_init(); + seq::simplify_result sr = node->simplify_and_init({}); VERIFY(sr == seq::simplify_result::satisfied || sr == seq::simplify_result::proceed); std::cout << " ok\n"; }