mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

Implement ensure_digit_axiom in theory_nseq (#9075)

Browse source 
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>
This commit is contained in:
Copilot 2026-03-20 19:46:22 -07:00 • committed by GitHub
parent f518faac9b
commit 2ab53072e9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_nseq.cpp
View file

@ -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<bool>(m_digits_initialized));
m_digits_initialized = true;
}
};
std::function<void(expr *)> mark_no_diseq = [&](expr *e) {
m_no_diseq_set.insert(e);

1
src/smt/theory_nseq.h
View file

@ -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<expr, euf::snode*> m_expr2snode;