1(* ========================================================================= *) 2(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Subsume :> Subsume = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Helper functions. *) 13(* ------------------------------------------------------------------------- *) 14 15fun 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 24local 25 fun addSym (lit,acc) = 26 case total Literal.sym lit of 27 NONE => acc 28 | SOME lit => lit :: acc 29in 30 fun clauseSym lits = List.foldl addSym lits lits; 31end; 32 33fun sortClause cl = 34 let 35 val lits = LiteralSet.toList cl 36 in 37 sortMap Literal.typedSymbols (revCompare Int.compare) lits 38 end; 39 40fun 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 51type clauseId = int; 52 53type clauseLength = int; 54 55local 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; 63in 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; 72end; 73 74(* ------------------------------------------------------------------------- *) 75(* A type of clause sets that supports efficient subsumption checking. *) 76(* ------------------------------------------------------------------------- *) 77 78datatype '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 88fun 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 98fun size (Subsume {empty, unit, nonunit = {clauses,...}}) = 99 length empty + LiteralNet.size unit + IntMap.size clauses; 100 101fun 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 134fun 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 160fun toString subsume = "Subsume{" ^ Int.toString (size subsume) ^ "}"; 161 162fun pp subsume = Print.ppMap toString Print.ppString subsume; 163 164(* ------------------------------------------------------------------------- *) 165(* Subsumption checking. *) 166(* ------------------------------------------------------------------------- *) 167 168local 169 fun matchLit lit' (lit,acc) = 170 case total (Literal.match Subst.empty lit') lit of 171 SOME sub => sub :: acc 172 | NONE => acc; 173in 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; 207end; 208 209local 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; 270in 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; 275end; 276 277(*MetisTrace4 278val 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 294val 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 311fun isSubsumed subs cl = Option.isSome (subsumes (K true) subs cl); 312 313fun isStrictlySubsumed subs cl = 314 Option.isSome (strictlySubsumes (K true) subs cl); 315 316(* ------------------------------------------------------------------------- *) 317(* Single clause versions. *) 318(* ------------------------------------------------------------------------- *) 319 320fun 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 330fun clauseStrictlySubsumes cl' cl = 331 if LiteralSet.size cl' > LiteralSet.size cl then NONE 332 else clauseSubsumes cl' cl; 333 334end 335