1(* ========================================================================= *) 2(* THE RESOLUTION PROOF PROCEDURE *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load 8 ["Moscow", "mlibUseful", "mlibTerm", "mlibThm", "mlibCanon", "mlibSupport", 9 "mlibStream", "mlibSolver", "mlibMeter", "mlibUnits", "mlibClauseset"]; 10*) 11 12(* 13*) 14structure mlibResolution :> mlibResolution = 15struct 16 17open mlibUseful mlibTerm mlibMeter mlibSolver; 18 19structure I = Intset; local open Intset in end; 20structure S = mlibStream; local open mlibStream in end; 21 22type clause = mlibClause.clause; 23type distance = mlibSupport.distance; 24 25(* ------------------------------------------------------------------------- *) 26(* Chatting. *) 27(* ------------------------------------------------------------------------- *) 28 29val module = "mlibResolution"; 30val () = add_trace {module = module, alignment = I} 31fun chatting l = tracing {module = module, level = l}; 32fun chat s = (trace s; true) 33 34(* ------------------------------------------------------------------------- *) 35(* Parameters. *) 36(* ------------------------------------------------------------------------- *) 37 38type parameters = 39 {clause_parm : mlibClause.parameters, 40 set_parm : mlibClauseset.parameters, 41 sos_parm : mlibSupport.parameters}; 42 43val defaults : parameters = 44 {clause_parm = mlibClause.defaults, 45 set_parm = mlibClauseset.defaults, 46 sos_parm = mlibSupport.defaults}; 47 48type 'a parmupdate = ('a -> 'a) -> parameters -> parameters; 49 50fun update_clause_parm f (parm : parameters) : parameters = 51 let val {clause_parm = c, sos_parm = a, set_parm = b} = parm 52 in {clause_parm = f c, sos_parm = a, set_parm = b} 53 end; 54 55fun update_set_parm f (parm : parameters) : parameters = 56 let val {clause_parm = c, sos_parm = a, set_parm = b} = parm 57 in {clause_parm = c, sos_parm = a, set_parm = f b} 58 end; 59 60fun update_sos_parm f (parm : parameters) : parameters = 61 let val {clause_parm = c, sos_parm = a, set_parm = b} = parm 62 in {clause_parm = c, sos_parm = f a, set_parm = b} 63 end; 64 65(* ------------------------------------------------------------------------- *) 66(* Helper functions *) 67(* ------------------------------------------------------------------------- *) 68 69fun ofilt _ NONE = NONE | ofilt p (s as SOME x) = if p x then s else NONE; 70 71local fun ins (c,i) = Intmap.insert (i, #id (mlibClause.dest_clause c), c); 72in fun insert cls init = foldl ins init cls; 73end; 74 75val thm_to_formula = list_mk_disj o mlibThm.clause; 76 77val clause_id = #id o mlibClause.dest_clause; 78 79fun clause_to_string cl = 80 PP.pp_to_string (!LINE_LENGTH) mlibClause.pp_clause cl; 81 82fun clauses_to_string cls = 83 PP.pp_to_string (!LINE_LENGTH) (pp_list mlibClause.pp_clause) cls; 84 85(* ------------------------------------------------------------------------- *) 86(* mlibResolution *) 87(* ------------------------------------------------------------------------- *) 88 89datatype resolution = RES of {set : mlibClauseset.clauseset, sos : mlibSupport.sos}; 90 91fun update_set b res = 92 let val RES {set = _, sos = a} = res 93 in RES {set = b, sos = a} 94 end; 95 96fun update_sos a res = 97 let val RES {set = b, sos = _} = res 98 in RES {set = b, sos = a} 99 end; 100 101fun dest (RES r) = r; 102 103fun size (RES {set,sos,...}) = 104 {used = mlibClauseset.size set, waiting = mlibSupport.size sos, 105 rewrites = mlibClause.size (mlibClauseset.rewrites set)}; 106 107fun units (RES {set,...}) = mlibClauseset.units set; 108 109fun new_units units (res as RES {set,...}) = 110 update_set (mlibClauseset.new_units units set) res; 111 112fun mk_axioms thms hyps = 113 let 114 val thms = map thm_to_formula thms 115 and hyps = map thm_to_formula hyps 116 in 117 if null thms then hyps else thms @ map Not hyps 118 end; 119 120fun mk_thms_hyps (clause_parm : mlibClause.parameters) thms hyps = 121 let 122 val thms = map (mlibClause.mk_clause clause_parm) thms 123 and hyps = map (mlibClause.mk_clause clause_parm) hyps 124 in 125 if #literal_order clause_parm then ([], hyps @ thms) else 126 let val (noneqs,eqs) = List.partition (null o mlibClause.largest_eqs) thms 127 in (noneqs, hyps @ eqs) 128 end 129 end; 130 131fun new (parm : parameters, units, thms, hyps) = 132 let 133 val {clause_parm,sos_parm,set_parm,...} = parm 134 val axioms = mk_axioms thms hyps 135 val (thms,hyps) = mk_thms_hyps clause_parm thms hyps 136 val set = mlibClauseset.empty (clause_parm,set_parm) 137 val set = mlibClauseset.new_units units set 138 val (thms,set) = mlibClauseset.factor thms set 139 val set = foldl (fn (c,s) => mlibClauseset.add c s) set thms 140 val (hyps,set) = mlibClauseset.factor hyps set 141 val sos = mlibSupport.new sos_parm axioms hyps 142 in 143 RES {set = set, sos = sos} 144 end; 145 146local 147 fun beef_up set = mlibClauseset.strengthen set o mlibClauseset.simplify set; 148 149 fun get_clause set sos n = 150 case mlibSupport.remove sos of NONE => (n,NONE) 151 | SOME (dcl,sos) => check set sos n dcl 152 and check set sos n (d,cl) = 153 case ofilt (not o mlibClauseset.subsumed set) (beef_up set cl) of 154 NONE => get_clause set sos (n + 1) 155 | SOME cl => (n, SOME ((d,cl),sos)); 156in 157 fun select res = 158 let 159 val RES {set,sos,...} = res 160 val (n,dcl_sos) = get_clause set sos 0 161 val _ = 0 < n andalso chatting 2 andalso chat ("x" ^ int_to_string n) 162 in 163 case dcl_sos of NONE => NONE 164 | SOME ((d,cl),sos) => 165 let 166 val res = update_sos sos res 167 val {order_stickiness, ...} = #parm (mlibClause.dest_clause cl) 168 val cl = if order_stickiness <= 2 then mlibClause.drop_order cl else cl 169 val set = mlibClauseset.add cl set 170 val res = update_set set res 171 in 172 SOME ((d,cl),res) 173 end 174 end; 175end; 176 177fun deduce cl res = 178 let 179 val _ = chatting 4 andalso 180 chat ("\ngiven clause:\n" ^ clause_to_string cl ^ "\n") 181 val RES {set,...} = res 182 val cl = mlibClause.FRESH_VARS cl 183 val cls = mlibClauseset.deduce set cl 184 in 185 cls 186 end; 187 188fun factor cls res = 189 let 190 val RES {set,...} = res 191 val (cls,set) = mlibClauseset.factor cls set 192 val res = update_set set res 193 val _ = chatting 4 andalso 194 chat ("\nnew clauses:\n" ^ clauses_to_string cls ^ "\n") 195 in 196 (cls,res) 197 end; 198 199fun add (dist,cls) res = 200 let 201 val RES {sos,...} = res 202 val sos = mlibSupport.add (dist,cls) sos 203 val res = update_sos sos res 204 in 205 res 206 end; 207 208fun advance res = 209 case select res of NONE => NONE 210 | SOME ((d,cl),res) => 211 let 212 val cls = deduce cl res 213 val (cls,res) = factor cls res 214 val res = add (d,cls) res 215 in 216 SOME res 217 end; 218 219fun resolution_to_string res = 220 let 221 val {used = u, waiting = w, rewrites = r} = size res 222 in 223 "(" ^ int_to_string u ^ "<-" ^ int_to_string w 224 ^ (if r = 0 then "" else "=" ^ int_to_string r) ^ ")" 225 end; 226 227val pp_resolution = pp_map resolution_to_string pp_string; 228 229(* ------------------------------------------------------------------------- *) 230(* The resolution procedure as a solver_node *) 231(* ------------------------------------------------------------------------- *) 232 233fun resolution_stream slice_ref units_ref = 234 let 235 fun stat func res () = 236 (chatting 3 andalso chat (resolution_to_string res); func res) 237 238 fun sq f x = 239 let 240 val _ = chatting 1 andalso chat "[" 241 val y = f x 242 val _ = chatting 1 andalso chat "]" 243 in 244 y 245 end 246 247 fun shove res = new_units (!units_ref) res 248 249 fun swipe res = units_ref := units res (* OK *) 250 251 fun record infs = record_infs (!slice_ref) infs 252 253 fun f res = 254 case select res of NONE => (swipe res; S.NIL) 255 | SOME dcl_res => g dcl_res 256 and g (dcl as (_,cl), res) = 257 if not (mlibClause.is_empty cl) then h dcl res 258 else (swipe res; S.CONS (SOME cl, stat (h dcl o shove) res)) 259 and h (d,cl) res = 260 let 261 val cls = deduce cl res 262 val (cls,res) = factor cls res 263 val () = record (length cls + #rewrites (size res)) 264 val res = add (d,cls) res 265 in 266 if check_meter (!slice_ref) then f res 267 else (swipe res; S.CONS (NONE, stat (f o shove) res)) 268 end; 269 in 270 fn (parm,thms,hyps) => stat f (sq new (parm,!units_ref,thms,hyps)) () 271 end; 272 273fun resolution' (name, parm : parameters) = 274 mk_solver_node 275 {name = name, 276 solver_con = 277 fn {slice = slice_ref, units = units_ref, thms, hyps} => 278 let 279 val _ = chatting 3 andalso chat 280 (name ^ "--initializing--#thms=" ^ int_to_string (length thms) ^ 281 "--#hyps=" ^ int_to_string (length hyps) ^ ".\n") 282 val solution_stream = 283 S.map (Option.map (sing o #thm o mlibClause.dest_clause)) o 284 resolution_stream slice_ref units_ref 285 in 286 fn [False] => solution_stream (parm,thms,hyps) | _ => S.NIL 287 end}; 288 289val resolution = resolution' ("resolution",defaults); 290 291end 292