mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-05 01:45:15 +00:00
Code Activity

Guard mod constraint: skip for period <= 1

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-10 20:14:53 +00:00
parent 2bae0f02c4
commit 334e6da60d
1 changed files with 19 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_seq_len.cpp
View file

@ -331,7 +331,7 @@ namespace smt {
// Semi-linear: lengths are {base + k * period : k >= 0} // Semi-linear: lengths are {base + k * period : k >= 0}
// Assert: // Assert:
// (s in R) => |s| >= base // (s in R) => |s| >= base
// (s in R) => |s| mod period = base mod period // (s in R) => |s| mod period = base mod period (only when period >= 2)
// |s| >= base // |s| >= base
expr_ref ge_base(m_autil.mk_ge(len, m_autil.mk_int(base)), m); expr_ref ge_base(m_autil.mk_ge(len, m_autil.mk_int(base)), m);
@ -347,22 +347,26 @@ namespace smt {
} }
// |s| mod period = base mod period // |s| mod period = base mod period
expr_ref mod_len(m_autil.mk_mod(len, m_autil.mk_int(period)), m); // Skip when period <= 1: period == 0 is already handled above;
expr_ref eq_mod(m.mk_eq(mod_len, m_autil.mk_int(base % period)), m); // period == 1 makes the constraint trivially true (n mod 1 = 0).
if (!ctx.b_internalized(eq_mod)) if (period >= 2) {
ctx.internalize(eq_mod, true); expr_ref mod_len(m_autil.mk_mod(len, m_autil.mk_int(period)), m);
literal eq_mod_lit = ctx.get_literal(eq_mod); expr_ref eq_mod(m.mk_eq(mod_len, m_autil.mk_int(base % period)), m);
ctx.mark_as_relevant(eq_mod_lit); if (!ctx.b_internalized(eq_mod))
{ ctx.internalize(eq_mod, true);
literal_vector lits; literal eq_mod_lit = ctx.get_literal(eq_mod);
lits.push_back(~lit); ctx.mark_as_relevant(eq_mod_lit);
lits.push_back(eq_mod_lit); {
assert_axiom(lits); literal_vector lits;
lits.push_back(~lit);
lits.push_back(eq_mod_lit);
assert_axiom(lits);
}
} }
TRACE(seq, tout << "seq_len: (s in R) => |s| >= " << base << " && |s| mod " TRACE(seq, tout << "seq_len: (s in R) => |s| >= " << base
<< period << " = " << (base % period) << " for s=" << mk_pp(s, m) << (period >= 2 ? " && |s| mod " + std::to_string(period) + " = " + std::to_string(base % period) : "")
<< " r=" << mk_pp(r, m) << "\n";); << " for s=" << mk_pp(s, m) << " r=" << mk_pp(r, m) << "\n";);
} }
} }