Crate smt2parser

Source
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§

CommandStream
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.