Source file `constraintsequivC.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
type t = {
  b1: Cp__Var0.tb;
  b2: Cp__Var0.tb;
  b3: Cp__Var0.tb;
  }

let compute_vars_ti (_c: t) (_si: Cp__Impl0.Si.t) : unit = ()

let compute_vars_tb (c: t) (sb: Cp__Impl0.Sb.t) : unit =
  (Cp__Impl0.Sb.add sb (c.b1));
  (Cp__Impl0.Sb.add sb (c.b2));
  (Cp__Impl0.Sb.add sb (c.b3))

let propagate (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env) (c: t) : unit =
  match (Cp__Type.get_bool e c.b1, Cp__Type.get_bool e c.b2) with
  | (Cp__DomB.V b1',
    Cp__DomB.V b2') ->
    Cp__ConstraintHelpers.set_bool e c.b3 (Utils__extstd__Bool.eqb b1' b2')
  | _ -> ()

let check_model (mo: (Z.t, bool) Cp__Type.model) (c: t) : bool =
  Utils__extstd__Bool.eqb (Utils__extstd__Bool.eqb (Cp__Type.get_mod_bool mo
                                                    c.b1)
                           (Cp__Type.get_mod_bool mo c.b2))
  (Cp__Type.get_mod_bool mo c.b3)