blob: f39382264ae4dec9c3bafb900b3d4094db0892aa (
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
61
62
63
64
65
66
67
68
69
70
71
|
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Smtcoq_extr
type solver = Zchaff | Verit
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 usage_msg = "Usage: smtcoq [-verit|-zchaff] <problem> <trace>" in
let verit = ref true in
let input_files = ref [] in
let anon_fun filename =
input_files := filename::!input_files
in
let usage_verit = "Uses the verifier for veriT (default); the problem must be a SMTLIB2 file, and the trace, veriT unsatisfiability trace" in
let usage_zchaff = "Uses the verifier for ZChaff; the problem must be a dimacs file, and the trace, ZChaff unsatisfiability trace" in
let speclist =
[("-verit", Arg.Set verit, usage_verit);
("-zchaff", Arg.Clear verit, usage_zchaff)]
in
Arg.parse speclist anon_fun usage_msg;
let s = if !verit then Verit else Zchaff in
let (pb, trace) =
try
match !input_files with
| [trace; pb] -> (pb, trace)
| _ -> assert false
with
| _ -> Arg.usage speclist usage_msg; exit 0
in
run s pb trace
|
