]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/superposition.mli
initial import of standalone matitaprover binary
[helm.git] / helm / software / components / ng_paramodulation / superposition.mli
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
13
14 module Superposition (B : Terms.Blob) : 
15   sig
16
17                         (* bag, maxvar, meeting point *)
18     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
19
20     (* The returned active set is the input one + the selected clause *)
21     val infer_right :
22           B.t Terms.bag -> 
23           int -> (* maxvar *)
24           B.t Terms.unit_clause -> (* selected passive *)
25           Index.Index(B).active_set ->
26             B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
27
28     val infer_left :  
29           B.t Terms.bag -> 
30           int -> (* maxvar *)
31           B.t Terms.unit_clause -> (* selected goal *)
32           Index.Index(B).active_set ->
33             B.t Terms.bag * int * B.t Terms.unit_clause list
34
35     val demodulate : 
36           B.t Terms.bag ->
37           B.t Terms.unit_clause ->
38           Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
39
40     val simplify : 
41           Index.Index(B).DT.t ->
42           int ->
43           B.t Terms.bag ->
44           B.t Terms.unit_clause ->
45             (B.t Terms.bag * B.t Terms.unit_clause) option
46
47     (* may raise success *)
48     val simplify_goal : 
49           int ->
50           Index.Index(B).DT.t ->
51           B.t Terms.bag ->
52           B.t Terms.unit_clause list ->
53           B.t Terms.unit_clause ->
54             (B.t Terms.bag * B.t Terms.unit_clause) option
55
56     val one_pass_simplification:
57       B.t Terms.unit_clause ->
58       Index.Index(B).active_set ->
59       B.t Terms.bag ->
60       int ->
61       (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
62
63
64     val keep_simplified:
65       B.t Terms.unit_clause ->
66       Index.Index(B).active_set ->
67       B.t Terms.bag ->
68       int ->
69       (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
70
71
72   end