flussab-btor2: flussab based BTOR2 parser

Cargo.toml

@@ -1,6 +1,6 @@
 [workspace]
 resolver = "2"
-members = ["flussab", "flussab-cnf", "flussab-aiger"]
+members = ["flussab", "flussab-cnf", "flussab-aiger", "flussab-btor2"]
 
 [profile.release]
 debug = true # Enables profiling with perf

flussab-btor2/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "flussab-btor2"
+version = "0.1.0"
+edition = "2021"
+description = "BTOR2 file format parser and writer"
+repository = "https://github.com/jix/flussab"
+license = "0BSD"
+readme = "README.md"
+keywords = ["btor", "btor2", "parser", "writer"]
+categories = ["parser-implementations", "encoding"]
+
+[dependencies]
+flussab = { version = "0.3.1", path = "../flussab" }
+thiserror = "1.0.50"
+bstr = "1.10.0"

flussab-btor2/LICENSE

@@ -0,0 +1,20 @@
+Copyrights in this software are retained by their respective authors. See the
+version control history for full authorship information.
+
+Except as otherwise noted (below and/or in individual files), this software is
+licensed under the following terms ("Zero-Clause BSD"):
+
+    Permission to use, copy, modify, and/or distribute this software for any
+    purpose with or without fee is hereby granted.
+
+    THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+    WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+    MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+    SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+    WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+    ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
+    IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+
+Unless you explicitly state otherwise, any contribution intentionally submitted
+for inclusion in this software by you shall be under the terms and conditions
+of the above license, without any additional terms or conditions.

flussab-btor2/README.md

@@ -0,0 +1,30 @@
+# Flussab AIGER
+
+[![github][github-badge]][github]
+[![crates.io][crate-badge]][crate]
+[![docs.rs][docs-badge]][docs]
+
+Parsing and writing of the [BTOR2 file format][btor] for representing circuits
+for word-level hardware model-checking. This library provides an efficient
+streaming parser for the BTOR2 file format as well as a BTOR2 writer.
+
+[btor]: https://github.com/Boolector/btor2tools
+[flussab]: https://crates.io/crates/flussab
+
+## License
+
+This software is available under the Zero-Clause BSD license, see
+[LICENSE](LICENSE) for full licensing information.
+
+### Contribution
+
+Unless you explicitly state otherwise, any contribution intentionally submitted
+for inclusion in this software by you shall be licensed as defined in
+[LICENSE](LICENSE).
+
+[github]: https://github.com/jix/flussab
+[crate]: https://crates.io/crates/flussab-btor2
+[docs]: https://docs.rs/flussab-btor2/*/flussab_btor2
+[github-badge]: https://img.shields.io/badge/github-jix/flussab-blueviolet?style=flat-square
+[crate-badge]: https://img.shields.io/crates/v/flussab-btor2?style=flat-square
+[docs-badge]: https://img.shields.io/badge/docs.rs-flussab_btor2-informational?style=flat-square

flussab-btor2/examples/roundtrip.rs

@@ -0,0 +1,26 @@
+use std::io::Write;
+
+use flussab::DeferredWriter;
+
+use flussab_btor2::{ParseError, Parser};
+
+fn main() {
+    if let Err(err) = main_err() {
+        eprintln!("error: {err}");
+    }
+}
+
+fn main_err() -> Result<(), ParseError> {
+    let stdin = std::io::stdin();
+    let stdout = std::io::stdout();
+
+    let mut parser = Parser::from_read(stdin, Default::default())?;
+    let mut target = DeferredWriter::from_write(stdout);
+
+    while let Some(line) = parser.next_line()? {
+        line.write_into(&mut target);
+    }
+    target.flush()?;
+
+    Ok(())
+}