mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 18:43:45 +00:00
Code Activity

add review comments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-15 12:23:17 -07:00
parent 1a8570ed3f
commit a4c9a5b2b0
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -124,6 +124,7 @@ namespace euf {
return snode_kind::s_in_re;
// uninterpreted constants of string sort are variables
// NSB review: check is_uninterp instead of is_uninterp_const.
if (is_uninterp_const(e) && m_seq.is_seq(e->get_sort()))
return snode_kind::s_var;
@ -149,6 +150,7 @@ namespace euf {
break;
case snode_kind::s_var:
// NSB review: a variable node can be a "value". Should it be ground then?
n->m_ground = false;
n->m_regex_free = true;
n->m_nullable = false;
@ -157,6 +159,7 @@ namespace euf {
break;
case snode_kind::s_unit:
// NSB review: SASSERT(n->num_args() == 1); and simplify code
n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
n->m_regex_free = true;
n->m_nullable = false;
@ -180,6 +183,8 @@ namespace euf {
case snode_kind::s_power: {
// s^n: nullable follows base, consistent with ZIPT's PowerToken
// the exponent n is assumed to be a symbolic integer, may or may not be zero
// NSB review: SASSERT(n->num_args() == 2); and simplify code
// NSB review: is this the correct definition of ground what about the exponent?
SASSERT(n->num_args() >= 1);
snode* base = n->arg(0);
n->m_ground = base->is_ground();
@ -269,6 +274,7 @@ namespace euf {
break;
case snode_kind::s_to_re:
// NSB review: are strings nullable or just empty
SASSERT(n->num_args() == 1);
n->m_ground = n->arg(0)->is_ground();
n->m_regex_free = false;
@ -287,6 +293,7 @@ namespace euf {
break;
default:
// NSB review: is this the correct defaults for unclassified nodes?
n->m_ground = true;
n->m_regex_free = true;
n->m_nullable = false;