mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 01:36:48 +00:00
Code Activity

First attempt to integrate seq_monadic in nseq

Browse source 
Bug with missing rewriting for integer side constraints
This commit is contained in:
CEisenhofer 2026-07-20 18:58:13 +02:00
parent d885580633
commit 45305b64cb
7 changed files with 118 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/smt_params.cpp
View file

@ -65,6 +65,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_nseq_regex_dynamic_decomposition = p.nseq_regex_dynamic_decomposition();
m_nseq_signature = p.nseq_signature();
m_nseq_fine_wilf = p.nseq_fine_wilf();
m_nseq_monadic_split = p.nseq_monadic_split();
m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq();
m_nseq_eager = p.nseq_eager();
m_nseq_harvest = p.nseq_harvest();
@ -186,6 +187,7 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nseq_regex_factorization_eager);
DISPLAY_PARAM(m_nseq_regex_dynamic_decomposition);
DISPLAY_PARAM(m_nseq_fine_wilf);
DISPLAY_PARAM(m_nseq_monadic_split);
DISPLAY_PARAM(m_nseq_axiomatize_diseq);
DISPLAY_PARAM(m_nseq_harvest);

1
src/params/smt_params.h
View file

@ -260,6 +260,7 @@ struct smt_params : public preprocessor_params,
bool m_nseq_regex_dynamic_decomposition = true;
bool m_nseq_signature = false;
bool m_nseq_fine_wilf = false;
bool m_nseq_monadic_split = false;
bool m_nseq_axiomatize_diseq = false;
bool m_nseq_eager = true;
unsigned m_nseq_harvest = 0;

1
src/params/smt_params_helper.pyg
View file

