SSL Subsume.sml Sprache: SML

(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES                        *)
(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

structure Subsume :> Subsume =
struct

open Useful;

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

fun findRest pred =
    let
      fun f _ [] = NONE
        | f ys (x :: xs) =
          if pred x then SOME (x, List.revAppend (ys,xs)) else f (x :: ys) xs
    in
      f []
    end;

local
  fun addSym (lit,acc) =
      case total Literal.sym lit of
        NONE => acc
      | SOME lit => lit :: acc
in
  fun clauseSym lits = List.foldl addSym lits lits;
end;

fun sortClause cl =
    let
      val lits = LiteralSet.toList cl
    in
      sortMap Literal.typedSymbols (revCompare Int.compare) lits
    end;

fun incompatible lit =
    let
      val lits = clauseSym [lit]
    in
      fn lit' => not (List.exists (can (Literal.unify Subst.empty lit')) lits)
    end;

(* ------------------------------------------------------------------------- *)
(* Clause ids and lengths.                                                   *)
(* ------------------------------------------------------------------------- *)

type clauseId = int;

type clauseLength = int;

local
  type idSet = (clauseId * clauseLength) Set.set;

  fun idCompare ((id1,len1),(id2,len2)) =
      case Int.compare (len1,len2) of
        LESS => LESS
      | EQUAL => Int.compare (id1,id2)
      | GREATER => GREATER;
in
  val idSetEmpty : idSet = Set.empty idCompare;

  fun idSetAdd (id_len,set) : idSet = Set.add set id_len;

  fun idSetAddMax max (id_len as (_,len), set) : idSet =
      if len <= max then Set.add set id_len else set;

  fun idSetIntersect set1 set2 : idSet = Set.intersect set1 set2;
end;

(* ------------------------------------------------------------------------- *)
(* A type of clause sets that supports efficient subsumption checking.       *)
(* ------------------------------------------------------------------------- *)

