src/metis/mlibClauseset.sml

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);