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
type ti = Cp__Var0.ti
type tb = Cp__Var0.tb
type interp = (Z.t, bool) Cp__Type.interp
let true_ : Cp__Var0.tb = 1
let zero_ : Cp__Var0.ti = 1
type context = {
mutable intmin: Z.t;
mutable intmax: Z.t;
mutable nexti: int;
mutable nextb: int;
mutable prob: Constraints__simple__Simple.t list;
}
let create_vari (c: context) (min_: Z.t) (max_: Z.t) : Cp__Var0.ti =
c.nexti <- c.nexti + 1;
let r = let o = let o1 = c.nexti in o1 - 1 in o in
c.intmin <- Z.min c.intmin min_;
c.intmax <- Z.max c.intmax max_;
let ctr1 =
{ Constraints__le__C.v1 = r; Constraints__le__C.v2 = zero_;
Constraints__le__C.i = max_; Constraints__le__C.b = true_ } in
let ctr2 =
{ Constraints__le__C.v1 = zero_; Constraints__le__C.v2 = r;
Constraints__le__C.i = Z.neg min_; Constraints__le__C.b = true_ } in
c.prob <-
Constraints__simple__Simple.Le ctr1 :: Constraints__simple__Simple.Le ctr2 ::
c.prob;
r
let create_varb (c: context) : Cp__Var0.tb =
if let o = c.nextb in o = true_ then c.nextb <- c.nextb + 1;
c.nextb <- c.nextb + 1;
let r = let o = let o1 = c.nextb in o1 - 1 in o in
ignore c.nextb;
c.prob <- Constraints__simple__Simple.BoolPresent r :: c.prob;
r
let create_context (_: unit) : context =
{ intmin = Z.zero; intmax = Z.zero; nexti = 1 + 1; nextb = 1 + 1; prob =
Constraints__simple__Simple.Cst { Constraints__cst__C.v = zero_;
Constraints__cst__C.i = Z.zero;
Constraints__cst__C.b = true_ } ::
Constraints__simple__Simple.IsTrue true_ :: [] }
let is_cst_reif (c: context) (v: Cp__Var0.ti) (iv: Z.t) (r: Cp__Var0.tb) :
unit =
c.prob <-
Constraints__simple__Simple.Cst { Constraints__cst__C.v = v;
Constraints__cst__C.i = iv;
Constraints__cst__C.b = r } ::
c.prob
let is_cst (c: context) (v: Cp__Var0.ti) (iv: Z.t) : unit =
is_cst_reif c v iv true_
let add_reif (c: context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti)
(v3: Cp__Var0.ti) (r: Cp__Var0.tb) : unit =
c.prob <-
Constraints__simple__Simple.Add { Constraints__add__C.v1 = v1;
Constraints__add__C.v2 = v2;
Constraints__add__C.v3 = v3;
Constraints__add__C.b = r } ::
c.prob
let add (c: context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti) (v3: Cp__Var0.ti) :
unit = add_reif c v1 v2 v3 true_
let le_reif (c: context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti) (cst: Z.t)
(r: Cp__Var0.tb) : unit =
c.prob <-
Constraints__simple__Simple.Le { Constraints__le__C.v1 = v1;
Constraints__le__C.v2 = v2;
Constraints__le__C.i = cst;
Constraints__le__C.b = r } :: c.prob
let le (c: context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti) (cst: Z.t) : unit =
le_reif c v1 v2 cst true_
let or1 (c: context) (b1: Cp__Var0.tb) (b2: Cp__Var0.tb) (b3: Cp__Var0.tb) :
unit =
c.prob <-
Constraints__simple__Simple.Or { Constraints__or__C.b1 = b1;
Constraints__or__C.b2 = b2;
Constraints__or__C.b3 = b3 } ::
c.prob
let equiv (c: context) (b1: Cp__Var0.tb) (b2: Cp__Var0.tb) (b3: Cp__Var0.tb) :
unit =
c.prob <-
Constraints__simple__Simple.Equiv { Constraints__equiv__C.b1 = b1;
Constraints__equiv__C.b2 = b2;
Constraints__equiv__C.b3 = b3 } ::
c.prob
let not_ (c: context) (b1: Cp__Var0.tb) (b2: Cp__Var0.tb) : unit =
c.prob <-
Constraints__simple__Simple.Not { Constraints__not___C.b1 = b1;
Constraints__not___C.b2 = b2 } ::
c.prob
let is_true (c: context) (b1: Cp__Var0.tb) : unit =
c.prob <- Constraints__simple__Simple.IsTrue b1 :: c.prob
let solve (c: context) : (Z.t, bool) Cp__Type.model =
All__All.start' c.prob c.intmin c.intmax