From 77d86343d0db161b24688ab2cbfbd0559810edbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2026 13:30:44 -0700 Subject: [PATCH] add the false literal callback Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 20 +++++++++++++++++--- src/smt/seq/seq_nielsen.h | 15 ++++++++++++--- src/smt/theory_nseq.cpp | 14 ++++++++++++++ 3 files changed, 43 insertions(+), 6 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index d53dae4a9..7fe30138f 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -244,6 +244,15 @@ namespace seq { return false; } + void nielsen_node::add_constraint(constraint const &c) { + m_constraints.push_back(c); + if (m_graph.m_literal_if_false) { + auto lit = m_graph.m_literal_if_false(c.fml); + if (lit != sat::null_literal) + m_conflict_literal = lit; + } + } + void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { SASSERT(s.m_var); for (auto &eq : m_str_eq) { @@ -304,6 +313,7 @@ namespace seq { return m_graph.m_solver.lower_bound(e, lo); } + bool nielsen_node::upper_bound(expr* e, rational& up) const { SASSERT(e); return m_graph.m_solver.upper_bound(e, up); @@ -365,8 +375,8 @@ namespace seq { // nielsen_graph // ----------------------------------------------- - nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver): - m(sg.get_manager()), + nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver): + m(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_solver(solver), @@ -504,7 +514,7 @@ namespace seq { if (e) seq.str.is_power(e, pow_base, pow_exp); if (pow_exp) { expr* zero = arith.mk_numeral(rational(0), true); - m_constraints.push_back( + add_constraint( constraint(m.mk_eq(pow_exp, zero), dep, m)); } nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep); @@ -3452,6 +3462,10 @@ namespace seq { continue; if (!n->is_currently_conflict()) continue; + if (n->m_conflict_literal != sat::null_literal) { + deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_literal)); + continue; + } for (str_eq const& eq : n->str_eqs()) deps = m_dep_mgr.mk_join(deps, eq.m_dep); for (str_mem const& mem : n->str_mems()) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 9f320e189..e24e8e5bc 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -473,7 +473,6 @@ namespace seq { std::ostream& display(std::ostream& out) const; }; - // edge in the Nielsen graph connecting two nodes // mirrors ZIPT's NielsenEdge class nielsen_edge { @@ -525,6 +524,7 @@ namespace seq { vector m_str_eq; // string equalities vector m_str_mem; // regex memberships vector m_constraints; // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe) + sat::literal m_conflict_literal = sat::null_literal; // character constraints (mirrors ZIPT's DisEqualities and CharRanges) @@ -577,10 +577,10 @@ namespace seq { void add_str_eq(str_eq const& eq) { m_str_eq.push_back(eq); } void add_str_mem(str_mem const& mem) { m_str_mem.push_back(mem); } - void add_constraint(constraint const& ic) { m_constraints.push_back(ic); } + void add_constraint(constraint const &ic); vector const& constraints() const { return m_constraints; } - vector& constraints() { return m_constraints; } + vector& constraints() { return m_constraints; } // Query current bounds for a variable from the arithmetic subsolver. // Falls der Subsolver keinen Bound liefert, werden konservative Defaults @@ -622,6 +622,7 @@ namespace seq { bool is_currently_conflict() const { return m_is_general_conflict || + m_conflict_literal != sat::null_literal || (m_reason != backtrack_reason::unevaluated && m_is_extended); } @@ -753,6 +754,10 @@ namespace seq { // inclusion, derivatives. Allocated in the constructor; owned by this graph. seq::seq_regex* m_seq_regex = nullptr; + // Callback to check that literals assumed in branches are not already assigned to false. + // returns the literal that is assigned to false, otherwise returns a null_literal + std::function m_literal_if_false; + // ----------------------------------------------- // Modification counter for substitution length tracking. // mirrors ZIPT's LocalInfo.CurrentModificationCnt @@ -786,6 +791,10 @@ namespace seq { nielsen_graph(euf::sgraph& sg, simple_solver& solver); ~nielsen_graph(); + void set_literal_if_false(std::function const& lif) { + m_literal_if_false = lif; + } + ast_manager &get_manager() { return m; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index f6d81bec1..039bdf4ba 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -80,6 +80,20 @@ namespace smt { m_axioms.set_phase(set_phase); m_axioms.set_ensure_digits(ensure_digit_axiom); m_axioms.set_mark_no_diseq(mark_no_diseq); + + std::function literal_if_false = [&](expr* e) { + bool is_not = m.is_not(e, e); + if (!ctx.e_internalized(e)) + return sat::null_literal; + literal lit = ctx.get_literal(e); + if (is_not) + lit.neg(); + if (ctx.get_assignment(lit) == l_false) + return lit; + return sat::null_literal; + }; + + m_nielsen.set_literal_if_false(literal_if_false); } // -----------------------------------------------------------------------