let decompose e =
  let rec loop acc = function
    | [] -> acc
    | (a,b) :: el when Term.eq a b ->
        loop acc el
    | (a,b) :: el -> 
        let (acc',el') = 
          match d_conc a, d_conc b  with   
            | Some(n1,m1,x1,y1), Some(n2,m2,x2,y2) ->
                if n1 = n2 then
                  (acc, ((x1,x2) :: (y1,y2) :: el))
                else if n1 < n2 then
                  let (x21,x22) = cut n2 n1 x2 in
                  let e1 = (x1,x21) in
                  let e2 = (y1, mk_conc (n2-n1) m2 x22 y2) in
                  (acc, (e1 :: (e2 :: el)))
                else (* n1 > n2 *)
                  let (x11,x12) = cut n1 n2 x1 in
                  let e1 = (x11,x2) in
                  let e2 = (mk_conc (n1-n2) m1 x12 y1, y2) in
                  (acc, (e1 :: e2 :: el))
            | Some(n,m,x,y), None ->
                let e1 = (mk_sub (n+m) 0 (n-1) b, x) in
                let e2 = (mk_sub (n+m) n (n+m-1) b, y) in
                (acc, (e1 :: e2 :: el))
            | None, Some(n,m,x,y) ->
                let e1 = (mk_sub (n+m) 0 (n-1) a, x) in
                let e2 = (mk_sub (n+m) n (n+m-1) a, y) in
                (acc, (e1 :: e2 :: el))
            | None, None ->
                (((a, b) :: acc), el)
        in
        loop acc' el'
  in
  loop [] [e] 




(** Solving is based on the equation ite(x,p,n) = (p or n) and exists delta. x = (p and (n => delta)) *)



and solve_bitwise n (a,b) =
  assert(n >= 0);
  let s = mk_bwiff n a b in
  let rec triangular_solve s e =
    match d_bitwise s with
      | Some (_,x,pos,neg) ->
          if is_one pos && is_zero neg then          (* poslit *)
            (x, pos) :: e
          else if is_zero pos && is_one neg then     (* neglit *)
            (x, pos) :: e
          else
            let t' = mk_bwconj n pos (mk_bwimp n neg (mk_fresh n)) in
            let e' = (x,t') :: e in
            let s' = mk_bwdisj n pos neg in
            if is_zero s' then
              raise Exc.Inconsistent
            else if is_one s' then
              e'
            else if is_bitwise s' then
              triangular_solve s' e'
            else
              (s', mk_one n) :: e'
      | None ->
          (s, mk_one n) :: e
  in
  if is_zero s then
    raise Exc.Inconsistent
  else if is_one s then
    []
  else
    triangular_solve s []