fork for Matita version B

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

diff --git a/matitaB/components/ng_paramodulation/superposition.mli b/matitaB/components/ng_paramodulation/superposition.mli
new file mode 100644 (file)
index 0000000..c67dbfb
--- /dev/null
+++ b/matitaB/components/ng_paramodulation/superposition.mli
@@ -0,0 +1,84 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
+
+module Superposition (B : Orderings.Blob) : 
+  sig
+
+                        (* bag, maxvar, meeting point *)
+    exception Success of 
+      B.t Terms.bag 
+      * int 
+      * B.t Terms.unit_clause
+      * B.t Terms.substitution
+
+    (* The returned active set is the input one + the selected clause *)
+    val infer_right :
+          B.t Terms.bag -> 
+          int -> (* maxvar *)
+          B.t Terms.unit_clause -> (* selected passive *)
+          Index.Index(B).active_set ->
+            B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
+
+    val infer_left :  
+          B.t Terms.bag -> 
+          int -> (* maxvar *)
+          B.t Terms.unit_clause -> (* selected goal *)
+          Index.Index(B).active_set ->
+            B.t Terms.bag * int * B.t Terms.unit_clause list
+
+    val demodulate : 
+          B.t Terms.bag ->
+          B.t Terms.unit_clause ->
+          Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
+
+    val simplify : 
+          Index.Index(B).DT.t ->
+          int ->
+          B.t Terms.bag ->
+          B.t Terms.unit_clause ->
+            B.t Terms.bag * (B.t Terms.unit_clause option)
+
+    (* may raise success *)
+    val simplify_goal :
+          no_demod:bool ->
+          int ->
+          Index.Index(B).DT.t ->
+          B.t Terms.bag ->
+          B.t Terms.unit_clause list ->
+          B.t Terms.unit_clause ->
+            (B.t Terms.bag * B.t Terms.unit_clause) option
+
+    val one_pass_simplification:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      int ->
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+    val keep_simplified:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      int ->
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+
+    val  orphan_murder:
+      B.t Terms.bag ->
+      B.t Terms.unit_clause list ->
+      B.t Terms.unit_clause ->
+      bool
+
+    val are_alpha_eq : 
+      B.t Terms.unit_clause ->
+      B.t Terms.unit_clause ->
+      bool
+  end