+(*
+ ||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