Require Import bdds.
Require Import List.

Definition Z_of_N (node : ad) :=
  match node with
  | N0 ⇒ 0%Z
  | Npos p ⇒ Zpos p
  end.

Definition test (be : bool_expr) :=
  match BDDof_bool_expr initBDDconfig initBDDneg_memo initBDDor_memo be with
  | ((bs, (share, counter)), (ad, _)) ⇒ (Z_of_N counter, Z_of_N ad)
  end.

Fixpoint testl (bel : list bool_expr) : list Z :=
  match bel with
  | nil ⇒ nil
  | be :: bel' ⇒
      match test be with
      | (counter, _) ⇒ counter :: testl bel'
      end
  end.

Definition Xor (be1 be2 : bool_expr) := Neg (Iff be1 be2).
Fixpoint Ands (bel : list bool_expr) : bool_expr :=
  match bel with
  | nil ⇒ One
  | be :: rest ⇒ match rest with
                  | nil ⇒ be
                  | _ ⇒ ANd be (Ands rest)
                  end
  end.
Fixpoint Ors (bel : list bool_expr) : bool_expr :=
  match bel with
  | nil ⇒ Zero
  | be :: rest ⇒ match rest with
                  | nil ⇒ be
                  | _ ⇒ Or be (Ors rest)
                  end
  end.
Fixpoint Iffs (bel : list bool_expr) : bool_expr :=
  match bel with
  | nil ⇒ One
  | be :: rest ⇒ match rest with
                  | nil ⇒ be
                  | _ ⇒ Iff be (Iffs rest)
                  end
  end.
Fixpoint even_len (l : list bool_expr) : bool :=
  match l with
  | nil ⇒ true
  | _ :: l' ⇒ negb (even_len l')
  end.
Definition Xors (bel : list bool_expr) :=
  (if even_len bel then Neg else fun be : bool_expr ⇒ be) (Iffs bel).