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
6structure LiteralNet :> LiteralNet =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* A type of literal sets that can be efficiently matched and unified.       *)
13(* ------------------------------------------------------------------------- *)
14
15type parameters = AtomNet.parameters;
16
17type 'a literalNet =
18    {positive : 'a AtomNet.atomNet,
19     negative : 'a AtomNet.atomNet};
20
21(* ------------------------------------------------------------------------- *)
22(* Basic operations.                                                         *)
23(* ------------------------------------------------------------------------- *)
24
25fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm};
26
27local
28  fun pos ({positive,...} : 'a literalNet) = AtomNet.size positive;
29
30  fun neg ({negative,...} : 'a literalNet) = AtomNet.size negative;
31in
32  fun size net = pos net + neg net;
33
34  fun profile net = {positive = pos net, negative = neg net};
35end;
36
37fun insert {positive,negative} ((true,atm),a) =
38    {positive = AtomNet.insert positive (atm,a), negative = negative}
39  | insert {positive,negative} ((false,atm),a) =
40    {positive = positive, negative = AtomNet.insert negative (atm,a)};
41
42fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
43
44fun filter pred {positive,negative} =
45    {positive = AtomNet.filter pred positive,
46     negative = AtomNet.filter pred negative};
47
48fun toString net = "LiteralNet[" ^ Int.toString (size net) ^ "]";
49
50fun pp ppA =
51    Print.ppMap
52      (fn {positive,negative} => (positive,negative))
53      (Print.ppOp2 " + NEGATIVE" (AtomNet.pp ppA) (AtomNet.pp ppA));
54
55(* ------------------------------------------------------------------------- *)
56(* Matching and unification queries.                                         *)
57(*                                                                           *)
58(* These function return OVER-APPROXIMATIONS!                                *)
59(* Filter afterwards to get the precise set of satisfying values.            *)
60(* ------------------------------------------------------------------------- *)
61
62fun match ({positive,...} : 'a literalNet) (true,atm) =
63    AtomNet.match positive atm
64  | match {negative,...} (false,atm) = AtomNet.match negative atm;
65
66fun matched ({positive,...} : 'a literalNet) (true,atm) =
67    AtomNet.matched positive atm
68  | matched {negative,...} (false,atm) = AtomNet.matched negative atm;
69
70fun unify ({positive,...} : 'a literalNet) (true,atm) =
71    AtomNet.unify positive atm
72  | unify {negative,...} (false,atm) = AtomNet.unify negative atm;
73
74end
75