tool: add ddSMT drivers and short readme

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.
+
+

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)
+

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)
+