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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique, ARM Ltd and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(** Generic part of constraint (ie the one to be checked
at the end of test run) *)
(* Type of locations on the right of LV atoms *)
type 'loc rloc =
| Loc of 'loc
| Deref of 'loc * int
val dump_rloc : ('loc -> string) -> 'loc rloc -> string
val compare_rloc : ('loc -> 'loc -> int) -> 'loc rloc -> 'loc rloc -> int
val rloc_of_loc : 'loc -> 'loc rloc
val loc_of_rloc : 'loc rloc -> 'loc
val map_rloc : ('a -> 'b) -> 'a rloc -> 'b rloc
val fold_rloc : ('loc -> 'b -> 'c) -> 'loc rloc -> 'b -> 'c
val match_rloc :
('loc -> 'r) -> ('loc -> int -> 'r) -> 'loc rloc -> 'r
(* Type of propositions and constraint *)
type ('loc,'v,'ftype) atom =
| LV of 'loc rloc * 'v
| LL of 'loc * 'loc
| FF of ('v,'ftype) Fault.atom
val dump_atom :
('loc -> string) -> ('loc -> string) -> (('c,'d,'e) Constant.t -> string) ->
('ftype -> string) -> ('loc,('c,'d,'e) Constant.t,'ftype) atom -> string
type ('loc,'v, 'ftype) prop =
| Atom of ('loc, 'v, 'ftype) atom
| Not of ('loc,'v,'ftype) prop
| And of ('loc,'v,'ftype) prop list
| Or of ('loc,'v,'ftype) prop list
| Implies of ('loc,'v,'ftype) prop * ('loc,'v,'ftype) prop
type 'prop constr =
ForallStates of 'prop
| ExistsState of 'prop
| NotExistsState of 'prop
type ('loc,'v,'ftype) cond = ('loc,'v,'ftype) prop constr
val constr_true : ('loc,'v,'ftype) cond
val is_true : ('loc,'v,'ftype) cond -> bool
val is_existential : 'prop constr -> bool
val prop_of : 'prop constr -> 'prop
(* val dnf : ('loc,'v) prop -> ('loc,'v) prop list list *)
(* Style of constraints in papers *)
type kind =
| Allow
| Forbid
| Require
| Unconstrained
val kind_of : 'a constr -> kind
val set_kind : kind -> 'a constr -> 'a constr
val pp_kind : kind -> string
val parse_kind : string -> kind option
val compare_kind : kind -> kind -> int
(* Polymorphic constraint combinators *)
val fold_prop :
(('loc, 'v, 'ftype) atom -> 'a -> 'a) -> ('loc,'v,'ftype) prop -> 'a -> 'a
val fold_constr :
(('loc, 'v, 'ftype) atom -> 'a -> 'a) -> ('loc,'v,'ftype) prop constr -> 'a -> 'a
val map_prop :
(('loc1, 'v1, 'ftype1) atom -> ('loc2, 'v2, 'ftype2) atom) ->
('loc1,'v1, 'ftype1) prop ->
('loc2,'v2,'ftype2) prop
val map_constr :
(('loc1, 'v1, 'ftype1) atom -> ('loc2, 'v2, 'ftype2) atom) ->
('loc1,'v1,'ftype1) prop constr ->
('loc2,'v2,'ftype2) prop constr
(* Pretty print *)
type 'atom pp_arg =
{ pp_true : string;
pp_false : string;
pp_not : string;
pp_or : string;
pp_and : string;
pp_implies : string;
pp_mbox : string -> string;
pp_atom : 'atom -> string; }
val pp_prop : ('loc,'v,'ftype) atom pp_arg -> ('loc,'v,'ftype) prop -> string
val dump_prop :
(('loc, 'v, 'ftype) atom -> string) -> out_channel -> ('loc,'v,'ftype) prop -> unit
val prop_to_string :
(('loc, 'v, 'ftype) atom -> string) -> ('loc,'v,'ftype) prop -> string
val dump_constraints :
out_channel -> (('loc,'v,'ftype) atom -> string) -> ('loc,'v,'ftype) prop constr -> unit
val constraints_to_string :
(('loc, 'v, 'ftype) atom -> string) -> ('loc,'v, 'ftype) prop constr -> string
|
