--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Clause.sml Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,349 @@
+(* ========================================================================= *)
+(* CLAUSE = ID + THEOREM *)
+(* Copyright (c) 2002-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Clause :> Clause =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+val newId =
+ let
+ val r = ref 0
+ in
+ fn () => case r of ref n => let val () = r := n + 1 in n end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of clause. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype literalOrder =
+ NoLiteralOrder
+ | UnsignedLiteralOrder
+ | PositiveLiteralOrder;
+
+type parameters =
+ {ordering : KnuthBendixOrder.kbo,
+ orderLiterals : literalOrder,
+ orderTerms : bool};
+
+type clauseId = int;
+
+type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm};
+
+datatype clause = Clause of clauseInfo;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val showId = ref false;
+
+local
+ val ppIdThm = Parser.ppPair Parser.ppInt Thm.pp;
+in
+ fun pp p (Clause {id,thm,...}) =
+ if !showId then ppIdThm p (id,thm) else Thm.pp p thm;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters =
+ {ordering = KnuthBendixOrder.default,
+ orderLiterals = UnsignedLiteralOrder, (*LCP: changed from PositiveLiteralOrder*)
+ orderTerms = true};
+
+fun mk info = Clause info
+
+fun dest (Clause info) = info;
+
+fun id (Clause {id = i, ...}) = i;
+
+fun thm (Clause {thm = th, ...}) = th;
+
+fun equalThms cl cl' = Thm.equal (thm cl) (thm cl');
+
+fun new parameters thm =
+ Clause {parameters = parameters, id = newId (), thm = thm};
+
+fun literals cl = Thm.clause (thm cl);
+
+fun isTautology (Clause {thm,...}) = Thm.isTautology thm;
+
+fun isContradiction (Clause {thm,...}) = Thm.isContradiction thm;
+
+(* ------------------------------------------------------------------------- *)
+(* The term ordering is used to cut down inferences. *)
+(* ------------------------------------------------------------------------- *)
+
+fun strictlyLess ordering x_y =
+ case KnuthBendixOrder.compare ordering x_y of
+ SOME LESS => true
+ | _ => false;
+
+fun isLargerTerm ({ordering,orderTerms,...} : parameters) l_r =
+ not orderTerms orelse not (strictlyLess ordering l_r);
+
+local
+ fun atomToTerms atm =
+ Term.Fn atm ::
+ (case total Atom.sym atm of NONE => [] | SOME atm => [Term.Fn atm]);
+
+ fun notStrictlyLess ordering (xs,ys) =
+ let
+ fun less x = List.exists (fn y => strictlyLess ordering (x,y)) ys
+ in
+ not (List.all less xs)
+ end;
+in
+ fun isLargerLiteral ({ordering,orderLiterals,...} : parameters) lits =
+ case orderLiterals of
+ NoLiteralOrder => K true
+ | UnsignedLiteralOrder =>
+ let
+ fun addLit ((_,atm),acc) = atomToTerms atm @ acc
+
+ val tms = LiteralSet.foldl addLit [] lits
+ in
+ fn (_,atm') => notStrictlyLess ordering (atomToTerms atm', tms)
+ end
+ | PositiveLiteralOrder =>
+ case LiteralSet.findl (K true) lits of
+ NONE => K true
+ | SOME (pol,_) =>
+ let
+ fun addLit ((p,atm),acc) =
+ if p = pol then atomToTerms atm @ acc else acc
+
+ val tms = LiteralSet.foldl addLit [] lits
+ in
+ fn (pol',atm') =>
+ if pol <> pol' then pol
+ else notStrictlyLess ordering (atomToTerms atm', tms)
+ end;
+end;
+
+fun largestLiterals (Clause {parameters,thm,...}) =
+ let
+ val litSet = Thm.clause thm
+ val isLarger = isLargerLiteral parameters litSet
+ fun addLit (lit,s) = if isLarger lit then LiteralSet.add s lit else s
+ in
+ LiteralSet.foldr addLit LiteralSet.empty litSet
+ end;
+
+(*TRACE6
+val largestLiterals = fn cl =>
+ let
+ val ppResult = LiteralSet.pp
+ val () = Parser.ppTrace pp "Clause.largestLiterals: cl" cl
+ val result = largestLiterals cl
+ val () = Parser.ppTrace ppResult "Clause.largestLiterals: result" result
+ in
+ result
+ end;
+*)
+
+fun largestEquations (cl as Clause {parameters,...}) =
+ let
+ fun addEq lit ort (l_r as (l,_)) acc =
+ if isLargerTerm parameters l_r then (lit,ort,l) :: acc else acc
+
+ fun addLit (lit,acc) =
+ case total Literal.destEq lit of
+ NONE => acc
+ | SOME (l,r) =>
+ let
+ val acc = addEq lit Rewrite.RightToLeft (r,l) acc
+ val acc = addEq lit Rewrite.LeftToRight (l,r) acc
+ in
+ acc
+ end
+ in
+ LiteralSet.foldr addLit [] (largestLiterals cl)
+ end;
+
+local
+ fun addLit (lit,acc) =
+ let
+ fun addTm ((path,tm),acc) = (lit,path,tm) :: acc
+ in
+ foldl addTm acc (Literal.nonVarTypedSubterms lit)
+ end;
+in
+ fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiterals cl);
+
+ fun allSubterms cl = LiteralSet.foldl addLit [] (literals cl);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Subsumption. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subsumes (subs : clause Subsume.subsume) cl =
+ Subsume.isStrictlySubsumed subs (literals cl);
+
+(* ------------------------------------------------------------------------- *)
+(* Simplifying rules: these preserve the clause id. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freshVars (Clause {parameters,id,thm}) =
+ Clause {parameters = parameters, id = id, thm = Rule.freshVars thm};
+
+fun simplify (Clause {parameters,id,thm}) =
+ case Rule.simplify thm of
+ NONE => NONE
+ | SOME thm => SOME (Clause {parameters = parameters, id = id, thm = thm});
+
+fun reduce units (Clause {parameters,id,thm}) =
+ Clause {parameters = parameters, id = id, thm = Units.reduce units thm};
+
+fun rewrite rewr (cl as Clause {parameters,id,thm}) =
+ let
+ fun simp th =
+ let
+ val {ordering,...} = parameters
+ val cmp = KnuthBendixOrder.compare ordering
+ in
+ Rewrite.rewriteIdRule rewr cmp id th
+ end
+
+(*TRACE4
+ val () = Parser.ppTrace Rewrite.pp "Clause.rewrite: rewr" rewr
+ val () = Parser.ppTrace Parser.ppInt "Clause.rewrite: id" id
+ val () = Parser.ppTrace pp "Clause.rewrite: cl" cl
+*)
+
+ val thm =
+ case Rewrite.peek rewr id of
+ NONE => simp thm
+ | SOME ((_,thm),_) => if Rewrite.isReduced rewr then thm else simp thm
+
+ val result = Clause {parameters = parameters, id = id, thm = thm}
+
+(*TRACE4
+ val () = Parser.ppTrace pp "Clause.rewrite: result" result
+*)
+ in
+ result
+ end
+(*DEBUG
+ handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Inference rules: these generate new clause ids. *)
+(* ------------------------------------------------------------------------- *)
+
+fun factor (cl as Clause {parameters,thm,...}) =
+ let
+ val lits = largestLiterals cl
+
+ fun apply sub = new parameters (Thm.subst sub thm)
+ in
+ map apply (Rule.factor' lits)
+ end;
+
+(*TRACE5
+val factor = fn cl =>
+ let
+ val () = Parser.ppTrace pp "Clause.factor: cl" cl
+ val result = factor cl
+ val () = Parser.ppTrace (Parser.ppList pp) "Clause.factor: result" result
+ in
+ result
+ end;
+*)
+
+fun resolve (cl1,lit1) (cl2,lit2) =
+ let
+(*TRACE5
+ val () = Parser.ppTrace pp "Clause.resolve: cl1" cl1
+ val () = Parser.ppTrace Literal.pp "Clause.resolve: lit1" lit1
+ val () = Parser.ppTrace pp "Clause.resolve: cl2" cl2
+ val () = Parser.ppTrace Literal.pp "Clause.resolve: lit2" lit2
+*)
+ val Clause {parameters, thm = th1, ...} = cl1
+ and Clause {thm = th2, ...} = cl2
+ val sub = Literal.unify Subst.empty lit1 (Literal.negate lit2)
+(*TRACE5
+ val () = Parser.ppTrace Subst.pp "Clause.resolve: sub" sub
+*)
+ val lit1 = Literal.subst sub lit1
+ val lit2 = Literal.negate lit1
+ val th1 = Thm.subst sub th1
+ and th2 = Thm.subst sub th2
+ val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
+(*TRACE5
+ (trace "Clause.resolve: th1 violates ordering\n"; false) orelse
+*)
+ raise Error "resolve: clause1: ordering constraints"
+ val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
+(*TRACE5
+ (trace "Clause.resolve: th2 violates ordering\n"; false) orelse
+*)
+ raise Error "resolve: clause2: ordering constraints"
+ val th = Thm.resolve lit1 th1 th2
+(*TRACE5
+ val () = Parser.ppTrace Thm.pp "Clause.resolve: th" th
+*)
+ val cl = Clause {parameters = parameters, id = newId (), thm = th}
+(*TRACE5
+ val () = Parser.ppTrace pp "Clause.resolve: cl" cl
+*)
+ in
+ cl
+ end;
+
+fun paramodulate (cl1,lit1,ort,tm1) (cl2,lit2,path,tm2) =
+ let
+(*TRACE5
+ val () = Parser.ppTrace pp "Clause.paramodulate: cl1" cl1
+ val () = Parser.ppTrace Literal.pp "Clause.paramodulate: lit1" lit1
+ val () = Parser.ppTrace pp "Clause.paramodulate: cl2" cl2
+ val () = Parser.ppTrace Literal.pp "Clause.paramodulate: lit2" lit2
+*)
+ val Clause {parameters, thm = th1, ...} = cl1
+ and Clause {thm = th2, ...} = cl2
+ val sub = Subst.unify Subst.empty tm1 tm2
+ val lit1 = Literal.subst sub lit1
+ and lit2 = Literal.subst sub lit2
+ and th1 = Thm.subst sub th1
+ and th2 = Thm.subst sub th2
+ val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
+(*TRACE5
+ (trace "Clause.paramodulate: cl1 ordering\n"; false) orelse
+*)
+ raise Error "paramodulate: with clause: ordering constraints"
+ val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
+(*TRACE5
+ (trace "Clause.paramodulate: cl2 ordering\n"; false) orelse
+*)
+ raise Error "paramodulate: into clause: ordering constraints"
+ val eqn = (Literal.destEq lit1, th1)
+ val eqn as (l_r,_) =
+ case ort of
+ Rewrite.LeftToRight => eqn
+ | Rewrite.RightToLeft => Rule.symEqn eqn
+ val _ = isLargerTerm parameters l_r orelse
+(*TRACE5
+ (trace "Clause.paramodulate: eqn ordering\n"; false) orelse
+*)
+ raise Error "paramodulate: equation: ordering constraints"
+ val th = Rule.rewrRule eqn lit2 path th2
+(*TRACE5
+ val () = Parser.ppTrace Thm.pp "Clause.paramodulate: th" th
+*)
+ in
+ Clause {parameters = parameters, id = newId (), thm = th}
+ end;
+
+end