Crate yaspar 

Yaspar

Yaspar is a parsing library strictly following the SMTLib standard.

It is composed of two parts:

1. A tokenizer, which can be found in crate::tokens::Tokenizer; given an iterator of chars, it tokenizes them into an iterator of SMTLib tokens;
2. A number of parsers, in the form of callbacks; given an implementation of the corresponding trait, e.g. crate::action::ParsingAction, a parser in crate::smtlib2 parses an iteration of tokens, and callbacks the functions defined in the trait at appropriate timings, or errors out, if the tokens are grammatically mal-formed.

One example of how to use this crate is to see crate::action::UnitAction. This object trivially admits all parsing actions, so it accepts and only accepts grammatically well-formed SMT scripts.

Re-exports

pub use crate::tokens::Tokenizer;

Modules

action

ast

The ast module contains the types that represent the values parsed from smt-lib.

position

smtlib2

tokens

A Tokenizer for SMTLib

Structs

Parser

Functions

binary_to_string

assume len >= the necessary number of bits to encode bytes

hex_to_string

assume len >= the necessary number of hex codes to encode bytes

is_simple_symbol

if s is a symbol, decide whether it is a simple symbol

smt_quoted_symbol_to_string

converts a quoted symbol representation to a string

smt_string_to_string

converts an SMT string into a normal Rust string

tokenize_str

obtain a tokenizer from a string