diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 629179ab3..6a2c730ca 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -116,6 +116,8 @@ namespace seq { m_int_constraints.reset(); m_char_diseqs.reset(); m_char_ranges.reset(); + m_var_lb.reset(); + m_var_ub.reset(); for (auto const& eq : parent.m_str_eq) m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs, eq.m_dep)); for (auto const& mem : parent.m_str_mem) @@ -133,6 +135,11 @@ namespace seq { for (auto const& kv : parent.m_char_ranges) { m_char_ranges.insert(kv.m_key, kv.m_value.clone()); } + // clone per-variable integer bounds + for (auto const& kv : parent.m_var_lb) + m_var_lb.insert(kv.m_key, kv.m_value); + for (auto const& kv : parent.m_var_ub) + m_var_ub.insert(kv.m_key, kv.m_value); } void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { @@ -151,6 +158,8 @@ namespace seq { mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement); mem.m_dep |= s.m_dep; } + // VarBoundWatcher: propagate bounds on s.m_var to variables in s.m_replacement + watch_var_bounds(s); } void nielsen_node::add_char_range(euf::snode* sym_char, char_set const& range) { @@ -182,6 +191,185 @@ namespace seq { existing.push_back(other); } + // ----------------------------------------------- + // nielsen_node: IntBounds methods + // mirrors ZIPT's AddLowerIntBound / AddHigherIntBound + // ----------------------------------------------- + + unsigned nielsen_node::var_lb(euf::snode* var) const { + if (!var) return 0; + unsigned v = 0; + m_var_lb.find(var->id(), v); + return v; + } + + unsigned nielsen_node::var_ub(euf::snode* var) const { + if (!var) return UINT_MAX; + unsigned v = UINT_MAX; + m_var_ub.find(var->id(), v); + return v; + } + + bool nielsen_node::add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep) { + if (!var || !var->is_var()) return false; + 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; + m_var_ub.find(id, cur_ub); + if (lb > cur_ub) { + m_is_general_conflict = true; + m_reason = backtrack_reason::arithmetic; + return true; + } + // add int_constraint: len(var) >= lb + ast_manager& m = m_graph->sg().get_manager(); + seq_util& seq = m_graph->sg().get_seq_util(); + arith_util arith(m); + expr_ref len_var(seq.str.mk_length(var->get_expr()), m); + expr_ref bound(arith.mk_int(lb), m); + m_int_constraints.push_back(int_constraint(len_var, bound, int_constraint_kind::ge, dep, m)); + 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(); + // 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; + m_var_lb.find(id, cur_lb); + if (cur_lb > ub) { + m_is_general_conflict = true; + m_reason = backtrack_reason::arithmetic; + return true; + } + // add int_constraint: len(var) <= ub + ast_manager& m = m_graph->sg().get_manager(); + seq_util& seq = m_graph->sg().get_seq_util(); + arith_util arith(m); + expr_ref len_var(seq.str.mk_length(var->get_expr()), m); + expr_ref bound(arith.mk_int(ub), m); + m_int_constraints.push_back(int_constraint(len_var, bound, int_constraint_kind::le, dep, m)); + return true; + } + + // VarBoundWatcher: after applying substitution s, propagate bounds on s.m_var + // to variables in s.m_replacement. + // If s.m_var has bounds [lo, hi], and the replacement decomposes into + // const_len concrete chars plus a list of variable tokens, then: + // - 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) { + if (!s.m_var) return; + unsigned id = s.m_var->id(); + unsigned lo = 0, hi = UINT_MAX; + m_var_lb.find(id, lo); + m_var_ub.find(id, hi); + if (lo == 0 && hi == UINT_MAX) 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); + + unsigned const_len = 0; + euf::snode_vector var_tokens; + for (euf::snode* t : tokens) { + if (t->is_char() || t->is_unit()) { + ++const_len; + } else if (t->is_var()) { + var_tokens.push_back(t); + } else { + // power or unknown token: cannot propagate simply, abort + return; + } + } + + if (var_tokens.empty()) { + // all concrete: check if const_len is within [lo, hi] + if (const_len < lo || (hi != UINT_MAX && const_len > hi)) { + m_is_general_conflict = true; + m_reason = backtrack_reason::arithmetic; + } + return; + } + + 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); + // const_len + len(y) <= hi => len(y) <= hi - const_len + if (hi != UINT_MAX) { + if (const_len > hi) { + m_is_general_conflict = true; + m_reason = backtrack_reason::arithmetic; + } else { + add_upper_int_bound(y, hi - const_len, s.m_dep); + } + } + } else { + // multiple variables: propagate upper bound to each + // (each variable contributes >= 0, so each <= hi - const_len) + if (hi != UINT_MAX) { + if (const_len > hi) { + m_is_general_conflict = true; + m_reason = backtrack_reason::arithmetic; + return; + } + unsigned each_ub = hi - const_len; + for (euf::snode* y : var_tokens) + add_upper_int_bound(y, each_ub, s.m_dep); + } + } + } + + // Initialize per-variable Parikh bounds from this node's regex memberships. + // For each str_mem (str ∈ regex) with bounded regex length [min_len, max_len], + // calls add_lower/upper_int_bound for the primary string variable (if str is + // a single variable) or stores a bound on the length expression otherwise. + void nielsen_node::init_var_bounds_from_mems() { + for (str_mem const& mem : m_str_mem) { + if (!mem.m_str || !mem.m_regex) continue; + unsigned min_len = 0, max_len = UINT_MAX; + m_graph->compute_regex_length_interval(mem.m_regex, min_len, max_len); + if (min_len == 0 && max_len == UINT_MAX) continue; + + // 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); + if (max_len < UINT_MAX) + add_upper_int_bound(mem.m_str, max_len, mem.m_dep); + } else { + // str is a concatenation or other term: add as general int_constraints + ast_manager& m = m_graph->sg().get_manager(); + arith_util arith(m); + expr_ref len_str = m_graph->compute_length_expr(mem.m_str); + if (min_len > 0) { + expr_ref bound(arith.mk_int(min_len), m); + m_int_constraints.push_back( + int_constraint(len_str, bound, int_constraint_kind::ge, mem.m_dep, m)); + } + if (max_len < UINT_MAX) { + expr_ref bound(arith.mk_int(max_len), m); + m_int_constraints.push_back( + int_constraint(len_str, bound, int_constraint_kind::le, mem.m_dep, m)); + } + } + } + } + void nielsen_node::apply_char_subst(euf::sgraph& sg, char_subst const& s) { if (!s.m_var) return; @@ -318,6 +506,7 @@ namespace seq { m_fresh_cnt = 0; m_num_input_eqs = 0; m_num_input_mems = 0; + m_root_constraints_asserted = false; } std::ostream& nielsen_graph::display(std::ostream& out) const { @@ -802,6 +991,10 @@ namespace seq { if (wi < m_str_mem.size()) m_str_mem.shrink(wi); + // IntBounds initialization: derive per-variable Parikh length bounds from + // remaining regex memberships and add to m_int_constraints. + init_var_bounds_from_mems(); + if (is_satisfied()) return simplify_result::satisfied; @@ -839,6 +1032,22 @@ namespace seq { // nielsen_graph: search // ----------------------------------------------------------------------- + void nielsen_graph::assert_root_constraints_to_solver() { + if (m_root_constraints_asserted) return; + m_root_constraints_asserted = true; + // Constraint.Shared: assert all root-level length/Parikh constraints + // to m_solver at the base level (no push/pop). These include: + // - len(lhs) = len(rhs) for each non-trivial string equality + // - len(str) >= min_len and len(str) <= max_len for each regex membership + // - len(x) >= 0 for each variable appearing in the root constraints + // Making these visible to the solver before the DFS allows arithmetic + // pruning at every node, not just the root. + vector constraints; + generate_length_constraints(constraints); + for (auto const& lc : constraints) + m_solver.assert_expr(lc.m_expr); + } + nielsen_graph::search_result nielsen_graph::solve() { if (!m_root) return search_result::sat; @@ -847,6 +1056,10 @@ namespace seq { m_sat_node = nullptr; m_sat_path.reset(); + // Constraint.Shared: assert root-level length/Parikh constraints to the + // solver at the base level, so they are visible during all feasibility checks. + assert_root_constraints_to_solver(); + // Iterative deepening: increment by 1 on each failure. // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it. m_depth_bound = 3; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 5b9cfcd89..1660be312 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -164,9 +164,10 @@ Abstract: has no ConstraintsIntEq or ConstraintsIntLe in nielsen_node. - IntBounds / VarBoundWatcher: per-variable integer interval bounds and the watcher mechanism that reruns bound propagation when a string variable is - substituted are not ported. + substituted — PORTED as nielsen_node::{add_lower_int_bound, + add_upper_int_bound, watch_var_bounds, init_var_bounds_from_mems}. - AddLowerIntBound() / AddHigherIntBound(): incremental interval tightening - with restart signaling is not ported. + — PORTED as the above add_lower/upper_int_bound methods. Character-level handling: - CharSubst: character-level variable substitution (symbolic char -> concrete @@ -214,7 +215,10 @@ Abstract: - GetSignature(): the constraint-pair signature used for subsumption candidate matching is not ported. - Constraint.Shared: the flag indicating whether a constraint should be - forwarded to the outer solver is not ported. + forwarded to the outer solver — PORTED as + nielsen_graph::assert_root_constraints_to_solver(), called at the start + of solve() to make all root-level length/Parikh constraints immediately + visible to m_solver. - Interpretation: the model-extraction class mapping string and integer variables to concrete values is not ported. ----------------------------------------------------------------------- @@ -490,6 +494,12 @@ namespace seq { vector m_str_mem; // regex memberships vector m_int_constraints; // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe) + // per-variable integer bounds for len(var). Mirrors ZIPT's IntBounds. + // key: snode id of the string variable. + // default lb = 0 (unrestricted); default ub = UINT_MAX (unrestricted). + u_map m_var_lb; // lower bound: lb <= len(var) + u_map m_var_ub; // upper bound: len(var) <= ub + // character constraints (mirrors ZIPT's DisEqualities and CharRanges) // key: snode id of the s_unit symbolic character u_map> m_char_diseqs; // ?c != {?d, ?e, ...} @@ -528,6 +538,28 @@ namespace seq { vector const& int_constraints() const { return m_int_constraints; } vector& int_constraints() { return m_int_constraints; } + // IntBounds: tighten the lower bound for len(var). + // Returns true if the bound was tightened (lb > current lower bound). + // When tightened without conflict, adds an int_constraint len(var) >= lb. + // When lb > current upper bound, sets arithmetic conflict (no constraint added) + // 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); + + // IntBounds: tighten the upper bound for len(var). + // Returns true if the bound was tightened (ub < current upper bound). + // When tightened without conflict, adds an int_constraint len(var) <= ub. + // When current lower bound > ub, sets arithmetic conflict (no constraint added) + // 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); + + // Query current bounds for a variable (default: 0 / UINT_MAX if not set). + unsigned var_lb(euf::snode* var) const; + unsigned var_ub(euf::snode* var) const; + // 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; } @@ -603,6 +635,19 @@ namespace seq { // sets changed=true, and returns false. bool handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side, dep_tracker const& dep, bool& changed); + + // VarBoundWatcher: after applying substitution s, propagate the bounds + // of s.m_var to variables appearing in s.m_replacement. + // 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); + + // Initialize per-variable Parikh bounds from this node's regex memberships. + // For each str_mem constraint (str ∈ regex) where regex has length bounds + // [min_len, max_len], adds lower/upper bound constraints for len(str). + // Called from simplify_and_init to populate IntBounds at node creation. + void init_var_bounds_from_mems(); }; // search statistics collected during Nielsen graph solving @@ -662,6 +707,10 @@ namespace seq { // ----------------------------------------------- simple_solver& m_solver; + // Constraint.Shared: guards re-assertion of root-level constraints. + // Set to true after assert_root_constraints_to_solver() is first called. + bool m_root_constraints_asserted = false; + public: // Construct with a caller-supplied solver. Ownership is NOT transferred; // the caller is responsible for keeping the solver alive. @@ -754,6 +803,16 @@ namespace seq { // Also generates len(x) >= 0 for each variable appearing in the equations. void generate_length_constraints(vector& constraints); + // build an arithmetic expression representing the length of an snode tree. + // concatenations are expanded to sums, chars to 1, empty to 0, + // variables to (str.len var_expr). + expr_ref compute_length_expr(euf::snode* n); + + // compute Parikh length interval [min_len, max_len] for a regex snode. + // uses seq_util::rex min_length/max_length on the underlying expression. + // max_len == UINT_MAX means unbounded. + void compute_regex_length_interval(euf::snode* regex, unsigned& min_len, unsigned& max_len); + private: search_result search_dfs(nielsen_node* node, unsigned depth, svector& cur_path); @@ -860,20 +919,17 @@ namespace seq { // find a power token facing a variable head bool find_power_vs_var(nielsen_node* node, euf::snode*& power, euf::snode*& var_head, str_eq const*& eq_out) const; - // build an arithmetic expression representing the length of an snode tree. - // concatenations are expanded to sums, chars to 1, empty to 0, - // variables to (str.len var_expr). - expr_ref compute_length_expr(euf::snode* n); - - // compute Parikh length interval [min_len, max_len] for a regex snode. - // uses seq_util::rex min_length/max_length on the underlying expression. - // max_len == UINT_MAX means unbounded. - void compute_regex_length_interval(euf::snode* regex, unsigned& min_len, unsigned& max_len); - // ----------------------------------------------- // Integer feasibility subsolver methods // ----------------------------------------------- + // Constraint.Shared: assert all root-level length/Parikh constraints to + // m_solver at the base level (outside push/pop). Called once at the start + // of solve(). Makes derived constraints immediately visible to m_solver + // for arithmetic pruning at every DFS node, not just the root. + // Mirrors ZIPT's Constraint.Shared forwarding mechanism. + void assert_root_constraints_to_solver(); + // collect int_constraints along the path from root to the given node, // including constraints from edges and nodes. void collect_path_int_constraints(nielsen_node* node, diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 7472755fb..ff9318e84 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -21,6 +21,15 @@ Abstract: #include "smt/theory_nseq.h" #include +// Trivial solver that always returns sat and ignores all assertions. +class nseq_basic_dummy_solver : public seq::simple_solver { +public: + void push() override {} + void pop(unsigned) override {} + void assert_expr(expr*) override {} + lbool check() override { return l_true; } +}; + // Test 1: instantiation of nielsen_graph compiles and doesn't crash static void test_nseq_instantiation() { std::cout << "test_nseq_instantiation\n"; @@ -28,7 +37,8 @@ static void test_nseq_instantiation() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); SASSERT(ng.root() == nullptr); SASSERT(ng.num_nodes() == 0); std::cout << " ok\n"; @@ -83,7 +93,8 @@ static void test_nseq_simplification() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); // Add a trivial equality: empty = empty euf::snode* empty1 = sg.mk_empty(); @@ -104,7 +115,8 @@ static void test_nseq_node_satisfied() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); seq::nielsen_node* node = ng.mk_node(); // empty node has no constraints => satisfied @@ -130,7 +142,8 @@ static void test_nseq_symbol_clash() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('a'); euf::snode* b = sg.mk_char('b'); @@ -155,7 +168,8 @@ static void test_nseq_var_eq_self() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x")); ng.add_str_eq(x, x); @@ -172,7 +186,8 @@ static void test_nseq_prefix_clash() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x")); euf::snode* a = sg.mk_char('a'); @@ -193,7 +208,8 @@ static void test_nseq_const_nielsen_solvable() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x")); euf::snode* y = sg.mk_var(symbol("y")); @@ -215,7 +231,8 @@ static void test_nseq_length_mismatch() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - seq::nielsen_graph ng(sg); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('a'); euf::snode* b = sg.mk_char('b'); diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp index b07a636de..c70afaf13 100644 --- a/src/test/nseq_zipt.cpp +++ b/src/test/nseq_zipt.cpp @@ -29,6 +29,15 @@ Abstract: #include #include +// Trivial solver that always returns sat and ignores all assertions. +class nseq_zipt_dummy_solver : public seq::simple_solver { +public: + void push() override {} + void pop(unsigned) override {} + void assert_expr(expr*) override {} + lbool check() override { return l_true; } +}; + // ----------------------------------------------------------------------- // Trivial simple_solver stub: optimistically assumes integer constraints // are always feasible (returns l_true without actually checking). diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index c96ebc6ce..c0d58fdd2 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -27,7 +27,7 @@ public: dummy_simple_solver() : seq::simple_solver() {} void push() override {} void pop(unsigned n) override {} - void assert_expr(expr *constraint) override {} + void assert_expr(expr *e) override {} lbool check() override { return l_true; } @@ -3133,6 +3133,390 @@ static void test_parikh_dep_tracking() { std::cout << " all constraints have non-empty deps\n"; } +// ----------------------------------------------------------------------- +// IntBounds / VarBoundWatcher tests (Task: IntBounds/Constraint.Shared) +// ----------------------------------------------------------------------- + +// tracking solver: records assert_expr calls for inspection +class tracking_solver : public seq::simple_solver { +public: + vector asserted; + ast_manager& m; + unsigned push_count = 0; + unsigned pop_count = 0; + lbool check_result = l_true; + + tracking_solver(ast_manager& m) : m(m) {} + void push() override { ++push_count; } + void pop(unsigned n) override { pop_count += n; } + void assert_expr(expr* e) override { asserted.push_back(expr_ref(e, m)); } + lbool check() override { return check_result; } + void reset_tracking() { + asserted.reset(); + push_count = 0; + pop_count = 0; + } +}; + +// test add_lower_int_bound: basic tightening adds int_constraint +static void test_add_lower_int_bound_basic() { + std::cout << "test_add_lower_int_bound_basic\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + seq_util seq(m); + + euf::snode* x = sg.mk_var(symbol("x")); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, x); // create root node + + seq::nielsen_node* node = ng.root(); + seq::dep_tracker dep; + + // initially no bounds + SASSERT(node->var_lb(x) == 0); + SASSERT(node->var_ub(x) == UINT_MAX); + SASSERT(node->int_constraints().empty()); + + // add lower bound lb=3: should tighten and add constraint + bool tightened = node->add_lower_int_bound(x, 3, dep); + SASSERT(tightened); + SASSERT(node->var_lb(x) == 3); + SASSERT(node->int_constraints().size() == 1); + SASSERT(node->int_constraints()[0].m_kind == seq::int_constraint_kind::ge); + + // add weaker lb=2: no tightening + tightened = node->add_lower_int_bound(x, 2, dep); + SASSERT(!tightened); + SASSERT(node->var_lb(x) == 3); + SASSERT(node->int_constraints().size() == 1); + + // add tighter lb=5: should tighten and add another constraint + tightened = node->add_lower_int_bound(x, 5, dep); + SASSERT(tightened); + SASSERT(node->var_lb(x) == 5); + SASSERT(node->int_constraints().size() == 2); + + std::cout << " ok\n"; +} + +// test add_upper_int_bound: basic tightening adds int_constraint +static void test_add_upper_int_bound_basic() { + std::cout << "test_add_upper_int_bound_basic\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, x); + + seq::nielsen_node* node = ng.root(); + seq::dep_tracker dep; + + SASSERT(node->var_ub(x) == UINT_MAX); + + // add upper bound ub=10: tightens + bool tightened = node->add_upper_int_bound(x, 10, dep); + SASSERT(tightened); + SASSERT(node->var_ub(x) == 10); + SASSERT(node->int_constraints().size() == 1); + SASSERT(node->int_constraints()[0].m_kind == seq::int_constraint_kind::le); + + // add weaker ub=20: no tightening + tightened = node->add_upper_int_bound(x, 20, dep); + SASSERT(!tightened); + SASSERT(node->var_ub(x) == 10); + SASSERT(node->int_constraints().size() == 1); + + // add tighter ub=5: tightens + tightened = node->add_upper_int_bound(x, 5, dep); + SASSERT(tightened); + SASSERT(node->var_ub(x) == 5); + SASSERT(node->int_constraints().size() == 2); + + std::cout << " ok\n"; +} + +// test add_lower_int_bound: conflict when lb > ub +static void test_add_bound_lb_gt_ub_conflict() { + std::cout << "test_add_bound_lb_gt_ub_conflict\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, x); + + seq::nielsen_node* node = ng.root(); + seq::dep_tracker dep; + + // set ub=3 first + node->add_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); + SASSERT(node->is_general_conflict()); + SASSERT(node->reason() == seq::backtrack_reason::arithmetic); + + std::cout << " ok\n"; +} + +// test clone_from: child inherits parent bounds +static void test_bounds_cloned() { + std::cout << "test_bounds_cloned\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + euf::snode* y = sg.mk_var(symbol("y")); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, y); + + seq::nielsen_node* parent = ng.root(); + seq::dep_tracker dep; + + // 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); + + // clone to child + seq::nielsen_node* child = ng.mk_child(parent); + + // child should have same bounds + SASSERT(child->var_lb(x) == 2); + SASSERT(child->var_ub(x) == 7); + SASSERT(child->var_lb(y) == 1); + SASSERT(child->var_ub(y) == UINT_MAX); + + // child's int_constraints should also be cloned (3 constraints: lb_x, ub_x, lb_y) + SASSERT(child->int_constraints().size() == parent->int_constraints().size()); + + std::cout << " ok\n"; +} + +// test VarBoundWatcher: substitution x→a·y propagates bounds from x to y +static void test_var_bound_watcher_single_var() { + std::cout << "test_var_bound_watcher_single_var\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + euf::snode* y = sg.mk_var(symbol("y")); + euf::snode* a = sg.mk_char('a'); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, y); + + seq::nielsen_node* node = ng.root(); + seq::dep_tracker dep; + + // set bounds: 3 <= len(x) <= 7 + node->add_lower_int_bound(x, 3, dep); + node->add_upper_int_bound(x, 7, dep); + node->int_constraints().reset(); // clear for clean count + + // apply substitution x → a·y + euf::snode* ay = sg.mk_concat(a, y); + seq::nielsen_subst s(x, ay, dep); + node->apply_subst(sg, s); + + // VarBoundWatcher should propagate: 3 <= 1+len(y) <= 7 + // => len(y) >= 2, len(y) <= 6 + SASSERT(node->var_lb(y) == 2); + SASSERT(node->var_ub(y) == 6); + + std::cout << " ok\n"; +} + +// test VarBoundWatcher: substitution with all-concrete replacement detects conflict +static void test_var_bound_watcher_conflict() { + std::cout << "test_var_bound_watcher_conflict\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + euf::snode* a = sg.mk_char('a'); + euf::snode* b = sg.mk_char('b'); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, a); + + seq::nielsen_node* node = ng.root(); + seq::dep_tracker dep; + + // set bounds: 3 <= len(x) (so x must have at least 3 chars) + node->add_lower_int_bound(x, 3, dep); + node->int_constraints().reset(); + + // apply substitution x → a·b (const_len=2 < lb=3) + euf::snode* ab = sg.mk_concat(a, b); + seq::nielsen_subst s(x, ab, dep); + node->apply_subst(sg, s); + + // should detect conflict: len(x) >= 3 but replacement has len=2 + SASSERT(node->is_general_conflict()); + SASSERT(node->reason() == seq::backtrack_reason::arithmetic); + + std::cout << " ok\n"; +} + +// test init_var_bounds_from_mems: simplify_and_init adds Parikh bounds +static void test_simplify_adds_parikh_bounds() { + std::cout << "test_simplify_adds_parikh_bounds\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + seq_util seq(m); + + euf::snode* x = sg.mk_var(symbol("x")); + + // create regex: to_re("AB") — exactly 2 chars + expr_ref ch_a(seq.str.mk_char('A'), m); + expr_ref ch_b(seq.str.mk_char('B'), m); + expr_ref unit_a(seq.str.mk_unit(ch_a), m); + expr_ref unit_b(seq.str.mk_unit(ch_b), m); + expr_ref re_ab(seq.re.mk_concat(seq.re.mk_to_re(unit_a), seq.re.mk_to_re(unit_b)), m); + euf::snode* regex = sg.mk(re_ab); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_mem(x, regex); + + seq::nielsen_node* node = ng.root(); + + // simplify_and_init should call init_var_bounds_from_mems + seq::simplify_result sr = node->simplify_and_init(ng); + (void)sr; + + // x ∈ to_re("AB") has min_len=2, max_len=2 + // so lb=2, ub=2 should be set on x + SASSERT(node->var_lb(x) == 2); + SASSERT(node->var_ub(x) == 2); + + std::cout << " ok\n"; +} + +// test assert_root_constraints_to_solver: root constraints are forwarded +static void test_assert_root_constraints_to_solver() { + std::cout << "test_assert_root_constraints_to_solver\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + seq_util seq(m); + + euf::snode* x = sg.mk_var(symbol("x")); + euf::snode* a = sg.mk_char('a'); + euf::snode* b = sg.mk_char('b'); + euf::snode* ab = sg.mk_concat(a, b); + + tracking_solver ts(m); + seq::nielsen_graph ng(sg, ts); + // equation: x = a·b → generates len(x) = 2 and len(x) >= 0 + ng.add_str_eq(x, ab); + + // solve() calls assert_root_constraints_to_solver() internally + ts.reset_tracking(); + ng.solve(); + + // should have asserted at least: len(x) = 2, len(x) >= 0 + SASSERT(ts.asserted.size() >= 2); + std::cout << " asserted " << ts.asserted.size() << " root constraints to solver\n"; + for (auto& e : ts.asserted) + std::cout << " " << mk_pp(e, m) << "\n"; + + std::cout << " ok\n"; +} + +// test assert_root_constraints_to_solver: called only once even across iterations +static void test_assert_root_constraints_once() { + std::cout << "test_assert_root_constraints_once\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + euf::snode* y = sg.mk_var(symbol("y")); + + tracking_solver ts(m); + seq::nielsen_graph ng(sg, ts); + ng.add_str_eq(x, y); + + // solve is called (iterative deepening runs multiple iterations) + ng.solve(); + unsigned count_first = ts.asserted.size(); + + // after reset, assert count should be 0 then non-zero again + // (reset clears m_root_constraints_asserted) + // We can't call solve() again on the same graph without reset, but + // we can verify the count is stable between iterations by checking + // that the same constraints weren't added multiple times. + // The simplest check: count > 0 (constraints were asserted) + SASSERT(count_first > 0); // x=y produces at least len(x)=len(y) and non-neg constraints + std::cout << " asserted " << count_first << " constraints total during solve\n"; + std::cout << " ok\n"; +} + +// test VarBoundWatcher with multiple variables in replacement +static void test_var_bound_watcher_multi_var() { + std::cout << "test_var_bound_watcher_multi_var\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + + euf::snode* x = sg.mk_var(symbol("x")); + euf::snode* y = sg.mk_var(symbol("y")); + euf::snode* z = sg.mk_var(symbol("z")); + + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); + ng.add_str_eq(x, y); + + seq::nielsen_node* node = ng.root(); + seq::dep_tracker dep; + + // set upper bound: len(x) <= 5 + node->add_upper_int_bound(x, 5, dep); + node->int_constraints().reset(); + + // apply substitution x → y·z (two vars, no constants) + euf::snode* yz = sg.mk_concat(y, z); + seq::nielsen_subst s(x, yz, dep); + node->apply_subst(sg, s); + + // len(y·z) <= 5 → each of y, z gets ub=5 + SASSERT(node->var_ub(y) == 5); + SASSERT(node->var_ub(z) == 5); + + std::cout << " ok\n"; +} + void tst_seq_nielsen() { test_dep_tracker(); test_str_eq(); @@ -3240,4 +3624,15 @@ void tst_seq_nielsen() { test_parikh_mixed_eq_mem(); test_parikh_full_seq_no_bounds(); test_parikh_dep_tracking(); + // IntBounds / VarBoundWatcher / Constraint.Shared tests + test_add_lower_int_bound_basic(); + test_add_upper_int_bound_basic(); + test_add_bound_lb_gt_ub_conflict(); + test_bounds_cloned(); + test_var_bound_watcher_single_var(); + test_var_bound_watcher_conflict(); + test_simplify_adds_parikh_bounds(); + test_assert_root_constraints_to_solver(); + test_assert_root_constraints_once(); + test_var_bound_watcher_multi_var(); }