blob: b88a280178a5fc0dc6eb8e29cf75a2b89fc5c44b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
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
|
