Support abc's dsec solver

Author: georgerennie

Valaig/External.lean

@@ -1,2 +1,3 @@
 import Valaig.External.Basic
 import Valaig.External.Ric3
+import Valaig.External.Abc

Valaig/External/Abc.lean

@@ -0,0 +1,25 @@
+import Valaig.External.Basic
+
+namespace Valaig.External
+
+def Abc.dsec (timeoutMs : Option Nat := none) : SafetyAigerMC :=
+  {
+    timeoutMs,
+    supportsAag := false,
+    interpretOutput,
+    safetyArgs,
+  }
+where
+  safetyArgs (problem : System.FilePath) : IO.Process.SpawnArgs :=
+    let cmd := "abc"
+    let cmdStr := s!"read {problem.toString}; "
+    let args := #["-c", cmdStr]
+    { cmd, args }
+
+  interpretOutput (out : IO.Process.Output) : EResult := do
+    if out.stdout.contains "Networks are equivalent." then
+      return Result.proof
+    else
+      return Result.counterexample
+
+end Valaig.External

Valaig/External/Basic.lean

@@ -8,6 +8,7 @@ open Valaig.Aig
 
 structure ExternalMC where
   timeoutMs : Option Nat := none
+  supportsAag : Bool := true
   interpretOutput (output : IO.Process.Output) : EResult
 
 structure SafetyAigerMC extends ExternalMC where
@@ -71,9 +72,15 @@ def checkSafety (config : SafetyAigerMC) (aig : Aiger) : IO EResult := do
   IO.FS.withTempDir fun dir => do
     -- Some solvers need the extension to be aag to work correctly so we create
     -- such a file rather than just using withTempFile
-    let path := dir / "model.aag"
-    IO.FS.withFile path .write fun handle => do
+    let aagPath := dir / "model.aag"
+    let aigPath := dir / "model.aig"
+    IO.FS.withFile aagPath .write fun handle => do
       aig.writeAag <| IO.FS.Stream.ofHandle handle
+
+      if ¬config.supportsAag then
+        let _ ← runProcess none { cmd := "aigtoaig", args := #[aagPath.toString, aigPath.toString] }
+
+      let path := if config.supportsAag then aagPath else aigPath
       let out ← runProcess config.timeoutMs (config.safetyArgs path)
       return out >>= config.interpretOutput