mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00
Code Activity

revert s_unknown

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-03 10:04:13 -07:00
parent 95dc44b409
commit cdccd389e9
2 changed files with 2 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -104,11 +104,7 @@ namespace euf {
if (m_seq.str.is_in_re(e))
return snode_kind::s_in_re;
// uninterpreted constants of string sort are variables
if (m_seq.is_seq(e->get_sort()) && (is_uninterp(e) || m_seq.is_skolem(e) || m_seq.str.is_at(e)))
return snode_kind::s_var;
return snode_kind::s_unknown; // it is an element of the seq
return snode_kind::s_var;
}
void sgraph::compute_metadata(snode* n) {
@ -473,8 +469,6 @@ namespace euf {
snode* sgraph::mk_concat(snode* a, snode* b) {
if (a->is_empty()) return b;
if (b->is_empty()) return a;
SASSERT(a->kind() != snode_kind::s_unknown);
SASSERT(b->kind() != snode_kind::s_unknown);
if (m_seq.is_re(a->get_expr()))
return mk(expr_ref(m_seq.re.mk_concat(a->get_expr(), b->get_expr()), m));
return mk(expr_ref(m_seq.str.mk_concat(a->get_expr(), b->get_expr()), m));

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

@ -52,8 +52,7 @@ namespace euf {
s_full_seq, // full sequence set r=.* (OP_RE_FULL_SEQ_SET)
s_range, // character range [lo,hi] (OP_RE_RANGE)
s_to_re, // string to regex (OP_SEQ_TO_RE)
s_in_re, // regex membership (OP_SEQ_IN_RE)
s_unknown, // something else
s_in_re // regex membership (OP_SEQ_IN_RE)
};
class snode {