(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-
module Superposition (B : Terms.Blob) :
sig
- val superposition_right_step :
+ exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+
+ (* 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 forward_simplify :
Index.Index(B).DT.t ->
- B.t Terms.bag * B.t Terms.unit_clause list
-
+ 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 :
+ 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