author | blanchet |
Thu, 24 Mar 2011 17:49:27 +0100 | |
changeset 42102 | fcfd07f122d4 |
parent 39502 | cffceed8e7fa |
child 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* THE WAITING SET OF CLAUSES *) |
|
39502 | 3 |
(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Waiting :> Waiting = |
|
7 |
struct |
|
8 |
||
9 |
open Useful; |
|
10 |
||
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
(* A type of waiting sets of clauses. *) |
|
13 |
(* ------------------------------------------------------------------------- *) |
|
14 |
||
15 |
type weight = real; |
|
16 |
||
17 |
type modelParameters = |
|
18 |
{model : Model.parameters, |
|
19 |
initialPerturbations : int, |
|
20 |
maxChecks : int option, |
|
21 |
perturbations : int, |
|
22 |
weight : weight} |
|
23 |
||
24 |
type parameters = |
|
25 |
{symbolsWeight : weight, |
|
26 |
variablesWeight : weight, |
|
27 |
literalsWeight : weight, |
|
28 |
models : modelParameters list}; |
|
29 |
||
30 |
type distance = real; |
|
31 |
||
32 |
datatype waiting = |
|
33 |
Waiting of |
|
34 |
{parameters : parameters, |
|
35 |
clauses : (weight * (distance * Clause.clause)) Heap.heap, |
|
36 |
models : Model.model list}; |
|
37 |
||
38 |
(* ------------------------------------------------------------------------- *) |
|
39 |
(* Basic operations. *) |
|
40 |
(* ------------------------------------------------------------------------- *) |
|
41 |
||
42 |
val defaultModels : modelParameters list = |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39407
diff
changeset
|
43 |
[{model = Model.default, |
39348 | 44 |
initialPerturbations = 100, |
45 |
maxChecks = SOME 20, |
|
46 |
perturbations = 0, |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39407
diff
changeset
|
47 |
weight = 1.0}]; |
39348 | 48 |
|
49 |
val default : parameters = |
|
50 |
{symbolsWeight = 1.0, |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39407
diff
changeset
|
51 |
literalsWeight = 1.0, |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39407
diff
changeset
|
52 |
variablesWeight = 1.0, |
39348 | 53 |
models = defaultModels}; |
54 |
||
55 |
fun size (Waiting {clauses,...}) = Heap.size clauses; |
|
56 |
||
57 |
val pp = |
|
58 |
Print.ppMap |
|
59 |
(fn w => "Waiting{" ^ Int.toString (size w) ^ "}") |
|
60 |
Print.ppString; |
|
61 |
||
62 |
(*MetisDebug |
|
63 |
val pp = |
|
64 |
Print.ppMap |
|
65 |
(fn Waiting {clauses,...} => |
|
42102 | 66 |
List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) |
39348 | 67 |
(Print.ppList (Print.ppTriple Print.ppReal Print.ppInt Clause.pp)); |
68 |
*) |
|
69 |
||
70 |
(* ------------------------------------------------------------------------- *) |
|
71 |
(* Perturbing the models. *) |
|
72 |
(* ------------------------------------------------------------------------- *) |
|
73 |
||
74 |
type modelClause = NameSet.set * Thm.clause; |
|
75 |
||
76 |
fun mkModelClause cl = |
|
77 |
let |
|
78 |
val lits = Clause.literals cl |
|
79 |
val fvs = LiteralSet.freeVars lits |
|
80 |
in |
|
81 |
(fvs,lits) |
|
82 |
end; |
|
83 |
||
42102 | 84 |
val mkModelClauses = List.map mkModelClause; |
39348 | 85 |
|
86 |
fun perturbModel M cls = |
|
42102 | 87 |
if List.null cls then K () |
39348 | 88 |
else |
89 |
let |
|
90 |
val N = {size = Model.size M} |
|
91 |
||
92 |
fun perturbClause (fv,cl) = |
|
93 |
let |
|
94 |
val V = Model.randomValuation N fv |
|
95 |
in |
|
96 |
if Model.interpretClause M V cl then () |
|
97 |
else Model.perturbClause M V cl |
|
98 |
end |
|
99 |
||
100 |
fun perturbClauses () = app perturbClause cls |
|
101 |
in |
|
102 |
fn n => funpow n perturbClauses () |
|
103 |
end; |
|
104 |
||
105 |
fun initialModel axioms conjecture parm = |
|
106 |
let |
|
107 |
val {model,initialPerturbations,...} : modelParameters = parm |
|
108 |
val m = Model.new model |
|
109 |
val () = perturbModel m conjecture initialPerturbations |
|
110 |
val () = perturbModel m axioms initialPerturbations |
|
111 |
in |
|
112 |
m |
|
113 |
end; |
|
114 |
||
115 |
fun checkModels parms models (fv,cl) = |
|
116 |
let |
|
117 |
fun check ((parm,model),z) = |
|
118 |
let |
|
119 |
val {maxChecks,weight,...} : modelParameters = parm |
|
120 |
val n = {maxChecks = maxChecks} |
|
121 |
val {T,F} = Model.check Model.interpretClause n model fv cl |
|
122 |
in |
|
123 |
Math.pow (1.0 + Real.fromInt T / Real.fromInt (T + F), weight) * z |
|
124 |
end |
|
125 |
in |
|
126 |
List.foldl check 1.0 (zip parms models) |
|
127 |
end; |
|
128 |
||
129 |
fun perturbModels parms models cls = |
|
130 |
let |
|
131 |
fun perturb (parm,model) = |
|
132 |
let |
|
133 |
val {perturbations,...} : modelParameters = parm |
|
134 |
in |
|
135 |
perturbModel model cls perturbations |
|
136 |
end |
|
137 |
in |
|
138 |
app perturb (zip parms models) |
|
139 |
end; |
|
140 |
||
141 |
(* ------------------------------------------------------------------------- *) |
|
142 |
(* Clause weights. *) |
|
143 |
(* ------------------------------------------------------------------------- *) |
|
144 |
||
145 |
local |
|
146 |
fun clauseSymbols cl = Real.fromInt (LiteralSet.typedSymbols cl); |
|
147 |
||
148 |
fun clauseVariables cl = |
|
149 |
Real.fromInt (NameSet.size (LiteralSet.freeVars cl) + 1); |
|
150 |
||
151 |
fun clauseLiterals cl = Real.fromInt (LiteralSet.size cl); |
|
152 |
||
153 |
fun clausePriority cl = 1e~12 * Real.fromInt (Clause.id cl); |
|
154 |
in |
|
155 |
fun clauseWeight (parm : parameters) mods dist mcl cl = |
|
156 |
let |
|
157 |
(*MetisTrace3 |
|
158 |
val () = Print.trace Clause.pp "Waiting.clauseWeight: cl" cl |
|
159 |
*) |
|
160 |
val {symbolsWeight,variablesWeight,literalsWeight,models,...} = parm |
|
161 |
val lits = Clause.literals cl |
|
162 |
val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight) |
|
163 |
val variablesW = Math.pow (clauseVariables lits, variablesWeight) |
|
164 |
val literalsW = Math.pow (clauseLiterals lits, literalsWeight) |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39407
diff
changeset
|
165 |
val modelsW = checkModels models mods mcl |
39348 | 166 |
(*MetisTrace4 |
167 |
val () = trace ("Waiting.clauseWeight: dist = " ^ |
|
168 |
Real.toString dist ^ "\n") |
|
169 |
val () = trace ("Waiting.clauseWeight: symbolsW = " ^ |
|
170 |
Real.toString symbolsW ^ "\n") |
|
171 |
val () = trace ("Waiting.clauseWeight: variablesW = " ^ |
|
172 |
Real.toString variablesW ^ "\n") |
|
173 |
val () = trace ("Waiting.clauseWeight: literalsW = " ^ |
|
174 |
Real.toString literalsW ^ "\n") |
|
175 |
val () = trace ("Waiting.clauseWeight: modelsW = " ^ |
|
176 |
Real.toString modelsW ^ "\n") |
|
177 |
*) |
|
178 |
val weight = dist * symbolsW * variablesW * literalsW * modelsW |
|
179 |
val weight = weight + clausePriority cl |
|
180 |
(*MetisTrace3 |
|
181 |
val () = trace ("Waiting.clauseWeight: weight = " ^ |
|
182 |
Real.toString weight ^ "\n") |
|
183 |
*) |
|
184 |
in |
|
185 |
weight |
|
186 |
end; |
|
187 |
end; |
|
188 |
||
189 |
(* ------------------------------------------------------------------------- *) |
|
190 |
(* Adding new clauses. *) |
|
191 |
(* ------------------------------------------------------------------------- *) |
|
192 |
||
193 |
fun add' waiting dist mcls cls = |
|
194 |
let |
|
195 |
val Waiting {parameters,clauses,models} = waiting |
|
196 |
val {models = modelParameters, ...} = parameters |
|
197 |
||
42102 | 198 |
(*MetisDebug |
199 |
val _ = not (List.null cls) orelse |
|
200 |
raise Bug "Waiting.add': null" |
|
201 |
||
202 |
val _ = length mcls = length cls orelse |
|
203 |
raise Bug "Waiting.add': different lengths" |
|
204 |
*) |
|
205 |
||
39348 | 206 |
val dist = dist + Math.ln (Real.fromInt (length cls)) |
207 |
||
208 |
fun addCl ((mcl,cl),acc) = |
|
209 |
let |
|
210 |
val weight = clauseWeight parameters models dist mcl cl |
|
211 |
in |
|
212 |
Heap.add acc (weight,(dist,cl)) |
|
213 |
end |
|
214 |
||
215 |
val clauses = List.foldl addCl clauses (zip mcls cls) |
|
216 |
||
217 |
val () = perturbModels modelParameters models mcls |
|
218 |
in |
|
219 |
Waiting {parameters = parameters, clauses = clauses, models = models} |
|
220 |
end; |
|
221 |
||
42102 | 222 |
fun add waiting (dist,cls) = |
223 |
if List.null cls then waiting |
|
224 |
else |
|
225 |
let |
|
39348 | 226 |
(*MetisTrace3 |
42102 | 227 |
val () = Print.trace pp "Waiting.add: waiting" waiting |
228 |
val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls |
|
39348 | 229 |
*) |
230 |
||
42102 | 231 |
val waiting = add' waiting dist (mkModelClauses cls) cls |
39348 | 232 |
|
233 |
(*MetisTrace3 |
|
42102 | 234 |
val () = Print.trace pp "Waiting.add: waiting" waiting |
39348 | 235 |
*) |
42102 | 236 |
in |
237 |
waiting |
|
238 |
end; |
|
39348 | 239 |
|
240 |
local |
|
241 |
fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2); |
|
242 |
||
243 |
fun empty parameters axioms conjecture = |
|
244 |
let |
|
245 |
val {models = modelParameters, ...} = parameters |
|
246 |
val clauses = Heap.new cmp |
|
42102 | 247 |
and models = List.map (initialModel axioms conjecture) modelParameters |
39348 | 248 |
in |
249 |
Waiting {parameters = parameters, clauses = clauses, models = models} |
|
250 |
end; |
|
251 |
in |
|
252 |
fun new parameters {axioms,conjecture} = |
|
253 |
let |
|
254 |
val mAxioms = mkModelClauses axioms |
|
255 |
and mConjecture = mkModelClauses conjecture |
|
256 |
||
257 |
val waiting = empty parameters mAxioms mConjecture |
|
258 |
in |
|
42102 | 259 |
if List.null axioms andalso List.null conjecture then waiting |
260 |
else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture) |
|
261 |
end |
|
262 |
(*MetisDebug |
|
263 |
handle e => |
|
264 |
let |
|
265 |
val () = Print.trace Print.ppException "Waiting.new: exception" e |
|
266 |
in |
|
267 |
raise e |
|
268 |
end; |
|
269 |
*) |
|
39348 | 270 |
end; |
271 |
||
272 |
(* ------------------------------------------------------------------------- *) |
|
273 |
(* Removing the lightest clause. *) |
|
274 |
(* ------------------------------------------------------------------------- *) |
|
275 |
||
276 |
fun remove (Waiting {parameters,clauses,models}) = |
|
277 |
if Heap.null clauses then NONE |
|
278 |
else |
|
279 |
let |
|
280 |
val ((_,dcl),clauses) = Heap.remove clauses |
|
42102 | 281 |
|
39348 | 282 |
val waiting = |
283 |
Waiting |
|
42102 | 284 |
{parameters = parameters, |
285 |
clauses = clauses, |
|
286 |
models = models} |
|
39348 | 287 |
in |
288 |
SOME (dcl,waiting) |
|
289 |
end; |
|
290 |
||
291 |
end |