From b8a001eab29e40a0c5821bcbace102f937b0fa87 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Sun, 8 Sep 2024 16:04:26 +0200
Subject: [PATCH] Add support for the imctk-eqy-engine

This is not added to the documentation, as this is currently intended
for internal use only.
---
 sbysrc/sby_core.py         |  1 +
 sbysrc/sby_engine_aiger.py | 32 +++++++++++++++++++++++++++++++-
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index c366e1b..a1c9d02 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -851,6 +851,7 @@ def __init__(self, sbyconfig, workdir, early_logs, reusedir, taskloop=None, logf
             "avy": os.getenv("AVY", "avy"),
             "btormc": os.getenv("BTORMC", "btormc"),
             "pono": os.getenv("PONO", "pono"),
+            "imctk-eqy-engine": os.getenv("IMCTK_EQY_ENGINE", "imctk-eqy-engine"),
         }
 
         self.taskloop = taskloop or SbyTaskloop()
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index fbdf999..934269a 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -16,7 +16,7 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import re, os, getopt, click
+import re, os, getopt, click, json
 from sby_core import SbyProc
 from sby_sim import sim_witness_trace
 
@@ -32,6 +32,7 @@ def run(mode, task, engine_idx, engine):
     status_2 = "UNKNOWN"
 
     model_variant = ""
+    json_output = False
 
     if solver_args[0] == "suprove":
         if mode not in ["live", "prove"]:
@@ -52,6 +53,14 @@ def run(mode, task, engine_idx, engine):
         solver_cmd = " ".join([task.exe_paths["aigbmc"], str(task.opt_depth - 1)] + solver_args[1:])
         status_2 = "PASS"  # aigbmc outputs status 2 when BMC passes
 
+    elif solver_args[0] == "imctk-eqy-engine":
+        model_variant = "_fold"
+        json_output = True
+        if mode != "prove":
+            task.error("The aiger solver 'imctk-eqy-engine' is only supported in prove mode.")
+        args = ["--bmc-depth", str(task.opt_depth), "--jsonl-output"]
+        solver_cmd = " ".join([task.exe_paths["imctk-eqy-engine"], *args, *solver_args[1:]])
+
     else:
         task.error(f"Invalid solver command {solver_args[0]}.")
 
@@ -91,6 +100,27 @@ def output_callback(line):
         nonlocal produced_cex
         nonlocal end_of_cex
 
+        if json_output:
+            # Forward log messages, but strip the prefix containing runtime and memory stats
+            if not line.startswith('{'):
+                print(line, file=proc.logfile, flush=True)
+                matched = re.match(r".*(TRACE|DEBUG|INFO|WARN|ERROR) (.*)", line)
+                if matched:
+                    if matched[1] == "INFO":
+                        task.log(matched[2])
+                    else:
+                        task.log(f"{matched[1]} {matched[2]}")
+                return None
+            event = json.loads(line)
+            if "aiw" in event:
+                print(event["aiw"], file=aiw_file)
+            if "status" in event:
+                if event["status"] == "pass":
+                    proc_status = "PASS"
+                elif event["status"] == "fail":
+                    proc_status = "FAIL"
+            return None
+
         if proc_status is not None:
             if not end_of_cex and not produced_cex and line.isdigit():
                 produced_cex = True