module BDDType
  use mach.peano.Peano
  use mach.int.Int63

  type bdd =
    | Bottom
    | Top
    | N int63 bdd bdd Peano.t (* N (var, true_branch, false_branch, id) *)

  type affectation = int63 -> bool

  (* Test whenever provided bdd has a node as root *)
  let predicate is_node (input : bdd) : bool =
    match input with
      | Bottom | Top -> false
      | N _ _ _ _ -> true
    end

  (* Test whenever provided bdd is a leaf *)
  let predicate is_leaf (input : bdd) : bool = not (is_node input)

  (* Return the `true_branch` of provided bdd *)
  let function true_branch (input : bdd) : bdd =
    requires { is_node input }
    match input with
      | N _ branch _ _ -> branch
      | _ -> absurd
    end

  (* Return the `false_branch` of provided bdd *)
  let function false_branch (input : bdd) : bdd =
    requires { is_node input }
    match input with
      | N _ _ branch _ -> branch
      | _ -> absurd
    end

  (* Return the id of variable of provided bdd *)
  let function var (input : bdd) : int63 =
    requires { is_node input }
    match input with
      | N var_id _ _ _ -> var_id
      | _ -> absurd
    end

  (* Return the id of provided bdd *)
  let function id (input : bdd) : Peano.t =
    match input with
      | Bottom -> Peano.zero
      | Top -> Peano.one
      | N _ _ _ node_id -> node_id
    end

  (* Equality of rank 0 *)
  let predicate eq0 (t1 : bdd) (t2 : bdd) : bool =
    eq (id t1) (id t2)

  (* Equality of rank 1 *)
  let predicate eq1 (t1 : bdd) (t2 : bdd) : bool =
    match t1, t2 with
      | Top, Top | Bottom, Bottom -> True
      | N var_1 true_1 false_1 _, N var_2 true_2 false_2 _ ->
          var_1 = var_2 && eq0 true_1 true_2 && eq0 false_1 false_2
      | _ -> False
    end

  (* Tuple equality over the BDD *)
  let predicate tuple_eq0 (t1 t2 : (bdd, bdd)) : bool =
    let l1, r1 = t1 in
    let l2, r2 = t2 in
    eq0 l1 l2 && eq0 r1 r2

  (* Value of a BDD with a given affectation *)
  let rec function value (f : affectation) (input : bdd) : bool =
    variant { input }
    match input with
      | Top -> True
      | Bottom -> False
      | N var_id true_b false_b _ ->
           if f var_id then value f true_b else value f false_b
    end

  (* Convert a Boolean to its corresponding leaf *)
  let bool_to_leaf (b : bool) : bdd = if b then Top else Bottom
    ensures { forall f : affectation. value f result = b }
    ensures { is_leaf result }

end

