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