#smt #solver #smt-lib

archived bin+lib smt2parser

Generic parser library for the SMT-LIB-2 format

11 releases (6 breaking)

0.6.1 Sep 8, 2021
0.6.0 Jul 9, 2021
0.5.2 Jul 8, 2021
0.1.0 Jan 28, 2021

#7 in #smt-lib

Download history 2837/week @ 2023-10-22 1979/week @ 2023-10-29 1568/week @ 2023-11-05 1915/week @ 2023-11-12 2065/week @ 2023-11-19 1907/week @ 2023-11-26 2009/week @ 2023-12-03 2300/week @ 2023-12-10 2304/week @ 2023-12-17 1267/week @ 2023-12-24 1654/week @ 2023-12-31 2305/week @ 2024-01-07 2087/week @ 2024-01-14 2123/week @ 2024-01-21 1704/week @ 2024-01-28 1534/week @ 2024-02-04

7,715 downloads per month
Used in 5 crates (4 directly)

MIT/Apache

190KB
5K SLoC

smt2parser

smt2parser on crates.io Documentation License License

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!\")");

Contributing

See the CONTRIBUTING file for how to help out.

License

This project is available under the terms of either the Apache 2.0 license or the MIT license.

Dependencies

~5.5MB
~83K SLoC