[r1813]: trunk / Toss / Solver / Structure.mli  Maximize  Restore  History

Download this file

300 lines (201 with data), 11.1 kB

  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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
(** Representing relational structures with real-valued functions. *)
(** {2 Modules used in structure representation.} *)
module IntMap : Map.S with type key = int (** Maps from int to 'alpha *)
module StringMap : Map.S with type key = string (** Maps from string to 'alpha*)
module Elems : Set.S with type elt = int (** Sets of integers *)
val add_elems : int list -> Elems.t -> Elems.t
val elems_of_list : int list -> Elems.t
module Tuples : Set.S with type elt = int array (** Sets of tuples of ints *)
val add_tuples : int array list -> Tuples.t -> Tuples.t
val tuples_of_list : int array list -> Tuples.t
(** {2 Structure type and basic getters.} *)
(** Elements are internally represented by integers, bu the structure
also stores a naming of elements. No element is named by a decimal
numeral other than its number to prevent misunderstandings.
Elements not appearing in [names] are assumed to be named
by their decimal numeral. *)
type structure
(** Comparison function for elements. *)
val compare_elems : int -> int -> int
(** Comparison function for structures. *)
val compare : structure -> structure -> int
(** Equality check on structures. *)
val equal : structure -> structure -> bool
(** Return the list of elements in a structure. *)
val elements : structure -> int list
(** Return the set of elements in a structure. *)
val elems : structure -> Elems.t
(** Return the assignment of constants in the structure. *)
val constants : structure -> (string * int) list
(** Number of elements in a structure. *)
val nbr_elems : structure -> int
(** Relations in the structure. *)
val relations : structure -> Tuples.t StringMap.t
(** Functions in the structure. *)
val functions : structure -> (float IntMap.t) StringMap.t
(** {3 Elements and their names.} *)
(** The integer corresponding to a given element name. *)
val elem_nbr : structure -> string -> int
(** The element name of an element (given by integers) *)
val elem_name : structure -> int -> string
(** The map containing element names. *)
val names : structure -> int StringMap.t
(** The inverse map of element names. *)
val inv_names : structure -> string IntMap.t
(** Replace the names of elements by new maps. *)
val replace_names : structure -> int StringMap.t -> string IntMap.t -> structure
(** {2 Basic helper functions} *)
(** Size of a relation, i.e. number of tuples in it. *)
val rel_size : structure -> string -> int
(** Reverse a map: make a string IntMap from an int StringMap. *)
val rev_string_to_int_map : int StringMap.t -> string IntMap.t
(** Reverse a map: make an int StringMap from a string IntMap. *)
val rev_int_to_string_map : string IntMap.t -> int StringMap.t
(** Return the empty structure (with empty signature). *)
val empty_structure : unit -> structure
(** Return the empty structure with given relational signature. *)
val empty_with_signat : (string * int) list -> structure
(** Return the list of relation tuples incident to an element [e] in [struc]. *)
val incident : structure -> int -> (string * int array list) list
(** Check if a relation holds for a tuple. *)
val check_rel : structure -> string -> int array -> bool
(** Graph of a relation in a model, returns an empty set if the
relation is not in the signature. *)
val rel_graph : string -> structure -> Tuples.t
(** Incidences of a relation in a model, returns an empty set if the
relation is not in the signature. *)
val rel_incidence : string -> structure -> Tuples.t array
(** Return the value of function [f] on [e] in [struc]. *)
val fun_val : structure -> string -> int -> float
(** Return the elements on which function [f] has value [x] in [struc]. *)
val elems_with_val : structure -> string -> float -> int list
(** Return the model assigned by [f] to [e] in [struc]. *)
val model_val : structure -> string -> int -> structure
(** Return the list of functions. *)
val f_signature : structure -> string list
(** Return the list of relations with their arities. *)
val rel_signature : structure -> (string * int) list
(** Cardinality of graphs of all relations in the structure. *)
val rel_sizes : structure -> (string * int) list
(** {2 Printing structures} *)
(** Print the elements [e] as string. *)
val elem_str : structure -> int -> string
(** Print the relation named [rel_name] with tuples [ts] as string.
Unless [print_arity] is false, print the arity if [ts] is empty. *)
val rel_str : ?print_arity:bool -> structure -> string -> Tuples.t -> string
(** Print the structure [struc] as string, in extensive form (not using
condensed representations like boards). If [show_empty] is false,
do not print the signatures of empty relations. *)
val ext_str : ?show_empty:bool -> structure -> string
(** Print the structure [struc] as string. *)
val str : ?show_empty:bool -> structure -> string
(** Print the relation with tuples [ts].
Unless [print_arity] is false, print the arity if [ts] is empty. *)
val fprint_rel : ?print_arity:bool -> structure -> Format.formatter ->
string * Tuples.t -> unit
val fprint_fun :
structure -> Format.formatter -> string * float IntMap.t -> unit
val fprint_ext_structure :
show_empty:bool -> Format.formatter -> structure -> unit
val fprint :
show_empty:bool -> Format.formatter -> structure -> unit
val print : ?show_empty:bool -> structure -> unit
val sprint : ?show_empty:bool -> structure -> string
(** Coordinates, column first, of a board element name. Raises
[Not_found] if the name is not of proper format. *)
val board_elem_coords : string -> int * int
(** Board element name under given coordinates, column first. Raises
[Not_found] if the coordinates are out of bounds. *)
val board_coords_name : int * int -> string
(** Compare two structures and explain the first difference met. *)
val compare_diff :
?cmp_funs:(float -> float -> bool) ->
structure -> structure -> bool * string
(** Elements from s1 which differ in s2, with differing relation names. *)
val diff_elems : structure -> structure -> (int * string list) list
(** {2 Adding elements possibly with string names} *)
(** Nonexisting elements or relations, signature mismatch, etc. *)
exception Structure_mismatch of string
(** Add element [e] to [struc] if it is not yet there. Return new structure. *)
val add_elem : structure -> ?name:string -> int -> structure
(** Add new element to [struc], return the updated structure and the
element. *)
val add_new_elem : structure -> ?name:string -> unit -> structure * int
val find_elem : structure -> string -> int
(** Find an element in the structure, and if not present, add new one. *)
val find_or_new_elem : structure -> string -> structure * int
(** {2 Adding relation tuples possibly with named elements} *)
(** Ensure relation named [rn] exists in [struc], add if needed. *)
val add_rel_name : string -> int -> structure -> structure
(** Add tuple [tp] to relation [rn] in structure [struc]. *)
val add_rel : structure -> string -> int array -> structure
(** Add tuple [tp] to relation [rn] in structure [struc]. *)
val add_rel_named_elems : structure -> string -> string array -> structure
(** Add tuple [tp] to relation [rn] in structure [struc] without
checking whether it and its elements already exist in the structure
and without checking arity. *)
val unsafe_add_rel : structure -> string -> int array -> structure
(** Add tuples [tps] to relation [rn] in structure [struc]. *)
val add_rels : structure -> string -> int array list -> structure
(** Add tuples [tps] to relation [rn] in structure [struc] without
checking for elements existence and arity matching. *)
val unsafe_add_rels : structure -> string -> int array list -> structure
(** Return a structure with a single relation of given arity, over a
single tuple, of different elements. *)
val free_for_rel : string -> int -> structure
(** {2 Adding function assignments possibly to named elements} *)
(** Add function assignment [e] -> [x] to function [fn] in structure [struc]. *)
val add_fun : structure -> string -> int * float -> structure
(** Add function assignments [assgns] to [fn] in structure [struc]. *)
val add_funs : structure -> string -> (int * float) list -> structure
(** Change function [fn] assignment for element [e] to [x] in [struc]. *)
val change_fun : structure -> string -> string -> float -> structure
val change_fun_int : structure -> string -> int -> float -> structure
(** {2 Global function to create structures from lists} *)
val create_from_lists : ?struc:structure -> string list ->
(string * int option * string array list, string * string) Aux.choice list ->
(string * (string * float) list) list -> structure
val create_from_lists_position: ?struc:structure -> string list ->
(string * int option * string array list, string * string) Aux.choice list ->
structure
val create_from_lists_range: float -> ?struc:structure -> string list ->
(string * int option * string array list, string * string) Aux.choice list ->
structure
(** {2 Removing relation tuples and elements from a structure} *)
(** Remove the tuple [tp] from relation [rn] in structure [struc]. *)
val del_rel : structure -> string -> int array -> structure
(** Remove the tuples [tps] from relation [rn] in structure [struc]. *)
val del_rels : structure -> string -> int array list -> structure
(** Remove all relations matching the predicate.
By default, also remove them from the signature. *)
val clear_rels :
?remove_from_sig:bool -> structure -> (string -> bool) -> structure
(** Remove the given function from [struc]. *)
val clear_fun : structure -> string -> structure
(** Remove element names from structure. *)
val clear_names : structure -> structure
(** Remove the element [e] and all incident relation tuples from [struc]. *)
val del_elem : structure -> int -> structure
(** Remove elements [es] and all incident relation tuples from
[struc]. Return the resulting structure and deleted relation tuples. *)
val del_elems : structure -> int list ->
structure * (string * int array list) list
(** Remove the elements that are not incident to any relation (and have
no defined properties, unless [ignore_funs] is given). *)
val gc_elems : ?ignore_funs:bool -> structure -> structure
(** Differing relations (used in solver cache) *)
val diffrels_struc: structure -> structure -> string list option
(** {2 Creating a structure from a TRS string} *)
(** Parse the TRS string, output messages and the resulting structure. *)
val struc_from_trs : string -> string * structure
(** {2 Parser Helpers} *)
exception Board_parse_error of string
(** Parse a rectangular board as a model, using "R" for rows, "C" for
columns, and the letter at a position for a unary
predicate. Line breaks '\n' are used for separating rows, spaces
' ' can be used for formatting, dot '.' is used for blank fields. *)
val parse_board :
?row_col_rels:string * string ->
?pos_initial:float * float ->
?pos_increment:float * float ->
?struc:structure -> string -> structure

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks