Source file constraints__cst__C.ml

type t = {
  v: 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.v))

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 di = { Cp__DomI.min = c.i; Cp__DomI.max = c.i } in
     Cp__ConstraintHelpers.set_int e c.v di)
  | Cp__DomB.V (false) ->
    (let d1 = Cp__Type.get_int e c.v in
     if
       Z.equal d1.Cp__DomI.min d1.Cp__DomI.max && Z.equal d1.Cp__DomI.min c.i
     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 (Cp__Type.get_mod_int mo c.v) c.i)
  (Cp__Type.get_mod_bool mo c.b)