1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_range_collapse.h
Abstract:
Recognize regexes that are boolean combinations of character-class
primitives (re.empty, re.full_char, re.range with concrete chars,
and re.union/inter/comp/diff over translatable arguments), and
materialize a seq::range_predicate back into a canonical regex AST.
Together with seq_rewriter integration, this lets any boolean
combination of character-class regexes collapse to a canonical
multi-range form, so that equivalent character classes share AST
identity, and downstream consumers (derivative, OneStep, caching)
can short-circuit them as pure range predicates.
Authors:
Margus Veanes (veanes) 2026
--*/
#pragma once
#include "ast/rewriter/seq_range_predicate.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/seq_decl_plugin.h"
namespace seq {
/**
* Convert a Boolean guard over the single character variable v0 = (:var 0) -- a
* derivative cofactor path condition -- into the range_predicate of the characters
* satisfying it. Recognizes {true, false, =, char.<=, and, or, not} over v0 and
* concrete characters; returns false (out untouched) on anything else.
*/
bool guard_to_range_predicate(seq_util& u, expr* v0, expr* guard, range_predicate& out);
/**
* If r is a boolean combination of character-class regex primitives
* over the unsigned character domain [0, max_char], compute the
* equivalent range_predicate and return true. Otherwise return false
* with out untouched.
*
* Recognized fragment (all character-class-preserving operations):
* re.empty -> empty
* re.full_char_set -> top
* re.range "c_lo" "c_hi" (concrete) -> [c_lo, c_hi]
* re.union r1 r2 -> p1 | p2
* re.intersection r1 r2 -> p1 & p2
* re.diff r1 r2 -> p1 - p2
*
* Notably re.complement is NOT recognized: it is a SEQUENCE-level
* complement (over all of Σ*), not a character-class complement, so
* collapsing it would change semantics whenever the result is used
* in any non-character-class context. Sequence-level rewrites for
* re.complement (double-comp, deMorgan, etc.) are handled directly
* in seq_rewriter::mk_re_complement.
*/
bool regex_to_range_predicate(seq_util& u, expr* r, range_predicate& out);
/**
* Canonical materialization of p as a regex AST over the given
* sequence sort. Two range_predicates with equal canonical
* representations produce structurally identical regex ASTs:
*
* empty -> re.empty
* top -> re.full_char_set
* single range [lo, hi] -> re.range "lo" "hi"
* multiple ranges -> right-associated re.union of single
* ranges, in increasing order of lo
* (matching the canonical range order
* held by range_predicate).
*/
expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort);
/**
* Unfolds and then folds the given regex expression.
* Unfolding, produces the symbolic derivative which is an expression with a free variable var 0
* of the character sort.
* Folding produces a regex expression that is equivalent to the original one.
* It is obtained by taking the cofactors of the unfold, and producing a range predicate
* from the conditions with var 0.
* Formally:
* cofactors F_i[var 0], r_i <- unfold(r)
* of_pred(\lambda ch . F_i[ch]) . r_i <- fold(F_i[var 0], r_i)
* union_i of_pred(\ ch. F_i[ch]) . r_i <- fold(unfold(r))
*/
expr_ref unfold_fold(seq_rewriter &rw, expr *r);
}