mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

Port propagate_eq from theory_seq for sk().is_eq in theory_nseq (#9165)

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7c0a330f-3f9f-4c5d-99f2-47fad013538f

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-03-29 15:44:18 -07:00 • committed by GitHub
parent 3db734d249
commit 09cde1f80c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_nseq.cpp
View file

@ -278,7 +278,17 @@ namespace smt {
// axioms added via relevant_eh → dequeue_axiom // axioms added via relevant_eh → dequeue_axiom
} }
else if (m_axioms.sk().is_eq(e, a, b) && is_true) { else if (m_axioms.sk().is_eq(e, a, b) && is_true) {
// TODO: port propagate_eq from theory_seq. enode* n1 = ensure_enode(a);
enode* n2 = ensure_enode(b);
if (n1->get_root() != n2->get_root()) {
literal lit(v, false);
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
justification* js = ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx, 1, &lit, 0, nullptr, n1, n2));
ctx.assign_eq(n1, n2, eq_justification(js));
}
} }
else if (m_seq.is_skolem(e) || else if (m_seq.is_skolem(e) ||
m_seq.str.is_nth_i(e) || m_seq.str.is_nth_i(e) ||