blob: 08f45a121bc9b956bfdbda2f24413bcd898bc31e (
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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Add Rec LoadPath "../src" as SMTCoq.
Require Import SMTCoq.
Require Import Bool PArray Int63 List ZArith.
Local Open Scope int63_scope.
(* zChaff vernacular commands *)
Time Zchaff_Checker "sat1.cnf" "sat1.zlog".
Time Zchaff_Checker "sat2.cnf" "sat2.zlog".
Time Zchaff_Checker "sat3.cnf" "sat3.zlog".
Time Zchaff_Checker "sat5.cnf" "sat5.zlog".
Time Zchaff_Checker "sat6.cnf" "sat6.zlog".
Time Zchaff_Checker "sat7.cnf" "sat7.zlog".
Time Zchaff_Checker "hole4.cnf" "hole4.zlog".
(* Time Zchaff_Checker "cmu-bmc-barrel6.cnf" "cmu-bmc-barrel6.zlog". *)
(* Time Zchaff_Checker "velev-sss-1.0-05.cnf" "velev-sss-1.0-05.zlog". *)
Time Zchaff_Theorem sat1 "sat1.cnf" "sat1.zlog".
Time Zchaff_Theorem sat2 "sat2.cnf" "sat2.zlog".
Time Zchaff_Theorem sat3 "sat3.cnf" "sat3.zlog".
Time Zchaff_Theorem sat5 "sat5.cnf" "sat5.zlog".
Time Zchaff_Theorem sat6 "sat6.cnf" "sat6.zlog".
Time Zchaff_Theorem sat7 "sat7.cnf" "sat7.zlog".
Time Zchaff_Theorem hole4 "hole4.cnf" "hole4.zlog".
Parse_certif_zchaff d1 t1 "sat1.cnf" "sat1.zlog".
Compute Sat_Checker.checker d1 t1.
Parse_certif_zchaff d2 t2 "sat2.cnf" "sat2.zlog".
Compute Sat_Checker.checker d2 t2.
Parse_certif_zchaff d3 t3 "sat3.cnf" "sat3.zlog".
Compute Sat_Checker.checker d3 t3.
Parse_certif_zchaff d5 t5 "sat5.cnf" "sat5.zlog".
Compute Sat_Checker.checker d5 t5.
Parse_certif_zchaff d6 t6 "sat6.cnf" "sat6.zlog".
Compute Sat_Checker.checker d6 t6.
Parse_certif_zchaff d7 t7 "sat7.cnf" "sat7.zlog".
Compute Sat_Checker.checker d7 t7.
Parse_certif_zchaff dhole4 thole4 "hole4.cnf" "hole4.zlog".
Compute Sat_Checker.checker dhole4 thole4.
(* Parse_certif_zchaff dcmubmcbarrel6 tcmubmcbarrel6 "cmu-bmc-barrel6.cnf" "cmu-bmc-barrel6.zlog". *)
(* Compute Sat_Checker.checker dcmubmcbarrel6 tcmubmcbarrel6. *)
(* Parse_certif_zchaff dvelevsss1005 tvelevsss1005 "velev-sss-1.0-05.cnf" "velev-sss-1.0-05.zlog". *)
(* Compute Sat_Checker.checker dvelevsss1005 tvelevsss1005. *)
|
