mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

Make sort required in sgraph::mk_var and nielsen_graph::mk_fresh_var

Browse source 
sgraph::mk_var(symbol const& name) silently hardcoded m_str_sort (always
String), which is wrong when sequences of other element sorts are in play.

Changes:
- euf_snode.h: add get_sort() convenience accessor (SASSERT that expr is
  non-null, then return expr->get_sort()) so call sites are readable and the
  precondition is checked in one place.
- euf_sgraph.h / euf_sgraph.cpp: make sort a required parameter of mk_var;
  remove the implicit use of m_str_sort.
- seq_nielsen.h / seq_nielsen.cpp: make sort a required parameter of
  mk_fresh_var; forward it to mk_var.
- All mk_fresh_var() call sites in seq_nielsen.cpp updated to derive the sort
  from the adjacent contextual snode via ->get_sort():
    lhead/rhead: sort of the variable being substituted
    lhs_toks[0]: sort of the equation's leading token (padding case)
    first: sort of the string membership variable
    base: sort of the power's base sequence

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-12 02:45:37 +00:00
parent 918418fdb8
commit 2ec09f88c4
5 changed files with 21 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_sgraph.cpp
View file

@ -450,8 +450,8 @@ namespace euf {
m_egraph.pop(num_scopes);
}
snode* sgraph::mk_var(symbol const& name) {
expr_ref e(m.mk_const(name, m_str_sort), m);
snode* sgraph::mk_var(symbol const& name, sort* s) {
expr_ref e(m.mk_const(name, s), m);
return mk(e);
}

2
src/ast/euf/euf_sgraph.h
View file

@ -126,7 +126,7 @@ namespace euf {
enode* mk_enode(expr* e);
// factory methods for creating snodes with corresponding expressions
snode* mk_var(symbol const& name);
snode* mk_var(symbol const& name, sort* s);
snode* mk_char(unsigned ch);
snode* mk_empty();
snode* mk_concat(snode* a, snode* b);

1
src/ast/euf/euf_snode.h
View file

@ -98,6 +98,7 @@ namespace euf {
public:
expr* get_expr() const { return m_expr; }
sort* get_sort() const { SASSERT(m_expr); return m_expr->get_sort(); }
snode_kind kind() const { return m_kind; }
unsigned id() const { return m_id; }
unsigned num_args() const { return m_num_args; }

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

@ -1225,7 +1225,7 @@ namespace seq {
}
// branch 2: y → char·fresh (progress)
{
euf::snode* fresh = mk_fresh_var();
euf::snode* fresh = mk_fresh_var(rhead->get_sort());
euf::snode* replacement = m_sg.mk_concat(lhead, fresh);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
@ -1248,7 +1248,7 @@ namespace seq {
}
// branch 2: x → char·fresh (progress)
{
euf::snode* fresh = mk_fresh_var();
euf::snode* fresh = mk_fresh_var(lhead->get_sort());
euf::snode* replacement = m_sg.mk_concat(rhead, fresh);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
@ -1294,7 +1294,7 @@ namespace seq {
}
// child 2: x → y·x' (progress)
{
euf::snode* fresh = mk_fresh_var();
euf::snode* fresh = mk_fresh_var(lhead->get_sort());
euf::snode* replacement = m_sg.mk_concat(rhead, fresh);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
@ -1304,7 +1304,7 @@ namespace seq {
}
// child 3: y → x·y' (progress)
{
euf::snode* fresh = mk_fresh_var();
euf::snode* fresh = mk_fresh_var(rhead->get_sort());
euf::snode* replacement = m_sg.mk_concat(lhead, fresh);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
@ -1534,7 +1534,7 @@ namespace seq {
euf::snode* pad = nullptr;
if (padding != 0) {
pad = mk_fresh_var();
pad = mk_fresh_var(lhs_toks[0]->get_sort());
if (padding > 0) {
// LHS prefix is longer by |padding| constants.
// Prepend pad to RHS prefix, append pad to LHS suffix.
@ -1585,10 +1585,10 @@ namespace seq {
// nielsen_graph: mk_fresh_var
// -----------------------------------------------------------------------
euf::snode* nielsen_graph::mk_fresh_var() {
euf::snode* nielsen_graph::mk_fresh_var(sort* s) {
++m_stats.m_num_fresh_vars;
std::string name = "v!" + std::to_string(m_fresh_cnt++);
return m_sg.mk_var(symbol(name.c_str()));
return m_sg.mk_var(symbol(name.c_str()), s);
}
euf::snode* nielsen_graph::mk_fresh_char_var() {
@ -1705,7 +1705,7 @@ namespace seq {
if (!deriv || deriv->is_fail())
continue;
euf::snode* fresh = mk_fresh_var();
euf::snode* fresh = mk_fresh_var(first->get_sort());
euf::snode* replacement = m_sg.mk_concat(ch, fresh);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
@ -2001,7 +2001,7 @@ namespace seq {
// Side constraint: n >= 1
// Use fresh power variable for u^(n-1)
{
euf::snode* fresh_power = mk_fresh_var();
euf::snode* fresh_power = mk_fresh_var(base->get_sort());
euf::snode* replacement = m_sg.mk_concat(base, fresh_power);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
@ -2040,8 +2040,8 @@ namespace seq {
// replacing x → z·fresh_post. This breaks the cycle because
// z is a new variable that won't trigger star_intr again.
euf::snode* x = first;
euf::snode* z = mk_fresh_var();
euf::snode* fresh_post = mk_fresh_var();
euf::snode* z = mk_fresh_var(x->get_sort());
euf::snode* fresh_post = mk_fresh_var(x->get_sort());
euf::snode* str_tail = m_sg.drop_first(mem.m_str);
// Build z ∈ R* membership: the star of the current regex
@ -2234,7 +2234,7 @@ namespace seq {
euf::snode* deriv = m_sg.brzozowski_deriv(mem.m_regex, mt);
if (deriv && deriv->is_fail()) continue;
euf::snode* fresh_var = mk_fresh_var();
euf::snode* fresh_var = mk_fresh_var(first->get_sort());
euf::snode* fresh_char = mk_fresh_char_var();
euf::snode* replacement = m_sg.mk_concat(fresh_char, fresh_var);
nielsen_node* child = mk_child(node);
@ -2282,8 +2282,8 @@ namespace seq {
// Side constraints: m >= 0, m < n (i.e., n >= m + 1)
{
expr_ref fresh_m = mk_fresh_int_var();
euf::snode* fresh_power = mk_fresh_var(); // represents base^m
euf::snode* fresh_suffix = mk_fresh_var(); // represents prefix(base)
euf::snode* fresh_power = mk_fresh_var(base->get_sort()); // represents base^m
euf::snode* fresh_suffix = mk_fresh_var(base->get_sort()); // represents prefix(base)
euf::snode* replacement = m_sg.mk_concat(fresh_power, fresh_suffix);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
@ -2302,7 +2302,7 @@ namespace seq {
// Branch 2: x = u^n · x' (variable extends past full power, non-progress)
// Side constraint: n >= 0
{
euf::snode* fresh_tail = mk_fresh_var();
euf::snode* fresh_tail = mk_fresh_var(base->get_sort());
// Peel one base unit (approximation of extending past the power)
euf::snode* replacement = m_sg.mk_concat(base, fresh_tail);
nielsen_node* child = mk_child(node);
@ -2357,7 +2357,7 @@ namespace seq {
// Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1)
// Side constraint: n >= 1
{
euf::snode* fresh = mk_fresh_var();
euf::snode* fresh = mk_fresh_var(base->get_sort());
euf::snode* replacement = m_sg.mk_concat(base, fresh);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);

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

@ -761,7 +761,7 @@ namespace seq {
search_result search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path);
// create a fresh variable with a unique name
euf::snode* mk_fresh_var();
euf::snode* mk_fresh_var(sort* s);
// create a fresh symbolic character: seq.unit(fresh_char_const)
// analogous to ZIPT's SymCharToken creation