module Arith:sig
..end
type
t
Var.Fd.t
and
integers.val i2e : int -> t
i2e n
returns an expression which evaluates to n
.val fd2e : Var.Fd.t -> t
fd2e v
returns an expression which evaluates to n
if the
variable v
is instantiated to n
.val e2fd : t -> Var.Fd.t
e2fd e
creates and returns a new variable v
and posts the constraint
fd2e v =~ e
.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 otherwise
(or on 64-bit processors, see the OCaml reference
manual), thus incomplete failures may happen
with native code compiled programs.val (+~) : t -> t -> t
val (-~) : t -> t -> t
val (*~) : t -> t -> t
val (**~) : t -> int -> t
val (/~) : t -> t -> t
val (%~) : t -> t -> t
Division_by_zero
is raised whenever the second argument evaluates to 0.val abs : t -> t
val sum : t array -> t
val sum_fd : 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 -> 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 : 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.val fprint : Pervasives.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)
.val (<~) : t -> t -> Cstr.t
val (<=~) : t -> t -> Cstr.t
val (=~) : t -> t -> Cstr.t
val (>=~) : t -> t -> Cstr.t
val (>~) : t -> t -> Cstr.t
val (<>~) : t -> t -> Cstr.t
val shift : Var.Fd.t -> int -> Var.Fd.t
shift x d
returns a finite domain variable constrained to be
equal to x+d
.1
when the constraint is
satisfied and to 0
if it is violated.
See module Reify
.val (<~~) : t -> t -> t
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
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
val set_boolsum_threshold : int -> unit
boolsum_threshold max_int
disables it.