Skip to content

Commit

Permalink
Crate for AIGER files + various smaller changes
Browse files Browse the repository at this point in the history
  • Loading branch information
jix committed Nov 14, 2023
1 parent fd7d41a commit 033aa3d
Show file tree
Hide file tree
Showing 15 changed files with 3,383 additions and 3 deletions.
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[workspace]
members = ["flussab", "flussab-cnf"]
members = ["flussab", "flussab-cnf", "flussab-aiger"]

[profile.release]
debug = true # Enables profiling with perf
17 changes: 17 additions & 0 deletions flussab-aiger/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
[package]
name = "flussab-aiger"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
flussab = { version = "0.3.0", path = "../flussab" }
thiserror = "1.0.30"
num-traits = "0.2.14"
zwohash = "0.1.2"

[dev-dependencies]
flussab-cnf = { version = "0.3.0", path = "../flussab-cnf" }
tempfile = "3.3.0"
duct = "0.13.6"
39 changes: 39 additions & 0 deletions flussab-aiger/examples/aagtoaig.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
use std::io::Write;

use flussab::DeferredWriter;

use flussab_aiger::{
aig::{Renumber, RenumberConfig},
ascii, binary, Error,
};

fn main() {
if let Err(err) = main_err() {
eprintln!("error: {err}");
}
}

fn main_err() -> Result<(), Error<u32>> {
let stdin = std::io::stdin();
let stdout = std::io::stdout();

let aag_reader = ascii::Parser::<u32>::from_read(stdin.lock(), ascii::Config::default())?;

let aag = aag_reader.parse()?;

let (aig, _) = Renumber::renumber_aig(
RenumberConfig::default()
.trim(true)
.structural_hash(true)
.const_fold(true),
&aag,
)?;

let aig_writer = DeferredWriter::from_write(stdout.lock());
let mut aag_writer = binary::Writer::<u32>::new(aig_writer);

aag_writer.write_ordered_aig(&aig);

aag_writer.flush()?;
Ok(())
}
78 changes: 78 additions & 0 deletions flussab-aiger/examples/roundtrip_aag.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
use flussab::DeferredWriter;

use flussab_aiger::{ascii, ParseError};

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 aag_reader = ascii::Parser::<u32>::from_read(stdin.lock(), ascii::Config::default())?;
let mut aag_writer = DeferredWriter::from_write(stdout.lock());
let aag_writer = ascii::Writer::<u32>::new(&mut aag_writer);

aag_writer.write_header(aag_reader.header());

let mut aag_reader = aag_reader.inputs()?;
while let Some(input) = aag_reader.next_input()? {
aag_writer.write_lit(input);
}

let mut aag_reader = aag_reader.latches()?;
while let Some(latch) = aag_reader.next_latch()? {
aag_writer.write_latch(latch);
}

let mut aag_reader = aag_reader.outputs()?;
while let Some(output) = aag_reader.next_output()? {
aag_writer.write_lit(output);
}

let mut aag_reader = aag_reader.bad_state_properties()?;
while let Some(bad_state_property) = aag_reader.next_bad_state_property()? {
aag_writer.write_lit(bad_state_property);
}

let mut aag_reader = aag_reader.invariant_constraints()?;
while let Some(invariant_constraint) = aag_reader.next_invariant_constraint()? {
aag_writer.write_lit(invariant_constraint);
}

let mut aag_reader = aag_reader.justice_properties()?;
while let Some(justice_property_size) = aag_reader.next_justice_property_size()? {
aag_writer.write_count(justice_property_size);
}

let mut aag_reader = aag_reader.justice_property_local_fairness_constraints()?;
while let Some(justice_property_local_fairness_constraint) =
aag_reader.next_justice_property_local_fairness_constraint()?
{
aag_writer.write_lit(justice_property_local_fairness_constraint);
}

let mut aag_reader = aag_reader.fairness_constraints()?;
while let Some(fairness_constraint) = aag_reader.next_fairness_constraint()? {
aag_writer.write_lit(fairness_constraint);
}

let mut aag_reader = aag_reader.and_gates()?;
while let Some(and_gate) = aag_reader.next_and_gate()? {
aag_writer.write_and_gate(and_gate);
}

let mut aag_reader = aag_reader.symbols()?;
while let Some(symbol) = aag_reader.next_symbol()? {
aag_writer.write_symbol(&symbol);
}

if let Some(comment) = aag_reader.comment()? {
aag_writer.write_comment(comment);
}

Ok(())
}
24 changes: 24 additions & 0 deletions flussab-aiger/examples/roundtrip_aag_buffered.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
use flussab::DeferredWriter;

use flussab_aiger::{ascii, ParseError};

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 aag_reader = ascii::Parser::<u32>::from_read(stdin.lock(), ascii::Config::default())?;

let aig = aag_reader.parse()?;

let mut aag_writer = DeferredWriter::from_write(stdout.lock());
let aag_writer = ascii::Writer::<u32>::new(&mut aag_writer);

aag_writer.write_aig(&aig);
Ok(())
}
24 changes: 24 additions & 0 deletions flussab-aiger/examples/roundtrip_aig_buffered.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
use flussab::DeferredWriter;

use flussab_aiger::{ascii, binary, ParseError};

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 aig_reader = binary::Parser::<u32>::from_read(stdin.lock(), binary::Config::default())?;

let aig = aig_reader.parse()?;

let mut aag_writer = DeferredWriter::from_write(stdout.lock());
let aag_writer = ascii::Writer::<u32>::new(&mut aag_writer);

aag_writer.write_ordered_aig(&aig);
Ok(())
}
Loading

0 comments on commit 033aa3d

Please sign in to comment.