From 2ab53072e9f2f105f0b065b156954635048c2aa9 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 20 Mar 2026 19:46:22 -0700 Subject: [PATCH] Implement ensure_digit_axiom in theory_nseq (#9075) Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/9b679ca3-dba7-469c-907a-9abd5edf1e1d Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/theory_nseq.cpp | 13 +++++++++++-- src/smt/theory_nseq.h | 1 + 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index b1854be09..c73eec720 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -60,8 +60,17 @@ namespace smt { literal lit = mk_literal(e); ctx.force_phase(lit); }; - std::function < void(void)> ensure_digit_axiom = [&]() { - throw default_exception("digit axioms should be added lazily via seq_axioms::ensure_digit_axiom"); + std::function < void(void)> ensure_digit_axiom = [this, add_clause]() { + if (!m_digits_initialized) { + for (unsigned i = 0; i < 10; ++i) { + expr_ref cnst(m_seq.mk_char('0' + i), m); + expr_ref_vector clause(m); + clause.push_back(m.mk_eq(m_axioms.sk().mk_digit2int(cnst), m_autil.mk_int(i))); + add_clause(clause); + } + get_context().push_trail(value_trail(m_digits_initialized)); + m_digits_initialized = true; + } }; std::function mark_no_diseq = [&](expr *e) { m_no_diseq_set.insert(e); diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index efcd1f672..338c00eaf 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -68,6 +68,7 @@ namespace smt { unsigned m_num_conflicts = 0; unsigned m_num_final_checks = 0; unsigned m_num_length_axioms = 0; + bool m_digits_initialized = false; // map from context enode to private sgraph snode obj_map m_expr2snode;