Generic program to run the extracted checkers

2 files changed, 48 insertions, 2 deletions

diff --git a/src/extraction/Makefile b/src/extraction/Makefile
index 07a30dd..8919438 100644
--- a/src/extraction/Makefile
+++ b/src/extraction/Makefile
@@ -1,7 +1,9 @@
 # List of user's files and name of the final program (edit this part)
 
-USERFILES=test.ml
-PROGRAM=test
+USERFILES=smtcoq.ml
+PROGRAM=smtcoq
+# USERFILES=test.ml
+# PROGRAM=test
 # USERFILES=../../../../examples/example.ml
 # PROGRAM=../../../../examples/example
 
diff --git a/src/extraction/smtcoq.ml b/src/extraction/smtcoq.ml
new file mode 100644
index 0000000..b88a280
--- /dev/null
+++ b/src/extraction/smtcoq.ml
@@ -0,0 +1,44 @@
+type solver = Zchaff | Verit
+
+
+let usage =
+"
+Usage: smtcoq [solver] problem trace
+Solver:
+  -zchaff   Uses the verifier for ZChaff (default); the problem must be a dimacs file, and the trace, ZChaff unsatisfiability trace
+  -verit    Uses the verifier for ZChaff; the problem must be a SMTLIB2 file, and the trace, veriT unsatisfiability trace
+
+"
+
+
+let string_of_solver = function
+  | Zchaff -> "ZChaff"
+  | Verit -> "veriT"
+
+
+let verifier_of_solver = function
+  | Zchaff -> Zchaff_checker.checker
+  | Verit -> Verit_checker.checker
+
+
+let run s pb trace =
+  Printf.printf "Calling the %s verifier on %s and %s...\n" (string_of_solver s) pb trace;
+  let v = verifier_of_solver s in
+  let t1 = Unix.time () in
+  let res = v pb trace in
+  let t2 = Unix.time () in
+  if res then
+    Printf.printf "The trace was correctly verified in %fs\n" (t2 -. t1)
+  else
+    Printf.printf "The verifier failed to check the trace :-(\n"
+
+
+
+let _ =
+  try
+    let s = if Sys.argv.(1) = "-verit" then Verit else Zchaff in
+    let pb = Sys.argv.((Array.length Sys.argv)-2) in
+    let trace = Sys.argv.((Array.length Sys.argv)-1) in
+    run s pb trace
+  with
+    | _ -> Printf.printf "%s" usage; exit 0