author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 39502 | cffceed8e7fa |
child 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *) |
|
39502 | 3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
39348 | 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 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39353
diff
changeset
|
42 |
fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l; |
39348 | 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 |