mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

deps

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-14 00:29:58 -07:00
parent 68d7917653
commit 53cc320efa
4 changed files with 21 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -43,7 +43,7 @@ NSB review:
namespace seq {
void deps_to_lits(dep_tracker const &deps, svector<enode_pair> &eqs, svector<sat::literal> &lits) {
void deps_to_lits(dep_tracker deps, svector<enode_pair> &eqs, svector<sat::literal> &lits) {
vector<dep_source, false> vs;
dep_manager::s_linearize(deps, vs);
for (dep_source const &d : vs) {
@ -4159,8 +4159,7 @@ namespace seq {
// Concrete character → to_re(unit(c))
expr* te = tok->get_expr();
SASSERT(te);
expr_ref tre(m_seq.re.mk_to_re(te), m);
tok_re = m_sg.mk(tre);
tok_re = m_sg.mk(m_seq.re.mk_to_re(te));
}
else if (tok->is_var()) {
// Variable → intersection of primitive regex constraints, or Σ*
@ -4173,6 +4172,8 @@ namespace seq {
expr_ref all_re(m_seq.re.mk_full_seq(m_seq.re.mk_re(str_sort)), m);
tok_re = m_sg.mk(all_re);
}
TRACE(seq, tout << "intersection-collection\n" << mk_pp(tok->get_expr(), m)
<< "\n" << mk_pp(tok_re->get_expr(), m) << "\n");
}
else if (tok->is_unit()) {
// Symbolic char — try to get char_range
@ -4182,8 +4183,6 @@ namespace seq {
// Build union of re.range for each interval
euf::snode* range_re = nullptr;
for (auto const& r : cs.first.ranges()) {
expr_ref lo(m_seq.mk_char(r.m_lo), m);
expr_ref hi(m_seq.mk_char(r.m_hi - 1), m);
expr_ref rng(m_seq.re.mk_range(
m_seq.str.mk_string(zstring(r.m_lo)),
m_seq.str.mk_string(zstring(r.m_hi - 1))), m);
@ -4221,8 +4220,7 @@ namespace seq {
expr* ae = approx->get_expr();
expr* te = tok_re->get_expr();
SASSERT(ae && te);
expr_ref cat(m_seq.re.mk_concat(ae, te), m);
approx = m_sg.mk(cat);
approx = m_sg.mk(m_seq.re.mk_concat(ae, te));
}
}
@ -4240,7 +4238,8 @@ namespace seq {
// TODO: Minimize the conflict here
lbool result = m_seq_regex->is_empty_bfs(inter_sn, 5000);
TRACE(seq, tout << "widen empty-intersect: " << result << " " << mk_pp(re, m)
<< " <= " << mk_pp(ae, m) << "\n" << mem_pp(m, mem) << "\n");
<< " <= " << mk_pp(ae, m) << "\n" << mem_pp(m, mem) << "\n";
display(tout, &node) << "\n");
return result == l_true;
}

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

@ -352,7 +352,7 @@ namespace seq {
using dep_tracker = dep_manager::dependency*;
// partition dep_source leaves from deps into enode pairs and sat literals.
void deps_to_lits(dep_tracker const& deps,
void deps_to_lits(dep_tracker deps,
svector<enode_pair>& eqs,
svector<sat::literal>& lits);
@ -831,7 +831,7 @@ namespace seq {
mutable dep_manager m_dep_mgr;
std::ostream &display(std::ostream &out, nielsen_node* n) const;
std::ostream &display(std::ostream &out, nielsen_node const* n) const;
public:
// Construct with a caller-supplied solver. Ownership is NOT transferred;

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

@ -25,7 +25,7 @@ Author:
namespace seq {
std::ostream& nielsen_graph::display(std::ostream& out, nielsen_node* n) const {
std::ostream& nielsen_graph::display(std::ostream& out, nielsen_node const* n) const {
out << " node[" << n->id() << "]";
if (n == m_root)
out << " (root)";

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

@ -148,15 +148,12 @@ namespace seq {
}
void seq_regex::set_self_stabilizing(euf::snode* regex) {
if (!regex)
return;
m_self_stabilizing.insert(regex->id());
if (regex)
m_self_stabilizing.insert(regex->id());
}
bool seq_regex::is_self_stabilizing(euf::snode* regex) const {
if (!regex)
return false;
return m_self_stabilizing.contains(regex->id());
return regex && m_self_stabilizing.contains(regex->id());
}
// -----------------------------------------------------------------------
@ -502,6 +499,8 @@ namespace seq {
// BFS regex emptiness check
// -----------------------------------------------------------------------
// NSB review: we have similar functionality in seq_rewriter::some_seq_in_re
// currently both these versions only relly work for strings not general sequences
lbool seq_regex::is_empty_bfs(euf::snode* re, unsigned max_states) {
if (!re)
return l_undef;
@ -603,8 +602,7 @@ namespace seq {
expr* r1 = result->get_expr();
expr* r2 = regexes[i]->get_expr();
SASSERT(r1 && r2);
expr_ref inter(seq.re.mk_inter(r1, r2), mgr);
result = m_sg.mk(inter);
result = m_sg.mk(seq.re.mk_inter(r1, r2));
SASSERT(result);
}
@ -662,18 +660,19 @@ namespace seq {
SASSERT(var);
seq_util& seq = m_sg.get_seq_util();
ast_manager& mgr = m_sg.get_manager();
ast_manager& m = m_sg.get_manager();
euf::snode* result = nullptr;
for (auto const& mem : node.str_mems()) {
SASSERT(mem.m_str && mem.m_regex);
// Primitive constraint: str is a single variable
if (!mem.is_primitive())
continue;
euf::snode* first = mem.m_str->first();
euf::snode *first = mem.m_str->first();
// NSB review: why is this "first" and not mem.m_str?
SASSERT(first);
if (first != var)
continue;
TRACE(seq, tout << mk_pp(first->get_expr(), m) << " " << mem_pp(m, mem) << " dep: " << mem.m_dep << "\n");
if (!result) {
result = mem.m_regex;
@ -683,7 +682,7 @@ namespace seq {
expr* r1 = result->get_expr();
expr* r2 = mem.m_regex->get_expr();
if (r1 && r2) {
expr_ref inter(seq.re.mk_inter(r1, r2), mgr);
expr_ref inter(seq.re.mk_inter(r1, r2), m);
result = m_sg.mk(inter);
dep = dep_mgr.mk_join(dep, mem.m_dep);
}