X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=6deb0a4eb7a07c7e090e856c35ffa76a8ceab732;hb=7477c3dbbc2fafe248d48302be0d6ba4cb38d062;hp=cce81944bd497d286b50c22c31d4055c3c4e5228;hpb=4ae7d510a430a2a6929f973d36b993d528772d64;p=helm.git diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index cce81944b..6deb0a4eb 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -37,21 +37,32 @@ module Superposition (B : Terms.Blob) : B.t Terms.unit_clause -> Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause - val forward_simplify : + val simplify : Index.Index(B).DT.t -> B.t Terms.bag -> B.t Terms.unit_clause -> (B.t Terms.bag * B.t Terms.unit_clause) option (* may raise success *) - val backward_simplify : + val simplify_goal : int -> Index.Index(B).DT.t -> B.t Terms.bag -> B.t Terms.unit_clause -> B.t Terms.bag * B.t Terms.unit_clause - end + val one_pass_simplification: + B.t Terms.unit_clause -> + Index.Index(B).active_set -> + B.t Terms.bag -> + (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option + + val keep_simplified: + B.t Terms.unit_clause -> + Index.Index(B).active_set -> + B.t Terms.bag -> + (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option + end