From e74b235d8734d480d6b0f991ce8c692c07ab1979 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 27 May 2026 17:25:39 +0200 Subject: [PATCH] Solve disequalities lazily --- src/params/smt_params.cpp | 2 + src/params/smt_params.h | 1 + src/params/smt_params_helper.pyg | 1 + src/smt/nseq_context_solver.h | 11 +- src/smt/seq/seq_nielsen.cpp | 215 +++++++++++++++++++++++++++++++ src/smt/seq/seq_nielsen.h | 57 +++++++- src/smt/seq/seq_nielsen_pp.cpp | 10 ++ src/smt/seq/seq_state.h | 6 + src/smt/theory_nseq.cpp | 46 +++++-- src/smt/theory_nseq.h | 4 +- 10 files changed, 337 insertions(+), 16 deletions(-) diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index 8d3112d4f..bc16cb674 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -59,6 +59,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_nseq_regex_precheck = p.nseq_regex_precheck(); m_nseq_regex_factorization_threshold = p.nseq_regex_factorization_threshold(); m_nseq_signature = p.nseq_signature(); + m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq(); m_up_persist_clauses = p.up_persist_clauses(); validate_string_solver(m_string_solver); if (_p.get_bool("arith.greatest_error_pivot", false)) @@ -173,6 +174,7 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nseq_parikh); DISPLAY_PARAM(m_nseq_regex_precheck); DISPLAY_PARAM(m_nseq_regex_factorization_threshold); + DISPLAY_PARAM(m_nseq_axiomatize_diseq); DISPLAY_PARAM(m_profile_res_sub); DISPLAY_PARAM(m_display_bool_var2expr); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 6c3806a02..bd22cbb09 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -254,6 +254,7 @@ struct smt_params : public preprocessor_params, bool m_nseq_regex_precheck = true; unsigned m_nseq_regex_factorization_threshold = 1; bool m_nseq_signature = false; + bool m_nseq_axiomatize_diseq = false; smt_params(params_ref const & p = params_ref()): m_string_solver(symbol("auto")){ diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 01042deed..dd143974c 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -131,6 +131,7 @@ def_module_params(module_name='smt', ('nseq.regex_precheck', BOOL, True, 'enable regex membership pre-check before DFS in theory_nseq: checks intersection emptiness per-variable and short-circuits SAT/UNSAT for regex-only problems'), ('nseq.regex_factorization_threshold', UINT, 1, 'maximum number of cases to factor a classical regex into in a single step (gives completeness on classical regexes)'), ('nseq.signature', BOOL, False, 'enable heuristic signature-based string equation splitting in Nielsen solver'), + ('nseq.axiomatize_diseq', BOOL, False, 'eagerly axiomatize sequence disequalities'), ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'), ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index b704dcf84..ba4fb091a 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -148,13 +148,20 @@ namespace smt { class context_solver : public seq::context_solver_i { smt::context &ctx; arith_value m_arith_value; + std::function m_add_diseq_axiom; public: - context_solver(smt::context& ctx): + context_solver(smt::context& ctx, std::function add_diseq_axiom = nullptr): ctx(ctx), - m_arith_value(ctx.get_manager()) { + m_arith_value(ctx.get_manager()), + m_add_diseq_axiom(add_diseq_axiom) { m_arith_value.init(&ctx); } + void add_diseq_axiom(expr* e1, expr* e2) override { + if (m_add_diseq_axiom) + m_add_diseq_axiom(e1, e2); + } + bool lower_bound(expr *e, rational &lo, literal_vector &lits, enode_pair_vector &eqs) const override { bool is_strict = true; return m_arith_value.get_lo(e, lo, is_strict, lits, eqs) && !is_strict && lo.is_int(); diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index ea5763879..5d7c5166e 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -233,10 +233,12 @@ namespace seq { void nielsen_node::clone_from(nielsen_node const& parent) { m_str_eq.reset(); + m_str_deq.reset(); m_str_mem.reset(); m_constraints.reset(); m_char_ranges.reset(); m_str_eq.append(parent.m_str_eq); + m_str_deq.append(parent.m_str_deq); m_str_mem.append(parent.m_str_mem); m_constraints.append(parent.m_constraints); @@ -248,6 +250,7 @@ namespace seq { m_regex_occurrence = parent.m_regex_occurrence; SASSERT(m_str_eq.size() == parent.m_str_eq.size()); + SASSERT(m_str_deq.size() == parent.m_str_deq.size()); SASSERT(m_str_mem.size() == parent.m_str_mem.size()); SASSERT(m_constraints.size() == parent.m_constraints.size()); } @@ -271,6 +274,12 @@ namespace seq { m_str_eq.push_back(eq); } + void nielsen_node::add_str_deq(str_deq const& deq) { + SASSERT(deq.m_lhs != nullptr); + SASSERT(deq.m_rhs != nullptr); + m_str_deq.push_back(deq); + } + void nielsen_node::add_str_mem(str_mem const& mem) { SASSERT(mem.m_str != nullptr); SASSERT(mem.m_regex != nullptr); @@ -327,6 +336,7 @@ namespace seq { } m_constraints.push_back(c); } + euf::snode *nielsen_graph::mk_fresh_char_var() {} void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { SASSERT(!s.m_var->is_char_or_unit() || s.m_replacement->is_char_or_unit()); @@ -343,6 +353,17 @@ namespace seq { } } + for (auto &deq : m_str_deq) { + const auto new_lhs = sg.subst(deq.m_lhs, s.m_var, s.m_replacement); + const auto new_rhs = sg.subst(deq.m_rhs, s.m_var, s.m_replacement); + if (new_lhs != deq.m_lhs || new_rhs != deq.m_rhs) { + deq.m_lhs = new_lhs; + deq.m_rhs = new_rhs; + deq.m_dep = m_graph.dep_mgr().mk_join(deq.m_dep, s.m_dep); + deq.sort(); + } + } + for (auto &mem : m_str_mem) { const auto new_str = sg.subst(mem.m_str, s.m_var, s.m_replacement); const auto new_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement); @@ -479,6 +500,20 @@ namespace seq { m_root->add_str_eq(eq); } + void nielsen_graph::add_str_deq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) { + if (!root()) + create_root(); + const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); + str_deq deq(lhs, rhs, dep); + // check if root node contains this equation already + if (std::ranges::any_of(m_root->str_deqs(), [&](const str_deq& e) { + return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; + })) + // already present, no need to add again + return; + m_root->add_str_deq(deq); + } + void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) { if (!root()) create_root(); @@ -502,6 +537,14 @@ namespace seq { m_root->add_str_eq(eq); } + void nielsen_graph::add_str_deq(euf::snode* lhs, euf::snode* rhs) { + if (!root()) + create_root(); + const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); + str_deq deq(lhs, rhs, dep); + m_root->add_str_deq(deq); + } + void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) { if (!root()) create_root(); @@ -1240,6 +1283,109 @@ namespace seq { changed = true; } + auto cannot_be_empty = [&](euf::snode* side) { + euf::snode_vector tokens; + side->collect_tokens(tokens); + const bool has_char = std::ranges::any_of(tokens, [](euf::snode* t){ return t->is_char(); }); + const bool all_eliminable = std::ranges::all_of(tokens, [](euf::snode* t){ + return t->is_var() || t->is_power(); + }); + return has_char || !all_eliminable; + }; + + unsigned wk = 0; + for (unsigned k = 0; k < m_str_deq.size(); ++k) { + str_deq& deq = m_str_deq[k]; + + if (deq.m_lhs == deq.m_rhs || (deq.m_lhs && deq.m_rhs && deq.m_lhs->is_empty() && deq.m_rhs->is_empty())) { + set_general_conflict(); + set_conflict(backtrack_reason::symbol_clash, deq.m_dep); + return simplify_result::conflict; + } + + if (deq.m_lhs->is_empty() && !deq.m_rhs->is_empty()) { + if (cannot_be_empty(deq.m_rhs)) continue; + } + else if (deq.m_rhs->is_empty() && !deq.m_lhs->is_empty()) { + if (cannot_be_empty(deq.m_lhs)) continue; + } + + // simplify constant-exponent powers + dep_tracker lhs_pow_dep = nullptr; + if (euf::snode* s = simplify_const_powers(this, sg, deq.m_lhs, lhs_pow_dep)) { + deq.m_lhs = s; + deq.m_dep = m_graph.dep_mgr().mk_join(deq.m_dep, lhs_pow_dep); + changed = true; + } + dep_tracker rhs_pow_dep = nullptr; + if (euf::snode* s = simplify_const_powers(this, sg, deq.m_rhs, rhs_pow_dep)) { + deq.m_rhs = s; + deq.m_dep = m_graph.dep_mgr().mk_join(deq.m_dep, rhs_pow_dep); + changed = true; + } + + // prefix/suffix cancellation + { + euf::snode_vector lhs_toks, rhs_toks; + deq.m_lhs->collect_tokens(lhs_toks); + deq.m_rhs->collect_tokens(rhs_toks); + + unsigned prefix = 0; + while (prefix < lhs_toks.size() && prefix < rhs_toks.size()) { + euf::snode* lt = lhs_toks[prefix]; + euf::snode* rt = rhs_toks[prefix]; + if (m.are_equal(lt->get_expr(), rt->get_expr())) { + ++prefix; + } + else if (sg.are_unit_distinct(lt, rt)) { + prefix = static_cast(-1); + break; + } + else + break; + } + if (prefix == static_cast(-1)) { + continue; + } + + unsigned lsz = lhs_toks.size(), rsz = rhs_toks.size(); + unsigned suffix = 0; + while (suffix < lsz - prefix && suffix < rsz - prefix) { + euf::snode* lt = lhs_toks[lsz - 1 - suffix]; + euf::snode* rt = rhs_toks[rsz - 1 - suffix]; + if (m.are_equal(lt->get_expr(), rt->get_expr())) { + ++suffix; + } else if (sg.are_unit_distinct(lt, rt)) { + suffix = static_cast(-1); + break; + } + else + break; + } + if (suffix == static_cast(-1)) { + continue; + } + + if (prefix > 0 || suffix > 0) { + deq.m_lhs = sg.drop_left(sg.drop_right(deq.m_lhs, suffix), prefix); + deq.m_rhs = sg.drop_left(sg.drop_right(deq.m_rhs, suffix), prefix); + changed = true; + } + } + + if (deq.m_lhs == deq.m_rhs || (deq.m_lhs->is_empty() && deq.m_rhs->is_empty())) { + set_general_conflict(); + set_conflict(backtrack_reason::symbol_clash, deq.m_dep); + return simplify_result::conflict; + } + + m_str_deq[wk++] = deq; + } + if (wk < m_str_deq.size()) { + m_str_deq.shrink(wk); + changed = true; + } + // pass 2: detect symbol clashes, empty-propagation, and prefix cancellation for (str_eq& eq : m_str_eq) { SASSERT(eq.well_formed()); @@ -1627,6 +1773,8 @@ namespace seq { } bool nielsen_node::is_satisfied() const { + if (!m_str_deq.empty()) + return false; if (any_of(m_str_eq, [](auto const &eq) { return !eq.is_trivial(); })) return false; if (any_of(m_str_mem, [this](auto const &m) { return !m.is_trivial(this) && !m.is_primitive();})) @@ -2761,6 +2909,10 @@ namespace seq { if (apply_var_num_unwinding_mem(node)) return ++m_stats.m_mod_var_num_unwinding_mem, true; + // let's unwindind a disequality + if (axiomatize_diseq(node)) + return ++m_stats.m_ax_diseq, true; + return false; } @@ -4272,6 +4424,68 @@ namespace seq { return true; } + // Cf. axioms::diseq_axiom + bool nielsen_graph::axiomatize_diseq(nielsen_node* node) { + SASSERT(node->m_str_eq.empty() && + std::ranges::all_of(node->m_str_mem, [](str_mem const& mem){ return mem.is_primitive(); })); + + if (node->m_str_deq.empty()) + return false; + + const str_deq& first = node->m_str_deq.back(); + euf::snode* u = first.m_lhs; + euf::snode* v = first.m_rhs; + + const expr_ref u_len(compute_length_expr(u), m); + const expr_ref v_len(compute_length_expr(v), m); + expr_ref len_eq(m.mk_eq(u_len, v_len), m); + str_eq eq_uv(u, v, first.m_dep); + sort *char_sort = nullptr; + VERIFY(seq().is_seq(u->get_sort(), char_sort)); + euf::snode* a = m_sg.mk(seq().str.mk_unit(m_sk.mk("diseq.a", u->get_expr(), v->get_expr(), char_sort).get())); + euf::snode* b = m_sg.mk(seq().str.mk_unit(m_sk.mk("diseq.b", u->get_expr(), v->get_expr(), char_sort).get())); + euf::snode* w = m_sg.mk(m_sk.mk("diseq.w", u->get_expr(), v->get_expr()).get()); + euf::snode* up = m_sg.mk(m_sk.mk("diseq.u'", u->get_expr(), v->get_expr()).get()); + euf::snode* vp = m_sg.mk(m_sk.mk("diseq.v'", u->get_expr(), v->get_expr()).get()); + const expr_ref up_len(compute_length_expr(up), m); + const expr_ref vp_len(compute_length_expr(vp), m); + euf::snode* wau = dir_concat(m_sg, dir_concat(m_sg, w, a, true), up, true); + euf::snode* wbv = dir_concat(m_sg, dir_concat(m_sg, w, b, true), vp, true); + const str_eq u_eq(u, wau, first.m_dep); + const str_eq v_eq(v, wbv, first.m_dep); + + // Branch 1: |u| < |v| + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + child->m_str_deq.pop_back(); + expr_ref cmp(this->a.mk_le(u_len, v_len), m); + m_rw(cmp); + e->add_side_constraint(constraint(cmp, first.m_dep, m)); + } + // Branch 2: |v| < |u| + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + child->m_str_deq.pop_back(); + expr_ref cmp(this->a.mk_le(v_len, u_len), m); + m_rw(cmp); + e->add_side_constraint(constraint(cmp, first.m_dep, m)); + } + // Branch 3: u = wau' && v = wbv' && |u'| = |v'| && a != b + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + child->m_str_deq.pop_back(); + child->add_str_eq(u_eq); + child->add_str_eq(v_eq); + child->add_constraint(constraint(m.mk_eq(up_len, vp_len), first.m_dep, m)); + e->add_side_constraint(constraint(m.mk_not(m.mk_eq(a->get_expr(), b->get_expr())), first.m_dep, m)); + } + + return true; + } + dep_tracker nielsen_graph::collect_conflict_deps() const { dep_tracker deps = nullptr; // todo: Add visit set if the graph could contain cycles in the future @@ -4822,6 +5036,7 @@ namespace seq { st.update("nseq mod var nielsen", m_stats.m_mod_var_nielsen); st.update("nseq mod var num unwind (eq)", m_stats.m_mod_var_num_unwinding_eq); st.update("nseq mod var num unwind (mem)", m_stats.m_mod_var_num_unwinding_mem); + st.update("nseq mod axiomatized disequalities", m_stats.m_ax_diseq); } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index e8630f5ee..9c7f2cced 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -369,6 +369,7 @@ namespace seq { virtual sat::literal literal_if_false(expr* e) { return sat::null_literal; } + virtual void add_diseq_axiom(expr* e1, expr* e2) {} }; @@ -418,6 +419,46 @@ namespace seq { return out << mk_pp(p.eq.m_lhs->get_expr(), p.m) << " == " << mk_pp(p.eq.m_rhs->get_expr(), p.m) << "\n"; } + // string disequality constraint: lhs != rhs + struct str_deq { + euf::snode* m_lhs; + euf::snode* m_rhs; + dep_tracker m_dep; + + str_deq(euf::snode* lhs, euf::snode* rhs, dep_tracker const& dep): + m_lhs(lhs), m_rhs(rhs), m_dep(dep) { + SASSERT(well_formed()); + } + + bool operator==(str_deq const& other) const { + return m_lhs == other.m_lhs && m_rhs == other.m_rhs; + } + + void sort() { + if (m_lhs->id() > m_rhs->id()) { + std::swap(m_lhs, m_rhs); + } + } + + bool contains_var(euf::snode* var) const { + return m_lhs->collect_tokens().contains(var) || m_rhs->collect_tokens().contains(var); + } + + bool well_formed() const { + return !!m_lhs && !!m_rhs; + } + }; + + struct deq_pp { + str_deq const &deq; + ast_manager &m; + deq_pp(str_deq const &e, ast_manager &m) : deq(e), m(m) {} + }; + + inline std::ostream &operator<<(std::ostream &out, deq_pp const &p) { + return out << mk_pp(p.deq.m_lhs->get_expr(), p.m) << " != " << mk_pp(p.deq.m_rhs->get_expr(), p.m) << "\n"; + } + // regex membership constraint: str in regex // mirrors ZIPT's StrMem struct str_mem { @@ -560,7 +601,11 @@ namespace seq { vector const& subst() const { return m_subst; } void add_subst(nielsen_subst const& s); - void add_side_constraint(constraint const& ic) { m_side_constraints.push_back(ic); } + void add_side_constraint(constraint const& ic) { + if (ic.fml.m().is_true(ic.fml)) + return; + m_side_constraints.push_back(ic); + } vector const& side_constraints() const { return m_side_constraints; } bool is_progress() const { return m_is_progress; } @@ -583,12 +628,12 @@ namespace seq { // constraints at this node vector m_str_eq; // string equalities + vector m_str_deq; // string disequalities vector m_str_mem; // regex memberships vector m_constraints; // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe) sat::literal m_conflict_external_literal = sat::null_literal; dep_tracker m_conflict_internal = nullptr; - // character constraints (mirrors ZIPT's DisEqualities and CharRanges) // key: snode id of the s_unit symbolic character u_map> m_char_ranges; // ?c in [lo, hi) @@ -629,10 +674,13 @@ namespace seq { // constraint access vector const& str_eqs() const { return m_str_eq; } vector& str_eqs() { return m_str_eq; } + vector const& str_deqs() const { return m_str_deq; } + vector& str_deqs() { return m_str_deq; } vector const& str_mems() const { return m_str_mem; } vector& str_mems() { return m_str_mem; } void add_str_eq(str_eq const& eq); + void add_str_deq(str_deq const& deq); void add_str_mem(str_mem const& mem); void add_constraint(constraint const &ic); @@ -793,6 +841,7 @@ namespace seq { unsigned m_mod_var_nielsen = 0; unsigned m_mod_var_num_unwinding_eq = 0; unsigned m_mod_var_num_unwinding_mem = 0; + unsigned m_ax_diseq = 0; void reset() { memset(this, 0, sizeof(nielsen_stats)); } }; @@ -969,10 +1018,12 @@ namespace seq { // add constraints to the root node from external solver void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r); + void add_str_deq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r); void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l); // test-friendly overloads (no external dependency tracking) void add_str_eq(euf::snode* lhs, euf::snode* rhs); + void add_str_deq(euf::snode* lhs, euf::snode* rhs); void add_str_mem(euf::snode* str, euf::snode* regex); // access all nodes @@ -1269,6 +1320,8 @@ namespace seq { bool apply_var_num_unwinding_mem(nielsen_node* node); + bool axiomatize_diseq(nielsen_node* node); + // find the first power token in any str_eq at this node static euf::snode* find_power_token(nielsen_node* node); diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 56ad10fc0..937388cbe 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -516,6 +516,7 @@ namespace seq { std::ostream& nielsen_node::to_html(std::ostream& out, obj_map& names, uint64_t& next_id, ast_manager& m) const { bool any = false; bool hasEq = false; + bool hasDisEq = false; bool hasMem = false; bool hasRange = false; @@ -528,6 +529,15 @@ namespace seq { << snode_label_html(eq.m_rhs, names, next_id, m) << "
"; } + // string disequalities + for (auto const& eq : m_str_deq) { + if (!any) { out << "Cnstr:
"; any = true; } + if (!hasDisEq) { out << "DisEq:
"; hasDisEq = true; } + out << snode_label_html(eq.m_lhs, names, next_id, m) + << " ≠ " + << snode_label_html(eq.m_rhs, names, next_id, m) + << "
"; + } // regex memberships for (auto const& mem : m_str_mem) { if (!any) { out << "Cnstr:
"; any = true; } diff --git a/src/smt/seq/seq_state.h b/src/smt/seq/seq_state.h index 2a29ced8f..263f994ba 100644 --- a/src/smt/seq/seq_state.h +++ b/src/smt/seq/seq_state.h @@ -33,6 +33,12 @@ namespace smt { : str_eq(lhs, rhs, dep), m_l(l), m_r(r) {} }; + struct tracked_str_deq : seq::str_deq { + enode *m_l, *m_r; + tracked_str_deq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep) + : str_deq(lhs, rhs, dep), m_l(l), m_r(r) {} + }; + struct tracked_str_mem : seq::str_mem { sat::literal lit; tracked_str_mem(euf::snode *str, euf::snode *regex, sat::literal lit, seq::dep_tracker const &dep) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index b9c8a5b56..49ba7d7df 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -36,7 +36,7 @@ namespace smt { m_egraph(m), m_sgraph(m, m_egraph), m_length_solver(m), - m_context_solver(ctx), + m_context_solver(ctx, [this](expr* e1, expr* e2) { m_axioms.diseq_axiom(e1, e2); }), m_nielsen(m_sgraph, m_length_solver, m_context_solver), m_axioms(m_th_rewriter), m_regex(m_sgraph), @@ -262,8 +262,19 @@ namespace smt { break; } } - else if (m_seq.is_seq(e1) && !m_no_diseq_set.contains(e1) && !m_no_diseq_set.contains(e2)) - m_axioms.diseq_axiom(e1, e2); + else if (m_seq.is_seq(e1) && !m_no_diseq_set.contains(e1) && !m_no_diseq_set.contains(e2)) { + if (get_fparams().m_nseq_axiomatize_diseq) + m_axioms.diseq_axiom(e1, e2); + else { + euf::snode *s1 = get_snode(e1); + euf::snode *s2 = get_snode(e2); + seq::dep_tracker dep = nullptr; + ctx.push_trail(restore_vector(m_prop_queue)); + m_prop_queue.push_back(deq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); + m_last_constraint_added = ctx.get_scope_level(); + m_can_hot_restart = false; + } + } else ; } @@ -408,6 +419,8 @@ namespace smt { auto const& item = m_prop_queue[m_prop_qhead++]; if (std::holds_alternative(item)) propagate_eq(std::get(item)); + else if (std::holds_alternative(item)) + propagate_deq(std::get(item)); else if (std::holds_alternative(item)) propagate_pos_mem(std::get(item)); else if (std::holds_alternative(item)) @@ -432,6 +445,11 @@ namespace smt { ensure_length_var(eq.m_r->get_expr()); } + void theory_nseq::propagate_deq(tracked_str_deq const& eq) { + ensure_length_var(eq.m_l->get_expr()); + ensure_length_var(eq.m_r->get_expr()); + } + void theory_nseq::propagate_pos_mem(tracked_str_mem const& mem) { SASSERT(mem.well_formed()); @@ -587,7 +605,7 @@ namespace smt { m_nielsen.reset(); m_can_hot_restart = true; - unsigned num_eqs = 0, num_mems = 0; + unsigned num_eqs = 0, num_deqs = 0, num_mems = 0; // transfer string equalities and regex memberships from prop_queue to nielsen graph root for (auto const& item : m_prop_queue) { @@ -596,6 +614,12 @@ namespace smt { m_nielsen.add_str_eq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r); ++num_eqs; } + if (std::holds_alternative(item)) { + SASSERT(!get_fparams().m_nseq_axiomatize_diseq); + auto const& eq = std::get(item); + m_nielsen.add_str_deq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r); + ++num_deqs; + } else if (std::holds_alternative(item)) { auto const& mem = std::get(item); int triv = m_regex.check_trivial(mem); @@ -626,7 +650,7 @@ namespace smt { } TRACE(seq, tout << "nseq populate: " << num_eqs << " eqs, " - << num_mems << " mems -> nielsen root\n"); + << num_deqs << " diseqs, " << num_mems << " mems -> nielsen root\n"); IF_VERBOSE(1, verbose_stream() << "nseq final_check: populating graph with " << num_eqs << " eqs, " << num_mems << " mems\n";); } @@ -641,12 +665,12 @@ namespace smt { } // Check if there are any eq/mem items in the propagation queue. - bool has_eq_or_mem = any_of(m_prop_queue, [](auto const &item) { - return std::holds_alternative(item) || std::holds_alternative(item); + bool has_eq_or_diseq_or_mem = any_of(m_prop_queue, [](auto const &item) { + return std::holds_alternative(item) || 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()) { + if (!has_eq_or_diseq_or_mem && m_ho_terms.empty() && !has_unhandled_preds()) { if (!check_stoi_coherence()) { TRACE(seq, tout << "nseq final_check: stoi coherence added axioms, FC_CONTINUE\n"); return FC_CONTINUE; @@ -665,7 +689,7 @@ namespace smt { return FC_CONTINUE; } - if (!has_eq_or_mem && !has_unhandled_preds()) { + if (!has_eq_or_diseq_or_mem && !has_unhandled_preds()) { if (!check_stoi_coherence()) { TRACE(seq, tout << "nseq final_check: stoi coherence added axioms, FC_CONTINUE\n"); return FC_CONTINUE; @@ -678,7 +702,7 @@ namespace smt { return FC_DONE; } - if (!has_eq_or_mem && has_unhandled_preds()) { + if (!has_eq_or_diseq_or_mem && has_unhandled_preds()) { TRACE(seq, tout << "nielsen root if null\n"); // this can happen for regex constraint only benchmarks // qf_s\20250410-matching\wildcard-matching-regex-67.smt2 @@ -803,7 +827,7 @@ namespace smt { TRACE(seq, tout << "nseq final_check: solve SAT, sat_node=" << (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 + SASSERT(has_eq_or_diseq_or_mem); // we should have axiomatized them bool all_sat = add_nielsen_assumptions(); diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 785d92d21..c23ebebee 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -53,10 +53,11 @@ namespace smt { // propagation queue items (variant over the distinct propagation cases) using eq_item = tracked_str_eq; // string equality + using deq_item = tracked_str_deq; // string disequality using mem_item = tracked_str_mem; // regex membership struct axiom_item { expr* e; }; // structural axiom for term e - using prop_item = std::variant; + using prop_item = std::variant; vector m_prop_queue; unsigned m_prop_qhead = 0; @@ -142,6 +143,7 @@ namespace smt { // propagation dispatch helpers void propagate_eq(tracked_str_eq const& eq); + void propagate_deq(tracked_str_deq const& deq); void propagate_pos_mem(tracked_str_mem const& mem); void enqueue_axiom(expr* e); void dequeue_axiom(expr* e);