39348
|
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 |
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 |
|
|
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
|