1(* ========================================================================= *)
2(* CLAUSE = ID + THEOREM                                                     *)
3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Clause :> Clause =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* Helper functions.                                                         *)
13(* ------------------------------------------------------------------------- *)
14
15val newId =
16    let
17      val r = ref 0
18
19      fun new () =
20          let
21            val ref n = r
22
23            val () = r := n + 1
24          in
25            n
26          end
27    in
28      fn () => Portable.critical new ()
29    end;
30
31(* ------------------------------------------------------------------------- *)
32(* A type of clause.                                                         *)
33(* ------------------------------------------------------------------------- *)
34
35datatype literalOrder =
36    NoLiteralOrder
37  | UnsignedLiteralOrder
38  | PositiveLiteralOrder;
39
40type parameters =
41     {ordering : KnuthBendixOrder.kbo,
42      orderLiterals : literalOrder,
43      orderTerms : bool};
44
45type clauseId = int;
46
47type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm};
48
49datatype clause = Clause of clauseInfo;
50
51(* ------------------------------------------------------------------------- *)
52(* Pretty printing.                                                          *)
53(* ------------------------------------------------------------------------- *)
54
55val showId = ref false;
56
57local
58  val ppIdThm = Print.ppPair Print.ppInt Thm.pp;
59in
60  fun pp (Clause {id,thm,...}) =
61      if !showId then ppIdThm (id,thm) else Thm.pp thm;
62end;
63
64fun toString cl = Print.toString pp cl;
65
66(* ------------------------------------------------------------------------- *)
67(* Basic operations.                                                         *)
68(* ------------------------------------------------------------------------- *)
69
70val default : parameters =
71    {ordering = KnuthBendixOrder.default,
72     orderLiterals = PositiveLiteralOrder,
73     orderTerms = true};
74
75fun mk info = Clause info
76
77fun dest (Clause info) = info;
78
79fun id (Clause {id = i, ...}) = i;
80
81fun thm (Clause {thm = th, ...}) = th;
82
83fun equalThms cl cl' = Thm.equal (thm cl) (thm cl');
84
85fun new parameters thm =
86    Clause {parameters = parameters, id = newId (), thm = thm};
87
88fun literals cl = Thm.clause (thm cl);
89
90fun isTautology (Clause {thm,...}) = Thm.isTautology thm;
91
92fun isContradiction (Clause {thm,...}) = Thm.isContradiction thm;
93
94(* ------------------------------------------------------------------------- *)
95(* The term ordering is used to cut down inferences.                         *)
96(* ------------------------------------------------------------------------- *)
97
98fun strictlyLess ordering x_y =
99    case KnuthBendixOrder.compare ordering x_y of
100      SOME LESS => true
101    | _ => false;
102
103fun isLargerTerm ({ordering,orderTerms,...} : parameters) l_r =
104    not orderTerms orelse not (strictlyLess ordering l_r);
105
106local
107  fun atomToTerms atm =
108      case total Atom.destEq atm of
109        NONE => [Term.Fn atm]
110      | SOME (l,r) => [l,r];
111
112  fun notStrictlyLess ordering (xs,ys) =
113      let
114        fun less x = List.exists (fn y => strictlyLess ordering (x,y)) ys
115      in
116        not (List.all less xs)
117      end;
118in
119  fun isLargerLiteral ({ordering,orderLiterals,...} : parameters) lits =
120      case orderLiterals of
121        NoLiteralOrder => K true
122      | UnsignedLiteralOrder =>
123        let
124          fun addLit ((_,atm),acc) = atomToTerms atm @ acc
125
126          val tms = LiteralSet.foldl addLit [] lits
127        in
128          fn (_,atm') => notStrictlyLess ordering (atomToTerms atm', tms)
129        end
130      | PositiveLiteralOrder =>
131        case LiteralSet.findl (K true) lits of
132          NONE => K true
133        | SOME (pol,_) =>
134          let
135            fun addLit ((p,atm),acc) =
136                if p = pol then atomToTerms atm @ acc else acc
137
138            val tms = LiteralSet.foldl addLit [] lits
139          in
140            fn (pol',atm') =>
141               if pol <> pol' then pol
142               else notStrictlyLess ordering (atomToTerms atm', tms)
143          end;
144end;
145
146fun largestLiterals (Clause {parameters,thm,...}) =
147    let
148      val litSet = Thm.clause thm
149      val isLarger = isLargerLiteral parameters litSet
150      fun addLit (lit,s) = if isLarger lit then LiteralSet.add s lit else s
151    in
152      LiteralSet.foldr addLit LiteralSet.empty litSet
153    end;
154
155(*MetisTrace6
156val largestLiterals = fn cl =>
157    let
158      val ppResult = LiteralSet.pp
159      val () = Print.trace pp "Clause.largestLiterals: cl" cl
160      val result = largestLiterals cl
161      val () = Print.trace ppResult "Clause.largestLiterals: result" result
162    in
163      result
164    end;
165*)
166
167fun largestEquations (cl as Clause {parameters,...}) =
168    let
169      fun addEq lit ort (l_r as (l,_)) acc =
170          if isLargerTerm parameters l_r then (lit,ort,l) :: acc else acc
171
172      fun addLit (lit,acc) =
173          case total Literal.destEq lit of
174            NONE => acc
175          | SOME (l,r) =>
176            let
177              val acc = addEq lit Rewrite.RightToLeft (r,l) acc
178              val acc = addEq lit Rewrite.LeftToRight (l,r) acc
179            in
180              acc
181            end
182    in
183      LiteralSet.foldr addLit [] (largestLiterals cl)
184    end;
185
186local
187  fun addLit (lit,acc) =
188      let
189        fun addTm ((path,tm),acc) = (lit,path,tm) :: acc
190      in
191        List.foldl addTm acc (Literal.nonVarTypedSubterms lit)
192      end;
193in
194  fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiterals cl);
195
196  fun allSubterms cl = LiteralSet.foldl addLit [] (literals cl);
197end;
198
199(* ------------------------------------------------------------------------- *)
200(* Subsumption.                                                              *)
201(* ------------------------------------------------------------------------- *)
202
203fun subsumes (subs : clause Subsume.subsume) cl =
204    Subsume.isStrictlySubsumed subs (literals cl);
205
206(* ------------------------------------------------------------------------- *)
207(* Simplifying rules: these preserve the clause id.                          *)
208(* ------------------------------------------------------------------------- *)
209
210fun freshVars (Clause {parameters,id,thm}) =
211    Clause {parameters = parameters, id = id, thm = Rule.freshVars thm};
212
213fun simplify (Clause {parameters,id,thm}) =
214    case Rule.simplify thm of
215      NONE => NONE
216    | SOME thm => SOME (Clause {parameters = parameters, id = id, thm = thm});
217
218fun reduce units (Clause {parameters,id,thm}) =
219    Clause {parameters = parameters, id = id, thm = Units.reduce units thm};
220
221fun rewrite rewr (cl as Clause {parameters,id,thm}) =
222    let
223      fun simp th =
224          let
225            val {ordering,...} = parameters
226            val cmp = KnuthBendixOrder.compare ordering
227          in
228            Rewrite.rewriteIdRule rewr cmp id th
229          end
230
231(*MetisTrace4
232      val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr
233      val () = Print.trace Print.ppInt "Clause.rewrite: id" id
234      val () = Print.trace pp "Clause.rewrite: cl" cl
235*)
236
237      val thm =
238          case Rewrite.peek rewr id of
239            NONE => simp thm
240          | SOME ((_,thm),_) => if Rewrite.isReduced rewr then thm else simp thm
241
242      val result = Clause {parameters = parameters, id = id, thm = thm}
243
244(*MetisTrace4
245      val () = Print.trace pp "Clause.rewrite: result" result
246*)
247    in
248      result
249    end
250(*MetisDebug
251    handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
252*)
253
254(* ------------------------------------------------------------------------- *)
255(* Inference rules: these generate new clause ids.                           *)
256(* ------------------------------------------------------------------------- *)
257
258fun factor (cl as Clause {parameters,thm,...}) =
259    let
260      val lits = largestLiterals cl
261
262      fun apply sub = new parameters (Thm.subst sub thm)
263    in
264      List.map apply (Rule.factor' lits)
265    end;
266
267(*MetisTrace5
268val factor = fn cl =>
269    let
270      val () = Print.trace pp "Clause.factor: cl" cl
271      val result = factor cl
272      val () = Print.trace (Print.ppList pp) "Clause.factor: result" result
273    in
274      result
275    end;
276*)
277
278fun resolve (cl1,lit1) (cl2,lit2) =
279    let
280(*MetisTrace5
281      val () = Print.trace pp "Clause.resolve: cl1" cl1
282      val () = Print.trace Literal.pp "Clause.resolve: lit1" lit1
283      val () = Print.trace pp "Clause.resolve: cl2" cl2
284      val () = Print.trace Literal.pp "Clause.resolve: lit2" lit2
285*)
286      val Clause {parameters, thm = th1, ...} = cl1
287      and Clause {thm = th2, ...} = cl2
288      val sub = Literal.unify Subst.empty lit1 (Literal.negate lit2)
289(*MetisTrace5
290      val () = Print.trace Subst.pp "Clause.resolve: sub" sub
291*)
292      val lit1 = Literal.subst sub lit1
293      val lit2 = Literal.negate lit1
294      val th1 = Thm.subst sub th1
295      and th2 = Thm.subst sub th2
296      val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
297(*MetisTrace5
298              (trace "Clause.resolve: th1 violates ordering\n"; false) orelse
299*)
300              raise Error "resolve: clause1: ordering constraints"
301      val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
302(*MetisTrace5
303              (trace "Clause.resolve: th2 violates ordering\n"; false) orelse
304*)
305              raise Error "resolve: clause2: ordering constraints"
306      val th = Thm.resolve lit1 th1 th2
307(*MetisTrace5
308      val () = Print.trace Thm.pp "Clause.resolve: th" th
309*)
310      val cl = Clause {parameters = parameters, id = newId (), thm = th}
311(*MetisTrace5
312      val () = Print.trace pp "Clause.resolve: cl" cl
313*)
314    in
315      cl
316    end;
317
318fun paramodulate (cl1,lit1,ort1,tm1) (cl2,lit2,path2,tm2) =
319    let
320(*MetisTrace5
321      val () = Print.trace pp "Clause.paramodulate: cl1" cl1
322      val () = Print.trace Literal.pp "Clause.paramodulate: lit1" lit1
323      val () = Print.trace Rewrite.ppOrient "Clause.paramodulate: ort1" ort1
324      val () = Print.trace Term.pp "Clause.paramodulate: tm1" tm1
325      val () = Print.trace pp "Clause.paramodulate: cl2" cl2
326      val () = Print.trace Literal.pp "Clause.paramodulate: lit2" lit2
327      val () = Print.trace Term.ppPath "Clause.paramodulate: path2" path2
328      val () = Print.trace Term.pp "Clause.paramodulate: tm2" tm2
329*)
330      val Clause {parameters, thm = th1, ...} = cl1
331      and Clause {thm = th2, ...} = cl2
332      val sub = Subst.unify Subst.empty tm1 tm2
333      val lit1 = Literal.subst sub lit1
334      and lit2 = Literal.subst sub lit2
335      and th1 = Thm.subst sub th1
336      and th2 = Thm.subst sub th2
337
338      val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
339              raise Error "Clause.paramodulate: with clause: ordering"
340      val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
341              raise Error "Clause.paramodulate: into clause: ordering"
342
343      val eqn = (Literal.destEq lit1, th1)
344      val eqn as (l_r,_) =
345          case ort1 of
346            Rewrite.LeftToRight => eqn
347          | Rewrite.RightToLeft => Rule.symEqn eqn
348(*MetisTrace6
349      val () = Print.trace Rule.ppEquation "Clause.paramodulate: eqn" eqn
350*)
351      val _ = isLargerTerm parameters l_r orelse
352              raise Error "Clause.paramodulate: equation: ordering constraints"
353      val th = Rule.rewrRule eqn lit2 path2 th2
354(*MetisTrace5
355      val () = Print.trace Thm.pp "Clause.paramodulate: th" th
356*)
357    in
358      Clause {parameters = parameters, id = newId (), thm = th}
359    end
360(*MetisTrace5
361    handle Error err =>
362      let
363        val () = trace ("Clause.paramodulate: failed: " ^ err ^ "\n")
364      in
365        raise Error err
366      end;
367*)
368
369end
370