Quelle  Clause.sml

(* ========================================================================= *)
(* CLAUSE = ID + THEOREM                                                     *)
(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

structure Clause :> Clause =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

val newId =
    let
      val r = ref 0

      fun new () =
          let
            val ref n = r

            val () = r := n + 1
          in
            n
          end
    in
      fn () => Portable.critical new ()
    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 = Print.ppPair Print.ppInt Thm.pp;
in
  fun pp (Clause {id,thm,...}) =
      if !showId then ppIdThm (id,thm) else Thm.pp thm;
end;

fun toString cl = Print.toString pp cl;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

val default : parameters =
    {ordering = KnuthBendixOrder.default,
     orderLiterals = 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 =
      case total Atom.destEq atm of
        NONE => [Term.Fn atm]
      | SOME (l,r) => [l,r];

  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;

(*MetisTrace6
val largestLiterals = fn cl =>
    let
      val ppResult = LiteralSet.pp
      val () = Print.trace pp "Clause.largestLiterals: cl" cl
      val result = largestLiterals cl
      val () = Print.trace 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
        List.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};

local
  fun simp rewr (parm : parameters) id th =
      let
        val {ordering,...} = parm
        val cmp = KnuthBendixOrder.compare ordering
      in
        Rewrite.rewriteIdRule rewr cmp id th
      end;
in
  fun rewrite rewr cl =
      let
        val Clause {parameters = parm, id, thm = th} = cl

(*MetisTrace4
        val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr
        val () = Print.trace Print.ppInt "Clause.rewrite: id" id
        val () = Print.trace pp "Clause.rewrite: cl" cl
*)

        val th =
            case Rewrite.peek rewr id of
              NONE => simp rewr parm id th
            | SOME ((_,th),_) =>
              if Rewrite.isReduced rewr then th else simp rewr parm id th

        val result = Clause {parameters = parm, id = id, thm = th}

(*MetisTrace4
        val () = Print.trace pp "Clause.rewrite: result" result
*)
      in
        result
      end
(*MetisDebug
      handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
*)
end;

(* ------------------------------------------------------------------------- *)
(* 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
      List.map apply (Rule.factor' lits)
    end;

(*MetisTrace5
val factor = fn cl =>
    let
      val () = Print.trace pp "Clause.factor: cl" cl
      val result = factor cl
      val () = Print.trace (Print.ppList pp) "Clause.factor: result" result
    in
      result
    end;
*)

fun resolve (cl1,lit1) (cl2,lit2) =
    let
(*MetisTrace5
      val () = Print.trace pp "Clause.resolve: cl1" cl1
      val () = Print.trace Literal.pp "Clause.resolve: lit1" lit1
      val () = Print.trace pp "Clause.resolve: cl2" cl2
      val () = Print.trace 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)
(*MetisTrace5
      val () = Print.trace 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
(*MetisTrace5
              (trace "Clause.resolve: th1 violates ordering\n"; false) orelse
*)
              raise Error "resolve: clause1: ordering constraints"
      val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
(*MetisTrace5
              (trace "Clause.resolve: th2 violates ordering\n"; false) orelse
*)
              raise Error "resolve: clause2: ordering constraints"
      val th = Thm.resolve lit1 th1 th2
(*MetisTrace5
      val () = Print.trace Thm.pp "Clause.resolve: th" th
*)
      val cl = Clause {parameters = parameters, id = newId (), thm = th}
(*MetisTrace5
      val () = Print.trace pp "Clause.resolve: cl" cl
*)
    in
      cl
    end;

fun paramodulate (cl1,lit1,ort1,tm1) (cl2,lit2,path2,tm2) =
    let
(*MetisTrace5
      val () = Print.trace pp "Clause.paramodulate: cl1" cl1
      val () = Print.trace Literal.pp "Clause.paramodulate: lit1" lit1
      val () = Print.trace Rewrite.ppOrient "Clause.paramodulate: ort1" ort1
      val () = Print.trace Term.pp "Clause.paramodulate: tm1" tm1
      val () = Print.trace pp "Clause.paramodulate: cl2" cl2
      val () = Print.trace Literal.pp "Clause.paramodulate: lit2" lit2
      val () = Print.trace Term.ppPath "Clause.paramodulate: path2" path2
      val () = Print.trace Term.pp "Clause.paramodulate: tm2" tm2
*)
      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
              raise Error "Clause.paramodulate: with clause: ordering"
      val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
              raise Error "Clause.paramodulate: into clause: ordering"

      val eqn = (Literal.destEq lit1, th1)
      val eqn as (l_r,_) =
          case ort1 of
            Rewrite.LeftToRight => eqn
          | Rewrite.RightToLeft => Rule.symEqn eqn
(*MetisTrace6
      val () = Print.trace Rule.ppEquation "Clause.paramodulate: eqn" eqn
*)
      val _ = isLargerTerm parameters l_r orelse
              raise Error "Clause.paramodulate: equation: ordering constraints"
      val th = Rule.rewrRule eqn lit2 path2 th2
(*MetisTrace5
      val () = Print.trace Thm.pp "Clause.paramodulate: th" th
*)
    in
      Clause {parameters = parameters, id = newId (), thm = th}
    end
(*MetisTrace5
    handle Error err =>
      let
        val () = trace ("Clause.paramodulate: failed: " ^ err ^ "\n")
      in
        raise Error err
      end;
*)

end