mirror of
https://github.com/Z3Prover/z3
synced 2026-04-07 05:02:48 +00:00
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>
This commit is contained in:
copilot-swe-agent[bot]
parent
8f90ae01a6
commit
f12ee63ff5
1 changed files with 56 additions and 77 deletions
|
|
@ -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_<varname>_<mod_count>
|
||||
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) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue