Source file `all__APIDefensive.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
type ti = Cp__Var0.ti

type tb = Cp__Var0.tb

type interp = (Z.t, bool) Cp__Type.interp

let true_ : Cp__Var0.tb = All__API.true_

let zero_ : Cp__Var0.ti = All__API.zero_

type context = All__API.context

let create_vari (c: All__API.context) (min_: Z.t) (max_: Z.t) : Cp__Var0.ti =
  All__API.create_vari c min_ max_

let create_varb (c: All__API.context) : Cp__Var0.tb = All__API.create_varb c

let create_context (_: unit) : All__API.context = All__API.create_context ()

exception UnknownVariable

let check_ti (c: All__API.context) (v: Cp__Var0.ti) : unit =
  if let q1_ = v in 1 <= q1_ && (let o = c.All__API.nexti in q1_ < o)
  then ()
  else raise UnknownVariable

let check_tb (c: All__API.context) (v: Cp__Var0.tb) : unit =
  if let q1_ = v in 1 <= q1_ && (let o = c.All__API.nextb in q1_ < o)
  then ()
  else raise UnknownVariable

let is_cst_reif (c: All__API.context) (v: Cp__Var0.ti) (iv: Z.t)
                (r: Cp__Var0.tb) : unit =
  check_ti c v; check_tb c r; All__API.is_cst_reif c v iv r

let is_cst (c: All__API.context) (v: Cp__Var0.ti) (iv: Z.t) : unit =
  check_ti c v; All__API.is_cst c v iv

let add_reif (c: All__API.context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti)
             (v3: Cp__Var0.ti) (r: Cp__Var0.tb) : unit =
  check_ti c v1;
  check_ti c v2;
  check_ti c v3;
  check_tb c r;
  All__API.add_reif c v1 v2 v3 r

let add (c: All__API.context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti)
        (v3: Cp__Var0.ti) : unit =
  check_ti c v1; check_ti c v2; check_ti c v3; All__API.add c v1 v2 v3

let le_reif (c: All__API.context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti)
            (cst: Z.t) (r: Cp__Var0.tb) : unit =
  check_ti c v1; check_ti c v2; check_tb c r; All__API.le_reif c v1 v2 cst r

let le (c: All__API.context) (v1: Cp__Var0.ti) (v2: Cp__Var0.ti) (cst: Z.t) :
  unit = check_ti c v1; check_ti c v2; All__API.le c v1 v2 cst

let or1 (c: All__API.context) (b1: Cp__Var0.tb) (b2: Cp__Var0.tb)
        (b3: Cp__Var0.tb) : unit =
  check_tb c b1; check_tb c b2; check_tb c b3; All__API.or1 c b1 b2 b3

let equiv (c: All__API.context) (b1: Cp__Var0.tb) (b2: Cp__Var0.tb)
          (b3: Cp__Var0.tb) : unit =
  check_tb c b1; check_tb c b2; check_tb c b3; All__API.equiv c b1 b2 b3

let not_ (c: All__API.context) (b1: Cp__Var0.tb) (b2: Cp__Var0.tb) : unit =
  check_tb c b1; check_tb c b2; All__API.not_ c b1 b2

let is_true (c: All__API.context) (b1: Cp__Var0.tb) : unit =
  check_tb c b1; All__API.is_true c b1

type model = {
  mod1: (Z.t, bool) Cp__Type.model;
  lasti: int;
  lastb: int;
  }

let solve (c: All__API.context) : model =
  let o = c.All__API.nextb - 1 in
  let o1 = c.All__API.nexti - 1 in
  let o2 = All__API.solve c in
  { mod1 = o2; lasti = o1; lastb = o }

let get_model_i (m: model) (v: Cp__Var0.ti) : Z.t =
  if let q1_ = v in 1 <= q1_ && q1_ <= m.lasti
  then ()
  else raise UnknownVariable;
  (Cp__Impl0.Hi.Make.Lock.find (m.mod1.Cp__Type.modi) v)

let get_model_b (m: model) (v: Cp__Var0.tb) : bool =
  if let q1_ = v in 1 <= q1_ && q1_ <= m.lastb
  then ()
  else raise UnknownVariable;
  (Cp__Impl0.Hb.Make.Lock.find (m.mod1.Cp__Type.modb) v)