products/sources/formale sprachen/Isabelle/Tools/Metis/src/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: CTL.thy   Sprache: Isabelle

Untersuchungsergebnis.sig Download desText {Text[127] Isabelle[135] Abap[169]}zum Wurzelverzeichnis wechseln

(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

signature LiteralNet =
sig

(* ------------------------------------------------------------------------- *)
(* A type of literal sets that can be efficiently matched and unified.       *)
(* ------------------------------------------------------------------------- *)

type parameters = {fifo : bool}

type 'a literalNet

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

val new : parameters -> 'a literalNet

val size : 'a literalNet -> int

val profile : 'a literalNet -> {positive : int, negative : int}

val insert : 'a literalNet -> Literal.literal * 'a -> 'a literalNet

val fromList : parameters -> (Literal.literal * 'a) list -> 'a literalNet

val filter : ('a -> bool) -> 'a literalNet -> 'a literalNet

val toString : 'a literalNet -> string

val pp : 'a Print.pp -> 'a literalNet Print.pp

(* ------------------------------------------------------------------------- *)
(* Matching and unification queries.                                         *)
(*                                                                           *)
(* These function return OVER-APPROXIMATIONS!                                *)
(* Filter afterwards to get the precise set of satisfying values.            *)
(* ------------------------------------------------------------------------- *)

val match : 'a literalNet -> Literal.literal -> 'a list

val matched : 'a literalNet -> Literal.literal -> 'a list

val unify : 'a literalNet -> Literal.literal -> 'a list

end

[ zur Elbe Produktseite wechseln0.108Quellennavigators  ]