Struct SmtChar 

pub struct SmtChar(/* private fields */);

A Unicode character used in SMT-LIB strings.

In the SMT-LIB string theory, a character is any Unicode code point in the inclusive range 0x0000 to 0x2FFFF.

SmtChar is a wrapper around a u32 and provides convenient methods to construct, inspect, and manipulate SMT-LIB characters safely.

Examples

use smt_str::SmtChar;

// Create a new `SmtChar` from a `u32` representing a Unicode code point.
let a = SmtChar::new(0x61); // 'a'
// Get the `u32` representation of the `SmtChar`.
assert_eq!(a.as_u32(), 0x61);
// Get the `char` representation of the `SmtChar`.
assert_eq!(a.as_char(), Some('a'));

// It is also possible to create an `SmtChar` from a `char`.
let b = SmtChar::from('b');
assert_eq!(b.as_u32(), 0x62);
assert_eq!(b.as_char(), Some('b'));

let surrogate = SmtChar::new(0xD800); // valid in SMT-LIB, invalid as Rust `char`
assert_eq!(surrogate.as_char(), None);

// Non-printable characters are escaped when displayed.
let newline = SmtChar::new(0x0A); // '\n'
assert_eq!(newline.to_string(), r#"\u{A}"#);

Implementations

impl SmtChar

pub const MAX: Self

The maximum SmtChar. This is the unicode code point 0x2FFFF.

pub const MIN: Self

The minimum SmtChar. This is the unicode code point 0x0000.

pub fn new(c: u32) -> Self

Creates a new SmtChar from a u32 code point. Panics if c as u32 > 0x2FFFF.

pub fn as_char(self) -> Option<char>

Get the char representation of this SmtChar, if it can be represented as a char. Returns None if this SmtChar is a surrogate code point.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('a');
assert_eq!(c.as_char(), Some('a'));
// This is a surrogate code point and cannot be represented as a `char`.
assert_eq!(SmtChar::new(55296).as_char(), None);

pub fn as_u32(self) -> u32

Get the u32 representation of this SmtChar. The u32 is the unicode code point of this SmtChar.

Examples

use smt_str::SmtChar;
assert_eq!(SmtChar::from('a').as_u32(), 97);
assert_eq!(SmtChar::from('🦀').as_u32(), 129408);

pub fn next(self) -> Self

Returns the next SmtChar in the range 0x0000 to 0x2FFFF. Panics if this SmtChar is the maximum SmtChar.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('a');
assert_eq!(c.next(), SmtChar::from('b'));

Cannot get the next character after the maximum SmtChar:

use smt_str::SmtChar;
let c = SmtChar::MAX;
let _ = c.next(); // panics

pub fn try_next(self) -> Option<Self>

Returns the next SmtChar in the range 0x0000 to 0x2FFFF, if it exists. Returns None if this SmtChar is the maximum SmtChar.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('a');
assert_eq!(c.try_next(), Some(SmtChar::from('b')));
assert_eq!(SmtChar::MAX.try_next(), None);

pub fn saturating_next(self) -> Self

Like next, but instead of panicking when this SmtChar is the maximum SmtChar, it returns the maximum SmtChar.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('a');
assert_eq!(c.saturating_next(), SmtChar::from('b'));
assert_eq!(SmtChar::MAX.saturating_next(), SmtChar::MAX);

pub fn prev(self) -> Self

Returns the previous SmtChar in the range 0x0000 to 0x2FFFF. Panics if this SmtChar is the minimum SmtChar.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('b');
assert_eq!(c.prev(), SmtChar::from('a'));

Cannot get the previous character before the minimum SmtChar:

use smt_str::SmtChar;
let c = SmtChar::MIN;
let _ = c.prev(); // panics

pub fn try_prev(self) -> Option<Self>

Returns the previous SmtChar in the range 0x0000 to 0x2FFFF, if it exists. Returns None if this SmtChar is the minimum SmtChar.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('b');
assert_eq!(c.try_prev(), Some(SmtChar::from('a')));
assert_eq!(SmtChar::MIN.try_prev(), None);

pub fn saturating_prev(self) -> Self

Like prev, but instead of panicking when this SmtChar is the minimum SmtChar, it returns the minimum SmtChar.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('b');
assert_eq!(c.saturating_prev(), SmtChar::from('a'));
assert_eq!(SmtChar::MIN.saturating_prev(), SmtChar::MIN);

pub fn printable(self) -> bool

Returns true if this SmtChar is a printable ASCII character. Printable ASCII characters are in the range 0x00020 to 0x0007E.

Examples

use smt_str::SmtChar;
assert!(SmtChar::from('a').printable());
assert!(!SmtChar::from('\n').printable());

pub fn escape(self) -> String

Escape this SmtChar as a Unicode escape sequence. The escape sequence is of the form \u{X} where X is the hexadecimal representation of the unicode code point. The function always chooses the shortest escape sequence, i.e., it uses the smallest number of digits and does not pad with zeros.

Examples

use smt_str::SmtChar;
assert_eq!(SmtChar::from('a').escape(), r#"\u{61}"#);
assert_eq!(SmtChar::from('\n').escape(), r#"\u{A}"#);
assert_eq!(SmtChar::from('🦀').escape(), r#"\u{1F980}"#);
assert_eq!(SmtChar::MAX.escape(), r#"\u{2FFFF}"#);
assert_eq!(SmtChar::MIN.escape(), r#"\u{0}"#);

pub fn unescape(escaped: &str) -> Option<Self>

Unescape a string that contains escaped characters. Escaped characters are of the following form:

• \uDDDD
• \u{D},
• \u{DD},
• \u{DDD},
• \u{DDDD},
• \u{DDDDD}

where D is a hexadecimal digit. In the case \u{DDDDD}, the first digit must be in the range 0 to 2. The function returns None if the input string is not a valid escaped character.

Examples

use smt_str::SmtChar;
assert_eq!(SmtChar::unescape(r#"\u{61}"#), Some(SmtChar::from('a')));
assert_eq!(SmtChar::unescape(r#"\u{A}"#), Some(SmtChar::from('\n')));
assert_eq!(SmtChar::unescape(r#"\u{1F980}"#), Some(SmtChar::from('🦀')));
assert_eq!(SmtChar::unescape(r#"\u{2FFFF}"#), Some(SmtChar::MAX));
assert_eq!(SmtChar::unescape(r#"\u{0}"#), Some(SmtChar::MIN));

// Invalid escape sequences

assert_eq!(SmtChar::unescape(r#"\u{3000A}"#), None); // out of range
assert_eq!(SmtChar::unescape(r#"\u{61"#), None); // missing closing brace
assert_eq!(SmtChar::unescape(r#"\u{}"#), None); // empty digits

Trait Implementations

impl Add for SmtChar

fn add(self, rhs: SmtChar) -> Self::Output

Adds another SmtChar to this SmtChar, shifting the unicode code point. The sum is the sum of the unicode code points of the two SmtChars. Panics if the resulting code point is greater than SMT_MAX_CODEPOINT (= 0x2FFFF).

Examples

use smt_str::SmtChar;
let c = SmtChar::from('a');
assert_eq!(c + SmtChar::new(1), SmtChar::from('b'));
assert_eq!(c + SmtChar::new(25), SmtChar::from('z'));

Overflowing the maximum code point panics:

use smt_str::SmtChar;
let c = SmtChar::MAX;
let _ = c + SmtChar::new(1); // panics

type Output = SmtChar

The resulting type after applying the + operator.

impl Arbitrary for SmtChar

fn arbitrary(g: &mut Gen) -> Self

Return an arbitrary value.

fn shrink(&self) -> Box<dyn Iterator<Item = Self>>

Return an iterator of values that are smaller than itself.

impl Clone for SmtChar

fn clone(&self) -> SmtChar

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SmtChar

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for SmtChar

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Display the SmtChar as a Unicode character if it is printable. Otherwise, display the character as a Unicode escape sequence (see SmtChar::escape). Additionally, backslashes and quotes are escaped.

impl From<SmtChar> for SmtString

fn from(c: SmtChar) -> Self

Converts to this type from the input type.

impl From<char> for SmtChar

fn from(c: char) -> Self

Converts to this type from the input type.

impl From<i32> for SmtChar

fn from(c: i32) -> Self

Converts to this type from the input type.

impl From<u16> for SmtChar

fn from(c: u16) -> Self

Converts to this type from the input type.

impl From<u32> for SmtChar

fn from(c: u32) -> Self

Converts to this type from the input type.

impl From<u8> for SmtChar

fn from(c: u8) -> Self

Converts to this type from the input type.

impl FromIterator<SmtChar> for Alphabet

fn from_iter<T: IntoIterator<Item = SmtChar>>(iter: T) -> Self

Creates a value from an iterator.

impl FromIterator<SmtChar> for SmtString

fn from_iter<I: IntoIterator<Item = SmtChar>>(iter: I) -> Self

Creates a value from an iterator.

impl Hash for SmtChar

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for SmtChar

fn cmp(&self, other: &SmtChar) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for SmtChar

fn eq(&self, other: &SmtChar) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for SmtChar

fn partial_cmp(&self, other: &SmtChar) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl SaturatingAdd for SmtChar

fn saturating_add(&self, v: &Self) -> Self

Adds another SmtChar to this SmtChar, saturating at the maximum unicode code point.

Examples

use smt_str::SmtChar;
use num_traits::ops::saturating::SaturatingAdd;
let c = SmtChar::from('a');
assert_eq!(c.saturating_add(&SmtChar::new(1)), SmtChar::from('b'));
assert_eq!(c.saturating_add(&SmtChar::new(25)), SmtChar::from('z'));
let c = SmtChar::MAX;
assert_eq!(c.saturating_add(&SmtChar::new(1)), SmtChar::MAX);

impl SaturatingSub for SmtChar

fn saturating_sub(&self, v: &Self) -> Self

Subtracts another SmtChar from this SmtChar, saturating at the minimum unicode code point.

Examples

use smt_str::SmtChar;
let c = SmtChar::from('z');
use num_traits::ops::saturating::SaturatingSub;
assert_eq!(c.saturating_sub(&SmtChar::new(1)), SmtChar::from('y'));
assert_eq!(c.saturating_sub(&SmtChar::new(25)), SmtChar::from('a'));
let c = SmtChar::MIN;
assert_eq!(c.saturating_sub(&SmtChar::new(1)), SmtChar::MIN);

impl Sub for SmtChar

fn sub(self, rhs: SmtChar) -> Self::Output

Subtracts another SmtChar from this SmtChar, shifting the unicode code point. The difference is the difference of the unicode code points of the two SmtChars. Panics if the resulting code point is less than SMT_MIN_CODEPOINT (= 0).

Examples

use smt_str::SmtChar;
let c = SmtChar::from('z');
assert_eq!(c - SmtChar::new(1), SmtChar::from('y'));
assert_eq!(c - SmtChar::new(25), SmtChar::from('a'));

Underflowing the minimum code point panics:

use smt_str::SmtChar;
let c = SmtChar::MIN;
let _ = c - SmtChar::new(1); // panics

type Output = SmtChar

The resulting type after applying the - operator.

impl Copy for SmtChar

impl Eq for SmtChar

impl StructuralPartialEq for SmtChar