blob: 5ba8ce07ecd74a6a2a059695cf9d68aac60a02d1 (
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
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
try
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
failwith "Error"
with | _ -> Printf.printf "The verifier failed to check the trace :-(\n"
let _ =
let (s,pb,trace) =
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
(s,pb,trace)
with
| _ -> Printf.printf "%s" usage; exit 0 in
run s pb trace
|
