/usr/lib/ocaml/facile/fcl_arith.mli is in libfacile-ocaml-dev 1.1.1-1build2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | (***********************************************************************)
(* *)
(* FaCiLe *)
(* A Functional Constraint Library *)
(* *)
(* Nicolas Barnier, Pascal Brisset, LOG, CENA *)
(* *)
(* Copyright 2004 CENA. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License. *)
(***********************************************************************)
(** {1 Arithmetic Expressions and Constraints}
*)
(** {% \paragraph{Overview} %} *)
(** This module provides functions and operators to build arithmetic
expressions and state (in/dis)equation constraints on them.
*)
(** {2 Basics} *)
type t
(** Type of arithmetic expressions over variables of type [Var.Fd.t] and
integers. *)
(*** Conversion *)
val i2e : int -> t
(** [i2e n] returns an expression which evaluates to [n]. *)
val fd2e : Fcl_var.Fd.t -> t
(** [fd2e v] returns an expression which evaluates to [n] if the
variable [v] is instantiated to [n]. *)
val e2fd : t -> Fcl_var.Fd.t
(** [e2fd e] creates and returns a new variable [v] and posts the constraint
[fd2e v =~ e]. *)
(** {2 Construction of Arithmetic Expressions} *)
(**
{b Only} if compiled in bytecode (using [facile.cma]),
the arithmetic operators check whether any integer overflow
(i.e. the result of an arithmetic operation on integers is
less than [min_int] or greater than [max_int]) occurs during
constraints internal computations and raise an assert failure.
Arithmetic operations are taken modulo {% $2^{31}$%} otherwise
(or {% $2^{63}$%} on 64-bit processors, see the OCaml reference
manual{% ~\cite{ocaml}%}), thus incomplete failures may happen
with native code compiled programs. *)
val (+~) : t -> t -> t
val (-~) : t -> t -> t
val ( *~) : t -> t -> t
(** Addition, substraction, multiplication on expressions. *)
val ( **~) : t -> int -> t
(** Exponentiation of an expression to an integer value. *)
val (/~) : t -> t -> t
val (%~) : t -> t -> t
(** Division and modulo on expressions. The exception [Division_by_zero]
is raised whenever the second argument evaluates to 0. *)
val abs : t -> t
(** Absolute value on expressions. *)
val sum : t array -> t
val sum_fd : Fcl_var.Fd.t array -> t
(** [sum exps] (resp. [sum_fd vars]) returns the sum of all the elements of an
array of expressions (resp. variables). Returns an expression that evaluates
to 0 if the array is empty. *)
val scalprod : int array -> t array -> t
val scalprod_fd : int array -> Fcl_var.Fd.t array -> t
(** [scalprod coeffs exps] (resp. [scalprod_fd coeffs vars]) returns the
scalar product of an array of integers and an array of expressions
(resp. variables).
Returns an expression that evaluates to 0 if both arrays are empty.
Raises [Invalid_argument] if the arrays don't have the same length. *)
val prod : t array -> t
val prod_fd : Fcl_var.Fd.t array -> t
(** [prod exps] (resp. [prod_fd vars]) returns the product of all the
elements of an array of expressions (resp. variables).
Returns an expression that evaluates to 1 if the array is empty. *)
(** {2 Access} *)
val fprint : out_channel -> t -> unit
(** [fprint chan e] prints expression [e] on channel [chan]. *)
val eval : t -> int
(** [eval e] returns the integer numerical value of a fully instantiated
expression [e]. Raises [Invalid_argument] if [e] is not instantiated. *)
val min_of_expr : t -> int
val max_of_expr : t -> int
(** [min_of_expr e] (resp. [max_of_expr e]) returns the minimal (resp. maximal)
possible value of expression [e]. *)
val min_max_of_expr : t -> (int * int)
(** [min_max_of_expr e] is equivalent to [(min_of_expr e, max_of_expr e)]. *)
(** {2 Arithmetic Constraints on Expressions} *)
(**
FaCiLe processes arithmetic constraints to try to simplify and factorize
common subexpressions. Furthermore, auxilliary variables are created to
handle non-linear expressions and substituted to the original terms.
So printing an arithmetic constraint may produce something quite
different from the user's input. *)
val (<~) : t -> t -> Fcl_cstr.t
val (<=~) : t -> t -> Fcl_cstr.t
val (=~) : t -> t -> Fcl_cstr.t
val (>=~) : t -> t -> Fcl_cstr.t
val (>~) : t -> t -> Fcl_cstr.t
val (<>~) : t -> t -> Fcl_cstr.t
(** Strictly less, less or equal, equal, greater or equal,
strictly greater and different constraints on expressions. *)
val shift : Fcl_var.Fd.t -> int -> Fcl_var.Fd.t
(** [shift x d] returns a finite domain variable constrained to be
equal to [x+d]. *)
(** {2 Reification} *)
(**
The following operators are shortcuts to lighten the writing of reified
expressions. They replace the corresponding constraint by an expression
equal to a boolean variable that is instantiated to [1] when the constraint is
satisfied and to [0] if it is violated.
See module [Reify] {% \ref{module:Reify}%}. *)
(** [e1 op~~ e2] is equivalent to [fd2e (Reify.boolean (e1 op~ e2))]. *)
val (<~~) : t -> t -> t
val (<=~~) : t -> t -> t
val (=~~) : t -> t -> t
val (>=~~) : t -> t -> t
val (>~~) : t -> t -> t
val (<>~~) : t -> t -> t
(** Reified strictly less, less or equal, equal, greater or equal,
strictly greater and different. *)
(** {2 Boolean sums setting}
FaCiLe tries to automatically optimize the processing of
boolean (0-1 variables) sums whenever their sizes are large enough. *)
val get_boolsum_threshold : unit -> int
(** Returns the minimum size for boolean sums optimization. (Default: 5) *)
val set_boolsum_threshold : int -> unit
(** Set the minimum size for boolean sums optimization.
[boolsum_threshold max_int] disables it. *)
|