@ -144,6 +144,7 @@ def_module_params(module_name='smt',
('nseq.regex_dynamic_decomposition', BOOL, True, 'decompose cyles detected by unwinding regexes'),
('nseq.signature', BOOL, False, 'enable heuristic signature-based string equation splitting in Nielsen solver'),
('nseq.fine_wilf', BOOL, False, 'enable Fine & Wilf overlap splitting for equations with different-base power heads in the Nielsen solver (breaks the divergent one-copy peel loop)'),
('nseq.monadic_split', BOOL, False, 'enable the continuation-regex intersection modifier (seq_monadic) in the Nielsen solver: closes a node when several memberships on the same sequence have a provably empty language intersection'),
('nseq.axiomatize_diseq', BOOL, False, 'eagerly axiomatize sequence disequalities'),
('nseq.eager', BOOL, True, 'enable the incremental eager structural Nielsen closure during propagation, detecting conflicts before final_check'),
('nseq.harvest', UINT, 0, 'benchmark-harvest mode: bound on non-progress Nielsen extension steps before dumping the current node as an .smt2 benchmark; 0 = disabled (normal sound reasoning). WARNING: intentionally unsound, for benchmark generation only'),

95
src/smt/seq/seq_nielsen.cpp
View file

@ -29,13 +29,12 @@ NSB review:
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_monadic.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/seq_skolem.h"
#include "ast/rewriter/var_subst.h"
#include "util/statistics.h"
#include <algorithm>
#include <cstdlib>
#include <set>
#include <stack>
#include <unordered_map>
#include <vector>
@ -165,7 +164,7 @@ namespace seq {
SASSERT(d);
if (d->is_fail())
continue; // ∇ can't start with c → infeasible split, drop
result[w++] = split_pair(result[i].m_d, d->get_expr(), m);
result[w++] = ::split_pair(result[i].m_d, d->get_expr(), m);
}
result.shrink(w);
}
@ -779,7 +778,7 @@ namespace seq {
m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_a_rw(m),
m_sk(m, m_rw), m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)),
m_seq_regex(alloc(seq::seq_regex, sg)), m_split_rw(sg.get_manager()), m_deriv_rw(sg.get_manager()),
m_partial_dfa_pin(sg.get_manager()) {
m_monadic_rw(sg.get_manager()), m_partial_dfa_pin(sg.get_manager()) {
}
nielsen_graph::~nielsen_graph() {
@ -885,6 +884,10 @@ namespace seq {
dealloc(st);
}
m_rf_states.reset();
// continuation-regex service: release its pinned derivative graph so a
// fresh problem starts with a clean cache (its pins would grow forever).
dealloc(m_monadic);
m_monadic = nullptr;
m_nodes.reset();
m_edges.reset();
m_root = nullptr;
@ -1582,7 +1585,6 @@ namespace seq {
// predicate is not internalized automatically (see the analogous
// gradient propagation in theory_nseq).
expr_ref div(a.mk_divides(a.mk_int(stride), a.mk_sub(len, a.mk_int(min_len))), m);
m_rw(div);
e->add_side_constraint(mk_constraint(div, dep));
}
}
@ -3685,6 +3687,13 @@ namespace seq {
if (!harvest_mode() && apply_regex_factorization(node))
return ++m_stats.m_mod_regex_factorization, true;
// Priority 8a: MonadicSplit - continuation-regex intersection (seq_monadic):
// close the node if several memberships on the same sequence have a
// provably empty language intersection. Sound one-way (conflict only);
// opt-in via smt.nseq.monadic_split. (skipped in benchmark-harvest mode)
if (!harvest_mode() && apply_monadic_split(node))
return ++m_stats.m_mod_monadic_split, true;
// Priority 8b: ConstNielsen - char vs var (2 children)
if (apply_const_nielsen(node))
return ++m_stats.m_mod_const_nielsen, true;
@ -5202,6 +5211,76 @@ namespace seq {
return false;
}
// -----------------------------------------------------------------------
// Modifier: apply_monadic_split (continuation-regex intersection, seq_monadic)
//
// Uses the continuation-regex service in ast/rewriter/seq_monadic.h. Several
// plain memberships s ∈ R_1, …, s ∈ R_k on the SAME left-hand sequence s
// are jointly satisfiable only if L(R_1) ∩ … ∩ L(R_k) ≠ ∅. split_manager
// decides emptiness of that intersection over one shared, globally cached
// Brzozowski-derivative graph, and — unlike apply_regex_factorization, which
// skips primitive memberships (x ∈ R with x a bare variable) — it also fires
// on those, catching groups that are only *jointly* empty.
//
// Only the sound direction is used: seq_monadic::intersect returns l_false
// exactly when the intersection is provably empty (note the convention is the
// OPPOSITE of seq_regex::check_intersection_emptiness, where l_true = empty).
// On l_false the node is a regex conflict. l_true (non-empty) and l_undef
// (STATE_CAP / undecidable nullability) fall through so the ordinary modifiers
// keep driving the node. No witness is consumed (the module's witness
// extraction is not sound yet) and no child is ever created, so this rule can
// never introduce an unsound SAT. Opt-in via smt.nseq.monadic_split.
// -----------------------------------------------------------------------
bool nielsen_graph::apply_monadic_split(nielsen_node* node) {
if (!m_monadic_split)
return false;
auto const& mems = node->str_mems();
const unsigned n = mems.size();
if (n < 2)
return false; // need at least two memberships to form an intersection
if (!m_monadic)
m_monadic = alloc(seq::split_manager, m_monadic_rw);
// Group plain memberships by their (slicing-equal) left-hand sequence and
// test the joint language intersection of each group of size >= 2.
bool_vector done;
done.resize(n, false);
for (unsigned i = 0; i < n; ++i) {
str_mem const& mi = mems[i];
if (done[i] || !mi.is_plain())
continue;
vector<seq::cont_regex> crs;
crs.push_back(m_monadic->embed(mi.m_regex->get_expr()));
dep_tracker dep = mi.m_dep;
done[i] = true;
for (unsigned j = i + 1; j < n; ++j) {
str_mem const& mj = mems[j];
if (done[j] || !mj.is_plain() || !mi.m_str->similar(mj.m_str, m))
continue;
crs.push_back(m_monadic->embed(mj.m_regex->get_expr()));
dep = m_dep_mgr.mk_join(dep, mj.m_dep);
done[j] = true;
}
if (crs.size() < 2)
continue; // no sibling membership on the same sequence
expr_ref_vector wit(m);
const lbool r = m_monadic->intersect(crs, 0, UINT_MAX, wit);
if (r != l_false)
continue; // non-empty (l_true) or undecided (l_undef): no conclusion
TRACE(seq, tout << "monadic split: empty intersection of " << crs.size()
<< " memberships on " << mem_pp(mi) << "\n");
node->set_general_conflict();
node->set_conflict(backtrack_reason::regex, dep);
return true;
}
return false;
}
bool nielsen_graph::fire_gpower_intro(
nielsen_node* node, str_eq const& eq,
euf::snode const* var, euf::snode_vector const& ground_prefix_orig, const bool fwd) {
@ -6372,7 +6451,10 @@ namespace seq {
}
constraint nielsen_graph::mk_constraint(expr *fml, dep_tracker const &dep) const {
return constraint(fml, dep, m);
// we need to rewrite e.g., division or <; otw. the integer solver will cry
expr_ref c(fml, m);
c = normalize_arith(m_rw, c);
return constraint(c, dep, m);
}
expr* nielsen_graph::get_power_exponent(euf::snode const* power) {
@ -6902,6 +6984,7 @@ namespace seq {
st.update("nseq mod view land", m_stats.m_mod_view_land);
st.update("nseq mod gpower intr", m_stats.m_mod_gpower_intr);
st.update("nseq mod regex fact", m_stats.m_mod_regex_factorization);
st.update("nseq mod monadic split", m_stats.m_mod_monadic_split);
st.update("nseq mod const nielsen", m_stats.m_mod_const_nielsen);
st.update("nseq mod signature split", m_stats.m_mod_signature_split);
st.update("nseq mod regex var", m_stats.m_mod_regex_var_split);

22
src/smt/seq/seq_nielsen.h
View file

@ -60,6 +60,7 @@ namespace seq {
class nielsen_graph;
class seq_parikh;
class seq_regex; // forward declaration (defined in smt/seq/seq_regex.h)
class split_manager; // continuation-regex service (defined in ast/rewriter/seq_monadic.h)
std::string snode_label_html(euf::snode const* n,
obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m, bool html_escape);
@ -866,6 +867,7 @@ namespace seq {
unsigned m_mod_view_land = 0;
unsigned m_mod_gpower_intr = 0;
unsigned m_mod_regex_factorization = 0;
unsigned m_mod_monadic_split = 0;
unsigned m_mod_const_nielsen = 0;
unsigned m_mod_regex_var_split = 0;
unsigned m_mod_signature_split = 0;
@ -943,6 +945,7 @@ namespace seq {
bool m_parikh_enabled = true;
bool m_signature_split = false;
bool m_fine_wilf = false;
bool m_monadic_split = false;
unsigned m_regex_factorization_threshold = 1;
bool m_regex_factorization_eager = false;
bool m_regex_dynamic_decomposition = true;
@ -1003,6 +1006,15 @@ namespace seq {
// across calls (a fresh seq_rewriter per consumed character was a
// dominant simplification cost).
seq_rewriter m_deriv_rw;
// Dedicated rewriter backing the continuation-regex service used by
// apply_monadic_split. Kept separate from m_split_rw / m_deriv_rw so its
// derivative caches never interleave with the suspended factorization
// iterators that reference those engines.
seq_rewriter m_monadic_rw;
// Continuation-regex split / intersection service (seq_monadic). Grows a
// shared, globally cached Brzozowski-derivative graph; allocated lazily on
// first use and released in reset().
seq::split_manager* m_monadic = nullptr;
// Owns the suspended factorization continuations (rf_state); nodes hold
// raw pointers into this pool. Freed in reset().
ptr_vector<rf_state> m_rf_states;
@ -1184,7 +1196,9 @@ namespace seq {
void set_signature_split(bool e) { m_signature_split = e; }
void set_fine_wilf(bool e) { m_fine_wilf = e; }
void set_monadic_split(bool e) { m_monadic_split = e; }
void set_regex_factorization_threshold(unsigned max) { m_regex_factorization_threshold = max; }
void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; }
void set_regex_dynamic_decomposition(bool e) { m_regex_dynamic_decomposition = e; }
@ -1668,6 +1682,12 @@ namespace seq {
// disjunction is refuted → the continuation node is a regex conflict.
bool apply_regex_factorization(nielsen_node* node);
// continuation-regex intersection modifier (seq_monadic). Detects a
// provably empty intersection of several plain memberships sharing the
// same left-hand sequence and reports the node as a regex conflict.
// Sound one-way only: never creates a child, never claims SAT.
bool apply_monadic_split(nielsen_node* node);
// Build a suspended factorization (boundary head/tail + split iterator)
// for `mem`. Returns null if the regex shape is unsupported (the engine
// cannot even start a split). Allocated into m_rf_states.

3
src/smt/seq_model.cpp
View file

@ -134,8 +134,6 @@ namespace smt {
return alloc(expr_wrapper_proc, to_app(e));
}
std::cout << mk_pp(n->get_expr(), m) << std::endl;
// For nth_u (underspecified nth): the Nielsen character-peel /
// regex-if-split records the chosen character as a relevant
// equality literal (e.g. (= (seq.nth_u x 0) (_ Char 65))), so the
@ -442,7 +440,6 @@ namespace smt {
if (a.is_numeral(e, val))
return val;
bool has_val = get_arith_value(_e, val);
CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";);
return val;

7
src/smt/theory_nseq.cpp
View file

@ -1020,6 +1020,7 @@ namespace smt {
m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh);
m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
m_nielsen.set_fine_wilf(get_fparams().m_nseq_fine_wilf);
m_nielsen.set_monadic_split(get_fparams().m_nseq_monadic_split);
m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager);
m_nielsen.set_regex_dynamic_decomposition(get_fparams().m_nseq_regex_dynamic_decomposition);
@ -1169,7 +1170,7 @@ namespace smt {
bool all_sat = true;
ctx.push_trail(reset_vector(m_nielsen_literals));
for (const auto& c : m_nielsen.sat_node()->constraints()) {
std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
// std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
auto lit = mk_literal(c.fml);
m_nielsen_literals.push_back(lit);
// Ensure Nielsen assumptions participate in SAT search instead of
@ -2182,8 +2183,8 @@ namespace smt {
expr_ref len_minus_l(m_autil.mk_sub(len_expr, l_expr), m);
expr_ref not_divides(m.mk_not(m_autil.mk_divides(g_expr, len_minus_l)), m);
prop_expr = m.mk_or(len_lt_l, not_divides);
m_th_rewriter(prop_expr); // the divisibility predicate needs to be rewritten as it won't happen
// automatically
m_th_rewriter(prop_expr);
// the divisibility predicate needs to be rewritten as it won't happen automatically
m_gradient_cache[s] = 1; // Reset gradient cache
}