From 8fd9cd6c0f1c5e33da01d6e6cefddb4a1ae92a18 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cornell.edu>
Date: Tue, 10 Dec 2024 14:02:08 -0500
Subject: [PATCH] cond synth: add espressor output

---
 tools/egraphs-cond-synth/.gitignore  |  1 +
 tools/egraphs-cond-synth/src/main.rs | 30 ++++++++++++++++++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/tools/egraphs-cond-synth/.gitignore b/tools/egraphs-cond-synth/.gitignore
index 504a08a..65a63de 100644
--- a/tools/egraphs-cond-synth/.gitignore
+++ b/tools/egraphs-cond-synth/.gitignore
@@ -1,2 +1,3 @@
 /*.json
 /*.csv
+/*.txt
diff --git a/tools/egraphs-cond-synth/src/main.rs b/tools/egraphs-cond-synth/src/main.rs
index cf2b72b..9749202 100644
--- a/tools/egraphs-cond-synth/src/main.rs
+++ b/tools/egraphs-cond-synth/src/main.rs
@@ -49,6 +49,11 @@ struct Args {
         help = "writes assignments, features and equivalence into a CSV table"
     )]
     write_csv: Option<PathBuf>,
+    #[arg(
+        long,
+        help = "writes features and equivalence into a PLA-style input file for espresso"
+    )]
+    write_espresso: Option<PathBuf>,
     #[arg(value_name = "RULE", index = 1)]
     rule: String,
 }
@@ -121,6 +126,10 @@ fn main() {
         write_csv(filename, &samples, &features).expect("failed to write CSV");
     }
 
+    if let Some(filename) = args.write_espresso {
+        write_espresso(filename, &features).expect("failed to write espresso file");
+    }
+
     if args.bdd_formula {
         let summarize_start = std::time::Instant::now();
         let formula = bdd_summarize(&features);
@@ -169,3 +178,24 @@ fn write_csv(
 
     Ok(())
 }
+
+fn write_espresso(filename: impl AsRef<Path>, features: &FeatureResult) -> std::io::Result<()> {
+    let mut o = std::io::BufWriter::new(std::fs::File::create(filename)?);
+
+    // the inputs are the features
+    writeln!(o, ".i {}", features.num_features())?;
+    // the output is whether it is equivalent or not
+    writeln!(o, ".o 1")?;
+
+    for (features, is_eq) in features.iter() {
+        for feature_on in features.iter() {
+            write!(o, "{}", (*feature_on) as u8)?;
+        }
+        writeln!(o, " {}", is_eq as u8)?;
+    }
+
+    // end
+    writeln!(o, ".e")?;
+
+    Ok(())
+}