#smt-lib #smt #solver

bin+lib smt2parser

SMT-LIB-2 格式的通用解析库

11 个版本 (6 个重大更新)

0.6.1 2021年9月8日
0.6.0 2021年7月9日
0.5.2 2021年7月8日
0.1.0 2021年1月28日

#smt-lib 中排名第 10

Download history 1626/week @ 2024-03-14 1355/week @ 2024-03-21 1364/week @ 2024-03-28 1555/week @ 2024-04-04 1283/week @ 2024-04-11 1439/week @ 2024-04-18 1598/week @ 2024-04-25 1266/week @ 2024-05-02 1802/week @ 2024-05-09 1850/week @ 2024-05-16 1780/week @ 2024-05-23 1763/week @ 2024-05-30 1985/week @ 2024-06-06 3123/week @ 2024-06-13 2809/week @ 2024-06-20 1778/week @ 2024-06-27

每月下载量 10,005
5 个crate中使用(4个直接使用)

MIT/Apache

190KB
5K SLoC

smt2parser

smt2parser on crates.io Documentation License License

此crate提供了一个适用于SMT2命令的通用解析器,这些命令由SMT-LIB-2标准指定。

命令将由用户提供的一个实现 visitors::Smt2Visitor 的特质进行解析并立即访问。

要获取具体语法值,请使用 concrete::SyntaxBuilder 作为访问者

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文件了解如何提供帮助。

许可证

此项目可在Apache 2.0许可证MIT许可证的条款下使用。

依赖项

~6.5MB
~100K SLoC