let rec compare a1 a2 = match a1, a2 with | True, True -> 0 | True, _ -> -1 | _, True -> 1 | False, False -> 0 | False, _ -> -1 | _, False -> 1 | Comp (x1, op1, y1), Comp (x2, op2, y2) -> let c1 = Term.compare x1 x2 in if c1 <> 0 then c1 else let c0 = Pervasives.compare op1 op2 in if c0 <> 0 then c0 else let c2 = Term.compare y1 y2 in c2 | Comp _, _ -> -1 | _, Comp _ -> 1 | Ite (sa1, a1, b1), Ite (sa2, a2, b2) -> let c = SAtom.compare sa1 sa2 in if c<>0 then c else let c = compare a1 a2 in if c<>0 then c else compare b1 b2