From ca12eae670c1cc60fcc0f7f644b8267531ac1071 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 21 May 2026 17:17:49 +0200 Subject: [PATCH] WIP: Undid internal constraints --- src/smt/seq/seq_nielsen.cpp | 125 ++++++++++++++++++--------------- src/smt/seq/seq_nielsen.h | 21 +++--- src/smt/seq/seq_nielsen_pp.cpp | 37 ++++++---- src/smt/seq/seq_parikh.cpp | 6 +- src/smt/smt_context.cpp | 1 + src/smt/theory_nseq.cpp | 9 +-- src/test/seq_nielsen.cpp | 4 +- 7 files changed, 109 insertions(+), 94 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 716cf9826..77d3cb29c 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -321,7 +321,7 @@ namespace seq { // We have to add all - even if some of it conflict // [otw. we would leave the node partially initialized] for (const auto f : *to_app(c.fml)) { - add_constraint(constraint(f, c.dep, c.internal, m)); + add_constraint(constraint(f, c.dep, m)); } return; } @@ -371,7 +371,7 @@ namespace seq { expr* var_c_expr = s.m_var->arg(0)->get_expr(); expr* repl_c_expr = s.m_replacement->arg(0)->get_expr(); add_constraint( - constraint(m.mk_eq(var_c_expr, repl_c_expr), s.m_dep, false, m)); + constraint(m.mk_eq(var_c_expr, repl_c_expr), s.m_dep, m)); if (m_char_ranges.contains(var_id)) { const auto range = m_char_ranges.find(var_id); // copy exactly @@ -425,7 +425,7 @@ namespace seq { seq.mk_le(seq.mk_char(ranges[i].m_lo), var), seq.mk_le(var, seq.mk_char(ranges[i].m_hi - 1))); } - add_constraint(constraint(m.mk_or(cases), dep, false, m)); + add_constraint(constraint(m.mk_or(cases), dep, m)); } // ----------------------------------------------- // nielsen_graph @@ -531,15 +531,15 @@ namespace seq { m_depth_bound = 0; m_fresh_cnt = 0; m_root_constraints_asserted = false; - m_mod_cnt.reset(); + //m_mod_cnt.reset(); m_partial_dfa_edges.reset(); m_partial_dfa_out.clear(); m_partial_dfa_in.clear(); m_partial_dfa_edge_index.clear(); m_projection_extract_idx = 0; m_projection_cover_size.reset(); - m_length_trail.reset(); - m_length_info.reset(); + //m_length_trail.reset(); + //m_length_info.reset(); m_dep_mgr.reset(); m_length_solver.reset(); SASSERT(m_nodes.empty()); @@ -555,7 +555,7 @@ namespace seq { // just assume it to be correct // Just add the constraint - we do not have to recompute it // [also it is on the set of side-conditions if we assert a satisfied node] - n->add_constraint(constraint(le, dep, false, m)); + n->add_constraint(constraint(le, dep, m)); } // ----------------------------------------------------------------------- @@ -1987,7 +1987,8 @@ namespace seq { 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(m.mk_eq(pow_exp, a.mk_int(0)), eq.m_dep)); + 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)); } nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), nullptr, eq.m_dep); e->add_subst(s); @@ -2103,7 +2104,8 @@ 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(m.mk_eq(pow_exp, zero), eq.m_dep)); + 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)); } return true; } @@ -2249,13 +2251,14 @@ namespace seq { for (unsigned j = 1; j < i; ++j) { prefix_sn = dir_concat(m_sg, prefix_sn, char_toks[j], fwd); } - euf::snode* replacement = dir_concat(m_sg, prefix_sn, - get_tail(var_node, compute_length_expr(prefix_sn).get(), fwd), fwd); + euf::snode* tail = get_tail(var_node, compute_length_expr(prefix_sn).get(), fwd); + euf::snode* replacement = dir_concat(m_sg, prefix_sn, tail, fwd); nielsen_subst s(var_node, replacement, mk_rewrite(a.mk_sub(compute_length_expr(var_node), compute_length_expr(prefix_sn))), eq.m_dep); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); + e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(tail), a.mk_int(0)), eq.m_dep)); e->add_subst(s); child->apply_subst(m_sg, s); return true; @@ -2318,9 +2321,11 @@ namespace seq { child->apply_subst(m_sg, s1); - euf::snode* replacement = dir_concat(m_sg, char_head, get_tail(var_head, a.mk_int(1), fwd), fwd); + euf::snode* tail = get_tail(var_head, a.mk_int(1), fwd); + euf::snode* replacement = dir_concat(m_sg, char_head, tail, fwd); child = mk_child(node); e = mk_edge(node, child, false); + e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(tail), a.mk_int(0)), eq.m_dep)); const nielsen_subst s2(var_head, replacement, mk_rewrite(a.mk_sub(compute_length_expr(var_head), a.mk_int(1))), eq.m_dep); e->add_subst(s2); child->apply_subst(m_sg, s2); @@ -3086,8 +3091,10 @@ 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(m.mk_eq(exp_n, zero), eq->m_dep)); + 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)); + } // Branch 2 (explored second): n >= 1 → peel one u: replace u^n with u · u^(n-1) // Side constraint: n >= 1 @@ -3946,7 +3953,7 @@ namespace seq { nielsen_node *child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); for (const auto f : cs) { - e->add_side_constraint(constraint(f, mem.m_dep, false, m)); + e->add_side_constraint(constraint(f, mem.m_dep, m)); } for (str_mem &cm : child->str_mems()) { if (cm == mem) { @@ -4190,7 +4197,8 @@ namespace seq { const nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, eq->m_dep); e->add_subst(s); child->apply_subst(m_sg, s); - e->add_side_constraint(mk_constraint(m.mk_eq(exp_n, zero), eq->m_dep)); + 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)); } // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1) @@ -4233,7 +4241,8 @@ 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(m.mk_eq(exp_n, zero), mem->m_dep)); + 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)); } // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1) @@ -4322,9 +4331,9 @@ namespace seq { return expr_ref(a.mk_add(left, right), m); } - euf::snode *length_term = nullptr; - if (m_length_info.find(n->id(), length_term) && length_term) - return expr_ref(length_term->get_expr(), m); + //euf::snode *length_term = nullptr; + //if (m_length_info.find(n->id(), length_term) && length_term) + // return expr_ref(length_term->get_expr(), m); return expr_ref(m_seq.str.mk_length(n->get_expr()), m); } @@ -4432,18 +4441,18 @@ namespace seq { expr_ref nielsen_graph::get_or_create_gpower_n_var(euf::snode* var) { SASSERT(var && var->is_var()); - unsigned mc = 0; - m_mod_cnt.find(var->id(), mc); + //unsigned mc = 0; + //m_mod_cnt.find(var->id(), mc); th_rewriter rw(m); - return m_sk.mk("gpn!", var->get_expr(), a.mk_int(mc), a.mk_int()); + return m_sk.mk("gpn!", var->get_expr()/*, a.mk_int(mc)*/, a.mk_int()); } expr_ref nielsen_graph::get_or_create_gpower_m_var(euf::snode* var) { SASSERT(var && var->is_var()); - unsigned mc = 0; - m_mod_cnt.find(var->id(), mc); + //unsigned mc = 0; + //m_mod_cnt.find(var->id(), mc); th_rewriter rw(m); - return m_sk.mk("gpm!", var->get_expr(), a.mk_int(mc), a.mk_int()); + return m_sk.mk("gpm!", var->get_expr()/*, a.mk_int(mc)*/, a.mk_int()); } void nielsen_graph::add_subst_length_constraints(nielsen_edge* e) { @@ -4467,7 +4476,7 @@ namespace seq { 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, true)); + 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. @@ -4479,7 +4488,8 @@ namespace seq { 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(m.mk_eq(lhs, rhs), s.m_dep, true)); + 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 @@ -4498,15 +4508,15 @@ namespace seq { 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); + //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); } } @@ -4515,18 +4525,18 @@ namespace seq { 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); + //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); } } @@ -4551,6 +4561,7 @@ namespace seq { // std::endl; if (lit != sat::null_literal) { node->set_external_conflict(lit, c.dep); + std::cout << "External conflict: " << mk_pp(c.fml, m) << " with literal " << lit << std::endl; return; } assert_to_subsolver(c); @@ -4576,7 +4587,9 @@ 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, true)); + //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)); // non-negativity for each variable (mod-count-aware) euf::snode_vector tokens; @@ -4586,7 +4599,7 @@ namespace seq { if (tok->is_var() && !seen_vars.contains(tok->id())) { seen_vars.insert(tok->id()); expr_ref len_var = compute_length_expr(tok); - node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep, true)); + node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep)); } } } @@ -4602,9 +4615,9 @@ namespace seq { expr_ref len_str = compute_length_expr(mem.m_str); if (min_len > 0) - node->add_constraint(mk_constraint(a.mk_ge(len_str, a.mk_int(min_len)), mem.m_dep, true)); + node->add_constraint(mk_constraint(a.mk_ge(len_str, a.mk_int(min_len)), mem.m_dep)); if (max_len < UINT_MAX) - node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep, true)); + node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep)); } } @@ -4665,14 +4678,14 @@ namespace seq { dep = m_length_solver.core(); m_length_solver.pop(1); if (result == l_false) { - n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, false, m)); + n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, m)); return true; } return false; } - constraint nielsen_graph::mk_constraint(expr* fml, dep_tracker const& dep, bool internal) const { - return constraint(fml, dep, internal, m); + constraint nielsen_graph::mk_constraint(expr *fml, dep_tracker const &dep) const { + return constraint(fml, dep, m); } expr* nielsen_graph::get_power_exponent(euf::snode* power) { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 9323428be..d216ec259 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -499,7 +499,6 @@ namespace seq { struct constraint { expr_ref fml; // the formula (eq, le, or ge, unit-diseq expression) dep_tracker dep; // tracks which input constraints contributed - bool internal; // don't push back to the outer solver (helpful if not necessary and it would reveal internal variables) static expr_ref simplify(expr* f, ast_manager& m) { //th_rewriter th(m); @@ -509,10 +508,10 @@ namespace seq { } constraint(ast_manager& m): - fml(m), dep(nullptr), internal(true) {} + fml(m), dep(nullptr) {} - constraint(expr* f, dep_tracker const& d, const bool internal, ast_manager& m): - fml(simplify(f, m)), dep(d), internal(internal) {} + constraint(expr* f, dep_tracker const& d, ast_manager& m): + fml(simplify(f, m)), dep(d) {} std::ostream& display(std::ostream& out) const; }; @@ -529,14 +528,13 @@ namespace seq { expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1) dep_tracker m_dep; // tracks which input constraints contributed length_kind m_kind; // determines propagation strategy - bool m_internal; - length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg), m_internal(true) {} + length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {} length_constraint(expr* e, dep_tracker const& dep, length_kind kind, const bool internal, ast_manager& m): - m_expr(e, m), m_dep(dep), m_kind(kind), m_internal(internal) {} + m_expr(e, m), m_dep(dep), m_kind(kind) {} constraint to_constraint() const { - return constraint(m_expr, m_dep, m_internal, m_expr.get_manager()); + return constraint(m_expr, m_dep, m_expr.get_manager()); } }; @@ -879,9 +877,8 @@ namespace seq { // Maps each variable to its current length term - - ptr_vector m_length_trail; - u_map m_length_info; + // ptr_vector m_length_trail; + // u_map m_length_info; u_map m_mod_cnt; // Arena for dep_tracker nodes. Declared mutable so that const methods @@ -1307,7 +1304,7 @@ namespace seq { bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep); // create an integer constraint: lhs rhs - constraint mk_constraint(expr* fml, dep_tracker const& dep, bool internal = false) const; + constraint mk_constraint(expr *fml, dep_tracker const &dep) const; // get the exponent expression from a power snode (arg(1)) static expr * get_power_exponent(euf::snode* power); diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 944870023..137fc5ed7 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -130,6 +130,23 @@ namespace seq { return result; } + std::string decode_recursive_name(expr* e, ast_manager& m) { + SASSERT(e && is_app(e)); + th_rewriter rw(m); + const skolem sk(m, rw); + expr* arg = e, *l, *r; + unsigned cnt = 0; + while (sk.is_slice(arg, arg, l, r)) { + cnt++; + } + if (to_app(arg)->get_num_args() != 0) + return ""; + std::string s = dot_html_escape(to_app(arg)->get_decl()->get_name().str()); + if (cnt == 0) + return s; + return s + "[" + std::to_string(cnt) + "]"; + } + static std::string code_to_str(unsigned code) { if (code >= 32 && code < 127 && code != '"' && code != '\\') { return std::string(reinterpret_cast(&code), 1); @@ -217,8 +234,10 @@ namespace seq { return r; } if (seq.str.is_length(e, x)) { - if (to_app(x)->get_num_args() == 0) - return "|" + dot_html_escape(to_app(x)->get_decl()->get_name().str()) + "|"; + std::string name = decode_recursive_name(x, m); + if (!name.empty()) { + return "|" + name + "|"; + } if (names.contains(x)) { return "|" + names[x] + "|"; } @@ -387,17 +406,6 @@ namespace seq { return dot_html_escape(os.str()); } - std::string decode_recursive_name(expr* e, ast_manager& m) { - SASSERT(e && is_app(e)); - th_rewriter rw(m); - const skolem sk(m, rw); - expr* arg = e, *l, *r; - while (sk.is_slice(arg, arg, l, r)) { } - if (to_app(arg)->get_num_args() != 0) - return ""; - return dot_html_escape(to_app(arg)->get_decl()->get_name().str()); - } - // Helper: render a snode as an HTML label for DOT output. // Groups consecutive s_char tokens into quoted strings, renders s_var by name, // shows s_power with superscripts, s_unit by its inner expression, @@ -539,8 +547,7 @@ namespace seq { // integer constraints std::vector int_constraints; for (auto const& ic : m_constraints) { - int_constraints.push_back( - (ic.internal ? "[I] " : "") + constraint_html(ic, names, next_id, m)); + int_constraints.push_back(constraint_html(ic, names, next_id, m)); } if (!int_constraints.empty()) { // eliminate duplicates diff --git a/src/smt/seq/seq_parikh.cpp b/src/smt/seq/seq_parikh.cpp index 57184426c..383d82180 100644 --- a/src/smt/seq/seq_parikh.cpp +++ b/src/smt/seq/seq_parikh.cpp @@ -210,11 +210,11 @@ namespace seq { expr_ref stride_expr(a.mk_int(stride), m); expr_ref stride_k(a.mk_mul(stride_expr, k_var), m); expr_ref rhs(a.mk_add(min_expr, stride_k), m); - out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, false, m)); + out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, m)); // Constraint 2: k ≥ 0 expr_ref zero(a.mk_int(0), m); - out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, false, m)); + out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, m)); // Constraint 3 (optional): k ≤ max_k when max_len is bounded. // max_k = floor((max_len - min_len) / stride) @@ -226,7 +226,7 @@ namespace seq { unsigned range = max_len - min_len; unsigned max_k = range / stride; expr_ref max_k_expr(a.mk_int(max_k), m); - out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, false, m)); + out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, m)); } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index dbf0c14de..2556dd39e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1912,6 +1912,7 @@ namespace smt { if (!is_pos) l.neg(); TRACE(decide, tout << "case split " << l << "\n" << "activity: " << get_activity(var) << "\n";); + std::cout << "Deciding " << mk_pp(literal2expr(l), m) << std::endl; assign(l, b_justification::mk_axiom(), true); return true; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index d1d8342b4..44253032c 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -850,11 +850,8 @@ namespace smt { //std::cout << "Nielsen assumptions:\n"; bool all_sat = true; ctx.push_trail(reset_vector(m_nielsen_literals)); - for (auto const& c : m_nielsen.sat_node()->constraints()) { - if (c.internal) { - std::cout << "Skipping internall assumption: "<< mk_pp(c.fml, m) << std::endl; - continue; - } + for (auto it = m_nielsen.sat_node()->constraints().rbegin(); it != m_nielsen.sat_node()->constraints().rend(); ++it) { + const auto& c = *it; std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; auto lit = mk_literal(c.fml); m_nielsen_literals.push_back(lit); @@ -883,7 +880,7 @@ namespace smt { ctx.push_trail(value_trail(m_context_solver.m_should_internalize)); m_context_solver.m_should_internalize = true; break; - } + } // use assumptions to bound search // "propagate(m_assumption_lit, lit)"; // to force the phase of lit to be true or force a conflict } diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index c4547ceb0..87c80073c 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -3388,14 +3388,14 @@ static void add_len_ge(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::sno ast_manager& m = ng.get_manager(); arith_util arith(m); expr_ref len(ng.seq().str.mk_length(var->get_expr()), m); - node->add_constraint(seq::constraint(arith.mk_ge(len, arith.mk_int(lb)), dep, false, m)); + node->add_constraint(seq::constraint(arith.mk_ge(len, arith.mk_int(lb)), dep, m)); } static void add_len_le(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::snode* var, unsigned ub, seq::dep_tracker dep) { ast_manager& m = ng.get_manager(); arith_util arith(m); expr_ref len(ng.seq().str.mk_length(var->get_expr()), m); - node->add_constraint(seq::constraint(arith.mk_le(len, arith.mk_int(ub)), dep, false, m)); + node->add_constraint(seq::constraint(arith.mk_le(len, arith.mk_int(ub)), dep, m)); } static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) {