Source file `constraintsleC.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
type t = {
  v1: Cp__Var0.ti;
  v2: Cp__Var0.ti;
  i: Z.t;
  b: Cp__Var0.tb;
  }

let compute_vars_ti (c: t) (si: Cp__Impl0.Si.t) : unit =
  (Cp__Impl0.Si.add si (c.v1)); (Cp__Impl0.Si.add si (c.v2))

let compute_vars_tb (c: t) (sb: Cp__Impl0.Sb.t) : unit =
  (Cp__Impl0.Sb.add sb (c.b))

let propagate (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env) (c: t) : unit =
  match Cp__Type.get_bool e c.b with
  | Cp__DomB.V (true) ->
    (let d1 = Cp__Type.get_int e c.v1 in let d2 = Cp__Type.get_int e c.v2 in
     Cp__ConstraintHelpers.set_int e
     c.v1
     { Cp__DomI.min = d1.Cp__DomI.min; Cp__DomI.max =
       Z.add d2.Cp__DomI.max c.i };
     Cp__ConstraintHelpers.set_int e
     c.v2
     { Cp__DomI.min = Z.sub d1.Cp__DomI.min c.i; Cp__DomI.max =
       d2.Cp__DomI.max })
  | Cp__DomB.V (false) ->
    (let d1 = Cp__Type.get_int e c.v1 in let d2 = Cp__Type.get_int e c.v2 in
     Cp__ConstraintHelpers.set_int e
     c.v1
     { Cp__DomI.min = Z.add (Z.add d2.Cp__DomI.min c.i) Z.one; Cp__DomI.max =
       d1.Cp__DomI.max };
     Cp__ConstraintHelpers.set_int e
     c.v2
     { Cp__DomI.min = d2.Cp__DomI.min; Cp__DomI.max =
       Z.sub (Z.sub d1.Cp__DomI.max c.i) Z.one })
  | Cp__DomB.Top -> ()

let check_model (mo: (Z.t, bool) Cp__Type.model) (c: t) : bool =
  Utils__extstd__Bool.eqb (Z.leq (Cp__Type.get_mod_int mo c.v1)
                           (Z.add (Cp__Type.get_mod_int mo c.v2) c.i))
  (Cp__Type.get_mod_bool mo c.b)