Crate aws_smt_strings

Support for manipulating SMT-style strings and regular expressions

Overview

This crate includes support for building and operating on string constants and regular expressions as defined in the SMT-LIB theory of strings.

The smt_strings module implements the SMT-LIB functions defined in the theory that do not use regular expressions.

The smt_regular_expressions module implements the SMT-LIB functions of that operate on regular expressions.

The crate also provides utilities for compiling regular expressions to deterministic finite-state automata, computing the derivatives of a regular expressions, checking whether a regular expression is empty, and so forth.

Module regular_expressions implements regular expression constructs, derivatives, and conversion to automata. Module automata provides functions for constructing and minimizing automata.

Modules

• automata
  Deterministic finite-state automata
• character_sets
  Character sets and alphabet partitions
• errors
  Error codes
• loop_ranges
  Loop ranges in regular expressions.
• regular_expressions
  Regular expressions
• smt_regular_expressions
  Regular expressions as defined in the SMT-LIB QF_S Theory The alphabet is the set of u32 between 0 and 0x2FFFF.
• smt_strings
  Basic string representation and operations for the SMT-LIB theory of strings