From f12ee63ff5bbca3451b81903e6fd9c7aaa1a6402 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 1 Apr 2026 03:47:31 +0000 Subject: [PATCH] remove arith aliases, reference a directly in nielsen_graph methods Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/a6a64bf1-86fc-41bc-a245-2f67656d5f63 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/seq_nielsen.cpp | 133 +++++++++++++++--------------------- 1 file changed, 56 insertions(+), 77 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 3d7751024..a4175a44f 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -321,9 +321,8 @@ namespace seq { bool nielsen_node::upper_bound(expr* e, rational& up) const { SASSERT(e); - arith_util& arith = m_graph.a; rational v; - if (arith.is_numeral(e, v)) { + if (m_graph.a.is_numeral(e, v)) { up = v; return true; } @@ -516,7 +515,6 @@ namespace seq { return true; } ast_manager& m = sg.get_manager(); - arith_util& arith = m_graph.a; seq_util& seq = sg.get_seq_util(); for (euf::snode* t : tokens) { if (t->is_var()) { @@ -530,7 +528,7 @@ namespace seq { expr* pow_base = nullptr, *pow_exp = nullptr; if (e) seq.str.is_power(e, pow_base, pow_exp); if (pow_exp) { - expr* zero = arith.mk_int(0); + expr* zero = m_graph.a.mk_int(0); add_constraint( constraint(m.mk_eq(pow_exp, zero), dep, m)); } @@ -821,7 +819,6 @@ namespace seq { euf::sgraph& sg = m_graph.sg(); ast_manager& m = sg.get_manager(); - arith_util& arith = m_graph.a; seq_util& seq = this->graph().seq(); bool changed = true; @@ -978,7 +975,7 @@ namespace seq { expr_ref norm_count = normalize_arith(m, count); bool pow_le_count = false, count_le_pow = false; rational diff; - if (get_const_power_diff(norm_count, pow_exp, arith, diff)) { + if (get_const_power_diff(norm_count, pow_exp, m_graph.a, diff)) { count_le_pow = diff.is_nonpos(); pow_le_count = diff.is_nonneg(); } @@ -997,13 +994,13 @@ namespace seq { } else if (pow_le_count) { // pow <= count: remainder goes to other_side - expr_ref rem = normalize_arith(m, arith.mk_sub(norm_count, pow_exp)); + expr_ref rem = normalize_arith(m, m_graph.a.mk_sub(norm_count, pow_exp)); expr_ref pw(seq.str.mk_power(base_e, rem), m); other_side = dir_concat(sg, sg.mk(pw), other_side, fwd); } else { // count <= pow: remainder goes to pow_side - expr_ref rem = normalize_arith(m, arith.mk_sub(pow_exp, norm_count)); + expr_ref rem = normalize_arith(m, m_graph.a.mk_sub(pow_exp, norm_count)); expr_ref pw(seq.str.mk_power(base_e, rem), m); pow_side = dir_concat(sg, sg.mk(pw), pow_side, fwd); } @@ -1039,19 +1036,19 @@ namespace seq { expr* lp = get_power_exp_expr(lh, seq); expr* rp = get_power_exp_expr(rh, seq); rational diff; - if (lp && rp && get_const_power_diff(rp, lp, arith, diff)) { + if (lp && rp && get_const_power_diff(rp, lp, m_graph.a, diff)) { // rp = lp + diff (constant difference) eq.m_lhs = dir_drop(sg, eq.m_lhs, 1, fwd); eq.m_rhs = dir_drop(sg, eq.m_rhs, 1, fwd); if (diff.is_pos()) { // rp > lp: put base^diff on RHS (direction-aware prepend/append) - expr_ref de(arith.mk_int(diff), m); + expr_ref de(m_graph.a.mk_int(diff), m); expr_ref pw(seq.str.mk_power(lb, de), m); eq.m_rhs = dir_concat(sg, sg.mk(pw), eq.m_rhs, fwd); } else if (diff.is_neg()) { // lp > rp: put base^(-diff) on LHS - expr_ref de(arith.mk_int(-diff), m); + expr_ref de(m_graph.a.mk_int(-diff), m); expr_ref pw(seq.str.mk_power(lb, de), m); eq.m_lhs = dir_concat(sg, sg.mk(pw), eq.m_lhs, fwd); } @@ -1074,9 +1071,9 @@ namespace seq { else { // we only know for sure that one is smaller than the other expr_ref d(m_graph.mk_fresh_int_var()); - expr_ref zero_e(arith.mk_int(0), m); - expr_ref d_plus_smaller(arith.mk_add(d, smaller_exp), m); - add_constraint(m_graph.mk_constraint(arith.mk_ge(d, zero_e), eq.m_dep)); + expr_ref zero_e(m_graph.a.mk_int(0), m); + expr_ref d_plus_smaller(m_graph.a.mk_add(d, smaller_exp), m); + add_constraint(m_graph.mk_constraint(m_graph.a.mk_ge(d, zero_e), eq.m_dep)); add_constraint(m_graph.mk_constraint(m.mk_eq(d_plus_smaller, larger_exp), eq.m_dep)); expr_ref pw(seq.str.mk_power(lb, d), m); euf::snode*& larger_side = lp_le_rp ? eq.m_rhs : eq.m_lhs; @@ -1512,7 +1509,6 @@ namespace seq { // pretty much all of them could cause divergence! // e.g., x \in aa* => don't apply substitution x / ax even though it looks "safe" to do // there might be another constraint x \in a* and they would just push the "a" back and forth! - arith_util& arith = a; for (unsigned eq_idx = 0; eq_idx < node->str_eqs().size(); ++eq_idx) { str_eq const& eq = node->str_eqs()[eq_idx]; @@ -1627,7 +1623,7 @@ namespace seq { child->apply_subst(m_sg, s); expr* pow_exp = get_power_exp_expr(pow_head, m_seq); if (pow_exp) { - expr *zero = arith.mk_int(0); + expr *zero = a.mk_int(0); e->add_side_constraint(mk_constraint(m.mk_eq(pow_exp, zero), eq.m_dep)); } return true; @@ -2090,7 +2086,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_eq_split(nielsen_node* node) { - arith_util& arith = a; for (unsigned eq_idx = 0; eq_idx < node->str_eqs().size(); ++eq_idx) { str_eq const& eq = node->str_eqs()[eq_idx]; @@ -2129,7 +2124,7 @@ namespace seq { euf::snode* pad = nullptr; if (padding != 0) { - expr *pad_var = skolem(m, rw).mk("eq-split", arith.mk_int(padding), eq.m_lhs->get_expr(), + expr *pad_var = skolem(m, rw).mk("eq-split", a.mk_int(padding), eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), eq.m_lhs->get_sort()); pad = m_sg.mk(pad_var); if (padding > 0) { @@ -2161,7 +2156,7 @@ namespace seq { // 1) len(pad) = |padding| (if padding variable was created) if (pad && pad->get_expr()) { expr_ref len_pad(m_seq.str.mk_length(pad->get_expr()), m); - expr_ref abs_pad(arith.mk_int(std::abs(padding)), m); + expr_ref abs_pad(a.mk_int(std::abs(padding)), m); e->add_side_constraint(mk_constraint(m.mk_eq(len_pad, abs_pad), eq.m_dep)); } // 2) len(eq1_lhs) = len(eq1_rhs) @@ -2458,7 +2453,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_num_cmp(nielsen_node* node) { - arith_util& arith = a; // Look for two directional endpoint power tokens with the same base. for (str_eq const& eq : node->str_eqs()) { @@ -2493,14 +2487,14 @@ namespace seq { { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - expr_ref n_plus_1(arith.mk_add(exp_n, arith.mk_int(1)), m); - e->add_side_constraint(mk_constraint(arith.mk_ge(exp_m, n_plus_1), eq.m_dep)); + expr_ref n_plus_1(a.mk_add(exp_n, a.mk_int(1)), m); + e->add_side_constraint(mk_constraint(a.mk_ge(exp_m, n_plus_1), eq.m_dep)); } // Branch 2 (explored second): m <= n (add constraint p ≥ c) { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, exp_m), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, exp_m), eq.m_dep)); } return true; } @@ -2521,7 +2515,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_split_power_elim(nielsen_node* node) { - arith_util& arith = a; seq_util& seq = this->seq(); for (str_eq const& eq : node->str_eqs()) { @@ -2555,21 +2548,21 @@ namespace seq { // Skip if ordering is already deterministic — simplify_and_init // pass 3c should have handled it. rational diff; - if (get_const_power_diff(norm_count, pow_exp, arith, diff)) + if (get_const_power_diff(norm_count, pow_exp, a, diff)) continue; // Branch 1: pow_exp < count (i.e., count >= pow_exp + 1) { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - expr_ref pow_plus1(arith.mk_add(pow_exp, arith.mk_int(1)), m); - e->add_side_constraint(mk_constraint(arith.mk_ge(norm_count, pow_plus1), eq.m_dep)); + expr_ref pow_plus1(a.mk_add(pow_exp, a.mk_int(1)), m); + e->add_side_constraint(mk_constraint(a.mk_ge(norm_count, pow_plus1), eq.m_dep)); } // Branch 2: count <= pow_exp (i.e., pow_exp >= count) { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - e->add_side_constraint(mk_constraint(arith.mk_ge(pow_exp, norm_count), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(pow_exp, norm_count), eq.m_dep)); } return true; } @@ -2587,7 +2580,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_const_num_unwinding(nielsen_node* node) { - arith_util& arith = a; euf::snode *power = nullptr; euf::snode *other_head = nullptr; @@ -2599,8 +2591,8 @@ namespace seq { SASSERT(power->is_power() && power->num_args() >= 1); euf::snode *base = power->arg(0); expr *exp_n = get_power_exponent(power); - expr *zero = arith.mk_int(0); - expr *one = arith.mk_int(1); + expr *zero = a.mk_int(0); + expr *one = a.mk_int(1); // Branch 1 (explored first): n = 0 → replace power with ε (progress) // Side constraint: n = 0 @@ -2623,7 +2615,7 @@ namespace seq { expr *power_e = power->get_expr(); SASSERT(power_e); expr *base_expr = to_app(power_e)->get_arg(0); - expr_ref n_minus_1 = normalize_arith(m, arith.mk_sub(exp_n, one)); + expr_ref n_minus_1 = normalize_arith(m, a.mk_sub(exp_n, one)); expr_ref nested_pow(seq.str.mk_power(base_expr, n_minus_1), m); euf::snode* nested_power_snode = m_sg.mk(nested_pow); @@ -2634,7 +2626,7 @@ namespace seq { e->add_subst(s2); child->apply_subst(m_sg, s2); if (exp_n) - e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, one), eq->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), eq->m_dep)); return true; } @@ -2824,7 +2816,6 @@ namespace seq { bool nielsen_graph::fire_gpower_intro( nielsen_node* node, str_eq const& eq, euf::snode* var, euf::snode_vector const& ground_prefix_orig, bool fwd) { - arith_util& arith = a; // Compress repeated patterns in the ground prefix (mirrors ZIPT's LcpCompressionFull). // E.g., [a,b,a,b] has minimal period 2 → use [a,b] as the power base. @@ -2894,7 +2885,7 @@ namespace seq { if (!power_snode) return false; - expr_ref zero(arith.mk_int(0), m); + expr_ref zero(a.mk_int(0), m); // Generate children mirroring ZIPT's GetDecompose: // P(t0 · t1 · ... · t_{k-1}) = P(t0) | t0·P(t1) | ... | t0·...·t_{k-2}·P(t_{k-1}) @@ -2946,15 +2937,15 @@ namespace seq { child->apply_subst(m_sg, s); // Side constraint: n >= 0 - e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_n, zero), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(fresh_n, zero), eq.m_dep)); // Side constraints for fresh partial exponent if (fresh_m.get()) { expr* inner_exp = get_power_exponent(tok); // m' >= 0 - e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_m, zero), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(fresh_m, zero), eq.m_dep)); // m' <= inner_exp - e->add_side_constraint(mk_constraint(arith.mk_ge(inner_exp, fresh_m), eq.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(inner_exp, fresh_m), eq.m_dep)); } } @@ -3310,7 +3301,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_power_split(nielsen_node* node) { - arith_util& arith = a; euf::snode* power = nullptr; euf::snode* var_head = nullptr; @@ -3321,7 +3311,7 @@ namespace seq { SASSERT(power->is_power() && power->num_args() >= 1); euf::snode* base = power->arg(0); - expr* zero = arith.mk_int(0); + expr* zero = a.mk_int(0); // Branch 1: enumerate all decompositions of the base. // x = base^m · prefix_i(base) where 0 <= m < n @@ -3386,15 +3376,15 @@ namespace seq { child->apply_subst(m_sg, s); // Side constraint: n >= 0 - e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_m, zero), eq->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(fresh_m, zero), eq->m_dep)); // Side constraints for fresh partial exponent if (fresh_inner_m.get()) { expr* inner_exp = get_power_exponent(tok); // m' >= 0 - e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_inner_m, zero), eq->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(fresh_inner_m, zero), eq->m_dep)); // m' <= inner_exp - e->add_side_constraint(mk_constraint(arith.mk_ge(inner_exp, fresh_inner_m), eq->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(inner_exp, fresh_inner_m), eq->m_dep)); } } } @@ -3423,7 +3413,6 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_var_num_unwinding_eq(nielsen_node* node) { - arith_util& arith = a; euf::snode* power = nullptr; euf::snode* var_head = nullptr; @@ -3435,8 +3424,8 @@ namespace seq { SASSERT(power->is_power() && power->num_args() >= 1); euf::snode* base = power->arg(0); expr* exp_n = get_power_exponent(power); - expr_ref zero(arith.mk_int(0), m); - expr_ref one(arith.mk_int(1), m); + expr_ref zero(a.mk_int(0), m); + expr_ref one(a.mk_int(1), m); // Branch 1: n = 0 → replace u^n with ε (progress) // Side constraint: n = 0 @@ -3461,14 +3450,13 @@ namespace seq { e->add_subst(s); child->apply_subst(m_sg, s); if (exp_n) - e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, one), eq->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), eq->m_dep)); } return true; } bool nielsen_graph::apply_var_num_unwinding_mem(nielsen_node* node) { - arith_util& arith = a; euf::snode* power = nullptr; str_mem const* mem = nullptr; @@ -3479,8 +3467,8 @@ namespace seq { SASSERT(power->is_power() && power->num_args() >= 1); euf::snode* base = power->arg(0); expr* exp_n = get_power_exponent(power); - expr_ref zero(arith.mk_int(0), m); - expr_ref one(arith.mk_int(1), m); + expr_ref zero(a.mk_int(0), m); + expr_ref one(a.mk_int(1), m); // Branch 1: n = 0 → replace u^n with ε (progress) // Side constraint: n = 0 @@ -3505,7 +3493,7 @@ namespace seq { e->add_subst(s); child->apply_subst(m_sg, s); if (exp_n) - e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, one), mem->m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), mem->m_dep)); } return true; @@ -3552,18 +3540,17 @@ namespace seq { // ----------------------------------------------------------------------- expr_ref nielsen_graph::compute_length_expr(euf::snode* n) { - arith_util& arith = a; if (n->is_empty()) - return expr_ref(arith.mk_int(0), m); + return expr_ref(a.mk_int(0), m); if (n->is_char_or_unit()) - return expr_ref(arith.mk_int(1), m); + return expr_ref(a.mk_int(1), m); if (n->is_concat()) { expr_ref left = compute_length_expr(n->arg(0)); expr_ref right = compute_length_expr(n->arg(1)); - return expr_ref(arith.mk_add(left, right), m); + return expr_ref(a.mk_add(left, right), m); } // For variables: consult modification counter. @@ -3586,7 +3573,6 @@ namespace seq { uint_set seen_vars; seq_util& seq = m_sg.get_seq_util(); - arith_util& arith = a; for (str_eq const& eq : m_root->str_eqs()) { if (eq.is_trivial()) continue; @@ -3606,7 +3592,7 @@ namespace seq { if (tok->is_var() && !seen_vars.contains(tok->id())) { seen_vars.insert(tok->id()); expr_ref len_var(seq.str.mk_length(tok->get_expr()), m); - expr_ref ge_zero(arith.mk_ge(len_var, arith.mk_int(0)), m); + expr_ref ge_zero(a.mk_ge(len_var, a.mk_int(0)), m); constraints.push_back(length_constraint(ge_zero, eq.m_dep, length_kind::nonneg, m)); } } @@ -3625,13 +3611,13 @@ namespace seq { // generate len(str) >= min_len when min_len > 0 if (min_len > 0) { - expr_ref bound(arith.mk_ge(len_str, arith.mk_int(min_len)), m); + expr_ref bound(a.mk_ge(len_str, a.mk_int(min_len)), m); constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, m)); } // generate len(str) <= max_len when bounded if (max_len < UINT_MAX) { - expr_ref bound(arith.mk_le(len_str, arith.mk_int(max_len)), m); + expr_ref bound(a.mk_le(len_str, a.mk_int(max_len)), m); constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, m)); } } @@ -3682,9 +3668,8 @@ namespace seq { return expr_ref(it->second, m); // Create a fresh integer variable: len__ - arith_util& arith = a; std::string name = "len!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - expr_ref fresh(m.mk_fresh_const(name.c_str(), arith.mk_int()), m); + expr_ref fresh(m.mk_fresh_const(name.c_str(), a.mk_int()), m); m_len_vars.push_back(fresh); m_len_var_cache.insert({key, fresh.get()}); return fresh; @@ -3715,9 +3700,8 @@ namespace seq { if (it != m_gpower_n_var_cache.end()) return expr_ref(it->second, m); - arith_util& arith = a; std::string name = "gpn!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - expr_ref fresh(m.mk_fresh_const(name.c_str(), arith.mk_int()), m); + expr_ref fresh(m.mk_fresh_const(name.c_str(), a.mk_int()), m); m_gpower_vars.push_back(fresh); m_gpower_n_var_cache.insert({key, fresh.get()}); return fresh; @@ -3731,9 +3715,8 @@ namespace seq { if (it != m_gpower_m_var_cache.end()) return expr_ref(it->second, m); - arith_util& arith = a; std::string name = "gpm!" + std::to_string(var->id()) + "!" + std::to_string(mod_count); - expr_ref fresh(m.mk_fresh_const(name.c_str(), arith.mk_int()), m); + expr_ref fresh(m.mk_fresh_const(name.c_str(), a.mk_int()), m); m_gpower_vars.push_back(fresh); m_gpower_m_var_cache.insert({key, fresh.get()}); return fresh; @@ -3743,7 +3726,6 @@ namespace seq { auto const& substs = e->subst(); bool has_non_elim = false; - arith_util& arith = a; // Step 1: Compute LHS (|x|) for each non-eliminating substitution // using current m_mod_cnt (before bumping). @@ -3761,7 +3743,7 @@ namespace seq { 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)); + e->add_side_constraint(mk_constraint(a.mk_ge(lhs, a.mk_int(0)), s.m_dep)); } if (has_non_elim) { @@ -3847,7 +3829,6 @@ namespace seq { if (node == m_root) return; - arith_util& arith = a; uint_set seen_vars; for (str_eq const& eq : node->str_eqs()) { @@ -3866,7 +3847,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(arith.mk_ge(len_var, arith.mk_int(0)), eq.m_dep)); + node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep)); } } } @@ -3883,9 +3864,9 @@ namespace seq { expr_ref len_str = compute_length_expr(mem.m_str); if (min_len > 0) - node->add_constraint(mk_constraint(arith.mk_ge(len_str, arith.mk_int(min_len)), mem.m_dep)); + 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(arith.mk_le(len_str, arith.mk_int(max_len)), mem.m_dep)); + node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep)); } } @@ -3915,16 +3896,15 @@ namespace seq { // fall through - ask the solver [expensive] // TODO: Maybe cache the result? - arith_util& arith = a; // The solver already holds all path constraints incrementally. // Temporarily add NOT(lhs <= rhs), i.e. lhs >= rhs + 1. // If that is unsat, then lhs <= rhs is entailed. - expr_ref one(arith.mk_int(1), m); - expr_ref rhs_plus_one(arith.mk_add(rhs, one), m); + expr_ref one(a.mk_int(1), m); + expr_ref rhs_plus_one(a.mk_add(rhs, one), m); m_solver.push(); - m_solver.assert_expr(arith.mk_ge(lhs, rhs_plus_one)); + m_solver.assert_expr(a.mk_ge(lhs, rhs_plus_one)); lbool result = m_solver.check(); m_solver.pop(1); return result == l_false; @@ -3944,9 +3924,8 @@ namespace seq { } expr_ref nielsen_graph::mk_fresh_int_var() { - arith_util& arith = a; std::string name = "n!" + std::to_string(m_fresh_cnt++); - return expr_ref(m.mk_fresh_const(name.c_str(), arith.mk_int()), m); + return expr_ref(m.mk_fresh_const(name.c_str(), a.mk_int()), m); } bool nielsen_graph::solve_sat_path_raw(model_ref& mdl) {