2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
14 module Superposition (B : Terms.Blob) :
17 exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
19 (* The returned active set is the input one + the selected clause *)
23 B.t Terms.unit_clause -> (* selected passive *)
24 Index.Index(B).active_set ->
25 B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
30 B.t Terms.unit_clause -> (* selected goal *)
31 Index.Index(B).active_set ->
32 B.t Terms.bag * int * B.t Terms.unit_clause list
36 B.t Terms.unit_clause ->
37 Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
39 val forward_simplify :
40 Index.Index(B).DT.t ->
42 B.t Terms.unit_clause ->
43 (B.t Terms.bag * B.t Terms.unit_clause) option
45 (* may raise success *)
46 val backward_simplify :
48 Index.Index(B).DT.t ->
50 B.t Terms.unit_clause ->
51 B.t Terms.bag * B.t Terms.unit_clause