Module re 

Core module for SMT-LIB regular expressions.

This module defines the core data structures and algorithms for working with regular expressions in the SMT-LIB theory of strings. Regular expressions are represented as abstract syntax trees (ASTs), where each node represents a regular operation or base case.

The module provides the following types:

• Regex — a reference-counted pointer to a regular expression node (ReNode).
• ReNode — a node in a regular expression AST.
• ReOp — the enum describing the different operations in a regular expression (e.g., re.*, re.union, re.diff).

Each ReNode contains a ReOp, which may be either a base case (e.g., a literal or character range), or a regular operation applied to one or more subexpressions. In the latter case, subexpressions are stored as reference-counted pointer (Regex), allowing for structural sharing of common subtrees. This means that if a regular expression contains the same subexpression multiple times, the corresponding ReOps will all point to the same ReNode instance.

For example, if the regex is

re.union(re.*(str.to_re("a")), re.comp(str.to_re("a")))`

then the re.* and re.comp operations will point to the same exact same ReNode instance for the subexpression str.to_re("a").

Structural sharing enables:

• Reduced memory usage
• Efficient equality and hashing (by node ID)
• Cheap cloning of regular expressions
• Caching of derived properties (e.g., nullable, alphabet, etc.)

Because of this, regular expressions must be created using the ReBuilder and cannot be constructed directly.

Example

use smt_str::re::*;
use std::rc::Rc;

// Create a regular expression builder
let mut builder = ReBuilder::default();

// Construct the regular expression `a``
let re_a = builder.to_re("a".into());

// Construct the regular expression `a*` and `comp(a)`
let re_star = builder.star(re_a.clone());
let re_comp = builder.comp(re_a.clone());

// The operand of `re_star` and `re_comp` are not only structurally equal
assert_eq!(re_star[0], re_comp[0]);
// but also share the same node in memory
assert!(Rc::ptr_eq(&re_star[0], &re_comp[0]));

Modules

deriv

Brzozowski derivatives for regular expression.

Structs

ReBuilder

A builder for constructing regular expressions in the SMT-LIB string theory.

ReNode

A node in the abstract syntax tree (AST) of a regular expression.

SubExpressions

An iterator over the subexpressions of a regular expression. Only iterates over the immediate subexpressions, not recursively.

Enums

ReOp

The core operations that define a regular expression.

Functions

union_of_chars

Checks whether the regular operator denotes a union of characters, expressed as a ranges. If it does, the ranges are returned as a vector. Otherwise, None is returned.

Type Aliases

ReId

Regex

A shared pointer to a regular expression node (ReNode).