mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 03:53:10 +00:00
Code Activity

create sub-class for tracked eq and mem relations to separate from seq_nielsen

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-18 09:46:49 -07:00
parent e7431400b4
commit 8ac8eb4ae7
6 changed files with 65 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -104,7 +104,6 @@ namespace seq {
void str_eq::sort() {
if (m_lhs && m_rhs && m_lhs->id() > m_rhs->id()) {
std::swap(m_lhs, m_rhs);
std::swap(m_l, m_r);
}
}
@ -199,15 +198,13 @@ namespace seq {
m_char_ranges.reset();
m_var_lb.reset();
m_var_ub.reset();
for (auto const& eq : parent.m_str_eq) {
m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs,eq.m_l, eq.m_r, eq.m_dep));
}
for (auto const& mem : parent.m_str_mem) {
m_str_mem.push_back(str_mem(mem.m_str, mem.m_regex, mem.m_lit, mem.m_history, mem.m_id, mem.m_dep));
}
for (auto const& ic : parent.m_int_constraints) {
for (auto const& eq : parent.m_str_eq)
m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs, eq.m_dep));
for (auto const& mem : parent.m_str_mem)
m_str_mem.push_back(str_mem(mem.m_str, mem.m_regex, mem.m_history, mem.m_id, mem.m_dep));
for (auto const& ic : parent.m_int_constraints)
m_int_constraints.push_back(ic);
}
// clone character disequalities
for (auto const& kv : parent.m_char_diseqs) {
ptr_vector<euf::snode> diseqs;
@ -331,7 +328,7 @@ namespace seq {
return true;
}
// add int_constraint: len(var) >= lb
ast_manager& m = m_graph.m();
ast_manager& m = m_graph.get_manager();
seq_util& seq = m_graph.seq();
arith_util arith(m);
expr_ref len_var(seq.str.mk_length(var->get_expr()), m);
@ -357,7 +354,7 @@ namespace seq {
return true;
}
// add int_constraint: len(var) <= ub
ast_manager& m = m_graph.m();
ast_manager& m = m_graph.get_manager();
seq_util& seq = m_graph.seq();
arith_util arith(m);
expr_ref len_var(seq.str.mk_length(var->get_expr()), m);
@ -461,7 +458,7 @@ namespace seq {
}
else {
// str is a concatenation or other term: add as general int_constraints
ast_manager& m = m_graph.m();
ast_manager& m = m_graph.get_manager();
arith_util arith(m);
expr_ref len_str = m_graph.compute_length_expr(mem.m_str);
if (min_len > 0) {
@ -537,7 +534,7 @@ namespace seq {
// -----------------------------------------------
nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver):
m_m(sg.get_manager()),
m(sg.get_manager()),
m_seq(sg.get_seq_util()),
m_sg(sg),
m_solver(solver),
@ -577,7 +574,7 @@ namespace seq {
if (!m_root)
m_root = mk_node();
dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
str_eq eq(lhs, rhs, l, r, dep);
str_eq eq(lhs, rhs, dep);
eq.sort();
m_root->add_str_eq(eq);
}
@ -588,7 +585,7 @@ namespace seq {
dep_tracker dep = m_dep_mgr.mk_leaf(l);
euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
unsigned id = next_mem_id();
m_root->add_str_mem(str_mem(str, regex, l, history, id, dep));
m_root->add_str_mem(str_mem(str, regex, history, id, dep));
}
void nielsen_graph::inc_run_idx() {
@ -892,9 +889,9 @@ namespace seq {
// Groups consecutive s_char tokens into quoted strings, renders s_var by name,
// shows s_power with superscripts, s_unit by its inner expression,
// and falls back to mk_pp (HTML-escaped) for other token kinds.
std::string snode_label_html(euf::snode const* n, ast_manager& m) {
if (!n)
return "null";
static std::string snode_label_html(euf::snode const* n, ast_manager& m) {
if (!n) return "null";
seq_util seq(m);
// collect all leaf tokens left-to-right
@ -2287,7 +2284,7 @@ namespace seq {
// m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
m_depth_bound = 3;
while (true) {
if (!m().inc()) {
if (!m.inc()) {
#ifdef Z3DEBUG
// Examining the Nielsen graph is probably the best way of debugging
std::string dot = to_dot();
@ -2335,7 +2332,7 @@ namespace seq {
m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
// check for external cancellation (timeout, user interrupt)
if (!m().inc())
if (!m.inc())
return search_result::unknown;
// check DFS node budget (0 = unlimited)
@ -2537,8 +2534,9 @@ namespace seq {
if (!lhead || !rhead)
continue;
// char vs var: branch 1: var -> ε, branch 2: var -> char·var
euf::snode* char_head = lhead->is_unit() ? lhead : (rhead->is_unit() ? rhead : nullptr);
// char vs var: branch 1: var -> ε, branch 2: var -> char·var (depending on direction)
// NSB review: add also case var -> unit·var
euf::snode* char_head = lhead->is_char() ? lhead : (rhead->is_char() ? rhead : nullptr);
euf::snode* var_head = lhead->is_var() ? lhead : (rhead->is_var() ? rhead : nullptr);
if (char_head && var_head) {
nielsen_node* child = mk_child(node);
@ -2861,8 +2859,8 @@ namespace seq {
auto& eqs = child->str_eqs();
eqs[eq_idx] = eqs.back();
eqs.pop_back();
eqs.push_back(str_eq(eq1_lhs, eq1_rhs, eq.m_l, eq.m_r, eq.m_dep));
eqs.push_back(str_eq(eq2_lhs, eq2_rhs, eq.m_l, eq.m_r, eq.m_dep));
eqs.push_back(str_eq(eq1_lhs, eq1_rhs, eq.m_dep));
eqs.push_back(str_eq(eq2_lhs, eq2_rhs, eq.m_dep));
// Int constraints on the edge.
// 1) len(pad) = |padding| (if padding variable was created)
@ -3411,11 +3409,11 @@ namespace seq {
nielsen_node* child = mk_child(node);
// Add membership: pr ∈ stab_base* (stabilizer constraint)
child->add_str_mem(str_mem(pr, star_sn, mem.m_lit, mem.m_history, next_mem_id(), mem.m_dep));
child->add_str_mem(str_mem(pr, star_sn, mem.m_history, next_mem_id(), mem.m_dep));
// Add remaining membership: po · tail ∈ R (same regex, trimmed history)
euf::snode* post_tail = str_tail->is_empty() ? po : m_sg.mk_concat(po, str_tail);
child->add_str_mem(str_mem(post_tail, mem.m_regex, mem.m_lit, nullptr, next_mem_id(), mem.m_dep));
child->add_str_mem(str_mem(post_tail, mem.m_regex, nullptr, next_mem_id(), mem.m_dep));
// Blocking constraint: po must NOT start with stab_base
// po ∈ complement(non_nullable(stab_base) · Σ*)
@ -3427,7 +3425,7 @@ namespace seq {
expr_ref block_re(seq.re.mk_complement(base_then_all), mgr);
euf::snode* block_sn = m_sg.mk(block_re);
if (block_sn)
child->add_str_mem(str_mem(po, block_sn, mem.m_lit, nullptr, next_mem_id(), mem.m_dep));
child->add_str_mem(str_mem(po, block_sn, nullptr, next_mem_id(), mem.m_dep));
}
// Substitute x → pr · po
@ -3925,6 +3923,7 @@ namespace seq {
}
}
#if 0
void nielsen_graph::explain_conflict(svector<std::pair<smt::enode*, smt::enode*>>& eqs,
svector<sat::literal>& mem_literals) const {
SASSERT(m_root);
@ -3939,6 +3938,7 @@ namespace seq {
mem_literals.push_back(std::get<sat::literal>(d));
}
}
#endif
// -----------------------------------------------------------------------
// nielsen_graph: length constraint generation

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

@ -353,12 +353,12 @@ namespace seq {
struct str_eq {
euf::snode* m_lhs;
euf::snode* m_rhs;
smt::enode *m_l, *m_r;
dep_tracker m_dep;
str_eq(): m_lhs(nullptr), m_rhs(nullptr), m_dep(nullptr) {}
str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r, dep_tracker const& dep):
m_lhs(lhs), m_rhs(rhs), m_l(l), m_r(r), m_dep(dep) {}
str_eq() = default;
str_eq(euf::snode* lhs, euf::snode* rhs, dep_tracker const& dep):
m_lhs(lhs), m_rhs(rhs), m_dep(dep) {}
bool operator==(str_eq const& other) const {
return m_lhs == other.m_lhs && m_rhs == other.m_rhs;
@ -379,14 +379,13 @@ namespace seq {
struct str_mem {
euf::snode* m_str;
euf::snode* m_regex;
sat::literal m_lit;
euf::snode* m_history; // tracks derivation history for cycle detection
unsigned m_id; // unique identifier
dep_tracker m_dep;
str_mem(): m_str(nullptr), m_regex(nullptr), m_history(nullptr), m_id(UINT_MAX), m_dep(nullptr) {}
str_mem(euf::snode* str, euf::snode* regex, sat::literal l, euf::snode* history, unsigned id, dep_tracker const& dep):
m_str(str), m_regex(regex), m_lit(l), m_history(history), m_id(id), m_dep(dep) {}
str_mem(euf::snode* str, euf::snode* regex, euf::snode* history, unsigned id, dep_tracker const& dep):
m_str(str), m_regex(regex), m_history(history), m_id(id), m_dep(dep) {}
bool operator==(str_mem const& other) const {
return m_id == other.m_id && m_str == other.m_str && m_regex == other.m_regex;
@ -747,7 +746,7 @@ namespace seq {
// mirrors ZIPT's NielsenGraph
class nielsen_graph {
friend class nielsen_node;
ast_manager& m_m;
ast_manager& m;
seq_util& m_seq;
euf::sgraph& m_sg;
region m_region;
@ -815,9 +814,11 @@ namespace seq {
nielsen_graph(euf::sgraph& sg, simple_solver& solver);
~nielsen_graph();
ast_manager &get_manager() {
return m;
}
euf::sgraph& sg() { return m_sg; }
ast_manager& m() { return m_m; }
ast_manager const& m() const { return m_m; }
seq_util& seq() { return m_seq; }
seq_util const& seq() const { return m_seq; }

2
src/smt/seq/seq_regex.cpp
View file

@ -770,7 +770,7 @@ namespace seq {
new_history = m_sg.mk(chain);
}
}
return seq::str_mem(mem.m_str, mem.m_regex, mem.m_lit, new_history, mem.m_id, mem.m_dep);
return seq::str_mem(mem.m_str, mem.m_regex, new_history, mem.m_id, mem.m_dep);
}
// -----------------------------------------------------------------------

2
src/smt/seq/seq_regex.h
View file

@ -246,7 +246,7 @@ namespace seq {
if (deriv)
propagate_self_stabilizing(parent_re, deriv);
euf::snode* new_str = m_sg.drop_first(mem.m_str);
return seq::str_mem(new_str, deriv, mem.m_lit, mem.m_history, mem.m_id, mem.m_dep);
return seq::str_mem(new_str, deriv, mem.m_history, mem.m_id, mem.m_dep);
}
// -----------------------------------------------------------------

24
src/smt/seq/seq_state.h
View file

@ -27,6 +27,18 @@ namespace smt {
class enode;
struct tracked_str_eq : public seq::str_eq {
enode *m_l, *m_r;
tracked_str_eq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep)
: seq::str_eq(lhs, rhs, dep), m_l(l), m_r(r) {}
};
struct tracked_str_mem : public seq::str_mem {
sat::literal lit;
tracked_str_mem(euf::snode *str, euf::snode *regex, sat::literal lit, euf::snode *history, unsigned id, seq::dep_tracker const &dep)
: seq::str_mem(str, regex, history, id, dep), lit(lit) {}
};
// source info for a string disequality
struct diseq_source {
enode* m_n1;
@ -34,8 +46,8 @@ namespace smt {
};
class seq_state {
vector<seq::str_eq> m_str_eqs;
vector<seq::str_mem> m_str_mems;
vector<tracked_str_eq> m_str_eqs;
vector<tracked_str_mem> m_str_mems;
vector<diseq_source> m_diseqs;
unsigned_vector m_str_eq_lim;
unsigned_vector m_str_mem_lim;
@ -64,20 +76,20 @@ namespace smt {
void add_str_eq(euf::snode* lhs, euf::snode* rhs, enode* n1, enode* n2) {
seq::dep_tracker dep = nullptr;
m_str_eqs.push_back(seq::str_eq(lhs, rhs, n1, n2, dep));
m_str_eqs.push_back(tracked_str_eq(lhs, rhs, n1, n2, dep));
}
void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal lit) {
seq::dep_tracker dep = nullptr;
m_str_mems.push_back(seq::str_mem(str, regex, lit, nullptr, m_next_mem_id++, dep));
m_str_mems.push_back(tracked_str_mem(str, regex, lit, nullptr, m_next_mem_id++, dep));
}
void add_diseq(enode* n1, enode* n2) {
m_diseqs.push_back({n1, n2});
}
vector<seq::str_eq> const& str_eqs() const { return m_str_eqs; }
vector<seq::str_mem> const& str_mems() const { return m_str_mems; }
vector<tracked_str_eq> const& str_eqs() const { return m_str_eqs; }
vector<tracked_str_mem> const& str_mems() const { return m_str_mems; }
vector<diseq_source> const& diseqs() const { return m_diseqs; }
diseq_source const& get_diseq(unsigned i) const { return m_diseqs[i]; }

14
src/smt/theory_nseq.cpp
View file

@ -282,7 +282,7 @@ namespace smt {
if (m_regex.is_empty_regex(mem.m_regex)) {
enode_pair_vector eqs;
literal_vector lits;
lits.push_back(mem.m_lit);
lits.push_back(mem.lit);
set_conflict(eqs, lits);
return;
}
@ -291,7 +291,7 @@ namespace smt {
if (mem.m_str->is_empty() && !mem.m_regex->is_nullable()) {
enode_pair_vector eqs;
literal_vector lits;
lits.push_back(mem.m_lit);
lits.push_back(mem.lit);
set_conflict(eqs, lits);
return;
}
@ -330,18 +330,18 @@ namespace smt {
continue; // trivially satisfied, skip
if (triv < 0) {
// trivially unsat: add anyway so solve() detects conflict
m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.m_lit);
m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.lit);
continue;
}
// pre-process: consume ground prefix characters
vector<seq::str_mem> processed;
if (!m_regex.process_str_mem(mem, processed)) {
// conflict during ground prefix consumption
m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.m_lit);
m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.lit);
continue;
}
for (auto const& pm : processed) {
m_nielsen.add_str_mem(pm.m_str, pm.m_regex, pm.m_lit);
m_nielsen.add_str_mem(pm.m_str, pm.m_regex, mem.lit);
}
}
@ -839,9 +839,9 @@ namespace smt {
literal_vector lits;
for (unsigned i : mem_indices) {
auto const &src = m_state.str_mems()[i];
SASSERT(ctx.get_assignment(src.m_lit) == l_true); // we already stored the polarity of the literal
SASSERT(ctx.get_assignment(src.lit) == l_true); // we already stored the polarity of the literal
lits.push_back(
src.m_lit);
src.lit);
}
TRACE(seq, tout << "nseq regex precheck: empty intersection for var "
<< var_id << ", conflict with " << lits.size() << " lits\n";);