]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/superposition.mli
update in ground and delayed_updating
[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 
19       B.t Terms.bag 
20       * int 
21       * B.t Terms.unit_clause
22       * B.t Terms.substitution
23
24     (* The returned active set is the input one + the selected clause *)
25     val infer_right :
26           B.t Terms.bag -> 
27           int -> (* maxvar *)
28           B.t Terms.unit_clause -> (* selected passive *)
29           Index.Index(B).active_set ->
30             B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
31
32     val infer_left :  
33           B.t Terms.bag -> 
34           int -> (* maxvar *)
35           B.t Terms.unit_clause -> (* selected goal *)
36           Index.Index(B).active_set ->
37             B.t Terms.bag * int * B.t Terms.unit_clause list
38
39     val demodulate : 
40           B.t Terms.bag ->
41           B.t Terms.unit_clause ->
42           Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
43
44     val simplify : 
45           Index.Index(B).DT.t ->
46           int ->
47           B.t Terms.bag ->
48           B.t Terms.unit_clause ->
49             B.t Terms.bag * (B.t Terms.unit_clause option)
50
51     (* may raise success *)
52     val simplify_goal :
53           no_demod:bool ->
54           int ->
55           Index.Index(B).DT.t ->
56           B.t Terms.bag ->
57           B.t Terms.unit_clause list ->
58           B.t Terms.unit_clause ->
59             (B.t Terms.bag * B.t Terms.unit_clause) option
60
61     val one_pass_simplification:
62       B.t Terms.unit_clause ->
63       Index.Index(B).active_set ->
64       B.t Terms.bag ->
65       int ->
66       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
67     val keep_simplified:
68       B.t Terms.unit_clause ->
69       Index.Index(B).active_set ->
70       B.t Terms.bag ->
71       int ->
72       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
73
74     val  orphan_murder:
75       B.t Terms.bag ->
76       B.t Terms.unit_clause list ->
77       B.t Terms.unit_clause ->
78       bool
79
80     val are_alpha_eq : 
81       B.t Terms.unit_clause ->
82       B.t Terms.unit_clause ->
83       bool
84   end