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