forked from cubicle-model-checker/cubicle
-
Notifications
You must be signed in to change notification settings - Fork 0
/
instantiation.ml
185 lines (155 loc) · 6.46 KB
/
instantiation.ml
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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
(**************************************************************************)
(* *)
(* Cubicle *)
(* *)
(* Copyright (C) 2011-2014 *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* *)
(* This file is distributed under the terms of the Apache Software *)
(* License version 2.0 *)
(* *)
(**************************************************************************)
open Format
open Options
open Ast
open Util
open Types
module H = Hstring
(*********************************************)
(* all permutations excepted impossible ones *)
(*********************************************)
let filter_impos perms impos =
List.filter (fun sigma ->
not (List.exists (List.for_all
(fun (x,y) -> H.list_mem_couple (x,y) sigma))
impos))
perms
let rec all_permutations_impos l1 l2 impos =
filter_impos (Variable.all_permutations l1 l2) impos
(****************************************************)
(* Improved relevant permutations (still quadratic) *)
(****************************************************)
let list_rev_split =
List.fold_left (fun (l1, l2) (x, y) -> x::l1, y::l2) ([], [])
let list_rev_combine =
List.fold_left2 (fun acc x1 x2 -> (x1, x2) :: acc) []
exception NoPermutations
let find_impossible a1 lx1 op c1 i2 a2 n2 impos obvs =
let i2 = ref i2 in
while !i2 < n2 do
let a2i = a2.(!i2) in
(match a2i, op with
| Atom.Comp (Access (a2, _), _, _), _ when not (H.equal a1 a2) ->
i2 := n2
| Atom.Comp (Access (a2, lx2), Eq,
(Elem (_, Constr) | Elem (_, Glob) | Arith _ as c2)), (Neq | Lt)
when Term.compare c1 c2 = 0 ->
if List.for_all2
(fun x1 x2 -> H.list_mem_couple (x1, x2) obvs) lx1 lx2 then
raise NoPermutations;
impos := (list_rev_combine lx1 lx2) :: !impos
| Atom.Comp (Access (a2, lx2), (Neq | Lt),
(Elem (_, Constr) | Elem (_, Glob) | Arith _ as c2)), Eq
when Term.compare c1 c2 = 0 ->
if List.for_all2
(fun x1 x2 -> H.list_mem_couple (x1, x2) obvs) lx1 lx2 then
raise NoPermutations;
impos := (list_rev_combine lx1 lx2) :: !impos
| Atom.Comp (Access (a2, lx2), Eq, (Elem (_, Constr) as c2)), Eq
when Term.compare c1 c2 <> 0 ->
if List.for_all2
(fun x1 x2 -> H.list_mem_couple (x1, x2) obvs) lx1 lx2 then
raise NoPermutations;
impos := (list_rev_combine lx1 lx2) :: !impos
| _ -> ());
incr i2
done
let clash_binding (x,y) l =
try not (H.equal (H.list_assoc_inv y l) x)
with Not_found -> false
let add_obv ((x,y) as p) obvs =
begin
try if clash_binding p !obvs || not (H.equal (H.list_assoc x !obvs) y) then
raise NoPermutations
with Not_found -> obvs := p :: !obvs
end
let obvious_impossible a1 a2 =
let n1 = Array.length a1 in
let n2 = Array.length a2 in
let obvs = ref [] in
let impos = ref [] in
let i1 = ref 0 in
let i2 = ref 0 in
while !i1 < n1 && !i2 < n2 do
let a1i = a1.(!i1) in
let a2i = a2.(!i2) in
(match a1i, a2i with
| Atom.Comp (Elem (x1, sx1), Eq, Elem (y1, sy1)),
Atom.Comp (Elem (x2, sx2), Eq, Elem (y2, sy2)) ->
begin
match sx1, sy1, sx2, sy2 with
| Glob, Constr, Glob, Constr
when H.equal x1 x2 && not (H.equal y1 y2) ->
raise NoPermutations
| Glob, Var, Glob, Var when H.equal x1 x2 ->
add_obv (y1,y2) obvs
| Glob, Var, Var, Glob when H.equal x1 y2 ->
add_obv (y1,x2) obvs
| Var, Glob, Glob, Var when H.equal y1 x2 ->
add_obv (x1,y2) obvs
| Var, Glob, Var, Glob when H.equal y1 y2 ->
add_obv (x1,x2) obvs
| _ -> ()
end
| Atom.Comp (Elem (x1, sx1), Eq, Elem (y1, sy1)),
Atom.Comp (Elem (x2, sx2), (Neq | Lt), Elem (y2, sy2)) ->
begin
match sx1, sy1, sx2, sy2 with
| Glob, Constr, Glob, Constr
when H.equal x1 x2 && H.equal y1 y2 ->
raise NoPermutations
| _ -> ()
end
| Atom.Comp (Access (a1, lx1), op,
(Elem (_, Constr) | Elem (_, Glob) | Arith _ as c1)),
Atom.Comp (Access (a, _), _,
(Elem (_, Constr) | Elem (_, Glob) | Arith _ ))
when H.equal a1 a ->
find_impossible a1 lx1 op c1 !i2 a2 n2 impos !obvs
| _ -> ());
if Atom.compare a1i a2i <= 0 then incr i1 else incr i2
done;
!obvs, !impos
(*******************************************)
(* Relevant permuations for fixpoint check *)
(*******************************************)
(****************************************************)
(* Find relevant quantifier instantiation for *)
(* \exists z_1,...,z_n. np => \exists x_1,...,x_m p *)
(****************************************************)
let relevant_permutations np p l1 l2 =
TimeRP.start ();
try
let obvs, impos = obvious_impossible p np in
let obvl1, obvl2 = list_rev_split obvs in
let l1 = List.filter (fun b -> not (H.list_mem b obvl1)) l1 in
let l2 = List.filter (fun b -> not (H.list_mem b obvl2)) l2 in
let perm = all_permutations_impos l1 l2 impos in
let r = List.rev_map (List.rev_append obvs) perm in
(* assert (List.for_all Variable.well_formed_subst r); *)
TimeRP.pause ();
r
with NoPermutations -> TimeRP.pause (); []
let relevant ~of_cube ~to_cube =
let of_vars, to_vars = of_cube.Cube.vars, to_cube.Cube.vars in
let dif = Variable.extra_vars of_vars to_vars in
let to_vars = if dif = [] then to_vars else to_vars@dif in
relevant_permutations to_cube.Cube.array of_cube.Cube.array of_vars to_vars
let exhaustive ~of_cube ~to_cube =
let of_vars, to_vars = of_cube.Cube.vars, to_cube.Cube.vars in
let dif = Variable.extra_vars of_vars to_vars in
let to_vars = if dif = [] then to_vars else to_vars@dif in
Variable.all_permutations of_vars to_vars