Metis/src/Active.sml

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)