Crate smt2parser[−][src]
This crate provides a generic parser for SMT2 commands, as specified by the SMT-LIB-2 standard.
Commands are parsed and immediately visited by a user-provided
implementation of the trait visitors::Smt2Visitor
.
To obtain concrete syntax values, use concrete::SyntaxBuilder
as a
visitor:
let input = b"(echo \"Hello world!\")(exit)"; let mut stream = CommandStream::new( &input[..], concrete::SyntaxBuilder, ); let commands = stream.collect::<Result<Vec<_>, _>>().unwrap(); assert!(matches!(commands[..], [ concrete::Command::Echo {..}, concrete::Command::Exit, ])); assert_eq!(commands[0].to_string(), "(echo \"Hello world!\")");
Modules
concrete | A concrete syntax tree together with building functions (aka parser visitors) and SEXP-printing functions. |
rewriter | Rewriting of Smt2 values |
stats | A demo implementation of visiting traits that counts things. |
visitors | The visiting traits expected by the SMT2 parser. |
Structs
CommandStream | Parse the input data and return a stream of interpreted SMT2 commands |
Position | Record a position in the input stream. |
Type Definitions
Binary | SMT2 binary values. |
Decimal | SMT2 decimal values. |
Hexadecimal | SMT2 hexadecimal values. |
Nibble | A base-16 digit. |
Numeral | SMT2 numeral values. |