Expand description
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 stream = CommandStream::new(
&input[..],
concrete::SyntaxBuilder,
Some("optional/path/to/file".to_string()),
);
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!\")");
Re-exports§
pub use concrete::Error;
Modules§
- concrete
- A concrete syntax tree together with building functions (aka parser visitors) and SEXP-printing functions.
- renaming
- Utilities for name resolution and renaming of bound symbols.
- 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§
- Command
Stream - Parse the input data and return a stream of interpreted SMT2 commands
- Position
- A position in the input. Record a position in the input stream.
Type Aliases§
- Binary
- SMT2 binary values.
- Decimal
- SMT2 decimal values.
- Hexadecimal
- SMT2 hexadecimal values.
- Nibble
- A base-16 digit.
- Numeral
- SMT2 numeral values.