Cubicle 1.1.2 documentation and source : Pre.make

let make_tau tr =
  let memo = ref [] in
  (fun x op y ->
  try 
    match find_assign memo tr x, find_assign memo tr y with
    | Single tx, Single ty -> Atom.Comp (tx, op, ty)
    | Single tx, Branch ls ->
       List.fold_right
	 (fun (ci, ti) f -> Atom.Ite(ci, Atom.Comp(tx, op, ti), f))
	 ls Atom.True
    | Branch ls, Single tx ->
       List.fold_right
	 (fun (ci, ti) f -> Atom.Ite(ci, Atom.Comp(ti, op, tx), f))
	 ls Atom.True
    | Branch ls1, Branch ls2 ->
       List.fold_right
	 (fun (ci, ti) f -> 
	  List.fold_right 
	    (fun (cj, tj) f ->
	     Atom.Ite(SAtom.union ci cj, Atom.Comp(ti, op, tj), f)) ls2 f)
	 ls1 Atom.True
  with Remove_lit_var _ -> Atom.True),
  (fun () -> memo := [])