From 3db734d249e96d2af29fff8cbf790ecff87beb73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Mar 2026 15:19:36 -0700 Subject: [PATCH] add note about propagate-eq Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 6 ++--- src/smt/theory_nseq.cpp | 45 +++++++++++++++++++++++++++++-------- 2 files changed, 39 insertions(+), 12 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 0d803a563..417b0948b 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -533,7 +533,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_numeral(rational(0), true); + expr* zero = arith.mk_int(0); add_constraint( constraint(m.mk_eq(pow_exp, zero), dep, m)); } @@ -553,7 +553,7 @@ namespace seq { // Check if exponent b equals exponent a + diff for some rational constant diff. // Uses syntactic matching on Z3 expression structure: pointer equality // detects shared sub-expressions created during ConstNumUnwinding. - // + // static bool get_const_power_diff(expr* b, expr* a, arith_util& arith, rational& diff) { if (a == b) { diff = rational(0); return true; } expr* x = nullptr, *y = nullptr; @@ -1692,7 +1692,7 @@ namespace seq { child->apply_subst(m_sg, s); expr* pow_exp = get_power_exp_expr(pow_head, seq); if (pow_exp) { - expr* zero = arith.mk_numeral(rational(0), true); + expr *zero = arith.mk_int(0); e->add_side_constraint(mk_constraint(m.mk_eq(pow_exp, zero), eq.m_dep)); } return true; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 7bbc63b66..0a7fa3e22 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -233,7 +233,7 @@ namespace smt { void theory_nseq::assign_eh(bool_var v, bool is_true) { expr* e = ctx.bool_var2expr(v); // std::cout << "assigned " << mk_pp(e, m) << " = " << is_true << std::endl; - expr* s = nullptr, *re = nullptr; + expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr; TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";); if (m_seq.str.is_in_re(e, s, re)) { euf::snode* sn_str = get_snode(s); @@ -277,6 +277,9 @@ namespace smt { else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { // axioms added via relevant_eh → dequeue_axiom } + else if (m_axioms.sk().is_eq(e, a, b) && is_true) { + // TODO: port propagate_eq from theory_seq. + } else if (m_seq.is_skolem(e) || m_seq.str.is_nth_i(e) || m_seq.str.is_nth_u(e) || @@ -506,9 +509,9 @@ namespace smt { } // Check if there are any eq/mem items in the propagation queue. - bool has_eq_or_mem = false; - for (auto const& item : m_prop_queue) - if (!std::holds_alternative(item)) { has_eq_or_mem = true; break; } + bool has_eq_or_mem = any_of(m_prop_queue, [](auto const &item) { + return std::holds_alternative(item) || std::holds_alternative(item); + }); // there is nothing to do for the string solver, as there are no string constraints if (!has_eq_or_mem && m_ho_terms.empty() && !has_unhandled_preds()) { @@ -516,6 +519,7 @@ namespace smt { m_nielsen.reset(); m_nielsen.create_root(); m_nielsen.set_sat_node(m_nielsen.root()); + TRACE(seq, display(tout << "empty nielsen\n")); return FC_DONE; } @@ -530,6 +534,7 @@ namespace smt { m_nielsen.reset(); m_nielsen.create_root(); m_nielsen.set_sat_node(m_nielsen.root()); + TRACE(seq, display(tout << "empty nielsen\n")); return FC_DONE; } @@ -561,6 +566,7 @@ namespace smt { // all regex constraints satisfiable, no word eqs → SAT IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";); m_nielsen.set_sat_node(m_nielsen.root()); + TRACE(seq, display(tout << "pre-check done\n")); return FC_DONE; default: break; @@ -590,21 +596,23 @@ namespace smt { << (m_nielsen.sat_node() ? "set" : "null") << "\n";); // Nielsen found a consistent assignment for positive constraints. SASSERT(has_eq_or_mem); // we should have axiomatized them - #if 0 - // TODO: add this pending review + if (!add_nielsen_assumptions()) return FC_CONTINUE; - #endif + + CTRACE(seq, !has_unhandled_preds(), display(tout << "done\n")); if (!has_unhandled_preds()) return FC_DONE; } + TRACE(seq, display(tout << "unknown\n")); IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNKNOWN, FC_GIVEUP\n";); return FC_GIVEUP; } bool theory_nseq::add_nielsen_assumptions() { + return true; bool has_undef = false; bool has_false = false; for (auto const& c : m_nielsen.sat_node()->constraints()) { @@ -614,13 +622,13 @@ namespace smt { case l_undef: has_undef = true; ctx.force_phase(lit); - IF_VERBOSE(2, verbose_stream() << + IF_VERBOSE(0, verbose_stream() << "nseq final_check: adding nielsen assumption " << c.fml << "\n";); break; case l_false: // do we really expect this to happen? has_false = true; - IF_VERBOSE(1, verbose_stream() + IF_VERBOSE(0, verbose_stream() << "nseq final_check: nielsen assumption " << c.fml << " is false\n";); ctx.force_phase(lit); break; @@ -629,6 +637,7 @@ namespace smt { if (has_undef) return false; if (has_false) { + IF_VERBOSE(0, verbose_stream() << "has false\n"); // fishy case. return false; } @@ -705,6 +714,24 @@ namespace smt { out << " str_mems: " << num_mems << "\n"; out << " prop_queue: " << m_prop_qhead << "/" << m_prop_queue.size() << "\n"; out << " ho_terms: " << m_ho_terms.size() << "\n"; + for (auto const &item : m_prop_queue) { + if (std::holds_alternative(item)) { + auto const& eq = std::get(item); + out << " eq: " << mk_bounded_pp(eq.m_l->get_expr(), m, 3) + << " = " << mk_bounded_pp(eq.m_r->get_expr(), m, 3) << "\n"; + } + else if (std::holds_alternative(item)) { + auto const& mem = std::get(item); + out << " mem: " << mk_bounded_pp(mem.m_str->get_expr(), m, 3) + << " in " << mk_bounded_pp(mem.m_regex->get_expr(), m, 3) + << " (lit: " << mem.lit << ")\n"; + } + else if (std::holds_alternative(item)) { + auto const& ax = std::get(item); + out << " axiom: " << mk_bounded_pp(ax.e, m, 3) << "\n"; + } + } + m_nielsen.display(out); } // -----------------------------------------------------------------------