1(* ========================================================================= *) 2(* THE WAITING SET OF CLAUSES *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Waiting :> Waiting = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* A type of waiting sets of clauses. *) 13(* ------------------------------------------------------------------------- *) 14 15type weight = real; 16 17type modelParameters = 18 {model : Model.parameters, 19 initialPerturbations : int, 20 maxChecks : int option, 21 perturbations : int, 22 weight : weight} 23 24type parameters = 25 {symbolsWeight : weight, 26 variablesWeight : weight, 27 literalsWeight : weight, 28 models : modelParameters list}; 29 30type distance = real; 31 32datatype 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 42val defaultModels : modelParameters list = 43 [{model = Model.default, 44 initialPerturbations = 100, 45 maxChecks = SOME 20, 46 perturbations = 0, 47 weight = 1.0}]; 48 49val default : parameters = 50 {symbolsWeight = 1.0, 51 literalsWeight = 1.0, 52 variablesWeight = 1.0, 53 models = defaultModels}; 54 55fun size (Waiting {clauses,...}) = Heap.size clauses; 56 57val pp = 58 Print.ppMap 59 (fn w => "Waiting{" ^ Int.toString (size w) ^ "}") 60 Print.ppString; 61 62(*MetisDebug 63val pp = 64 Print.ppMap 65 (fn Waiting {clauses,...} => 66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) 67 (Print.ppList (Print.ppTriple Print.ppReal Print.ppInt Clause.pp)); 68*) 69 70(* ------------------------------------------------------------------------- *) 71(* Perturbing the models. *) 72(* ------------------------------------------------------------------------- *) 73 74type modelClause = NameSet.set * Thm.clause; 75 76fun mkModelClause cl = 77 let 78 val lits = Clause.literals cl 79 val fvs = LiteralSet.freeVars lits 80 in 81 (fvs,lits) 82 end; 83 84val mkModelClauses = List.map mkModelClause; 85 86fun perturbModel M cls = 87 if List.null cls then K () 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 105fun 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 115fun 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 129fun 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 145local 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); 154in 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) 165 val modelsW = checkModels models mods mcl 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; 187end; 188 189(* ------------------------------------------------------------------------- *) 190(* Adding new clauses. *) 191(* ------------------------------------------------------------------------- *) 192 193fun add' waiting dist mcls cls = 194 let 195 val Waiting {parameters,clauses,models} = waiting 196 val {models = modelParameters, ...} = parameters 197 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 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 222fun add waiting (dist,cls) = 223 if List.null cls then waiting 224 else 225 let 226(*MetisTrace3 227 val () = Print.trace pp "Waiting.add: waiting" waiting 228 val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls 229*) 230 231 val waiting = add' waiting dist (mkModelClauses cls) cls 232 233(*MetisTrace3 234 val () = Print.trace pp "Waiting.add: waiting" waiting 235*) 236 in 237 waiting 238 end; 239 240local 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 247 and models = List.map (initialModel axioms conjecture) modelParameters 248 in 249 Waiting {parameters = parameters, clauses = clauses, models = models} 250 end; 251in 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 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*) 270end; 271 272(* ------------------------------------------------------------------------- *) 273(* Removing the lightest clause. *) 274(* ------------------------------------------------------------------------- *) 275 276fun remove (Waiting {parameters,clauses,models}) = 277 if Heap.null clauses then NONE 278 else 279 let 280 val ((_,dcl),clauses) = Heap.remove clauses 281 282 val waiting = 283 Waiting 284 {parameters = parameters, 285 clauses = clauses, 286 models = models} 287 in 288 SOME (dcl,waiting) 289 end; 290 291end 292