Cubicle 1.1.2 documentation and source : Enumsolver_types.check_bottom

let check_bottom_clause a =
  let v = a.var.ident.ivalues in
  if not (is_bottom a) then None
  else begin
    assert (Vec.size v > 1);
    let size = ref 1 in
    let c = ref [a.neg] in
    (* eprintf "--check trail--@."; *)
    (* for i = 1 to Vec.size v - 1 do *)
    (*   eprintf "%a : %d@." Debug.atom (fst (Vec.get v i)) (snd (Vec.get v i)); *)
    (* done; *)
    (* eprintf "%a@." Debug.atom a; *)
    (* eprintf "---------------@."; *)

    for i = 1 to Vec.size v - 1 do
      let b = (fst (Vec.get v i)) in
      if b.var.level > 0 then begin
        c := b.neg :: !c;
        incr size
      end
    done;
    let cl = make_clause (fresh_ename ()) !c !size true [] in
    (* printf "check_bottom -> %a@." Debug.clause c; *)
    Some cl
  end