Cubicle 1.1.2 documentation and source : Enumsolver_types.enqueue

let enqueue_ident a =
  let values = a.var.ident.ivalues in
  Vec.push values (a, ((snd (Vec.last values)) land a.value));
  let l = ref [] in
  let ivars = a.var.ident.ivars in
  let lvl = a.var.level in
  for i = 0 to Vec.size ivars - 1 do
    let v = Vec.get ivars i in
    if v.level < 0 then
    match check_bottom_clause v.pa with
      | Some c ->
          l := (v.na, c, lvl) :: !l
      | None -> 
          match check_bottom_clause v.na
          with
            | Some c ->
                l := (v.pa, c, lvl) :: !l
            | None -> ()
  done;
  !l