blob: 47cdb3eaf27aa3d2431b58d8c8ef671365e3b2e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: ccalgo.mli,v 1.6.2.1 2004/07/16 19:29:58 herbelin Exp $ *)
type pa_constructor
(*{head: int; arity: int; args: (int * int) list}*)
module PacMap:Map.S with type key=int * int
type term =
Symb of Term.constr
| Appli of term * term
| Constructor of Names.constructor*int*int
type rule =
Congruence
| Axiom of Names.identifier
| Injection of int*int*int*int
type equality =
{lhs : int;
rhs : int;
rule : rule}
module ST :
sig
type t
val empty : unit -> t
val enter : int -> int * int -> t -> unit
val query : int * int -> t -> int
val delete : int -> t -> unit
val delete_list : int list -> t -> unit
end
module UF :
sig
type t
exception Discriminable of int * int * int * int * t
val empty : unit -> t
val find : t -> int -> int
val size : t -> int -> int
val get_constructor : t -> int -> Names.constructor
val pac_arity : t -> int -> int * int -> int
val mem_node_pac : t -> int -> int * int -> int
val add_pacs : t -> int -> pa_constructor PacMap.t ->
int list * equality list
val term : t -> int -> term
val subterms : t -> int -> int * int
val add : t -> term -> int
val union : t -> int -> int -> equality -> int list * equality list
val join_path : t -> int -> int ->
((int*int)*equality) list*
((int*int)*equality) list
end
val combine_rec : UF.t -> int list -> equality list
val process_rec : UF.t -> equality list -> int list
val cc : UF.t -> unit
val make_uf :
(Names.identifier * (term * term)) list -> UF.t
val add_one_diseq : UF.t -> (term * term) -> int * int
val add_disaxioms :
UF.t -> (Names.identifier * (term * term)) list ->
(Names.identifier * (int * int)) list
val check_equal : UF.t -> int * int -> bool
val find_contradiction : UF.t ->
(Names.identifier * (int * int)) list ->
(Names.identifier * (int * int))
|
