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
|
(***********************************************************************)
(* *)
(* 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. *)
(***********************************************************************)
open Fcl_misc.Operators
open Fcl_var
open Fcl_expr
type t = Fcl_expr.t
let fprint = Fcl_expr.fprint
let eval = Fcl_expr.eval
let min_of_expr = Fcl_expr.min_of_expr
let max_of_expr = Fcl_expr.max_of_expr
let min_max_of_expr = Fcl_expr.min_max_of_expr
let i2e x = Inte x
let fd2e x = match Fd.value x with Val i -> Inte i | _ -> Fde (Var x)
let ( +~ ) x y =
let l = List.sort compare_intexpr [(1, x); (1, y)] in
Agg (Pluse, l, 0)
let sum tx =
let l =
List.sort compare_intexpr (List.map (fun x -> (1, x)) (Array.to_list tx)) in
Agg (Pluse, l, 0)
let sum_fd tx = sum (Array.map fd2e tx)
let ( *~ ) x y =
let l = List.sort compare_intexpr [(1, x); (1, y)] in
Agg (Multe, l, 1)
let ( -~ ) x y = Agg (Pluse, [(-1, y); (1, x)], 0)
let ( /~ ) x y = Bin (Dive, x, y)
let ( %~ ) x y = Bin (Mode, x, y)
let abs x = Un (Abse, x)
let ( **~ ) x n =
if n < 0 then Fcl_debug.fatal_error "**~ : negative exponent"
else if n = 0 then Inte 1
else Agg (Multe, [(n, x)], 1)
let prod es =
let l = List.map (fun x -> (1, x)) (Array.to_list es) in
let l = List.sort compare_intexpr l in
Agg (Multe, l, 1)
let prod_fd vs = prod (Array.map fd2e vs)
let scalprod scals exps =
if Array.length scals <> Array.length exps then
Fcl_debug.fatal_error "Arith.scalprod : arrays have not the same length";
sum (Array.mapi (fun i ei -> ei *~ i2e scals.(i)) exps)
let scalprod_fd ints vars = scalprod ints (Array.map fd2e vars)
let (=~) e1 e2 = constrain (e1 -~ e2) Fcl_linear.Equal
let (<>~) e1 e2 = constrain (e1 -~ e2) Fcl_linear.Diff
let (<=~) e1 e2 = constrain (e1 -~ e2) Fcl_linear.LessThan
let (>=~) e1 e2 = e2 <=~ e1
let (<~) e1 e2 = constrain (e1 -~ e2 +~ i2e 1) Fcl_linear.LessThan
let (>~) e1 e2 = e2 <~ e1
let e2fd e =
match reduce e with
Inte x -> Fd.int x
| Fde (Var v) -> v
| Fde (Aux _) -> assert false
| re -> begin
let (a, b) = min_max_of_expr re in
let v = Fd.interval a b in
Fcl_cstr.post (fd2e v =~ re);
v end
let reify_bin op e1 e2 = fd2e (Fcl_reify.boolean (op e1 e2))
let (=~~) = reify_bin (=~)
let (>=~~) = reify_bin (>=~)
let (<=~~) = reify_bin (<=~)
let (<~~) = reify_bin (<~)
let (>~~) = reify_bin (>~)
let (<>~~) = reify_bin (<>~)
let shift x d =
let (a, b) = Fd.min_max x in
let y = Fd.interval (a + d) (b + d) in
Fcl_cstr.post (Fcl_linear.shift_cstr y x d);
y
let get_boolsum_threshold = Fcl_linear.get_boolsum_threshold
let set_boolsum_threshold = Fcl_linear.set_boolsum_threshold
|
