mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

Add sort parameter to sgraph::mk_var

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-11 21:25:56 +00:00
parent 3d530b9398
commit 76ba240ee2
3 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -450,8 +450,9 @@ 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) {
if (!s) s = m_str_sort;
expr_ref e(m.mk_const(name, s), m);
return mk(e);
}

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

@ -125,8 +125,10 @@ namespace euf {
// register expression in both sgraph and egraph
enode* mk_enode(expr* e);
sort* get_str_sort() const { return m_str_sort; }
// factory methods for creating snodes with corresponding expressions
snode* mk_var(symbol const& name);
snode* mk_var(symbol const& name, sort* s = nullptr);
snode* mk_char(unsigned ch);
snode* mk_empty();
snode* mk_concat(snode* a, snode* b);

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

@ -2216,7 +2216,7 @@ namespace seq {
euf::snode* nielsen_graph::mk_fresh_var() {
++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()), m_sg.get_str_sort());
}
euf::snode* nielsen_graph::mk_fresh_char_var() {