1(* ========================================================================= *) 2(* THE SET OF SUPPORT *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load ["mlibHeap", "UNLINK", "mlibThm", "mlibSubsumers1"]; 8*) 9 10(* 11*) 12structure mlibSupport :> mlibSupport = 13struct 14 15infix |-> ##; 16 17open mlibUseful mlibTerm; 18 19structure I = Intmap; local open Intmap in end; 20structure H = mlibHeap; local open mlibHeap in end; 21structure M = mlibModel; local open mlibModel in end; 22structure C = mlibClause; local open mlibClause in end; 23 24type 'a heap = 'a H.heap; 25type clause = C.clause; 26 27(* ------------------------------------------------------------------------- *) 28(* Chatting. *) 29(* ------------------------------------------------------------------------- *) 30 31val module = "mlibSupport"; 32val () = add_trace {module = module, alignment = I} 33fun chatting l = tracing {module = module, level = l}; 34fun chat s = (trace s; true) 35 36(* ------------------------------------------------------------------------- *) 37(* Parameters. *) 38(* ------------------------------------------------------------------------- *) 39 40type parameters = 41 {size_power : real, 42 literal_power : real, 43 model_power : real, 44 model_perts : int, 45 model_checks : int, 46 model_parms : M.parameters list}; 47 48type 'a parmupdate = ('a -> 'a) -> parameters -> parameters; 49 50val defaults = 51 {size_power = 1.0, 52 literal_power = 1.0, 53 model_power = 1.0, 54 model_perts = 100, 55 model_checks = 20, 56 model_parms = []}; 57 58fun update_size_power f (parm : parameters) : parameters = 59 let val {size_power = s, literal_power = r, model_power = m, 60 model_perts = p, model_checks = c, model_parms = z} = parm 61 in {size_power = f s, literal_power = r, model_power = m, 62 model_perts = p, model_checks = c, model_parms = z} 63 end; 64 65fun update_literal_power f (parm : parameters) : parameters = 66 let val {size_power = s, literal_power = r, model_power = m, 67 model_perts = p, model_checks = c, model_parms = z} = parm 68 in {size_power = s, literal_power = f r, model_power = m, 69 model_perts = p, model_checks = c, model_parms = z} 70 end; 71 72fun update_model_power f (parm : parameters) : parameters = 73 let val {size_power = s, literal_power = r, model_power = m, 74 model_perts = p, model_checks = c, model_parms = z} = parm 75 in {size_power = s, literal_power = r, model_power = f m, 76 model_perts = p, model_checks = c, model_parms = z} 77 end; 78 79fun update_model_perts f (parm : parameters) : parameters = 80 let val {size_power = s, literal_power = r, model_power = m, 81 model_perts = p, model_checks = c, model_parms = z} = parm 82 in {size_power = s, literal_power = r, model_power = m, 83 model_perts = f p, model_checks = c, model_parms = z} 84 end; 85 86fun update_model_checks f (parm : parameters) : parameters = 87 let val {size_power = s, literal_power = r, model_power = m, 88 model_perts = p, model_checks = c, model_parms = z} = parm 89 in {size_power = s, literal_power = r, model_power = m, 90 model_perts = p, model_checks = f c, model_parms = z} 91 end; 92 93fun update_model_parms f (parm : parameters) : parameters = 94 let val {size_power = s, literal_power = r, model_power = m, 95 model_perts = p, model_checks = c, model_parms = z} = parm 96 in {size_power = s, literal_power = r, model_power = m, 97 model_perts = p, model_checks = c, model_parms = f z} 98 end; 99 100(* ------------------------------------------------------------------------- *) 101(* Helper functions. *) 102(* ------------------------------------------------------------------------- *) 103 104fun clause_to_formula cl = list_mk_disj (C.literals cl); 105 106val clause_id = #id o C.dest_clause; 107 108fun clause_to_string cl = PP.pp_to_string (!LINE_LENGTH) mlibClause.pp_clause cl; 109 110val clause_lits = Real.fromInt o length o C.literals; 111 112(* ------------------------------------------------------------------------- *) 113(* Calculate clause_size (ignoring type annotations) *) 114(* ------------------------------------------------------------------------- *) 115 116local 117 fun sz n [] = n 118 | sz n (Fn (":", [tm, _]) :: tms) = sz n (tm :: tms) 119 | sz n (Var _ :: tms) = sz (n + 1) tms 120 | sz n (Fn (_,l) :: tms) = sz (n + 1) (l @ tms); 121 fun lsz (l,n) = sz n [dest_atom (literal_atom l)]; 122in 123 val clause_size = Real.fromInt o foldl lsz 0 o C.literals; 124end; 125 126(* ------------------------------------------------------------------------- *) 127(* Calculate average satisfiability in the models *) 128(* ------------------------------------------------------------------------- *) 129 130local 131 fun small_space _ _ 0 _ = true 132 | small_space N n i k = 133 let val k = k * N in k <= n andalso small_space N n (i - 1) k end; 134 135 fun sat_clause m n fm = 136 if small_space (M.size m) n (length (FV fm)) 1 then M.count m fm 137 else (M.checkn m fm n, n); 138in 139 fun sat_mod_fm m fm n = 140 let val (i,k) = sat_clause m n fm 141 in Real.fromInt i / Real.fromInt k 142 end; 143end; 144 145fun sat_mod_fms _ [] _ = raise Bug "sat_mod_fms: no formulas" 146 | sat_mod_fms m fms n = 147 let val sum = foldl (fn (fm,x) => sat_mod_fm m fm n + x) 0.0 fms 148 in sum / Real.fromInt (length fms) 149 end; 150 151fun sat_wmod_fm (w,m) fm n = w * (sat_mod_fm m fm n) + (1.0 - w); 152 153fun clause_sat [] _ _ = 0.0 154 | clause_sat wmods cl n = 155 let 156 val fm = clause_to_formula cl 157 val sum = foldl (fn (wmod,x) => sat_wmod_fm wmod fm n + x) 0.0 wmods 158 in 159 sum / Real.fromInt (length wmods) 160 end; 161 162(* ------------------------------------------------------------------------- *) 163(* mlibClause weights. *) 164(* ------------------------------------------------------------------------- *) 165 166local 167 fun priority n = 1e~12 * Real.fromInt n; 168in 169 fun clause_weight (parm : parameters) clsat dist cl = 170 let 171 val {size_power, literal_power, model_power, ...} = parm 172 val {id, ...} = C.dest_clause cl 173 val siz = Math.pow (clause_size cl, size_power) 174 val lit = Math.pow (clause_lits cl, literal_power) 175 val sat = Math.pow (1.0 + clsat, model_power) 176 val w = siz * lit * sat * (1.0 + dist) + priority id 177 val _ = chatting 5 andalso 178 chat ("clause_weight: " ^ clause_to_string cl ^ " -> " ^ 179 real_to_string w ^ "\n") 180 in 181 w 182 end; 183end; 184 185(* ------------------------------------------------------------------------- *) 186(* The set of support type *) 187(* ------------------------------------------------------------------------- *) 188 189type distance = real; 190 191datatype sos = SOS of 192 {parm : parameters, 193 clauses : (real * (real * clause)) heap, 194 distance : real I.intmap, 195 models : (real * mlibModel.model) list}; 196 197fun update_clauses c sos = 198 let val SOS {parm = p, clauses = _, distance = d, models = m} = sos 199 in SOS {parm = p, clauses = c, distance = d, models = m} 200 end; 201 202fun update_distance d sos = 203 let val SOS {parm = p, clauses = c, distance = _, models = m} = sos 204 in SOS {parm = p, clauses = c, distance = d, models = m} 205 end; 206 207fun update_models m sos = 208 let val SOS {parm = p, clauses = c, distance = d, models = _} = sos 209 in SOS {parm = p, clauses = c, distance = d, models = m} 210 end; 211 212(* ------------------------------------------------------------------------- *) 213(* Basic operations *) 214(* ------------------------------------------------------------------------- *) 215 216val empty_heap : (real * (real * clause)) heap = 217 H.empty (fn ((m,_),(n,_)) => Real.compare (m,n)); 218 219local 220 val TEST_MODEL_SIZES = [10,11]; 221 fun test_model n = M.new {size = n, fix = M.pure_fix}; 222 val test_models = map test_model TEST_MODEL_SIZES; 223in 224 fun is_prob_taut n fm = List.all (fn m => M.checkn m fm n = n) test_models; 225end; 226 227local 228 fun pert_models [] _ _ mods = [] 229 | pert_models fms p n mods = 230 let val mods = map (M.perturb fms p) mods 231 in map (fn m => (sat_mod_fms m fms n, m)) mods 232 end; 233 234 fun chatmods wmods = 235 chat ("{" ^ join "," (map (percent_to_string o fst) wmods) ^ "}"); 236in 237 fun new_models _ _ _ [] = [] 238 | new_models fms p n mps = 239 let 240 val mods = map M.new mps 241 val fms = List.filter (not o is_prob_taut n) fms 242 val wmods = pert_models fms p n mods 243 val _ = chatting 2 andalso chatmods wmods 244 in 245 wmods 246 end; 247end; 248 249fun empty parm fms = 250 let 251 val {model_perts,model_checks,model_parms,...} = parm 252 val models = new_models fms model_perts model_checks model_parms 253 in 254 SOS {parm = parm, clauses = empty_heap, distance = I.empty (), 255 models = models} 256 end; 257 258fun ssize (SOS {clauses,...}) = H.size clauses; 259 260val pp_sos = pp_map (fn s => "S<" ^ int_to_string (ssize s) ^ ">") pp_string; 261 262(* ------------------------------------------------------------------------- *) 263(* Adding new clauses *) 264(* ------------------------------------------------------------------------- *) 265 266fun add1 dist (cl,sos) = 267 let 268 val SOS {parm,clauses,distance,models,...} = sos 269 val {model_checks,...} = parm 270 val {id,...} = C.dest_clause cl 271 val dist = 272 case I.peek (distance, id) of NONE => dist | SOME d => Real.min (dist,d) 273 val distance = I.insert (distance,id,dist) 274 val sat = clause_sat models cl model_checks 275 val weight = clause_weight parm sat dist cl 276 val sos = update_clauses (H.add (weight,(dist,cl)) clauses) sos 277 val sos = update_distance distance sos 278 in 279 sos 280 end; 281 282fun inc_dist d n = d + log2 (Real.fromInt (1 + n)); 283 284fun add (dist,cls) sos = 285 let val dist = inc_dist dist (length cls) 286 in foldl (add1 dist) sos cls 287 end; 288 289fun new parm fms cls = foldl (add1 0.0) (empty parm fms) cls; 290 291(* ------------------------------------------------------------------------- *) 292(* Removing the lightest clause *) 293(* ------------------------------------------------------------------------- *) 294 295fun remove sos = 296 let 297 val SOS {clauses,...} = sos 298 in 299 if H.is_empty clauses then NONE else 300 let 301 val ((_,dcl),cls) = H.remove clauses 302 val sos = update_clauses cls sos 303 in 304 SOME (dcl,sos) 305 end 306 end; 307 308local 309 fun f acc sos = 310 case remove sos of NONE => rev acc 311 | SOME ((_,cl),sos) => f (cl :: acc) sos; 312in 313 val to_list = f []; 314end; 315 316(* ------------------------------------------------------------------------- *) 317(* Rebinding for signature *) 318(* ------------------------------------------------------------------------- *) 319 320val size = ssize; 321 322end 323