Lines Matching refs:cl
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 ^