39348
|
1 |
(* ========================================================================= *)
|
|
2 |
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
|
39349
|
3 |
(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
|
39348
|
4 |
(* ========================================================================= *)
|
|
5 |
|
|
6 |
structure Subsume :> Subsume =
|
|
7 |
struct
|
|
8 |
|
|
9 |
open Useful;
|
|
10 |
|
|
11 |
(* ------------------------------------------------------------------------- *)
|
|
12 |
(* Helper functions. *)
|
|
13 |
(* ------------------------------------------------------------------------- *)
|
|
14 |
|
|
15 |
fun findRest pred =
|
|
16 |
let
|
|
17 |
fun f _ [] = NONE
|
|
18 |
| f ys (x :: xs) =
|
|
19 |
if pred x then SOME (x, List.revAppend (ys,xs)) else f (x :: ys) xs
|
|
20 |
in
|
|
21 |
f []
|
|
22 |
end;
|
|
23 |
|
|
24 |
local
|
|
25 |
fun addSym (lit,acc) =
|
|
26 |
case total Literal.sym lit of
|
|
27 |
NONE => acc
|
|
28 |
| SOME lit => lit :: acc
|
|
29 |
in
|
|
30 |
fun clauseSym lits = List.foldl addSym lits lits;
|
|
31 |
end;
|
|
32 |
|
|
33 |
fun sortClause cl =
|
|
34 |
let
|
|
35 |
val lits = LiteralSet.toList cl
|
|
36 |
in
|
|
37 |
sortMap Literal.typedSymbols (revCompare Int.compare) lits
|
|
38 |
end;
|
|
39 |
|
|
40 |
fun incompatible lit =
|
|
41 |
let
|
|
42 |
val lits = clauseSym [lit]
|
|
43 |
in
|
|
44 |
fn lit' => not (List.exists (can (Literal.unify Subst.empty lit')) lits)
|
|
45 |
end;
|
|
46 |
|
|
47 |
(* ------------------------------------------------------------------------- *)
|
|
48 |
(* Clause ids and lengths. *)
|
|
49 |
(* ------------------------------------------------------------------------- *)
|
|
50 |
|
|
51 |
type clauseId = int;
|
|
52 |
|
|
53 |
type clauseLength = int;
|
|
54 |
|
|
55 |
local
|
|
56 |
type idSet = (clauseId * clauseLength) Set.set;
|
|
57 |
|
|
58 |
fun idCompare ((id1,len1),(id2,len2)) =
|
|
59 |
case Int.compare (len1,len2) of
|
|
60 |
LESS => LESS
|
|
61 |
| EQUAL => Int.compare (id1,id2)
|
|
62 |
| GREATER => GREATER;
|
|
63 |
in
|
|
64 |
val idSetEmpty : idSet = Set.empty idCompare;
|
|
65 |
|
|
66 |
fun idSetAdd (id_len,set) : idSet = Set.add set id_len;
|
|
67 |
|
|
68 |
fun idSetAddMax max (id_len as (_,len), set) : idSet =
|
|
69 |
if len <= max then Set.add set id_len else set;
|
|
70 |
|
|
71 |
fun idSetIntersect set1 set2 : idSet = Set.intersect set1 set2;
|
|
72 |
end;
|
|
73 |
|
|
74 |
(* ------------------------------------------------------------------------- *)
|
|
75 |
(* A type of clause sets that supports efficient subsumption checking. *)
|
|
76 |
(* ------------------------------------------------------------------------- *)
|
|
77 |
|
|
78 |
datatype 'a subsume =
|
|
79 |
Subsume of
|
|
80 |
{empty : (Thm.clause * Subst.subst * 'a) list,
|
|
81 |
unit : (Literal.literal * Thm.clause * 'a) LiteralNet.literalNet,
|
|
82 |
nonunit :
|
|
83 |
{nextId : clauseId,
|
|
84 |
clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map,
|
|
85 |
fstLits : (clauseId * clauseLength) LiteralNet.literalNet,
|
|
86 |
sndLits : (clauseId * clauseLength) LiteralNet.literalNet}};
|
|
87 |
|
|
88 |
fun new () =
|
|
89 |
Subsume
|
|
90 |
{empty = [],
|
|
91 |
unit = LiteralNet.new {fifo = false},
|
|
92 |
nonunit =
|
|
93 |
{nextId = 0,
|
|
94 |
clauses = IntMap.new (),
|
|
95 |
fstLits = LiteralNet.new {fifo = false},
|
|
96 |
sndLits = LiteralNet.new {fifo = false}}};
|
|
97 |
|
|
98 |
fun size (Subsume {empty, unit, nonunit = {clauses,...}}) =
|
|
99 |
length empty + LiteralNet.size unit + IntMap.size clauses;
|
|
100 |
|
|
101 |
fun insert (Subsume {empty,unit,nonunit}) (cl',a) =
|
|
102 |
case sortClause cl' of
|
|
103 |
[] =>
|
|
104 |
let
|
|
105 |
val empty = (cl',Subst.empty,a) :: empty
|
|
106 |
in
|
|
107 |
Subsume {empty = empty, unit = unit, nonunit = nonunit}
|
|
108 |
end
|
|
109 |
| [lit] =>
|
|
110 |
let
|
|
111 |
val unit = LiteralNet.insert unit (lit,(lit,cl',a))
|
|
112 |
in
|
|
113 |
Subsume {empty = empty, unit = unit, nonunit = nonunit}
|
|
114 |
end
|
|
115 |
| fstLit :: (nonFstLits as sndLit :: otherLits) =>
|
|
116 |
let
|
|
117 |
val {nextId,clauses,fstLits,sndLits} = nonunit
|
|
118 |
val id_length = (nextId, LiteralSet.size cl')
|
|
119 |
val fstLits = LiteralNet.insert fstLits (fstLit,id_length)
|
|
120 |
val (sndLit,otherLits) =
|
|
121 |
case findRest (incompatible fstLit) nonFstLits of
|
|
122 |
SOME sndLit_otherLits => sndLit_otherLits
|
|
123 |
| NONE => (sndLit,otherLits)
|
|
124 |
val sndLits = LiteralNet.insert sndLits (sndLit,id_length)
|
|
125 |
val lits' = otherLits @ [fstLit,sndLit]
|
|
126 |
val clauses = IntMap.insert clauses (nextId,(lits',cl',a))
|
|
127 |
val nextId = nextId + 1
|
|
128 |
val nonunit = {nextId = nextId, clauses = clauses,
|
|
129 |
fstLits = fstLits, sndLits = sndLits}
|
|
130 |
in
|
|
131 |
Subsume {empty = empty, unit = unit, nonunit = nonunit}
|
|
132 |
end;
|
|
133 |
|
|
134 |
fun filter pred (Subsume {empty,unit,nonunit}) =
|
|
135 |
let
|
|
136 |
val empty = List.filter (pred o #3) empty
|
|
137 |
|
|
138 |
val unit = LiteralNet.filter (pred o #3) unit
|
|
139 |
|
|
140 |
val nonunit =
|
|
141 |
let
|
|
142 |
val {nextId,clauses,fstLits,sndLits} = nonunit
|
|
143 |
val clauses' = IntMap.filter (pred o #3 o snd) clauses
|
|
144 |
in
|
|
145 |
if IntMap.size clauses = IntMap.size clauses' then nonunit
|
|
146 |
else
|
|
147 |
let
|
|
148 |
fun predId (id,_) = IntMap.inDomain id clauses'
|
|
149 |
val fstLits = LiteralNet.filter predId fstLits
|
|
150 |
and sndLits = LiteralNet.filter predId sndLits
|
|
151 |
in
|
|
152 |
{nextId = nextId, clauses = clauses',
|
|
153 |
fstLits = fstLits, sndLits = sndLits}
|
|
154 |
end
|
|
155 |
end
|
|
156 |
in
|
|
157 |
Subsume {empty = empty, unit = unit, nonunit = nonunit}
|
|
158 |
end;
|
|
159 |
|
|
160 |
fun toString subsume = "Subsume{" ^ Int.toString (size subsume) ^ "}";
|
|
161 |
|
|
162 |
fun pp subsume = Print.ppMap toString Print.ppString subsume;
|
|
163 |
|
|
164 |
(* ------------------------------------------------------------------------- *)
|
|
165 |
(* Subsumption checking. *)
|
|
166 |
(* ------------------------------------------------------------------------- *)
|
|
167 |
|
|
168 |
local
|
|
169 |
fun matchLit lit' (lit,acc) =
|
|
170 |
case total (Literal.match Subst.empty lit') lit of
|
|
171 |
SOME sub => sub :: acc
|
|
172 |
| NONE => acc;
|
|
173 |
in
|
|
174 |
fun genClauseSubsumes pred cl' lits' cl a =
|
|
175 |
let
|
|
176 |
fun mkSubsl acc sub [] = SOME (sub, sortMap length Int.compare acc)
|
|
177 |
| mkSubsl acc sub (lit' :: lits') =
|
|
178 |
case List.foldl (matchLit lit') [] cl of
|
|
179 |
[] => NONE
|
|
180 |
| [sub'] =>
|
|
181 |
(case total (Subst.union sub) sub' of
|
|
182 |
NONE => NONE
|
|
183 |
| SOME sub => mkSubsl acc sub lits')
|
|
184 |
| subs => mkSubsl (subs :: acc) sub lits'
|
|
185 |
|
|
186 |
fun search [] = NONE
|
|
187 |
| search ((sub,[]) :: others) =
|
|
188 |
let
|
|
189 |
val x = (cl',sub,a)
|
|
190 |
in
|
|
191 |
if pred x then SOME x else search others
|
|
192 |
end
|
|
193 |
| search ((_, [] :: _) :: others) = search others
|
|
194 |
| search ((sub, (sub' :: subs) :: subsl) :: others) =
|
|
195 |
let
|
|
196 |
val others = (sub, subs :: subsl) :: others
|
|
197 |
in
|
|
198 |
case total (Subst.union sub) sub' of
|
|
199 |
NONE => search others
|
|
200 |
| SOME sub => search ((sub,subsl) :: others)
|
|
201 |
end
|
|
202 |
in
|
|
203 |
case mkSubsl [] Subst.empty lits' of
|
|
204 |
NONE => NONE
|
|
205 |
| SOME sub_subsl => search [sub_subsl]
|
|
206 |
end;
|
|
207 |
end;
|
|
208 |
|
|
209 |
local
|
|
210 |
fun emptySubsumes pred empty = List.find pred empty;
|
|
211 |
|
|
212 |
fun unitSubsumes pred unit =
|
|
213 |
let
|
|
214 |
fun subLit lit =
|
|
215 |
let
|
|
216 |
fun subUnit (lit',cl',a) =
|
|
217 |
case total (Literal.match Subst.empty lit') lit of
|
|
218 |
NONE => NONE
|
|
219 |
| SOME sub =>
|
|
220 |
let
|
|
221 |
val x = (cl',sub,a)
|
|
222 |
in
|
|
223 |
if pred x then SOME x else NONE
|
|
224 |
end
|
|
225 |
in
|
|
226 |
first subUnit (LiteralNet.match unit lit)
|
|
227 |
end
|
|
228 |
in
|
|
229 |
first subLit
|
|
230 |
end;
|
|
231 |
|
|
232 |
fun nonunitSubsumes pred nonunit max cl =
|
|
233 |
let
|
|
234 |
val addId = case max of NONE => idSetAdd | SOME n => idSetAddMax n
|
|
235 |
|
|
236 |
fun subLit lits (lit,acc) =
|
|
237 |
List.foldl addId acc (LiteralNet.match lits lit)
|
|
238 |
|
|
239 |
val {nextId = _, clauses, fstLits, sndLits} = nonunit
|
|
240 |
|
|
241 |
fun subCl' (id,_) =
|
|
242 |
let
|
|
243 |
val (lits',cl',a) = IntMap.get clauses id
|
|
244 |
in
|
|
245 |
genClauseSubsumes pred cl' lits' cl a
|
|
246 |
end
|
|
247 |
|
|
248 |
val fstCands = List.foldl (subLit fstLits) idSetEmpty cl
|
|
249 |
val sndCands = List.foldl (subLit sndLits) idSetEmpty cl
|
|
250 |
val cands = idSetIntersect fstCands sndCands
|
|
251 |
in
|
|
252 |
Set.firstl subCl' cands
|
|
253 |
end;
|
|
254 |
|
|
255 |
fun genSubsumes pred (Subsume {empty,unit,nonunit}) max cl =
|
|
256 |
case emptySubsumes pred empty of
|
|
257 |
s as SOME _ => s
|
|
258 |
| NONE =>
|
|
259 |
if max = SOME 0 then NONE
|
|
260 |
else
|
|
261 |
let
|
|
262 |
val cl = clauseSym (LiteralSet.toList cl)
|
|
263 |
in
|
|
264 |
case unitSubsumes pred unit cl of
|
|
265 |
s as SOME _ => s
|
|
266 |
| NONE =>
|
|
267 |
if max = SOME 1 then NONE
|
|
268 |
else nonunitSubsumes pred nonunit max cl
|
|
269 |
end;
|
|
270 |
in
|
|
271 |
fun subsumes pred subsume cl = genSubsumes pred subsume NONE cl;
|
|
272 |
|
|
273 |
fun strictlySubsumes pred subsume cl =
|
|
274 |
genSubsumes pred subsume (SOME (LiteralSet.size cl)) cl;
|
|
275 |
end;
|
|
276 |
|
|
277 |
(*MetisTrace4
|
|
278 |
val subsumes = fn pred => fn subsume => fn cl =>
|
|
279 |
let
|
|
280 |
val ppCl = LiteralSet.pp
|
|
281 |
val ppSub = Subst.pp
|
|
282 |
val () = Print.trace ppCl "Subsume.subsumes: cl" cl
|
|
283 |
val result = subsumes pred subsume cl
|
|
284 |
val () =
|
|
285 |
case result of
|
|
286 |
NONE => trace "Subsume.subsumes: not subsumed\n"
|
|
287 |
| SOME (cl,sub,_) =>
|
|
288 |
(Print.trace ppCl "Subsume.subsumes: subsuming cl" cl;
|
|
289 |
Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
|
|
290 |
in
|
|
291 |
result
|
|
292 |
end;
|
|
293 |
|
|
294 |
val strictlySubsumes = fn pred => fn subsume => fn cl =>
|
|
295 |
let
|
|
296 |
val ppCl = LiteralSet.pp
|
|
297 |
val ppSub = Subst.pp
|
|
298 |
val () = Print.trace ppCl "Subsume.strictlySubsumes: cl" cl
|
|
299 |
val result = strictlySubsumes pred subsume cl
|
|
300 |
val () =
|
|
301 |
case result of
|
|
302 |
NONE => trace "Subsume.subsumes: not subsumed\n"
|
|
303 |
| SOME (cl,sub,_) =>
|
|
304 |
(Print.trace ppCl "Subsume.subsumes: subsuming cl" cl;
|
|
305 |
Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
|
|
306 |
in
|
|
307 |
result
|
|
308 |
end;
|
|
309 |
*)
|
|
310 |
|
|
311 |
fun isSubsumed subs cl = Option.isSome (subsumes (K true) subs cl);
|
|
312 |
|
|
313 |
fun isStrictlySubsumed subs cl =
|
|
314 |
Option.isSome (strictlySubsumes (K true) subs cl);
|
|
315 |
|
|
316 |
(* ------------------------------------------------------------------------- *)
|
|
317 |
(* Single clause versions. *)
|
|
318 |
(* ------------------------------------------------------------------------- *)
|
|
319 |
|
|
320 |
fun clauseSubsumes cl' cl =
|
|
321 |
let
|
|
322 |
val lits' = sortClause cl'
|
|
323 |
and lits = clauseSym (LiteralSet.toList cl)
|
|
324 |
in
|
|
325 |
case genClauseSubsumes (K true) cl' lits' lits () of
|
|
326 |
SOME (_,sub,()) => SOME sub
|
|
327 |
| NONE => NONE
|
|
328 |
end;
|
|
329 |
|
|
330 |
fun clauseStrictlySubsumes cl' cl =
|
|
331 |
if LiteralSet.size cl' > LiteralSet.size cl then NONE
|
|
332 |
else clauseSubsumes cl' cl;
|
|
333 |
|
|
334 |
end
|