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