Lines Matching refs:cl
96 fun add_unit cl units =
97 let val {thm, ...} = dest_clause cl in U.add thm units end;
99 fun add_subsum cl = S.add (literals cl |-> cl);
228 fun beef_up (SET {units, ...}) cl =
230 val () = taut cl
231 val cl = NEQ_VARS cl
232 val () = taut cl
233 val cl = DEMODULATE units cl
235 cl
250 fun AX cl lits = mk_clause (#parm (dest_clause cl)) (mlibThm.AXIOM lits);
267 | spl cl acc [c] = rev (AX cl c :: acc)
268 | spl cl acc (c1 :: c2 :: cs) =
270 in spl cl (AX cl (c1 @ [p]) :: acc) ((Not p :: c2) :: cs)
273 fun split_clause cl comps =
276 val cls = spl cl [] comps
278 ("\nsplit: components of clause " ^ clause_to_string cl ^ ":\n"
284 fun split cl =
286 val lits = map (fn lit => (FV lit, lit)) (literals cl)
291 case components [] vlits of [] => [cl]
292 | [_] => [cl]
293 | l => split_clause cl (rev (if null glits then l else glits :: l))
301 fun subsum subs cl =
304 case total (INST sub) c of NONE => false | SOME d => subsumes d cl
306 mlibStream.exists f (S.subsumes' subs (literals cl))
315 fun add_rewr cl set =
316 if not (is_rewr cl) then (cl,set) else
319 val cl = mlibClause.drop_order cl
320 val r = mlibClause.add cl r
325 (cl,set)
328 fun add cl set =
335 val (cl,set) = add_rewr cl set
336 val set = update_units (add_unit cl u) set
337 val set = update_clauses (cl :: c) set
338 val set = update_subsumers (add_subsum cl s) set
339 val set = update_literals (foldl f l (largest_lits cl)) set
340 val set = update_equalities (foldl g e (largest_eqs cl)) set
341 val set = update_subterms (foldl g p (largest_tms cl)) set
345 chat ("\nlargest_lits cl:\n" ^
348 (largest_lits cl)) ^ "\n")
376 fn cl =>
380 val res = foldl (resolvants l) res (largest_lits cl)
381 val res = foldl (paramods_from p) res (largest_eqs cl)
382 val res = foldl (paramods_into e) res (largest_tms cl)
394 fun clause_mem cl s =
395 let val {id, ...} = dest_clause cl in Intset.member (s,id) end;
444 fun mk_init_id (cl,(s,s')) =
445 case total dest_rewr cl of NONE => (s,s')
466 case List.find (fn cl => #id (dest_clause cl) = i) c of SOME cl => cl
488 fun pred cl = not (clause_mem cl ns)
515 val cls = List.filter (fn cl => clause_mem cl i) c
530 fun utility cl =
531 case length (literals cl) of 0 => ~1
532 | 1 => if is_rewr cl then 0 else 1
540 fun ins (parm : parameters) cl (cls,set,subs) =
542 val (cl,set) = add_rewr cl set
543 val set = update_units (add_unit cl (units set)) set
544 val subs = if is_subsumption parm then add_subsum cl subs else subs
546 (cl :: cls, set, subs)
561 fun fac1 parm (cl,acc) =
562 foldl (fn (cl,acc) => ins parm cl acc) acc (quality parm true acc cl);
564 fun facl parm (cl,acc) =
565 foldl (fn (cl,acc) => foldl (fac1 parm) (ins parm cl acc) (FACTOR cl)) acc
566 (quality parm false acc cl);