(* MINES-PONTS 2000 *)
 

  let VMAX = 127 ;;

  type formule = | vrai
                 | faux 
                 | variable of int
                 | et       of formule * formule
                 | ou       of formule * formule
                 | implique of formule * formule
                 | non      of formule ;;
                  
  type  liste_de_formules == formule list ;;

  let liste_vide () = let l = [vrai] in tl(l) ;;

  let ajoute (f:formule) l =  f::l ;;
  
  let est_vide  l = l = tl[vrai] ;;
  
  let un_element (l:formule list) = match l with
         | [] -> failwith "Liste vide1"
         | t::q -> t ;;
  
  let reste  (l:formule list) = match l with
         | [] -> failwith "Liste vide2"
         | t::q -> q ;;
  
  type ensemble_de_formules =  
                              { V   : bool;
                                F   : bool; 
                                tbl : bool vect;
                                lf  : formule  list} ;;
            
 
  let ensemble_vide () = { V = false;
                           F = false; 
                           tbl = make_vect VMAX false;
                           lf = [] };;

  let que_des_variables e = e.lf=[] ;;
  
  let intersection e1 e2 = 
    let rec aux i = 
        if i = VMAX then false 
        else (e1.tbl.(i) && e2.tbl.(i)) || aux (i+1)
    in aux 0 ;;
    
  let ajouter_formule e f = match f with
       |       vrai  -> {V = true; F = e.F;  tbl = e.tbl; lf = e.lf}
       |       faux  -> {V = e.V ; F = true; tbl = e.tbl; lf = e.lf}
       | variable(i) -> let t = e.tbl in t.(i) <- true;
                        {V = e.V; F = e.F; tbl = t; lf = e.lf}
       |   _         -> {V = e.V; F = e.F; tbl = e.tbl; lf = ajoute f e.lf}
  ;;
            
  let formule_suivante e  =
    ({V = e.V; F = e.F; tbl = e.tbl; lf = reste e.lf}, un_element e.lf) ;;   
                            
  (*----------------------------------------------------------------------*)
 
  let rec verifier u v =
    if que_des_variables u && que_des_variables v
    then u.F || v.V || intersection u v 
    else if not (que_des_variables u) 
         then let (uu,f) = formule_suivante u in match f with
 
    | et(a,b) -> verifier (ajouter_formule (ajouter_formule uu a) b) v             
 
    | non a   -> let w = if que_des_variables  uu
                         then (* R1 *) ajouter_formule uu vrai 
                         else (* R2 *) uu                     
                 in verifier w (ajouter_formule v a) 
 
    | ou(a,b) -> (* R3 et R4 *)
                     verifier (ajouter_formule uu a) v
                  && verifier (ajouter_formule uu b) v               
 
    | implique(a,b) -> let w = if que_des_variables uu
                               then (* R5 *) ajouter_formule uu vrai
                               else (* R6 *) uu
                       in    verifier (ajouter_formule uu b) v 
                          && verifier w (ajouter_formule v a)  
    |  _  -> failwith "Erreur 1"

          else if not (que_des_variables v)
               then let (vv,g) = formule_suivante v in match g with

    | ou(a,b) -> verifier u (ajouter_formule (ajouter_formule vv a) b)            
 
    | non a   -> let w = if que_des_variables  vv
                         then (* R7 *) ajouter_formule vv faux
                         else (* R8 *) vv 
                 in verifier (ajouter_formule  u a) w
  
    | et(a,b) -> (* R9 et R10 *)
                     verifier u (ajouter_formule vv a)
                  && verifier u (ajouter_formule vv a)
 
    | implique(a,b) -> (* R11 et R12 *)
                       verifier(ajouter_formule u a)(ajouter_formule vv b)  
 
   |  _  -> failwith "Erreur 2"
    
           else failwith "Erreur 3" ;;    
 
  let tautologie f =
    verifier (ajouter_formule (ensemble_vide()) vrai)  
             (ajouter_formule (ensemble_vide()) f) ;;     
             

  let essai = implique(
                    implique(variable 1,implique(variable 2,variable 3)),
                    implique(implique(variable 1,variable 2),
                             implique(variable 1,variable 3)));;
                           
  tautologie essai;;