From 945ee577c02a052f3f242b98235c1df2f64f7f28 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 18 Mar 2021 13:44:53 -0400
Subject: [PATCH] tool: add ddSMT drivers and short readme

---
 src/tools/README.md             | 13 +++++++++++++
 src/tools/ddsmt_driver_sat.py   | 15 +++++++++++++++
 src/tools/ddsmt_driver_unsat.py | 21 +++++++++++++++++++++
 3 files changed, 49 insertions(+)
 create mode 100644 src/tools/README.md
 create mode 100755 src/tools/ddsmt_driver_sat.py
 create mode 100755 src/tools/ddsmt_driver_unsat.py

diff --git a/src/tools/README.md b/src/tools/README.md
new file mode 100644
index 00000000..ce8571b6
--- /dev/null
+++ b/src/tools/README.md
@@ -0,0 +1,13 @@
+
+## ddSMT
+
+to use ddSMT (from https://github.com/ddsmt/ddSMT/issues):
+
+Assuming `bad_file.smt2` is UNSAT but sidekick returns SAT:
+```sh
+ddsmt.py -vv bad_file.smt2 foo.smt2 ./src/tools/ddsmt_driver_unsat.py
+```
+
+Once it's done, `foo.smt2` should contain a minimal problematic file.
+
+
diff --git a/src/tools/ddsmt_driver_sat.py b/src/tools/ddsmt_driver_sat.py
new file mode 100755
index 00000000..0ea73cee
--- /dev/null
+++ b/src/tools/ddsmt_driver_sat.py
@@ -0,0 +1,15 @@
+#!/usr/bin/python
+
+import subprocess, sys
+
+filename: str = sys.argv[1]
+
+z3_out = subprocess.run([b'z3', filename], capture_output=True).stdout
+if b'sat' not in z3_out or b'unsat' in z3_out or b'error' in z3_out:
+    sys.exit(0)
+
+b_out = subprocess.run([b'./mc2', filename], capture_output=True).stdout
+if b_out.startswith(b'Unsat') and b'Error' not in b_out:
+    print('ohno', file=sys.stderr)
+    sys.exit(1)
+
diff --git a/src/tools/ddsmt_driver_unsat.py b/src/tools/ddsmt_driver_unsat.py
new file mode 100755
index 00000000..b51f84b7
--- /dev/null
+++ b/src/tools/ddsmt_driver_unsat.py
@@ -0,0 +1,21 @@
+#!/usr/bin/python
+
+# minimize unsat problem
+
+import subprocess, sys
+
+filename: str = sys.argv[1]
+
+z3_out = subprocess.run([b'z3', filename], capture_output=True).stdout
+if b'unsat' not in z3_out or b'error' in z3_out:
+    print("z3 failed")
+    sys.exit(1)
+
+b_out = subprocess.run([b'./sidekick', filename], capture_output=True).stdout
+if b'Sat' not in b_out or b'Error' in b_out:
+    print('ohno', file=sys.stderr)
+    print(b_out, sys.stderr)
+    sys.exit(2)
+
+sys.exit(0)
+