OPEN aST

LET PASBESOIN = REF FALSE

LET EST_DE_VALEUR_1 = REF []

LET EST_DE_VALEUR_0 = REF []

MODULE TYPE choice = SIG
  VAL CHOICE : aST.cNF.T -> aST.VAR
END

MODULE dEFAULTcHOICE = STRUCT
  LET CHOICE : aST.cNF.T -> aST.VAR = FUN CNF -> FAILWITH "TODO: CHOICE"
END

MODULE TYPE solver = SIG
  VAL SOLVE : aST.T -> aST.MODEL OPTION
END

LET EST_ELLE_VIDE C =
  IF aST.cLAUSE.IS_EMPTY C THEN (
    PRINT_ENDLINE "CLAUSE VIDE !";
    PASBESOIN := TRUE)

LET EST_UN_SINGLETON C =
  LET X = aST.cLAUSE.CHOOSE C IN
  LET D = aST.cLAUSE.REMOVE X C IN
  aST.cLAUSE.IS_EMPTY C

(*SI ON RENCONTRE UNE CLAUSE QUI EST UN SINGLETON, ON LA DÉGAGE ET ON AJOUTE SON SINGLETON*)

LET REC PRINT_LISTE L =
  MATCH L WITH
  | [] -> ()
  | Y :: Q ->
      PRINT_INT Y;
      PRINT_LISTE Q

LET SATISFAIRE_CLAUSES_SINGLETONS C P =
  IF EST_UN_SINGLETON C THEN
    LET X = aST.cLAUSE.CHOOSE C IN
    IF X > 0 THEN EST_DE_VALEUR_1 := X :: !EST_DE_VALEUR_1
    ELSE EST_DE_VALEUR_0 := X :: !EST_DE_VALEUR_0

(*
LET EMONDER_EN_CASCADE L  P =
   IF aST.cNF.IS_EMPTY P
    THEN (P, sOME !EST_DE_VALEUR_1)
    ELSE ((LET F Y = SATISFAIRE_CLAUSES_SINGLETONS Y !P0 IN aST.cNF.ITER (F) !P0 ; PRINT_STRING "LES LITTERAUX EN SINGLETONS POSITIFS SONT : " ;  PRINT_LISTE !EST_DE_VALEUR_1  ; PRINT_ENDLINE "" ; PRINT_STRING "LES LITTERAUX EN SINGLETONS NEGATIFS SONT : " ;  PRINT_LISTE !EST_DE_VALEUR_0  ; PRINT_ENDLINE "" ;  (*ON RECUPÈRE LES SINGLETONS*)
    LET REC AUX L = MATCH L WITH
        |[] -> !P0
        |Y :: Q -> PRINT_INT Y ; PRINT_ENDLINE " A ÉTÉ RETIRÉ" ; LET RETIRER_CERTAINES_CLAUSES C = IF aST.cLAUSE.MEM Y C
          THEN (P0 := aST.cNF.REMOVE C !P0)
          ELSE (IF aST.cLAUSE.MEM (-Y) C
                THEN (LET F Z = IF aST.cLAUSE.EQUAL Z C THEN (aST.cLAUSE.REMOVE (-Y) C) ELSE (Z) IN P0 := aST.cNF.MAP (F) !P0)
                ELSE ())
          IN aST.cNF.ITER (RETIRER_CERTAINES_CLAUSES) !P0 ;
        IN P0 := AUX (!EST_DE_VALEUR_1 @ !EST_DE_VALEUR_0) ; IF aST.cNF.IS_EMPTY !P0 THEN (sOME !EST_DE_VALEUR_1) ELSE ( aST.cNF.ITER (EST_ELLE_VIDE) !P0 ; IF !PASBESOIN THEN (PRINT_ENDLINE "TEST DU nONE" ; nONE) ELSE (nONE))))
*)

LET FONCTION_dpll : aST.T -> aST.MODEL OPTION =
 FUN P ->
  LET MODELE = REF [] IN
  LET P0 = REF P.CNF IN
  PASBESOIN := FALSE;
  aST.cNF.ITER EST_ELLE_VIDE !P0;
  IF !PASBESOIN THEN nONE (*IL YA UNE CLAUSE VIDE, DONC C'EST UNSAT *)
  ELSE IF aST.cNF.IS_EMPTY !P0 THEN sOME !MODELE
    (*SI IL N'Y A PLUS DE CLAUSES ALORS C'EST VRAI*)
  ELSE
    LET F Y = SATISFAIRE_CLAUSES_SINGLETONS Y !P0 IN
    aST.cNF.ITER F !P0;
    PRINT_STRING "LES LITTERAUX EN SINGLETONS POSITIFS SONT : ";
    PRINT_LISTE !EST_DE_VALEUR_1;
    PRINT_ENDLINE "";
    PRINT_STRING "LES LITTERAUX EN SINGLETONS NEGATIFS SONT : ";
    PRINT_LISTE !EST_DE_VALEUR_0;
    PRINT_ENDLINE "";
    (*ON RECUPÈRE LES SINGLETONS*)
    LET REC AUX L =
      MATCH L WITH
      | [] -> !P0
      | Y :: Q ->
          PRINT_INT Y;
          LET FLAG = REF FALSE IN
          PRINT_ENDLINE " A ÉTÉ RETIRÉ";
          LET RETIRER_CERTAINES_CLAUSES C =
            (*DÉFINITION D'UNE FONCTION QU'ON VA APPLIQUER À P0*)
            IF aST.cLAUSE.MEM Y C THEN P0 := aST.cNF.REMOVE C !P0
            ELSE IF aST.cLAUSE.MEM (-Y) C (*ICI Y N'EST PAS MEMBRE DE C*) THEN
              LET F Z =
                IF aST.cLAUSE.EQUAL Z C THEN
                  LET D = aST.cLAUSE.REMOVE (-Y) C IN
                  IF EST_UN_SINGLETON D THEN (
                    LET X0 = aST.cLAUSE.CHOOSE D IN
                    aST.cNF.REMOVE C !P0;
                    FLAG := TRUE)
                  ELSE D
                ELSE Z
              IN
              P0 := aST.cNF.MAP F !P0
          IN
          aST.cNF.ITER RETIRER_CERTAINES_CLAUSES !P0;
          IF !FLAG THEN AUX (X0 :: Q) ELSE AUX Q
    IN
    P0 := AUX (!EST_DE_VALEUR_1 @ !EST_DE_VALEUR_0);
    IF aST.cNF.IS_EMPTY !P0 THEN sOME !EST_DE_VALEUR_1
    ELSE (
      aST.cNF.ITER EST_ELLE_VIDE !P0;
      IF !PASBESOIN THEN (
        PRINT_ENDLINE "TEST DU nONE";
        nONE)
      ELSE nONE)

MODULE dpll (c : choice) : solver = STRUCT
  LET SOLVE : aST.T -> aST.MODEL OPTION = FONCTION_dpll
END