Resolve "add horn sat algorithm"

Closes #5 (closed) Closes #4 (closed)

project1/bin/xor.ml

@@ -18,23 +18,38 @@ module Term : Dolmen_dimacs.Term
 
 end
 
+let positify (b,l) =
+  let one = ref b in
+  let rec aux = function
+    | [] -> []
+    | h::l -> 
+      if h<0 then begin
+        one := not !one;
+        (-h)::(aux l)
+      end else 
+        h::(aux l)
+  in 
+  let l = aux l in
+  !one,l
+  
+
 module Statement(Term : Dolmen_dimacs.Term with type t = int) : Dolmen_dimacs.Statement
   with type location =  Std.Loc.t
    and type term = Term.t
-   and type t = int list
+   and type t = bool * (int list) 
 = struct
 
   type location = Std.Loc.t
   type term = int
-  type t = int list
+  type t = bool * (int list) 
 
   let p_cnf ?loc _ _ =
     let _ = loc in
-    []
+    false,[]
 
   let clause ?loc l =
     let _ = loc in
-    l
+    positify (false,l)
 
 end
 
@@ -44,19 +59,20 @@ module S = Set.Make(struct type t = int let compare = compare end)
 
 let parse_file = fun x -> snd (M.parse_file x)
 
-let stmt_to_string = print_list (print_list string_of_int)
+let stmt_to_string = print_list (fun (b,l) -> "("^(string_of_bool b)^print_list string_of_int l^")")
 
-let flatten (l: int list list) =
-  let rec aux : int list list -> int list list = function
+let flatten (l : (bool * int list) list) =
+  let rec aux = function
     | [] ->    []
-    | []::l ->  []::(aux l)
+    | (n,[])::l ->  (n,[])::(aux l)
     | [l] ->   [l]
-    | [x]::l -> [x]::(aux l)
-    | (h::t)::l -> (
-        let not_t = List.map (fun x -> -x) t in
-        aux (List.map
-               (fun x -> List.flatten (List.map (fun x -> if x = h then not_t else [x]) x))
-               l)
+    | ((_,[_]) as clause)::l -> (positify clause)::(aux l)
+    | ((_,_::_) as clause)::l -> (
+        let (b,not_t) = positify clause in
+        let foo = aux (List.map
+               (fun (n,x) -> positify (n <> b,List.flatten (List.map (fun x -> if x = h then not_t else [x]) x)))
+               l) in
+        foo
       ) in
   aux l
 
@@ -72,19 +88,22 @@ let add_unsat_duplicate (trace : string list ref) (x : int) =
   let buffer = Buffer.create 100 in
   Buffer.add_string buffer "UNSAT\n Found duplicate variable :";
   Buffer.add_string buffer (string_of_int x);
-  trace := Buffer.contents buffer::!trace
+  trace := (Buffer.contents buffer)::!trace
 
 let process (statements: M.statement list) =
-
-  let trace : string list ref = ref [stmt_to_string statements] in
+  let statements = List.tl statements in
+  let trace : string list ref = ref ["Formula to test :"] in
+  trace := (stmt_to_string statements)::!trace;
   let l = flatten statements in
-  trace := (stmt_to_string l)::!trace;
+  trace := "Flattened formula :"::!trace;
+  trace :=(stmt_to_string l)::!trace;
 
+  (*TODO fix*)
   let rec aux seen (l : M.statement list): int list =
     add_state trace seen l;
     match l with
     | [] -> List.of_seq (S.to_seq seen)
-    | [ll] -> 
+    | [(b,ll)] -> 
       List.fold_left (fun seen x -> 
           if S.mem x seen then (
             add_unsat_duplicate trace x; failwith "unsat"
@@ -94,13 +113,16 @@ let process (statements: M.statement list) =
         ll
       |> S.to_seq
       |> List.of_seq
-    | []::_ -> trace := "Empty clause found, UNSAT"::!trace; failwith "unsat"
-    | [x]::t -> aux (S.add x seen) t
-    | (_::_)::_ -> failwith "the list is not flattened"
+    | (b,[])::l -> 
+        if b then begin
+          trace := "Empty clause found, UNSAT"::!trace; failwith "unsat"
+        end else aux seen l
+    | (b,[x])::t -> aux (S.add x seen) t
+    | (_,_::_)::_ -> failwith "the list is not flattened"
   in 
 
   try
     let model = aux S.empty l in
-    Ok(model,!trace)
+    Ok(model,List.rev !trace)
   with
-    _ -> Error !trace
+    _ -> Error (List.rev !trace)