mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

fix CI: add set_lower/upper_int_bound to nielsen_node, fix nseq_basic simplify_and_init call

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/68ff7081-aa79-475d-9b6c-181c32e8c983

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-31 21:05:44 +00:00
parent 587400bc3d
commit 367ae39a50
3 changed files with 31 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/seq/seq_nielsen.cpp
View file

@ -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;

11
src/smt/seq/seq_nielsen.h
View file

@ -530,6 +530,12 @@ namespace seq {
u_map<ptr_vector<euf::snode>> m_char_diseqs; // ?c != {?d, ?e, ...}
u_map<char_set> 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<rational> m_lower_int_bounds;
u_map<rational> m_upper_int_bounds;
// edges
ptr_vector<nielsen_edge> 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<ptr_vector<euf::snode>> const& char_diseqs() const { return m_char_diseqs; }
u_map<char_set> const& char_ranges() const { return m_char_ranges; }

2
src/test/nseq_basic.cpp
View file

@ -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";
}