]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/superposition.mli
Moved benchmarks to new folder
[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 : Orderings.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           no_demod:bool ->
50           int ->
51           Index.Index(B).DT.t ->
52           B.t Terms.bag ->
53           B.t Terms.unit_clause list ->
54           B.t Terms.unit_clause ->
55             (B.t Terms.bag * B.t Terms.unit_clause) option
56
57     val one_pass_simplification:
58       B.t Terms.unit_clause ->
59       Index.Index(B).active_set ->
60       B.t Terms.bag ->
61       int ->
62       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
63
64
65     val keep_simplified:
66       B.t Terms.unit_clause ->
67       Index.Index(B).active_set ->
68       B.t Terms.bag ->
69       int ->
70       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
71
72     val  orphan_murder:
73       B.t Terms.bag ->
74       B.t Terms.unit_clause list ->
75       B.t Terms.unit_clause ->
76       bool
77
78
79   end