datatype 'a subsume =
    Subsume of
      {empty : (Thm.clause * Subst.subst * 'a) list,
       unit : (Literal.literal * Thm.clause * 'a) LiteralNet.literalNet,
       nonunit :
         {nextId : clauseId,
          clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map,
          fstLits : (clauseId * clauseLength) LiteralNet.literalNet,
          sndLits : (clauseId * clauseLength) LiteralNet.literalNet}};

fun new () =
    Subsume
      {empty = [],
       unit = LiteralNet.new {fifo = false},
       nonunit =
         {nextId = 0,
          clauses = IntMap.new (),
          fstLits = LiteralNet.new {fifo = false},
          sndLits = LiteralNet.new {fifo = false}}};

fun size (Subsume {empty, unit, nonunit = {clauses,...}}) =
    length empty + LiteralNet.size unit + IntMap.size clauses;

fun insert (Subsume {empty,unit,nonunit}) (cl',a) =
    case sortClause cl' of
      [] =>
      let
        val empty = (cl',Subst.empty,a) :: empty
      in
        Subsume {empty = empty, unit = unit, nonunit = nonunit}
      end
    | [lit] =>
      let
        val unit = LiteralNet.insert unit (lit,(lit,cl',a))
      in
        Subsume {empty = empty, unit = unit, nonunit = nonunit}
      end
    | fstLit :: (nonFstLits as sndLit :: otherLits) =>
      let
        val {nextId,clauses,fstLits,sndLits} = nonunit
        val id_length = (nextId, LiteralSet.size cl')
        val fstLits = LiteralNet.insert fstLits (fstLit,id_length)
        val (sndLit,otherLits) =
            case findRest (incompatible fstLit) nonFstLits of
              SOME sndLit_otherLits => sndLit_otherLits
            | NONE => (sndLit,otherLits)
        val sndLits = LiteralNet.insert sndLits (sndLit,id_length)
        val lits' = otherLits @ [fstLit,sndLit]
        val clauses = IntMap.insert clauses (nextId,(lits',cl',a))
        val nextId = nextId + 1
        val nonunit = {nextId = nextId, clauses = clauses,
                       fstLits = fstLits, sndLits = sndLits}
      in
        Subsume {empty = empty, unit = unit, nonunit = nonunit}
      end;

fun filter pred (Subsume {empty,unit,nonunit}) =
    let
      val empty = List.filter (pred o #3) empty

      val unit = LiteralNet.filter (pred o #3) unit

      val nonunit =
          let
            val {nextId,clauses,fstLits,sndLits} = nonunit
            val clauses' = IntMap.filter (pred o #3 o snd) clauses
          in
            if IntMap.size clauses = IntMap.size clauses' then nonunit
            else
              let
                fun predId (id,_) = IntMap.inDomain id clauses'
                val fstLits = LiteralNet.filter predId fstLits
                and sndLits = LiteralNet.filter predId sndLits
              in
                {nextId = nextId, clauses = clauses',
                 fstLits = fstLits, sndLits = sndLits}
              end
          end
    in
      Subsume {empty = empty, unit = unit, nonunit = nonunit}
    end;

fun toString subsume = "Subsume{" ^ Int.toString (size subsume) ^ "}";

fun pp subsume = Print.ppMap toString Print.ppString subsume;

(* ------------------------------------------------------------------------- *)
(* Subsumption checking.                                                     *)
(* ------------------------------------------------------------------------- *)

local
  fun matchLit lit' (lit,acc) =
      case total (Literal.match Subst.empty lit') lit of
        SOME sub => sub :: acc
      | NONE => acc;
in
  fun genClauseSubsumes pred cl' lits' cl a =
      let
        fun mkSubsl acc sub [] = SOME (sub, sortMap length Int.compare acc)
          | mkSubsl acc sub (lit' :: lits') =
            case List.foldl (matchLit lit') [] cl of
              [] => NONE
            | [sub'] =>
              (case total (Subst.union sub) sub' of
                 NONE => NONE
               | SOME sub => mkSubsl acc sub lits')
            | subs => mkSubsl (subs :: acc) sub lits'

        fun search [] = NONE
          | search ((sub,[]) :: others) =
            let
              val x = (cl',sub,a)
            in
              if pred x then SOME x else search others
            end
          | search ((_, [] :: _) :: others) = search others
          | search ((sub, (sub' :: subs) :: subsl) :: others) =
            let
              val others = (sub, subs :: subsl) :: others
            in
              case total (Subst.union sub) sub' of
                NONE => search others
              | SOME sub => search ((sub,subsl) :: others)
            end
      in
        case mkSubsl [] Subst.empty lits' of
          NONE => NONE
        | SOME sub_subsl => search [sub_subsl]
      end;
end;

local
  fun emptySubsumes pred empty = List.find pred empty;

  fun unitSubsumes pred unit =
      let
        fun subLit lit =
            let
              fun subUnit (lit',cl',a) =
                  case total (Literal.match Subst.empty lit') lit of
                    NONE => NONE
                  | SOME sub =>
                    let
                      val x = (cl',sub,a)
                    in
                      if pred x then SOME x else NONE
                    end
            in
              first subUnit (LiteralNet.match unit lit)
            end
      in
        first subLit
      end;

  fun nonunitSubsumes pred nonunit max cl =
      let
        val addId = case max of NONE => idSetAdd | SOME n => idSetAddMax n

        fun subLit lits (lit,acc) =
            List.foldl addId acc (LiteralNet.match lits lit)

        val {nextId = _, clauses, fstLits, sndLits} = nonunit

        fun subCl' (id,_) =
            let
              val (lits',cl',a) = IntMap.get clauses id
            in
              genClauseSubsumes pred cl' lits' cl a
            end

        val fstCands = List.foldl (subLit fstLits) idSetEmpty cl
        val sndCands = List.foldl (subLit sndLits) idSetEmpty cl
        val cands = idSetIntersect fstCands sndCands
      in
        Set.firstl subCl' cands
      end;

  fun genSubsumes pred (Subsume {empty,unit,nonunit}) max cl =
      case emptySubsumes pred empty of
        s as SOME _ => s
      | NONE =>
        if max = SOME 0 then NONE
        else
          let
            val cl = clauseSym (LiteralSet.toList cl)
          in
            case unitSubsumes pred unit cl of
              s as SOME _ => s
            | NONE =>
              if max = SOME 1 then NONE
              else nonunitSubsumes pred nonunit max cl
          end;
in
  fun subsumes pred subsume cl = genSubsumes pred subsume NONE cl;

  fun strictlySubsumes pred subsume cl =
      genSubsumes pred subsume (SOME (LiteralSet.size cl)) cl;
end;

(*MetisTrace4
val subsumes = fn pred => fn subsume => fn cl =>
    let
      val ppCl = LiteralSet.pp
      val ppSub = Subst.pp
      val () = Print.trace ppCl "Subsume.subsumes: cl" cl
      val result = subsumes pred subsume cl
      val () =
          case result of
            NONE => trace "Subsume.subsumes: not subsumed\n"
          | SOME (cl,sub,_) =>
            (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl;
             Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
    in
      result
    end;

val strictlySubsumes = fn pred => fn subsume => fn cl =>
    let
      val ppCl = LiteralSet.pp
      val ppSub = Subst.pp
      val () = Print.trace ppCl "Subsume.strictlySubsumes: cl" cl
      val result = strictlySubsumes pred subsume cl
      val () =
          case result of
            NONE => trace "Subsume.subsumes: not subsumed\n"
          | SOME (cl,sub,_) =>
            (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl;
             Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
    in
      result
    end;
*)

fun isSubsumed subs cl = Option.isSome (subsumes (K true) subs cl);

fun isStrictlySubsumed subs cl =
    Option.isSome (strictlySubsumes (K true) subs cl);

(* ------------------------------------------------------------------------- *)
(* Single clause versions.                                                   *)
(* ------------------------------------------------------------------------- *)

fun clauseSubsumes cl' cl =
    let
      val lits' = sortClause cl'
      and lits = clauseSym (LiteralSet.toList cl)
    in
      case genClauseSubsumes (K true) cl' lits' lits () of
        SOME (_,sub,()) => SOME sub
      | NONE => NONE
    end;

fun clauseStrictlySubsumes cl' cl =
    if LiteralSet.size cl' > LiteralSet.size cl then NONE
    else clauseSubsumes cl' cl;

end

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.