Metis/src/Active.sml

280       fun add (_,cl,acc) = cl :: acc
533 fun deduceResolution literals cl (lit as (_,atm), acc) =
535       fun resolve (cl_lit,acc) =
537             SOME cl' => cl' :: acc
538           | NONE => acc
543       if Atom.isEq atm then acc
545         List.foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
548 fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =
550       fun para (cl_lit_path_tm,acc) =
552             SOME cl' => cl' :: acc
553           | NONE => acc
555       List.foldl para acc (TermNet.unify subterms tm)
558 fun deduceParamodulationInto equations cl ((lit,path,tm),acc) =
560       fun para (cl_lit_ort_tm,acc) =
562             SOME cl' => cl' :: acc
563           | NONE => acc
565       List.foldl para acc (TermNet.unify equations tm)
589       val acc = []
590       val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits
591       val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
592       val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
593       val acc = List.rev acc
596       val () = Print.trace (Print.ppList Clause.pp) "Active.deduce: acc" acc
599       acc
638         fun addRewr (id,acc) =
639             if IntMap.inDomain id clauses then IntSet.add acc id else acc
641         fun addReduce ((l,r,ord),acc) =
654               fun addRed ((cl,tm),acc) =
662                     if IntSet.member id acc then acc
663                     else if not (isValidRewr tm) then acc
664                     else IntSet.add acc id
673               List.foldl addRed acc (TermNet.matched allSubterms l)
676         fun addEquation redexResidues (id,acc) =
678               NONE => acc
679             | SOME eqn_ort => List.foldl addReduce acc (redexResidues eqn_ort)
819   fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
826           and acc = cl :: acc
828           (active,subsume,acc)
841   fun factor' active acc [] = (active, List.rev acc)
842     | factor' active acc cls =
846         val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
849         factor' active acc cls