Source file `cp__ConstraintHelpers.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
type env = (Cp__DomI.t, Cp__DomB.t) Cp__Type.env

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

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

module Interp =
struct type t = (Z.t, bool) Cp__Type.interp end

let update_bool (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env) (v: Cp__Var0.tb)
                (di: bool) : unit =
  (Cp__Impl0.Hbb.Make.set (e.Cp__Type.domb) v (Cp__DomB.V di));
  e.Cp__Type.dirty <- true

let set_bool (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env) (v: Cp__Var0.tb)
             (di: bool) : unit =
  match Cp__Type.get_bool e v with
  | Cp__DomB.Top ->
    (Cp__Impl0.Hbb.Make.set (e.Cp__Type.domb) v (Cp__DomB.V di));
    e.Cp__Type.dirty <- true
  | Cp__DomB.V di2 ->
    if Utils__extstd__Bool.eqb di di2 then () else raise Cp__Type.Unsat

let update_int (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env) (v: Cp__Var0.ti)
               (di: Cp__DomI.t) : unit =
  (Cp__Impl0.Hbi.Make.set (e.Cp__Type.domi) v di); e.Cp__Type.dirty <- true

let min (x: Z.t) (y: Z.t) : Z.t = if Z.leq x y then x else y

let max (x: Z.t) (y: Z.t) : Z.t = if Z.leq x y then y else x

let set_int (e: (Cp__DomI.t, Cp__DomB.t) Cp__Type.env) (v: Cp__Var0.ti)
            (di: Cp__DomI.t) : unit =
  let di2 = Cp__Type.get_int e v in
  let min2 = max di.Cp__DomI.min di2.Cp__DomI.min in
  let max2 = min di.Cp__DomI.max di2.Cp__DomI.max in
  if Z.leq min2 max2
  then
    if Z.equal min2 di2.Cp__DomI.min && Z.equal max2 di2.Cp__DomI.max
    then ()
    else
      begin
        let d = { Cp__DomI.min = min2; Cp__DomI.max = max2 } in
        (Cp__Impl0.Hbi.Make.set (e.Cp__Type.domi) v d);
        e.Cp__Type.dirty <- true end
  else raise Cp__Type.Unsat