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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
(**************************************************************************)
(* *)
(* 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 SmtCertif
open SmtForm
open SatAtom
open SmtTrace
open Zchaff
open Sat_checker
let mkInt = ExtrNative.of_int
let mkArray = ExtrNative.of_array
let make_roots first last =
let roots = Array.make (last.id + 2) (mkArray (Array.make 1 (mkInt 0))) in
let mk_elem l =
let x = match Form.pform l with
| Fatom x -> x + 2
| _ -> assert false in
mkInt (if Form.is_pos l then x lsl 1 else (x lsl 1) lxor 1) in
let r = ref first in
while !r.id < last.id do
let root = Array.of_list (get_val !r) in
let croot = Array.make (Array.length root + 1) (mkInt 0) in
Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
roots.(!r.id) <- mkArray croot;
r := next !r
done;
let root = Array.of_list (get_val !r) in
let croot = Array.make (Array.length root + 1) (mkInt 0) in
Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
roots.(!r.id) <- mkArray croot;
mkArray roots
let to_coq to_lit (cstep,
cRes, cImmFlatten,
cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj,
cImmBuildProj,cImmBuildDef,cImmBuildDef2,
cEqTr, cEqCgr, cEqCgrP,
cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim, cHole) confl =
let step_to_coq c =
match c.kind with
| Res res ->
let size = List.length res.rtail + 3 in
let args = Array.make size (mkInt 0) in
args.(0) <- mkInt (get_pos res.rc1);
args.(1) <- mkInt (get_pos res.rc2);
let l = ref res.rtail in
for i = 2 to size - 2 do
match !l with
| c::tl ->
args.(i) <- mkInt (get_pos c);
l := tl
| _ -> assert false
done;
Sat_Checker.Res (mkInt (get_pos c), mkArray args)
| _ -> assert false in
let def_step =
Sat_Checker.Res (mkInt 0, mkArray [|mkInt 0|]) in
let r = ref confl in
let nc = ref 0 in
while not (isRoot !r.kind) do r := prev !r; incr nc done;
let last_root = !r in
let size = !nc in
let max = (Parray.trunc_size (Uint63.of_int 4194303)) - 1 in
let q,r1 = size / max, size mod max in
let trace =
let len = if r1 = 0 then q + 1 else q + 2 in
Array.make len (mkArray [|def_step|]) in
for j = 0 to q - 1 do
let tracej = Array.make (Parray.trunc_size (Uint63.of_int 4194303)) def_step in
for i = 0 to max - 1 do
r := next !r;
tracej.(i) <- step_to_coq !r;
done;
trace.(j) <- mkArray tracej
done;
if r1 <> 0 then begin
let traceq = Array.make (r1 + 1) def_step in
for i = 0 to r1-1 do
r := next !r;
traceq.(i) <- step_to_coq !r;
done;
trace.(q) <- mkArray traceq
end;
(mkArray trace, last_root)
let checker fdimacs ftrace =
SmtTrace.clear ();
let _,first,last,reloc = import_cnf fdimacs in
let d = make_roots first last in
let max_id, confl = import_cnf_trace reloc ftrace first last in
let (tres,_) =
to_coq (fun _ -> assert false) certif_ops confl in
let certif =
Sat_Checker.Certif (mkInt (max_id + 1), tres, mkInt (get_pos confl)) in
Sat_Checker.checker d certif
|
