src/metis/mlibClause.sml

224 fun free_vars cl =
225   FVL (constraint_vars (#order (dest_clause cl))) (literals cl);
229 fun dest_rewr cl =
231     val {parm, thm, id, ...} = dest_clause cl
260   fun pp_clause cl = f (!show_id) (!show_constraint) cl;
351 fun drop_order (cl as CL (p,i,th,c,d)) =
352   if T.null c then cl else CL (p, i, th, no_constraints p, d);
358 fun subsumes (cl as CL (_,_,th,c,_)) (cl' as CL (_,_,th',c',_)) =
378 fun add cl rewrs =
380     val (i,th) = dest_rewr cl
397 fun INST sub (cl as CL (p,i,th,c,d)) =
398   if mlibSubst.null sub then cl
401 fun FRESH_VARS cl =
403     val fvs = free_vars cl
407     INST sub cl
411   fun match_occurs cl l r =
420       INST sub cl
423   fun dest_neq cl lit =
428       case total (match_occurs cl l) r of SOME cl => cl
429       | NONE => match_occurs cl r l
432   fun neq_simp1 cl = first (total (dest_neq cl)) (literals cl);
434   fun neq_simp cl = case neq_simp1 cl of NONE => cl | SOME cl => neq_simp cl;
438   fun NEQ_VARS cl =
439     (case neq_simp1 cl of NONE => cl | SOME cl => eq_factor (neq_simp cl))
443 fun DEMODULATE units (cl as CL (p,i,th,c,d)) =
448     if mlibThm.clause th = lits then cl else CL (p,i,th,c,d)
460   fun GEN_REWRITE _ (REWR ({term_order = false, ...}, _)) cl = cl
461     | GEN_REWRITE ord (REWR (_,rw)) cl = rewrite0 ord rw cl;
463   fun REWRITE rws cl =
464     if not (chatting 1) then GEN_REWRITE true rws cl else
466         val res = GEN_REWRITE true rws cl
467         val _ = literals cl <> literals res andalso chat
468           ("\nREWRITE: " ^ PP.pp_to_string 60 pp_clause cl ^
475   fun QREWRITE rws cl =
476     if not (chatting 1) then GEN_REWRITE false rws cl else
478         val res = GEN_REWRITE false rws cl
479         val _ = literals cl <> literals res andalso chat
480           ("\nQREWRITE: " ^ PP.pp_to_string 60 pp_clause cl ^
566   fun FAC x lits sub cl =
568       val CL (p,_,th,c,_) = INST sub cl
573       CL (p, new_id (), th, c, Factor cl)
576   fun final cl sub lr x targs =
580           val lits = map (formula_subst sub) (literals cl)
585           (hits, total (FAC x lits sub) cl)
593   fun factor ((cl,n) |-> lit) =
597         | f ((s,[]) :: paths) acc = f paths (final cl s true x [lit] acc)
608       f [(|<>|, List.drop (literals cl, n + 1))]
611   fun factor_eq ((cl,n,b) |-> x) =
614       val lit = List.nth (literals cl, n)
617         | f ((s,[]) :: paths) acc = f paths (final cl s b x [lit,lit'] acc)
631       f [(|<>|, List.drop (literals cl, n + 1))]
634   fun FACTOR' cl =
636       fun fac acc = foldl (uncurry factor) acc (largest_noneq_lits cl)
637       fun fac_eq acc = foldl (uncurry factor_eq) acc (largest_peqs cl)
643   fun FACTOR cl =
644     if not (chatting 1) then FACTOR' cl else
646         val res = FACTOR' cl
648           ("\nFACTOR: " ^ PP.pp_to_string 60 pp_clause cl ^