package colibrics

  1. Overview
  2. Docs

Source file all__API.ml

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