module Hashtbl
  use map.Map

  type key

  val predicate eq key key : bool

  type t 'a = abstract {
    mutable contents: map key 'a ;
    mutable domain: map key bool
  }
  invariant {
    (      (* All similar key have the same status in the table's domain *)
      forall u v : key. eq u v -> domain u = domain v
    ) /\ ( (* If two key are similar and one is in the table,
              they map to the same value *)
      forall u v : key. eq u v /\ domain u ->
          Map.([]) contents u =  Map.([]) contents v
    )
  }
  by { contents = (fun _ -> any 'a) ; domain = (fun _ -> false) }

  function is_in (h: t 'a) (k: key) : bool =
    h.domain k

  function val_of (h : t 'a) (k : key) : 'a = Map.([]) h.contents k

  val create (_u : unit) : t 'a
   ensures { forall k : key. is_in result k = false }

  val put (h: t 'a) (k: key) (v: 'a) : unit
    writes { h }
    ensures { forall k' : key. eq k k' -> is_in h k' /\ val_of h k' = v }
    ensures { forall k' : key. not eq k k' -> val_of h k' = val_of (old h) k'
                /\ is_in h k' = is_in (old h) k' }

  exception NotFound

  val find (h: t 'a) (k: key) : 'a
    ensures { is_in h k /\ val_of h k = result }
    raises  { NotFound -> not is_in h k }

  val mem (h: t 'a) (k: key) : bool
    ensures { result = is_in h k }
end

module HashConsingHashtbl
  use BDDType
  clone export Hashtbl with type key = bdd, val eq = eq1
end

module BDDAssociationMap
  use BDDType
  clone export Hashtbl with type key = bdd, val eq = eq0
end

module BDDTupleAssociationMap
  use BDDType

  clone export Hashtbl with type key = (bdd, bdd), val eq = tuple_eq0
end

module BDD
  use int.Int
  use mach.peano.Peano
  use mach.int.Int63
  use export BDDType

  use HashConsingHashtbl as HCMap

  (* A value is mem_tbl in the table if it is in the table and it is
     linked to itself *)
  predicate mem_tbl (tbl : HCMap.t bdd) (k : bdd) =
    HCMap.is_in tbl k /\ HCMap.val_of tbl k = k

  (* A value is well-formed (ie a ROBDD) if its mem_tbl in the hash-consign
     table or it's a leaf *)
  predicate well_formed (tbl : HCMap.t bdd) (k : bdd) =
    is_leaf k \/ mem_tbl tbl k

  type hctable = { tbl : HCMap.t bdd; mutable next_id : Peano.t }

  (* Top and Bottom are not in the Table *)
  invariant { not HCMap.is_in tbl Top /\ not HCMap.is_in tbl Bottom }

  (* Each BDD mem_tbl in table is Ordered [True Branch] *)
  invariant { forall u : bdd. mem_tbl tbl u -> is_node (true_branch u) ->
                var u < var (true_branch u) }

  (* Each BDD mem_tbl in table is Ordered [False Branch] *)
  invariant { forall u : bdd. mem_tbl tbl u -> is_node (false_branch u) ->
                var u < var (false_branch u) }

  (* No BDD mem_tbl in table has the same branch twice *)
  invariant { forall u : bdd. mem_tbl tbl u -> true_branch u <> false_branch u }

  (* Each BDD in the domain is in the same equivalence-class of eq1 to its
     associated value *)
  invariant { forall u : bdd. HCMap.is_in tbl u -> eq1 u (HCMap.val_of tbl u) }

  (* Each BDD mem_tbl in table has a unique id *)
  invariant { forall u v : bdd. mem_tbl tbl u /\ mem_tbl tbl v /\ u <> v ->
                (id u).v <> (id v).v }

  (* Each BDD mem_tbl in table has a id lower than next_id *)
  invariant { forall u : bdd. mem_tbl tbl u -> (id u).v < next_id.v }

  (* Transitivity of true_branch for the BDD mem_tbl in table *)
  invariant { forall u : bdd. mem_tbl tbl u ->
                well_formed tbl (true_branch u) }

  (* Transitivity of false_branch for the BDD mem_tbl in table *)
  invariant { forall u : bdd. mem_tbl tbl u ->
                well_formed tbl (false_branch u) }

  (* Next_id begin at 2 *)
  invariant { next_id >= 2 }

  (* Each BDD mem_tbl in table have an id greater than 2 *)
  invariant { forall u : bdd. mem_tbl tbl u -> id u >= 2 }

  by { tbl = HCMap.create (); next_id = Peano.succ Peano.one }

  (* Each BDD is now uniquily present in the table *)
  lemma bdd_is_unique :
    forall hc : hctable, u v : bdd. mem_tbl hc.tbl u /\ mem_tbl hc.tbl v ->
        var u = var v -> true_branch u = true_branch v ->
          false_branch u = false_branch v ->
            u = v

  (* All BDD well-formed in the 'old_hc' Hash-consign table are still
     well-formed in the newer one *)
  predicate still_well_formed (old_hc new_hc : hctable) =
    forall u : bdd. well_formed old_hc.tbl u -> well_formed new_hc.tbl u

  (* With the hash-consign, for well-formed BDD, eq1 is the same as the
     logical equality *)
  lemma eq1_match_logic :
    forall hc : hctable, u v : bdd. well_formed hc.tbl u ->
      well_formed hc.tbl v -> u = v <-> eq1 u v

  (* With the hash-consign, for well-formed BDD, eq0 is the same as the
     logical equality *)
  lemma eq0_match_logic :
    forall hc : hctable, u v : bdd. well_formed hc.tbl u ->
      well_formed hc.tbl v -> u = v <-> eq0 u v

  (* Create an empty hctable *)
  let create_hctable () : hctable =
    { tbl = HCMap.create () ; next_id = Peano.succ Peano.one }

  (* From two bdd and a variable, we create a new BDD in the table *)
  let create_node (hc : hctable) (v : int63) (t : bdd) (f : bdd) : bdd =
    (* If t is a node, var t > v *)
    requires { is_node t -> var t > v }

    (* If f is a node, var f > v *)
    requires { is_node f -> var f > v }

    (* t is well-formed in the hash-consign table *)
    requires { well_formed hc.tbl t }

    (* f is well-formed in the hash-consign table *)
    requires { well_formed hc.tbl f }

    (* The old well-formed bdd are still well-formed *)
    ensures { still_well_formed (old hc) hc }

    (* All well-formed BDD in the current hash-consign table where well-formed
       in the old hash-consign table or they are the result *)
    ensures { forall u : bdd. u <> result ->
                well_formed (old hc).tbl u = well_formed hc.tbl u }

    (* The result is well-formed *)
    ensures { well_formed hc.tbl result }

    (* If t <> f, var result = v *)
    ensures { t <> f -> var result = v }

    (* If t = f and is_node t, var result = var t *)
    ensures { t = f -> is_node t -> var t = var result }

    (* If result is a node, var result <= v *)
    ensures { is_node result -> var result >= v }

    (* Interpretation of a ROBDD *)
    ensures { forall a : affectation.
                value a result = if a v then value a t else value a f }

    (* result was either well_formed in the old hash-table and the next_id
       hasn't change or result have as id the old next_id *)
    ensures { well_formed (old hc).tbl result /\ hc.next_id = old hc.next_id \/
                id result = (old hc).next_id = hc.next_id - 1 }

    if eq0 t f then
      t
    else
      let bdd_candidate = N v t f Peano.zero in
      try
        HCMap.find hc.tbl bdd_candidate
      with HCMap.NotFound ->
        let new_node = N v t f hc.next_id in
        HCMap.put hc.tbl bdd_candidate new_node;
        hc.next_id <- Peano.succ hc.next_id;
        new_node
      end
end

module Not
  use BDD
  use int.Int
  use BDDAssociationMap as MemoMap

  (* Test if 'not_bdd' is the correct value of the 'orig_bdd' bdd by the
     not operation *)
  predicate is_not_bdd (not_bdd : bdd) (orig_bdd : bdd) =
    forall f : affectation. value f not_bdd = not value f orig_bdd

  type memoMap = { hc : hctable; m : MemoMap.t bdd }

  (* Top and Bottom are not in the memoisation table *)
  invariant { not MemoMap.is_in m Top /\ not MemoMap.is_in m Bottom }

  (* All BDD in the Memoisation Table are in the HashConsign Table *)
  invariant { forall u : bdd. MemoMap.is_in m u -> id u < hc.next_id }

  (* All BDD in the Memoisation Table have their value in the
     HashConsign Table *)
  invariant { forall u : bdd. MemoMap.is_in m u ->
                well_formed hc.tbl (MemoMap.val_of m u) }

  (* All values are images of the not operation of their key *)
  invariant { forall u : bdd. mem_tbl hc.tbl u -> MemoMap.is_in m u ->
                is_not_bdd (MemoMap.val_of m u) u }

  (* The variable of the keys are <= than the variable of the value *)
  invariant { forall u : bdd. mem_tbl hc.tbl u ->
                MemoMap.is_in m u ->
                  is_node (MemoMap.val_of m u) ->
                    var u <= var (MemoMap.val_of m u) }

  by { hc = create_hctable (); m = MemoMap.create () }

  let init_memo_map (hc : hctable) : memoMap =
    { hc = hc ; m = MemoMap.create () }

  (* Memoised unary operation *)
  let rec apply (map : memoMap) (b : bdd) : bdd =
    (* The input BDD must be well-formed. *)
    requires { well_formed map.hc.tbl b }

    (* The result is well-formed *)
    ensures { well_formed map.hc.tbl result }

    (* If the input is a node, then it is in the table *)
    ensures { is_node b -> MemoMap.is_in map.m b }

    (* If the input is a node, then its associated value in the table is
       the result *)
    ensures { is_node b -> MemoMap.val_of map.m b = result }

    (* If the result is a node, then the input must be a node and var result
       is >= than var b *)
    ensures { is_node result -> var b <= var result /\ is_node b }

    (* All the old well-formed bdd in map.hc are still well-formed in map.hc *)
    ensures { still_well_formed (old map.hc) map.hc }

    (* All old BDD in the table are concerved and their value too *)
    ensures { forall u : bdd. MemoMap.is_in (old map).m u ->
                MemoMap.is_in map.m u /\
                  MemoMap.val_of (old map).m u = MemoMap.val_of map.m u }

    (* No changes have been made to the memo_table if the input is a leaf *)
    ensures { is_leaf b -> forall u : bdd.
                MemoMap.is_in (old map).m u = MemoMap.is_in map.m u }

    (* The result is the result of the not operation *)
    ensures { is_not_bdd result b }

    (*  The next_id of the hash-consign table can only increase *)
    ensures { map.hc.next_id >= (old map).hc.next_id }

    variant { b }
    match b with
      | Bottom -> Top
      | Top -> Bottom
      | _ ->
        try
          MemoMap.find map.m b
        with MemoMap.NotFound ->
            let new_tb = apply map (true_branch b) in
            let new_fb = apply map (false_branch b) in
            let new_value = create_node map.hc (var b) new_tb new_fb
            in
            MemoMap.put map.m b new_value;
            new_value
        end
    end
end

module Size
  use BDD
  use int.Int
  use mach.peano.Peano
  use set.Fset
  use ref.Ref
  use BDDAssociationMap as HashMap

  (* Subnodes of b *)
  function subnodes (b : bdd) : fset bdd =
    match b with
      | Top | Bottom -> empty
      | N _ true_bdd false_bdd _ ->
              add b (union (subnodes true_bdd) (subnodes false_bdd))
    end

  (* If the true branch of a node u is a node,
     then it is in the subnodes of u *)
  lemma true_branch_in_sub_nodes:
    forall u : bdd. is_node u /\ is_node (true_branch u) ->
      mem (true_branch u) (subnodes u)

  (* If the false branch of a node u is a node,
     then it is in the subnodes of u *)
  lemma false_branch_in_sub_nodes:
    forall u : bdd. is_node u /\ is_node (false_branch u) ->
      mem (false_branch u) (subnodes u)

  (* If u is a subnode of v and true_branch u is a node,
     then true_branch u is a subnode of v *)
  lemma sub_nodes_with_true_branch:
    forall u v [@induction] : bdd. mem u (subnodes v) ->
      is_node (true_branch u) -> mem (true_branch u) (subnodes v)

  (* If u is a subnode of v and false_branch u is a node,
     then false_branch u is a subnode of v *)
  lemma sub_nodes_with_false_branch:
    forall u v [@induction] : bdd. mem u (subnodes v) ->
      is_node (false_branch u) -> mem (false_branch u) (subnodes v)

  (* u is in its subnodes *)
  lemma bdd_in_their_subnodes:
    forall u : bdd. is_node u -> mem u (subnodes u)

  (* All the variable of b are in [0; n [ *)
  predicate var_bounded_bdd (n : int) (b : bdd) =
    forall u : bdd. mem u (subnodes b) -> n > var u >= 0

  (* Top and Bottom are not in the subnodes of any bdd *)
  let rec lemma top_bottom_not_in_subnodes (b : bdd) =
    ensures { not mem Top (subnodes b) }
    ensures { not mem Bottom (subnodes b) }
    match b with
      | Top | Bottom -> ()
      | N _ t f _ -> top_bottom_not_in_subnodes t; top_bottom_not_in_subnodes f
    end

  (* Compute the number of Nodes in a well-formed BDD *)
  let size (ghost hc : hctable) (in_bdd : bdd) : Peano.t =
    (* in_bdd is well-formed *)
    requires { well_formed hc.tbl in_bdd }

    (* The result is the cardinal of the subnodes of in_bdd *)
    ensures { result = cardinal (subnodes in_bdd) }

    let m = HashMap.create () in
    let ghost ref s = empty in
    let ref cpt = Peano.zero in

    let rec loop (b : bdd) =
      (* b is a well-formed bdd *)
      requires { mem_tbl hc.tbl b }

      (* b must be a subnode of in_bdd *)
      requires { mem b (subnodes in_bdd) }

      (* The hash-table m has the same domain as the ghost set s *)
      requires { forall u : bdd. mem u s <->
                  mem_tbl hc.tbl u /\ HashMap.is_in m u }

      (* cpt is the cardinal of the ghost set s *)
      requires { cpt = cardinal s }

      (* All the nodes in the ghost set s are subnodes of in_bdd *)
      requires { forall u : bdd. mem u s -> mem u (subnodes in_bdd) }

      (* The hash-table m still has the same domain as the ghost set s *)
      ensures { forall u : bdd. mem u s <->
                  mem_tbl hc.tbl u /\ HashMap.is_in m u }

      (* All the subnodes of b are now in the ghost set s *)
      ensures { forall u : bdd. mem u (subnodes b) -> mem u s }

      (* cpt is still the cardinal of the ghost set s *)
      ensures { cpt = cardinal s }

      (* The ghost set s is only getting bigger *)
      ensures { forall u : bdd. mem u (old s) -> mem u s }

      (* The ghost set s is contained in the subnodes of in_bdd *)
      ensures { forall u : bdd. mem u s -> mem u (subnodes in_bdd) }

      variant { b }
      if not HashMap.mem m b then (
        cpt <- Peano.succ cpt;
        HashMap.put m b ();
        s <- Fset.add b s
      );
      if is_node (true_branch b) then
        loop (true_branch b);
      if is_node (false_branch b) then
        loop (false_branch b)
    in
    if is_node in_bdd then
      loop in_bdd;
    assert { s == subnodes in_bdd };
    cpt
end

module BinOp
  use BDD
  use int.Int
  use mach.int.Int63
  use int.MinMax
  use BDDTupleAssociationMap as MemoMap

  (* Binary boolean function to customise *)
  val function bool_op (b1 b2 : bool) : bool

  (* Test if 'res' is the correct value of the 'left' and 'right'
     bdd by the bool operation *)
  predicate is_result (res left right : bdd) =
    forall f : affectation. value f res = bool_op (value f left) (value f right)

  type memoMap = { hc : hctable; m : MemoMap.t bdd }

  (* Top and Bottom are not in the memoisation table *)
  invariant { not MemoMap.is_in m (Top, Top)       /\
              not MemoMap.is_in m (Bottom, Top)    /\
              not MemoMap.is_in m (Bottom, Bottom) /\
              not MemoMap.is_in m (Top, Bottom) }

  (* All BDD in the Memoisation Table have their value in the
     HashConsign Table *)
  invariant { forall u v : bdd. MemoMap.is_in m (u, v) ->
                well_formed hc.tbl (MemoMap.val_of m (u, v)) }

  (* All values are images of the not operation of their key *)
  invariant { forall u v : bdd. well_formed hc.tbl u ->
                well_formed hc.tbl v -> MemoMap.is_in m (u, v) ->
                  is_result (MemoMap.val_of m (u, v)) u v }

  (* The variable of the keys are <= than the variable of the value (if the value is a node) *)
  invariant { forall u v : bdd. well_formed hc.tbl u -> well_formed hc.tbl v -> MemoMap.is_in m (u, v)
                                    -> is_node (MemoMap.val_of m (u, v)) -> is_node u -> is_leaf v
                                           -> var u <= var (MemoMap.val_of m (u, v)) }

  invariant { forall u v : bdd. well_formed hc.tbl u -> well_formed hc.tbl v -> MemoMap.is_in m (u, v)
                                    -> is_node (MemoMap.val_of m (u, v)) -> is_leaf u -> is_node v
                                           -> var v <= var (MemoMap.val_of m (u, v)) }

  invariant { forall u v : bdd. well_formed hc.tbl u -> well_formed hc.tbl v -> MemoMap.is_in m (u, v)
                                    -> is_node (MemoMap.val_of m (u, v)) -> is_node u -> is_node v
                                           -> min (var u) (var v) <= var (MemoMap.val_of m (u, v)) }

  (* The bdd in the keys have their id < than the next id of the hash-consign table *)
  invariant { forall u v : bdd. MemoMap.is_in m (u, v) -> id u < hc.next_id /\ id v < hc.next_id }

  by { hc = create_hctable (); m = MemoMap.create () }

  let init_memo_map (hc : hctable) : memoMap =
    { hc = hc ; m = MemoMap.create () }

  (* Memoised binary operation *)
  let rec apply (map : memoMap) (l r : bdd) : bdd =
    (* Input BDDs must be well-formed. *)
    requires { well_formed map.hc.tbl l /\ well_formed map.hc.tbl r }

    (* The result is well-formed *)
    ensures { well_formed map.hc.tbl result }

    (* If the result is a node, then one of the input bdd is a node *)
    ensures { not is_node result \/ is_node l \/ is_node r }

    (* If one of the input bdd is a node, then the tuple is in the table *)
    ensures { is_node l \/ is_node r -> MemoMap.is_in map.m (l, r) }

    (* If the tuple is in the table, then its associated value in the table is the result *)
    ensures { is_node l \/ is_node r -> MemoMap.val_of map.m (l, r) = result }

    (* If the result if a node and the l is the only node of the input, then the var_id of the result is >= than var_id l *)
    ensures { is_node result -> is_node l -> is_leaf r -> var l <= var result }

    (* If the result if a node and the r is the only node of the input, then the var_id of the result is >= than var_id r *)
    ensures { is_node result -> is_leaf l -> is_node r -> var r <= var result }

    (* If the result if a node and (l, r) are two nodes, then the var_id of the result is >= than min of the var of r and l *)
    ensures { is_node result -> is_node l -> is_node r -> min (var l) (var r) <= var result }

    (* All the old well-formed bdd in map.hc are still well-formed in map.hc *)
    ensures { still_well_formed (old map.hc) map.hc }

    (* All old BDD in the table are concerved and their value too *)
    ensures { forall u : (bdd, bdd). MemoMap.is_in (old map).m u -> MemoMap.is_in map.m u /\ MemoMap.val_of (old map).m u = MemoMap.val_of map.m u }

    (* No changes have been made to the memo_table if the input is a tuple of leaves *)
    ensures { is_leaf l /\ is_leaf r -> forall u : (bdd, bdd). MemoMap.is_in (old map).m u = MemoMap.is_in map.m u }

    (* The result is the result of the bool operation *)
    ensures { is_result result l r }

    variant { l, r }
    if is_leaf l && is_leaf r then
      match l, r with
        | Top,    Top    -> bool_to_leaf (bool_op true true)
        | Top,    Bottom -> bool_to_leaf (bool_op true false)
        | Bottom, Top    -> bool_to_leaf (bool_op false true)
        | Bottom, Bottom -> bool_to_leaf (bool_op false false)
        | _ -> absurd
      end
    else
        try
          MemoMap.find map.m (l, r)
        with MemoMap.NotFound ->
          let result =
            match (is_leaf l, is_leaf r) with
              | True , True  -> (* is_leaf l /\ is_leaf r *)
                  absurd
              | True , False -> (* is_leaf l /\ is_node r *)
                  create_node map.hc (var r)
                                     (apply map l (true_branch r))
                                     (apply map l (false_branch r))
              | False, True  -> (* is_node l /\ is_leaf r *)
                  create_node map.hc (var l)
                                     (apply map (true_branch l) r)
                                     (apply map (false_branch l) r)
              | False, False -> (* is_node l /\ is_node r *)
                  if var l = var r then
                    (* same variable for l and r *)
                    create_node map.hc (var l)
                                       (apply map (true_branch l) (true_branch r))
                                       (apply map (false_branch l) (false_branch r))
                  else if var l > var r then
                    (* var l comme after var r *)
                    create_node map.hc (var r)
                                       (apply map l (true_branch r))
                                       (apply map l (false_branch r))
                  else
                    (* var r comme after var l *)
                    create_node map.hc (var l)
                                       (apply map (true_branch l) r)
                                       (apply map (false_branch l) r)
            end
          in
          MemoMap.put map.m (l, r) result;
          result
        end
end

module And
  let function bool_op (a b : bool) : bool = a && b
  clone export BinOp with val bool_op = bool_op
end

module Or
  let function bool_op (a b : bool) : bool = a || b
  clone export BinOp with val bool_op = bool_op
end

module Implies
  let function bool_op (a b : bool) : bool = not a || b
  clone export BinOp with val bool_op = bool_op
end

module Sat
  use BDD
  use Size
  use seq.Seq
  use set.Fset
  use mach.int.Int63
  use int.Int

  let rec lemma value_match (hc : hctable) (u v : affectation) (b : bdd) =
    requires { well_formed hc.tbl b }
    requires { is_node b -> forall y : int63. y >= var b -> u y  = v y }
    ensures { value u b = value v b }
    variant  { b }
    if is_leaf b then ()
    else
      if u (var b) then
        value_match hc u v (true_branch b)
      else
        value_match hc u v (false_branch b)

  predicate sat (b : bdd) =
    exists f : affectation. value f b = True

  lemma top_is_sat:
    sat Top
    by value (fun _ -> False) Top = True

  let rec lemma nodes_are_sat (hc : hctable) (b : bdd) : affectation =
    requires { mem_tbl hc.tbl b }
    ensures {
    value result b = True }
    variant { b }
    match b with
      | N v Bottom f _ ->
          match f with
            | Top -> (fun _ -> False)
            | Bottom -> absurd
            | N _ _ _ _ ->  let u = nodes_are_sat hc f in (fun x -> if x = v then False else u x)
          end
      | N v t _ _ ->
          match t with
            | Top -> (fun _ -> True)
            | Bottom -> absurd
            | N _ _ _ _ -> let u = nodes_are_sat hc t in (fun x -> if x = v then True else u x)
          end
      | _ -> absurd
    end

  let predicate is_sat (ghost hc : hctable) (b : bdd) =
    requires { well_formed hc.tbl b }
    ensures { result <-> sat b }
    match b with
      | Bottom -> False
      | Top | N _ _ _ _ -> True
    end
end

module AnySat
  use BDD
  use Size
  use Sat
  use mach.int.Int63
  use int.Int
  use seq.Seq
  use set.Fset
  use mach.array.Array63

  (* Predicate to get the value of a BDD with an array *)
  let rec ghost predicate array_value (sol : array bool) (b : bdd) =
    requires { var_bounded_bdd sol.length b }
    variant { b }
    match b with
      | Top -> True
      | Bottom -> False
      | N v t f _ -> if sol[v] then array_value sol t else array_value sol f
    end

  let rec lemma array_value_same_eval (b : bdd) (sol : array bool) (affect : affectation) =
    requires { var_bounded_bdd sol.length b }
    requires { forall x : int63. 0 <= x < sol.length -> sol[x] = affect x }
    ensures { array_value sol b <-> value affect b }
    variant { b }
    match b with
      | Top | Bottom -> ()
      | N v t f _ -> if sol[v] then array_value_same_eval t sol affect else array_value_same_eval f sol affect
    end

  (* Give an affectation for each var in [0; n[ that satisfy the bdd. *)
  let any_sat (ghost hc : hctable) (n : int63) (b : bdd) : array bool =
    (* Well-formed bdd *)
    requires { well_formed hc.tbl b }

    (* All the variable are in [0; n [ *)
    requires { var_bounded_bdd n b }

    (* n >=0 *)
    requires { n >= 0 }

    (* If b is sat, the result is an affectation that satisfy the bdd *)
    ensures { sat b -> array_value result b = True }

    let sol = Array63.make n False in
    let rec _loop (u : bdd) =
      (* Well-formed BDD *)
      requires { well_formed hc.tbl u }

      (* All the variable are in [0; n [ *)
      requires { var_bounded_bdd n u }

      (* u is a subnodes of b or u is Top *)
      requires { u = Top \/ mem u (subnodes b) }

      (* All the cell between (var u) and n are set to False
         (No modification of the array is this range has been made) *)
      requires { forall x : int. is_node u -> n > x >= var u -> sol[x] = False }

      (* This build a correct affectation that satisfy u *)
      ensures { array_value sol u }

      (* If u is a node, all the modification before our variable are kept *)
      ensures { forall x : int63. is_node u -> 0 <= x < var u -> (old sol)[x] = sol[x] }

      (* We do not modify the array if u = Top *)
      ensures { u = Top -> old sol = sol }

      variant { u }
      match u with
        | Top -> ()
        | Bottom -> absurd
        | N v t Bottom _ -> sol[v] <- True; _loop t
        | N _ _ f _ -> _loop f
      end
    in
    if is_node b then _loop b;
    sol
end

module CountSat
  use BDD
  use Size
  use mach.int.Int63
  use set.Fset
  use seq.Seq
  use int.Int
  use int.Power

  (* Predicate to get the value of a BDD with a sequence *)
  let rec ghost predicate seq_value (sol : seq bool) (b : bdd) =
    requires { var_bounded_bdd sol.length b }
    variant { b }
    match b with
      | Top -> True
      | Bottom -> False
      | N v t f _ -> if sol[Int63.to_int v] then seq_value sol t else seq_value sol f
    end

  (* seq_value and value give the same output for similar affectation *)
  let rec lemma array_value_same_eval (b : bdd) (sol : seq bool) (affect : affectation) =
    requires { var_bounded_bdd sol.length b }
    requires { forall x : int63. 0 <= x < sol.length -> sol[x] = affect x }
    ensures { seq_value sol b <-> value affect b }
    variant { b }
    match b with
      | Top | Bottom -> ()
      | N v t f _ -> if sol[Int63.to_int v] then array_value_same_eval t sol affect else array_value_same_eval f sol affect
    end

  (* build all the interpretation satifying a BDD *)
  let rec function all_sat (ghost hc : hctable) (nb_var : int63) (v_id : int63) (ghost a : seq bool) (b : bdd) : (card : int, ghost set : fset (seq bool)) =
    (* v_id is in [0; nb_var] *)
    requires { nb_var >= v_id >= 0 }

    (* All variable are < than nb_var *)
    requires { var_bounded_bdd nb_var b }

    (* b is well-formed *)
    requires { well_formed hc.tbl b }

    (* If b is a node, var b >= v_id *)
    requires { is_node b -> v_id <= var b }

    (* a is of length max_var *)
    requires { a.length = nb_var }

    (* The size of all the sequences in the result is max_var - v_id *)
    ensures { forall u : seq bool. mem u set -> u.length = nb_var }

    (* All sequences in the result satisfies b *)
    ensures { forall u : seq bool. mem u set -> seq_value u b = True }

    (* All sequences have the same begining as a *)
    ensures { forall u : seq bool. mem u set -> forall i : int. 0 <= i < v_id -> a[i] = u[i] }

    (* If u is a sequences satifying b then u is in result *)
    ensures { forall u : seq bool. u.length = nb_var -> seq_value u b = True -> (forall i : int. 0 <= i < v_id -> a[i] = u[i]) -> mem u set }

    (* card is tha cardinal of the set built *)
    ensures { card = cardinal set }

    (* If b is Bottom, no affectation can satisfy it *)
    ensures { b = Bottom -> set = Fset.empty /\ card = 0 }

    (* If b is top, there is 2^(nb_var - v_id) affectation satisfying it (which begining is False) *)
    ensures { b = Top -> card = power 2 (nb_var - v_id) }

    variant { nb_var - v_id }
    match b with
      | Bottom -> let ghost res = Fset.empty in 0, res
      | Top ->
          if nb_var = v_id then
            let ghost res = Fset.singleton a in
            1, res
          else
            let b_true = set a (Int63.to_int v_id) True in
            let b_false = set a (Int63.to_int v_id) False in
            let true_card, true_set = all_sat hc nb_var (v_id + 1) b_true b in
            let false_card, false_set = all_sat hc nb_var (v_id + 1) b_false b in
            assert { Fset.disjoint true_set false_set };
            assert { true_card = false_card };
            let ghost res = Fset.union true_set false_set in
            true_card + false_card, res
      | N v t f _ ->
          let b_true = set a (Int63.to_int v_id) True in
          let b_false = set a (Int63.to_int v_id) False in
          if v = v_id then
            let true_card, true_set = all_sat hc nb_var (v_id + 1) b_true t in
            let false_card, false_set = all_sat hc nb_var (v_id + 1) b_false f in
            assert { Fset.disjoint true_set false_set };
            let ghost res = Fset.union true_set false_set in
            true_card + false_card, res
          else
            let true_card, true_set = all_sat hc nb_var (v_id + 1) b_true b in
            let false_card, false_set = all_sat hc nb_var (v_id + 1) b_false b in
            assert { Fset.disjoint true_set false_set };
            let ghost res = Fset.union true_set false_set in
            true_card + false_card, res
    end

  let function count_sat (ghost hc : hctable) (nb_var : int63) (b : bdd) : (card : int, ghost set : fset (seq bool)) =
    (* v_id is in [0; nb_var] *)
    requires { nb_var >= 0 }

    (* All variable are < than nb_var *)
    requires { var_bounded_bdd nb_var b }

    (* b is well-formed *)
    requires { well_formed hc.tbl b }

    (* If u is a sequences satifying b then u is in result *)
    ensures { forall u : seq bool. u.length = nb_var /\ seq_value u b = True <-> mem u set }

    (* card is tha cardinal of the set built *)
    ensures { card = cardinal set }

    all_sat hc nb_var 0 (Seq.create (Int63.to_int nb_var) (fun _ -> False)) b

end