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 [char]s, 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.

Yaspar

Yet Another SMT Parser in Rust

This crate provides a parser for the SMT-LIB 2.7 language generated by the LARLPOP parser generator.

Security

See CONTRIBUTING for more information.

License

This project is licensed under the Apache-2.0 License.