Crate smt_str

Crate smt_str 

Source
Expand description

This crate provides types and utilities for working with SMT-LIB strings. An SMT-LIB string is a sequence of characters with unicode code points in the range 0x0000 to 0x2FFFF (first two planes of Unicode). The underlying semantics differ from those of Rusts native charandString` types:

  • Character model: Rust’s char type represents any Unicode scalar value which is not a surrogate code point. In SMT-LIB, a character is a unicode code point in the range 0x0000 to 0x2FFFF, including surrogate code points (which are not valid Rust chars).
  • String length: In Rust, the length of a string is counted in bytes whereas in In SMT-LIB, the length of a string is counted in characters. For example, if a character takes more than one byte to encode (such as 🦀), Rust’s String.len() will return the number of bytes. In order to obtain the number of characters, one must count the number of chars in the string instead, which can easily lead to errors.
  • Escaping: In SMT-LIB, the only escape sequences are of the form \uXXXX and \u{X...}. Especially, there are no escape sequences for control characters, such as \n or \t, that are present in Rust.

This crate provides a convenient way to work with SMT-LIB strings through the SmtChar and SmtString types.

  • SmtChar represents a Unicode code point in the range 0x0000 to 0x2FFFF (including surrogates).
  • SmtString represents a sequence of SmtChar values and offers parsing, manipulation, and search utilities that conform to the SMT-LIB specification.

Modules§

alphabet
Character ranges and alphabets for SMT-LIB strings.
automata
re
Core module for SMT-LIB regular expressions.
sampling

Structs§

CharIterator
An iterator over the characters in the range start to end.
SmtChar
A Unicode character used in SMT-LIB strings.
SmtString
An SMT-LIB string is a sequence of characters with unicode code points in the range 0x0000 to 0x2FFFF (first two planes of Unicode). The characters are represented by the SmtChar type.

Constants§

SMT_MAX_CODEPOINT
The maximum unicode character.
SMT_MIN_CODEPOINT
The minimum unicode character.