author | wenzelm |
Wed, 20 Jun 2007 22:07:52 +0200 | |
changeset 23442 | 028e39e5e8f3 |
child 23510 | 4521fead5609 |
permissions | -rw-r--r-- |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
1 |
(* ========================================================================= *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
2 |
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
3 |
(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
4 |
(* ========================================================================= *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
5 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
6 |
structure Subsume :> Subsume = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
7 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
open Useful; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
10 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
12 |
(* Helper functions. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
13 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
14 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
15 |
fun findRest pred = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
16 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
17 |
fun f _ [] = NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
| f ys (x :: xs) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
if pred x then SOME (x, List.revAppend (ys,xs)) else f (x :: ys) xs |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
f [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
24 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
25 |
fun addSym (lit,acc) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
26 |
case total Literal.sym lit of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
27 |
NONE => acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
28 |
| SOME lit => lit :: acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
29 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
30 |
fun clauseSym lits = List.foldl addSym lits lits; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
32 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
33 |
fun sortClause cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
34 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
35 |
val lits = LiteralSet.toList cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
36 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
37 |
sortMap Literal.typedSymbols (revCompare Int.compare) lits |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
38 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
39 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
40 |
fun incompatible lit = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
41 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
42 |
val lits = clauseSym [lit] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
43 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
44 |
fn lit' => not (List.exists (can (Literal.unify Subst.empty lit')) lits) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
45 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
46 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
47 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
48 |
(* Clause ids and lengths. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
49 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
50 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
51 |
type clauseId = int; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
52 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
53 |
type clauseLength = int; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
54 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
55 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
56 |
type idSet = (clauseId * clauseLength) Set.set; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
57 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
58 |
fun idCompare ((id1,len1),(id2,len2)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
59 |
case Int.compare (len1,len2) of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
60 |
LESS => LESS |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
61 |
| EQUAL => Int.compare (id1,id2) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
62 |
| GREATER => GREATER; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
63 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
64 |
val idSetEmpty : idSet = Set.empty idCompare; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
65 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
66 |
fun idSetAdd (id_len,set) : idSet = Set.add set id_len; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
67 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
68 |
fun idSetAddMax max (id_len as (_,len), set) : idSet = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
69 |
if len <= max then Set.add set id_len else set; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
70 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
71 |
fun idSetIntersect set1 set2 : idSet = Set.intersect set1 set2; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
72 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
73 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
74 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
75 |
(* A type of clause sets that supports efficient subsumption checking. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
76 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
77 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
78 |
datatype 'a subsume = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
79 |
Subsume of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
80 |
{empty : (Thm.clause * Subst.subst * 'a) list, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
81 |
unit : (Literal.literal * Thm.clause * 'a) LiteralNet.literalNet, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
82 |
nonunit : |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
83 |
{nextId : clauseId, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
84 |
clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
85 |
fstLits : (clauseId * clauseLength) LiteralNet.literalNet, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
86 |
sndLits : (clauseId * clauseLength) LiteralNet.literalNet}}; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
87 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
88 |
fun new () = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
89 |
Subsume |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
90 |
{empty = [], |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
91 |
unit = LiteralNet.new {fifo = false}, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
92 |
nonunit = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
93 |
{nextId = 0, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
94 |
clauses = IntMap.new (), |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
95 |
fstLits = LiteralNet.new {fifo = false}, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
96 |
sndLits = LiteralNet.new {fifo = false}}}; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
97 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
98 |
fun size (Subsume {empty, unit, nonunit = {clauses,...}}) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
99 |
length empty + LiteralNet.size unit + IntMap.size clauses; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
100 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
101 |
fun insert (Subsume {empty,unit,nonunit}) (cl',a) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
102 |
case sortClause cl' of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
103 |
[] => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
104 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
105 |
val empty = (cl',Subst.empty,a) :: empty |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
106 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
107 |
Subsume {empty = empty, unit = unit, nonunit = nonunit} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
108 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
109 |
| [lit] => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
110 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
111 |
val unit = LiteralNet.insert unit (lit,(lit,cl',a)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
112 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
113 |
Subsume {empty = empty, unit = unit, nonunit = nonunit} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
114 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
115 |
| fstLit :: (nonFstLits as sndLit :: otherLits) => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
116 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
117 |
val {nextId,clauses,fstLits,sndLits} = nonunit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
118 |
val id_length = (nextId, LiteralSet.size cl') |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
119 |
val fstLits = LiteralNet.insert fstLits (fstLit,id_length) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
120 |
val (sndLit,otherLits) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
121 |
case findRest (incompatible fstLit) nonFstLits of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
122 |
SOME sndLit_otherLits => sndLit_otherLits |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
123 |
| NONE => (sndLit,otherLits) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
124 |
val sndLits = LiteralNet.insert sndLits (sndLit,id_length) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
125 |
val lits' = otherLits @ [fstLit,sndLit] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
126 |
val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
127 |
val nextId = nextId + 1 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
128 |
val nonunit = {nextId = nextId, clauses = clauses, |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
129 |
fstLits = fstLits, sndLits = sndLits} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
130 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
131 |
Subsume {empty = empty, unit = unit, nonunit = nonunit} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
132 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
133 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
134 |
fun filter pred (Subsume {empty,unit,nonunit}) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
135 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
136 |
val empty = List.filter (pred o #3) empty |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
137 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
138 |
val unit = LiteralNet.filter (pred o #3) unit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
139 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
140 |
val nonunit = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
141 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
142 |
val {nextId,clauses,fstLits,sndLits} = nonunit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
143 |
val clauses' = IntMap.filter (pred o #3 o snd) clauses |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
144 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
145 |
if IntMap.size clauses = IntMap.size clauses' then nonunit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
146 |
else |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
147 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
148 |
fun predId (id,_) = IntMap.inDomain id clauses' |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
149 |
val fstLits = LiteralNet.filter predId fstLits |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
150 |
and sndLits = LiteralNet.filter predId sndLits |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
151 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
152 |
{nextId = nextId, clauses = clauses', |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
153 |
fstLits = fstLits, sndLits = sndLits} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
154 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
155 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
156 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
157 |
Subsume {empty = empty, unit = unit, nonunit = nonunit} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
158 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
159 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
160 |
fun toString subsume = "Subsume{" ^ Int.toString (size subsume) ^ "}"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
161 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
162 |
fun pp p = Parser.ppMap toString Parser.ppString p; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
163 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
164 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
165 |
(* Subsumption checking. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
166 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
167 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
168 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
169 |
fun matchLit lit' (lit,acc) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
170 |
case total (Literal.match Subst.empty lit') lit of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
171 |
SOME sub => sub :: acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
172 |
| NONE => acc; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
173 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
174 |
fun genClauseSubsumes pred cl' lits' cl a = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
175 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
176 |
fun mkSubsl acc sub [] = SOME (sub, sortMap length Int.compare acc) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
177 |
| mkSubsl acc sub (lit' :: lits') = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
178 |
case List.foldl (matchLit lit') [] cl of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
179 |
[] => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
180 |
| [sub'] => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
181 |
(case total (Subst.union sub) sub' of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
182 |
NONE => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
183 |
| SOME sub => mkSubsl acc sub lits') |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
184 |
| subs => mkSubsl (subs :: acc) sub lits' |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
185 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
186 |
fun search [] = NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
187 |
| search ((sub,[]) :: others) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
188 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
189 |
val x = (cl',sub,a) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
190 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
191 |
if pred x then SOME x else search others |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
192 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
193 |
| search ((_, [] :: _) :: others) = search others |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
194 |
| search ((sub, (sub' :: subs) :: subsl) :: others) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
195 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
196 |
val others = (sub, subs :: subsl) :: others |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
197 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
198 |
case total (Subst.union sub) sub' of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
199 |
NONE => search others |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
200 |
| SOME sub => search ((sub,subsl) :: others) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
201 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
202 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
203 |
case mkSubsl [] Subst.empty lits' of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
204 |
NONE => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
205 |
| SOME sub_subsl => search [sub_subsl] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
206 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
207 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
208 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
209 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
210 |
fun emptySubsumes pred empty = List.find pred empty; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
211 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
212 |
fun unitSubsumes pred unit = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
213 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
214 |
fun subLit lit = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
215 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
216 |
fun subUnit (lit',cl',a) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
217 |
case total (Literal.match Subst.empty lit') lit of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
218 |
NONE => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
219 |
| SOME sub => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
220 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
221 |
val x = (cl',sub,a) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
222 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
223 |
if pred x then SOME x else NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
224 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
225 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
226 |
first subUnit (LiteralNet.match unit lit) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
227 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
228 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
229 |
first subLit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
230 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
231 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
232 |
fun nonunitSubsumes pred nonunit max cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
233 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
234 |
val addId = case max of NONE => idSetAdd | SOME n => idSetAddMax n |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
235 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
236 |
fun subLit lits (lit,acc) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
237 |
List.foldl addId acc (LiteralNet.match lits lit) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
238 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
239 |
val {nextId = _, clauses, fstLits, sndLits} = nonunit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
240 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
241 |
fun subCl' (id,_) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
242 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
243 |
val (lits',cl',a) = IntMap.get clauses id |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
244 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
245 |
genClauseSubsumes pred cl' lits' cl a |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
246 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
247 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
248 |
val fstCands = List.foldl (subLit fstLits) idSetEmpty cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
249 |
val sndCands = List.foldl (subLit sndLits) idSetEmpty cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
250 |
val cands = idSetIntersect fstCands sndCands |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
251 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
252 |
Set.firstl subCl' cands |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
253 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
254 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
255 |
fun genSubsumes pred (Subsume {empty,unit,nonunit}) max cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
256 |
case emptySubsumes pred empty of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
257 |
s as SOME _ => s |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
258 |
| NONE => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
259 |
if max = SOME 0 then NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
260 |
else |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
261 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
262 |
val cl = clauseSym (LiteralSet.toList cl) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
263 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
264 |
case unitSubsumes pred unit cl of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
265 |
s as SOME _ => s |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
266 |
| NONE => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
267 |
if max = SOME 1 then NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
268 |
else nonunitSubsumes pred nonunit max cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
269 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
270 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
271 |
fun subsumes pred subsume cl = genSubsumes pred subsume NONE cl; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
272 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
273 |
fun strictlySubsumes pred subsume cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
274 |
genSubsumes pred subsume (SOME (LiteralSet.size cl)) cl; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
275 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
276 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
277 |
(*TRACE4 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
278 |
val subsumes = fn pred => fn subsume => fn cl => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
279 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
280 |
val ppCl = LiteralSet.pp |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
281 |
val ppSub = Subst.pp |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
282 |
val () = Parser.ppTrace ppCl "Subsume.subsumes: cl" cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
283 |
val result = subsumes pred subsume cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
284 |
val () = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
285 |
case result of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
286 |
NONE => trace "Subsume.subsumes: not subsumed\n" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
287 |
| SOME (cl,sub,_) => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
288 |
(Parser.ppTrace ppCl "Subsume.subsumes: subsuming cl" cl; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
289 |
Parser.ppTrace ppSub "Subsume.subsumes: subsuming sub" sub) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
290 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
291 |
result |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
292 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
293 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
294 |
val strictlySubsumes = fn pred => fn subsume => fn cl => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
295 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
296 |
val ppCl = LiteralSet.pp |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
297 |
val ppSub = Subst.pp |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
298 |
val () = Parser.ppTrace ppCl "Subsume.strictlySubsumes: cl" cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
299 |
val result = strictlySubsumes subsume cl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
300 |
val () = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
301 |
case result of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
302 |
NONE => trace "Subsume.subsumes: not subsumed\n" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
303 |
| SOME (cl,sub,_) => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
304 |
(Parser.ppTrace ppCl "Subsume.subsumes: subsuming cl" cl; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
305 |
Parser.ppTrace ppSub "Subsume.subsumes: subsuming sub" sub) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
306 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
307 |
result |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
308 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
309 |
*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
310 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
311 |
fun isSubsumed subs cl = Option.isSome (subsumes (K true) subs cl); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
312 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
313 |
fun isStrictlySubsumed subs cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
314 |
Option.isSome (strictlySubsumes (K true) subs cl); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
315 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
316 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
317 |
(* Single clause versions. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
318 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
319 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
320 |
fun clauseSubsumes cl' cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
321 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
322 |
val lits' = sortClause cl' |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
323 |
and lits = clauseSym (LiteralSet.toList cl) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
324 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
325 |
case genClauseSubsumes (K true) cl' lits' lits () of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
326 |
SOME (_,sub,()) => SOME sub |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
327 |
| NONE => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
328 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
329 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
330 |
fun clauseStrictlySubsumes cl' cl = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
331 |
if LiteralSet.size cl' > LiteralSet.size cl then NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
332 |
else clauseSubsumes cl' cl; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
333 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
334 |
end |