Added optionnal one pass simplification (instead of keep_simplified)

[helm.git] / helm / software / components / ng_paramodulation / superposition.mli

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index d7efb1b42b8921d4bb225575cc5bab1aea7639a9..6deb0a4eb7a07c7e090e856c35ffa76a8ceab732 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -51,6 +51,13 @@ module Superposition (B : Terms.Blob) :
           B.t Terms.unit_clause ->
             B.t Terms.bag * B.t Terms.unit_clause
 
+    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 ->