|
1 (* ========================================================================= *) |
|
2 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *) |
|
3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure LiteralNet :> LiteralNet = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* A type of literal sets that can be efficiently matched and unified. *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 type parameters = AtomNet.parameters; |
|
16 |
|
17 type 'a literalNet = |
|
18 {positive : 'a AtomNet.atomNet, |
|
19 negative : 'a AtomNet.atomNet}; |
|
20 |
|
21 (* ------------------------------------------------------------------------- *) |
|
22 (* Basic operations. *) |
|
23 (* ------------------------------------------------------------------------- *) |
|
24 |
|
25 fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm}; |
|
26 |
|
27 local |
|
28 fun pos ({positive,...} : 'a literalNet) = AtomNet.size positive; |
|
29 |
|
30 fun neg ({negative,...} : 'a literalNet) = AtomNet.size negative; |
|
31 in |
|
32 fun size net = pos net + neg net; |
|
33 |
|
34 fun profile net = {positive = pos net, negative = neg net}; |
|
35 end; |
|
36 |
|
37 fun 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 |
|
42 fun fromList parm l = foldl (fn (lit_a,n) => insert n lit_a) (new parm) l; |
|
43 |
|
44 fun filter pred {positive,negative} = |
|
45 {positive = AtomNet.filter pred positive, |
|
46 negative = AtomNet.filter pred negative}; |
|
47 |
|
48 fun toString net = "LiteralNet[" ^ Int.toString (size net) ^ "]"; |
|
49 |
|
50 fun pp ppA = |
|
51 Parser.ppMap |
|
52 (fn {positive,negative} => (positive,negative)) |
|
53 (Parser.ppBinop " + 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 |
|
62 fun match ({positive,...} : 'a literalNet) (true,atm) = |
|
63 AtomNet.match positive atm |
|
64 | match {negative,...} (false,atm) = AtomNet.match negative atm; |
|
65 |
|
66 fun matched ({positive,...} : 'a literalNet) (true,atm) = |
|
67 AtomNet.matched positive atm |
|
68 | matched {negative,...} (false,atm) = AtomNet.matched negative atm; |
|
69 |
|
70 fun unify ({positive,...} : 'a literalNet) (true,atm) = |
|
71 AtomNet.unify positive atm |
|
72 | unify {negative,...} (false,atm) = AtomNet.unify negative atm; |
|
73 |
|
74 end |