let rec add d s =
  Trace.msg "d" "Add" d Fact.pp_diseq;
  let (x,y,_) = Fact.d_diseq d in
  let xd = deq s x in
  let yd = deq s y in
  let xd' = Term.Set.add y xd in
  let yd' = Term.Set.add x yd in
  match xd == xd', yd == yd' with
    | true, true -> 
        (Term.Set.empty, s)
    | true, false ->
        Trace.msg "d" "Update" (x, y) Term.pp_diseq;
        (Term.Set.singleton y, Term.Map.add y yd' s)
    | false, true -> 
        Trace.msg "d" "Update" (x, y) Term.pp_diseq;
        (Term.Set.singleton x, Term.Map.add x xd' s)
    | false, false -> 
        Trace.msg "d" "Update" (x, y) Term.pp_diseq;
        let ch' = Term.Set.add x (Term.Set.singleton y) in
        let s' = Term.Map.add x xd' (Term.Map.add y yd' s) in
          (ch', s')