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