From f14aaa57c4bb20c36b8e09252443948c2b3a56c1 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 11 Jan 2023 18:36:06 +0100
Subject: [PATCH] avy: Fold aiger model using abc to support assumptions

---
 sbysrc/sby_core.py         | 12 ++++++++++++
 sbysrc/sby_engine_aiger.py |  7 +++++--
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index f0fcf29..ae28b6a 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -1146,6 +1146,18 @@ class SbyTask(SbyConfig):
 
             return [proc]
 
+        if model_name == "aig_fold":
+            proc = SbyProc(
+                self,
+                model_name,
+                self.model("aig"),
+                f"""cd {self.workdir}/model; {self.exe_paths["abc"]} -c 'read_aiger design_aiger.aig; fold; strash; write_aiger design_aiger_fold.aig'""",
+                logfile=open(f"{self.workdir}/model/design_aiger_fold.log", "w")
+            )
+            proc.checkretcode = True
+
+            return [proc]
+
         self.error(f"Invalid model name: {model_name}")
 
     def model(self, model_name):
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index d6e14d8..d7a5a31 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -31,6 +31,8 @@ def run(mode, task, engine_idx, engine):
 
     status_2 = "UNKNOWN"
 
+    model_variant = ""
+
     if solver_args[0] == "suprove":
         if mode not in ["live", "prove"]:
             task.error("The aiger solver 'suprove' is only supported in live and prove modes.")
@@ -39,6 +41,7 @@ def run(mode, task, engine_idx, engine):
         solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:])
 
     elif solver_args[0] == "avy":
+        model_variant = "_fold"
         if mode != "prove":
             task.error("The aiger solver 'avy' is only supported in prove mode.")
         solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
@@ -71,8 +74,8 @@ def run(mode, task, engine_idx, engine):
     proc = SbyProc(
         task,
         f"engine_{engine_idx}",
-        task.model("aig"),
-        f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig",
+        task.model(f"aig{model_variant}"),
+        f"cd {task.workdir}; {solver_cmd} model/design_aiger{model_variant}.aig",
         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
     )
     if solver_args[0] not in ["avy"]: