1(* ========================================================================= *) 2(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature LiteralNet = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of literal sets that can be efficiently matched and unified. *) 11(* ------------------------------------------------------------------------- *) 12 13type parameters = {fifo : bool} 14 15type 'a literalNet 16 17(* ------------------------------------------------------------------------- *) 18(* Basic operations. *) 19(* ------------------------------------------------------------------------- *) 20 21val new : parameters -> 'a literalNet 22 23val size : 'a literalNet -> int 24 25val profile : 'a literalNet -> {positive : int, negative : int} 26 27val insert : 'a literalNet -> Literal.literal * 'a -> 'a literalNet 28 29val fromList : parameters -> (Literal.literal * 'a) list -> 'a literalNet 30 31val filter : ('a -> bool) -> 'a literalNet -> 'a literalNet 32 33val toString : 'a literalNet -> string 34 35val pp : 'a Print.pp -> 'a literalNet Print.pp 36 37(* ------------------------------------------------------------------------- *) 38(* Matching and unification queries. *) 39(* *) 40(* These function return OVER-APPROXIMATIONS! *) 41(* Filter afterwards to get the precise set of satisfying values. *) 42(* ------------------------------------------------------------------------- *) 43 44val match : 'a literalNet -> Literal.literal -> 'a list 45 46val matched : 'a literalNet -> Literal.literal -> 'a list 47 48val unify : 'a literalNet -> Literal.literal -> 'a list 49 50end 51