Lines Matching refs:active
208 (* A type of active clause sets. *)
218 datatype active =
236 fun setRewrite active rewrite =
240 subterms,allSubterms,...} = active
285 fun saturation active =
295 val cls = clauses active
300 val Active {parameters,...} = active
315 fun toStr active = "Active{" ^ Int.toString (size active) ^ "}"
432 fun simplifyActive simp active =
434 val Active {units,rewrite,subsume,...} = active
440 (* Add a clause into the active set. *)
496 fun addClause active cl =
500 equations,subterms,allSubterms} = active
515 fun addFactorClause active cl =
519 equations,subterms,allSubterms} = active
568 fun deduce active cl =
570 val Active {parameters,literals,equations,subterms,...} = active
603 (* Extract clauses from the active set that can be simplified. *)
607 fun clause_rewritables active =
609 val Active {clauses,rewrite,...} = active
632 fun rewrite_rewritables active rewr_ids =
634 val Active {parameters,rewrite,clauses,allSubterms,...} = active
693 fun choose_clause_rewritables active ids = size active <= length ids
695 fun rewritables active ids =
696 if choose_clause_rewritables active ids then clause_rewritables active
697 else rewrite_rewritables active ids;
700 val rewritables = fn active => fn ids =>
702 val clause_ids = clause_rewritables active
703 val rewrite_ids = rewrite_rewritables active ids
711 val () = Print.trace pp "Active.rewritables: active" active
721 if choose_clause_rewritables active ids then clause_ids else rewrite_ids
725 fun delete active ids =
726 if IntSet.null ids then active
742 allSubterms} = active
763 fun extract_rewritables (active as Active {clauses,rewrite,...}) =
764 if Rewrite.isReduced rewrite then (active,[])
771 val active = setRewrite active rewrite
772 val ids = rewritables active ids
779 (delete active ids, cls)
792 fun prefactor_simplify active subsume =
794 val Active {parameters,units,rewrite,...} = active
800 fun postfactor_simplify active subsume =
802 val Active {parameters,units,rewrite,...} = active
819 fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
820 case postfactor_simplify active subsume cl of
824 val active = addFactorClause active cl
828 (active,subsume,acc)
831 fun factor1 (cl, active_subsume_acc as (active,subsume,_)) =
832 case prefactor_simplify active subsume cl of
841 fun factor' active acc [] = (active, List.rev acc)
842 | factor' active acc cls =
845 val subsume = getSubsume active
846 val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
847 val (active,cls) = extract_rewritables active
849 factor' active acc cls
852 fun factor active cls = factor' active [] cls;
856 val factor = fn active => fn cls =>
860 val (active,cls') = factor active cls
863 (active,cls')
868 (* Create a new active clause set and initialize clauses. *)
878 val active = empty parameters
879 val (active,axioms) = factor active (List.map mk_clause axioms)
880 val (active,conjecture) = factor active (List.map mk_clause conjecture)
882 (active, {axioms = axioms, conjecture = conjecture})
886 (* Add a clause into the active set and deduce all consequences. *)
889 fun add active cl =
890 case simplifyActive maxSimplify active cl of
891 NONE => (active,[])
893 if Clause.isContradiction cl' then (active,[cl'])
894 else if not (Clause.equalThms cl cl') then factor active [cl']
900 val active = addClause active cl
902 val cls = deduce active cl
903 val (active,cls) = factor active cls
909 (active,cls)