(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-module Superposition (B : Terms.Blob) :
+module Superposition (B : Orderings.Blob) :
sig
- exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+ (* 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.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 ->
+ int ->
B.t Terms.bag ->
B.t Terms.unit_clause ->
- (B.t Terms.bag * B.t Terms.unit_clause) option
+ B.t Terms.bag * (B.t Terms.unit_clause option)
(* may raise success *)
- val backward_simplify :
+ 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
-
- end
+ (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