Source file `constraintsaddC.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
type t = {
  v1: Cp__Var0.ti;
  v2: Cp__Var0.ti;
  v3: Cp__Var0.ti;
  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));
  (Cp__Impl0.Si.add si (c.v3))

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
     let d3 = Cp__Type.get_int e c.v3 in
     let mind3 =
       Cp__ConstraintHelpers.max (Z.add d1.Cp__DomI.min d2.Cp__DomI.min)
       d3.Cp__DomI.min in
     let maxd3 =
       Cp__ConstraintHelpers.min (Z.add d1.Cp__DomI.max d2.Cp__DomI.max)
       d3.Cp__DomI.max in
     let mind1 =
       Cp__ConstraintHelpers.max (Z.sub d3.Cp__DomI.min d2.Cp__DomI.max)
       d1.Cp__DomI.min in
     let maxd1 =
       Cp__ConstraintHelpers.min (Z.sub d3.Cp__DomI.max d2.Cp__DomI.min)
       d1.Cp__DomI.max in
     let mind2 =
       Cp__ConstraintHelpers.max (Z.sub mind3 maxd1) d2.Cp__DomI.min in
     let maxd2 =
       Cp__ConstraintHelpers.min (Z.sub maxd3 mind1) d2.Cp__DomI.max in
     let mind31 = Cp__ConstraintHelpers.max (Z.add mind1 mind2) mind3 in
     let maxd31 = Cp__ConstraintHelpers.min (Z.add maxd1 maxd2) maxd3 in
     let mind11 = Cp__ConstraintHelpers.max (Z.sub mind31 maxd2) mind1 in
     let maxd11 = Cp__ConstraintHelpers.min (Z.sub maxd31 mind2) maxd1 in
     let mind21 = Cp__ConstraintHelpers.max (Z.sub mind31 maxd11) mind2 in
     let maxd21 = Cp__ConstraintHelpers.min (Z.sub maxd31 mind11) maxd2 in
     Cp__ConstraintHelpers.set_int e
     c.v1
     { Cp__DomI.min = mind11; Cp__DomI.max = maxd11 };
     Cp__ConstraintHelpers.set_int e
     c.v2
     { Cp__DomI.min = mind21; Cp__DomI.max = maxd21 };
     Cp__ConstraintHelpers.set_int e
     c.v3
     { Cp__DomI.min = mind31; Cp__DomI.max = maxd31 })
  | Cp__DomB.V (false) ->
    (let d1 = Cp__Type.get_int e c.v1 in let d2 = Cp__Type.get_int e c.v2 in
     let d3 = Cp__Type.get_int e c.v3 in
     if
       Z.equal d1.Cp__DomI.min d1.Cp__DomI.max && Z.equal d2.Cp__DomI.min
                                                  d2.Cp__DomI.max && 
                                                  Z.equal d3.Cp__DomI.min
                                                  d3.Cp__DomI.max && 
                                                  Z.equal (Z.add d1.Cp__DomI.min
                                                           d2.Cp__DomI.min)
                                                  d3.Cp__DomI.min
     then raise Cp__Type.Unsat)
  | Cp__DomB.Top -> ()

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