1(* OCaml interface: domain-independent functions.
2   Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3   Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5This file is part of the Parma Polyhedra Library (PPL).
6
7The PPL is free software; you can redistribute it and/or modify it
8under the terms of the GNU General Public License as published by the
9Free Software Foundation; either version 3 of the License, or (at your
10option) any later version.
11
12The PPL is distributed in the hope that it will be useful, but WITHOUT
13ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
15for more details.
16
17You should have received a copy of the GNU General Public License
18along with this program; if not, write to the Free Software Foundation,
19Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21For the most up-to-date information see the Parma Polyhedra Library
22site: http://bugseng.com/products/ppl/ . *)
23
24open Gmp
25
26exception PPL_arithmetic_overflow of string
27let _ = Callback.register_exception "PPL_arithmetic_overflow"
28          (PPL_arithmetic_overflow "any string")
29
30exception PPL_timeout_exception
31let _ = Callback.register_exception "PPL_timeout_exception"
32          (PPL_timeout_exception)
33
34exception PPL_internal_error of string
35let _ = Callback.register_exception "PPL_internal_error"
36          (PPL_internal_error "any string")
37
38exception PPL_unknown_standard_exception of string
39let _ = Callback.register_exception "PPL_unknown_standard_exception"
40          (PPL_unknown_standard_exception "any string")
41
42exception PPL_unexpected_error of string
43let _ = Callback.register_exception "PPL_unexpected_error"
44          (PPL_unexpected_error "any string")
45
46type degenerate_element =
47    Universe
48  | Empty
49
50type linear_expression =
51    Variable of int
52  | Coefficient of Z.t
53  | Unary_Plus of linear_expression
54  | Unary_Minus of linear_expression
55  | Plus of linear_expression * linear_expression
56  | Minus of linear_expression * linear_expression
57  | Times of Z.t * linear_expression
58
59type linear_constraint =
60    Less_Than of linear_expression * linear_expression
61  | Less_Or_Equal of linear_expression * linear_expression
62  | Equal of linear_expression * linear_expression
63  | Greater_Than of linear_expression * linear_expression
64  | Greater_Or_Equal of linear_expression * linear_expression
65
66type linear_generator =
67    Line of linear_expression
68  | Ray of linear_expression
69  | Point of linear_expression * Z.t
70  | Closure_Point of linear_expression * Z.t
71
72type linear_grid_generator =
73    Grid_Line of linear_expression
74  | Grid_Parameter of linear_expression * Z.t
75  | Grid_Point of linear_expression * Z.t
76
77type poly_gen_relation =
78    Subsumes
79
80type poly_con_relation =
81    Is_Disjoint
82  | Strictly_Intersects
83  | Is_Included
84  | Saturates
85
86type relation_with_congruence =
87    Is_Disjoint
88  | Strictly_Intersects
89  | Is_Included
90
91type linear_congruence = linear_expression * linear_expression * Z.t
92
93type constraint_system = linear_constraint list
94
95type generator_system = linear_generator list
96
97type grid_generator_system = linear_grid_generator list
98
99type congruence_system = linear_congruence list
100
101(* Note: the "_RS" suffix is to avoid name clashes with the declaration
102   of linear_constraint. *)
103type relation_symbol = Less_Than_RS | Less_Or_Equal_RS | Equal_RS
104                       | Greater_Than_RS | Greater_Or_Equal_RS
105
106type bounded_integer_type_overflow = Overflow_Wraps
107                                     | Overflow_Undefined
108                                     | Overflow_Impossible
109
110type bounded_integer_type_representation = Unsigned
111                                           | Signed_2_Complement
112
113type bounded_integer_type_width = Bits_8
114                                  | Bits_16
115                                  | Bits_32
116                                  | Bits_64
117                                  | Bits_128
118
119type complexity_class = Polynomial_Complexity
120                        | Simplex_Complexity
121                        | Any_Complexity
122
123type optimization_mode = Minimization | Maximization
124
125type mip_problem_status = Unfeasible_Mip_Problem | Unbounded_Mip_Problem
126                        | Optimized_Mip_Problem
127
128type control_parameter_name = Pricing
129
130type control_parameter_value = Pricing_Steepest_Edge_Float
131                             | Pricing_Steepest_Edge_Exact
132                             | Pricing_Textbook
133
134type mip_problem
135
136external ppl_version_major:
137unit -> int = "ppl_version_major"
138
139external ppl_version_minor:
140unit -> int = "ppl_version_minor"
141
142external ppl_version_revision:
143unit -> int = "ppl_version_revision"
144
145external ppl_version_beta:
146unit -> int = "ppl_version_beta"
147
148external ppl_version:
149unit -> string = "ppl_version"
150
151external ppl_banner:
152unit -> string = "ppl_banner"
153
154external ppl_io_wrap_string:
155string -> int -> int -> int -> string = "ppl_io_wrap_string"
156
157external ppl_max_space_dimension:
158unit -> int = "ppl_max_space_dimension"
159
160external ppl_Coefficient_bits:
161unit -> int = "ppl_Coefficient_bits"
162
163external ppl_Coefficient_is_bounded:
164unit -> bool = "ppl_Coefficient_is_bounded"
165
166external ppl_Coefficient_max:
167unit -> Z.t = "ppl_Coefficient_max"
168
169external ppl_Coefficient_min:
170unit -> Z.t = "ppl_Coefficient_min"
171
172external ppl_Linear_Expression_is_zero:
173linear_expression -> bool = "ppl_Linear_Expression_is_zero"
174
175external ppl_Linear_Expression_all_homogeneous_terms_are_zero:
176linear_expression -> bool
177      = "ppl_Linear_Expression_all_homogeneous_terms_are_zero"
178
179external ppl_set_rounding_for_PPL:
180unit -> unit = "ppl_set_rounding_for_PPL"
181
182external ppl_restore_pre_PPL_rounding:
183unit -> unit = "ppl_restore_pre_PPL_rounding"
184
185external ppl_irrational_precision:
186unit -> int = "ppl_irrational_precision"
187
188external ppl_set_irrational_precision:
189int -> unit = "ppl_set_irrational_precision"
190
191external ppl_set_timeout:
192int -> unit = "ppl_set_timeout"
193
194external ppl_reset_timeout:
195unit -> unit = "ppl_reset_timeout"
196
197external ppl_set_deterministic_timeout:
198int -> int -> unit = "ppl_set_deterministic_timeout"
199
200external ppl_reset_deterministic_timeout:
201unit -> unit = "ppl_reset_deterministic_timeout"
202
203external ppl_new_MIP_Problem_from_space_dimension:
204  int -> mip_problem = "ppl_new_MIP_Problem_from_space_dimension"
205
206external ppl_new_MIP_Problem:
207  int -> constraint_system -> linear_expression
208    -> optimization_mode -> mip_problem
209      = "ppl_new_MIP_Problem"
210
211external ppl_MIP_Problem_space_dimension:
212  mip_problem -> int = "ppl_MIP_Problem_space_dimension"
213
214external ppl_MIP_Problem_integer_space_dimensions:
215  mip_problem -> int list = "ppl_MIP_Problem_integer_space_dimensions"
216
217external ppl_MIP_Problem_constraints:
218  mip_problem -> constraint_system = "ppl_MIP_Problem_constraints"
219
220external ppl_MIP_Problem_add_space_dimensions_and_embed:
221  mip_problem -> int -> unit
222      = "ppl_MIP_Problem_add_space_dimensions_and_embed"
223
224external ppl_MIP_Problem_add_to_integer_space_dimensions:
225  mip_problem -> int list -> unit
226      = "ppl_MIP_Problem_add_to_integer_space_dimensions"
227
228external ppl_MIP_Problem_add_constraint:
229  mip_problem -> linear_constraint -> unit
230      = "ppl_MIP_Problem_add_constraint"
231
232external ppl_MIP_Problem_add_constraints:
233  mip_problem -> constraint_system -> unit
234      = "ppl_MIP_Problem_add_constraints"
235
236external ppl_MIP_Problem_set_objective_function:
237  mip_problem -> linear_expression -> unit
238      = "ppl_MIP_Problem_set_objective_function"
239
240external ppl_MIP_Problem_is_satisfiable:
241  mip_problem -> bool
242      = "ppl_MIP_Problem_is_satisfiable"
243
244external ppl_MIP_Problem_solve:
245  mip_problem -> mip_problem_status
246      = "ppl_MIP_Problem_solve"
247
248external ppl_MIP_Problem_optimization_mode:
249  mip_problem -> optimization_mode
250      = "ppl_MIP_Problem_optimization_mode"
251
252external ppl_MIP_Problem_feasible_point:
253  mip_problem -> linear_generator
254      = "ppl_MIP_Problem_feasible_point"
255
256external ppl_MIP_Problem_optimizing_point:
257  mip_problem -> linear_generator
258      = "ppl_MIP_Problem_optimizing_point"
259
260external ppl_MIP_Problem_objective_function:
261  mip_problem -> linear_expression
262      = "ppl_MIP_Problem_objective_function"
263
264external ppl_MIP_Problem_optimal_value:
265  mip_problem -> Z.t * Z.t
266      = "ppl_MIP_Problem_optimal_value"
267
268external ppl_MIP_Problem_evaluate_objective_function:
269  mip_problem -> linear_generator  -> Z.t * Z.t
270      = "ppl_MIP_Problem_evaluate_objective_function"
271
272external ppl_MIP_Problem_OK:
273  mip_problem -> bool
274      = "ppl_MIP_Problem_OK"
275
276external ppl_MIP_Problem_clear:
277  mip_problem -> unit
278      = "ppl_MIP_Problem_clear"
279
280external ppl_MIP_Problem_set_optimization_mode:
281  mip_problem -> optimization_mode -> unit
282      = "ppl_MIP_Problem_set_optimization_mode"
283
284external ppl_MIP_Problem_set_control_parameter:
285  mip_problem -> control_parameter_value -> unit
286      = "ppl_MIP_Problem_set_control_parameter"
287
288external ppl_MIP_Problem_get_control_parameter:
289  mip_problem -> control_parameter_name -> control_parameter_value
290      = "ppl_MIP_Problem_get_control_parameter"
291
292external ppl_MIP_Problem_swap:
293  mip_problem -> mip_problem -> unit
294      = "ppl_MIP_Problem_swap"
295
296external ppl_MIP_Problem_ascii_dump:
297  mip_problem -> string
298      = "ppl_MIP_Problem_ascii_dump"
299
300
301type pip_problem_status = Unfeasible_Pip_Problem
302                        | Optimized_Pip_Problem
303
304type pip_problem_control_parameter_name = Cutting_Strategy | Pivot_Row_Strategy
305
306type pip_problem_control_parameter_value = Cutting_Strategy_First
307                                         | Cutting_Strategy_Deepest
308                                         | Cutting_Strategy_All
309                                         | Pivot_Row_Strategy_First
310                                         | Pivot_Row_Strategy_Max_Column
311
312type artificial_parameter = linear_expression * Z.t
313
314type pip_tree_node
315
316type pip_problem
317
318external ppl_new_PIP_Problem_from_space_dimension:
319  int -> pip_problem = "ppl_new_PIP_Problem_from_space_dimension"
320
321external ppl_new_PIP_Problem:
322  int -> constraint_system -> int list -> pip_problem
323    = "ppl_new_PIP_Problem"
324
325external ppl_PIP_Problem_space_dimension:
326  pip_problem -> int = "ppl_PIP_Problem_space_dimension"
327
328external ppl_PIP_Problem_parameter_space_dimensions:
329  pip_problem -> int list = "ppl_PIP_Problem_parameter_space_dimensions"
330
331external ppl_PIP_Problem_constraints:
332  pip_problem -> constraint_system = "ppl_PIP_Problem_constraints"
333
334external ppl_PIP_Problem_add_space_dimensions_and_embed:
335  pip_problem -> int -> int -> unit
336      = "ppl_PIP_Problem_add_space_dimensions_and_embed"
337
338external ppl_PIP_Problem_add_to_parameter_space_dimensions:
339  pip_problem -> int list -> unit
340      = "ppl_PIP_Problem_add_to_parameter_space_dimensions"
341
342external ppl_PIP_Problem_add_constraint:
343  pip_problem -> linear_constraint -> unit
344      = "ppl_PIP_Problem_add_constraint"
345
346external ppl_PIP_Problem_add_constraints:
347  pip_problem -> constraint_system -> unit
348      = "ppl_PIP_Problem_add_constraints"
349
350external ppl_PIP_Problem_is_satisfiable:
351  pip_problem -> bool
352      = "ppl_PIP_Problem_is_satisfiable"
353
354external ppl_PIP_Problem_solve:
355  pip_problem -> pip_problem_status
356      = "ppl_PIP_Problem_solve"
357
358external ppl_PIP_Problem_solution:
359  pip_problem -> pip_tree_node
360      = "ppl_PIP_Problem_solution"
361
362external ppl_PIP_Problem_optimizing_solution:
363  pip_problem -> pip_tree_node
364      = "ppl_PIP_Problem_optimizing_solution"
365
366external ppl_PIP_Problem_get_big_parameter_dimension:
367  pip_problem -> int = "ppl_PIP_Problem_get_big_parameter_dimension"
368
369external ppl_PIP_Problem_has_big_parameter_dimension:
370  pip_problem -> bool = "ppl_PIP_Problem_has_big_parameter_dimension"
371
372external ppl_PIP_Problem_set_big_parameter_dimension:
373  pip_problem -> int -> unit = "ppl_PIP_Problem_set_big_parameter_dimension"
374
375external ppl_PIP_Problem_OK:
376  pip_problem -> bool
377      = "ppl_PIP_Problem_OK"
378
379external ppl_PIP_Problem_clear:
380  pip_problem -> unit
381      = "ppl_PIP_Problem_clear"
382
383external ppl_PIP_Problem_set_control_parameter:
384  pip_problem -> pip_problem_control_parameter_value -> unit
385      = "ppl_PIP_Problem_set_control_parameter"
386
387external ppl_PIP_Problem_get_control_parameter:
388  pip_problem -> pip_problem_control_parameter_name
389              -> pip_problem_control_parameter_value
390      = "ppl_PIP_Problem_get_control_parameter"
391
392external ppl_PIP_Problem_swap:
393  pip_problem -> pip_problem -> unit
394      = "ppl_PIP_Problem_swap"
395
396external ppl_PIP_Problem_ascii_dump:
397  pip_problem -> string
398      = "ppl_PIP_Problem_ascii_dump"
399
400external ppl_PIP_Tree_Node_constraints:
401  pip_tree_node -> constraint_system
402      = "ppl_PIP_Tree_Node_constraints"
403
404external ppl_PIP_Tree_Node_artificials:
405  pip_tree_node -> artificial_parameter list
406      = "ppl_PIP_Tree_Node_artificials"
407
408external ppl_PIP_Tree_Node_OK:
409  pip_tree_node -> bool
410      = "ppl_PIP_Tree_Node_OK"
411
412external ppl_PIP_Tree_Node_ascii_dump:
413  pip_tree_node -> string
414      = "ppl_PIP_Tree_Node_ascii_dump"
415
416external ppl_PIP_Tree_Node_is_bottom:
417  pip_tree_node -> bool
418      = "ppl_PIP_Tree_Node_is_bottom"
419
420external ppl_PIP_Tree_Node_is_solution:
421  pip_tree_node -> bool
422      = "ppl_PIP_Tree_Node_is_solution"
423
424external ppl_PIP_Tree_Node_parametric_values:
425  pip_tree_node -> int -> linear_expression
426      = "ppl_PIP_Tree_Node_parametric_values"
427
428external ppl_PIP_Tree_Node_is_decision:
429  pip_tree_node -> bool
430      = "ppl_PIP_Tree_Node_is_decision"
431
432external ppl_PIP_Tree_Node_true_child:
433  pip_tree_node -> pip_tree_node
434      = "ppl_PIP_Tree_Node_true_child"
435
436external ppl_PIP_Tree_Node_false_child:
437  pip_tree_node -> pip_tree_node
438      = "ppl_PIP_Tree_Node_false_child"
439