Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

@@ -91,17 +91,18 @@ let stmt_to_string = print_list (fun (b,l) -> "("^(string_of_bool b)^","^print_l
 let flatten nb_var trace (l : (bool * int list) list) =
   let _ = nb_var in 
   let rec aux = function
-    | [] ->    []
+    | [] ->         []
     | (n,[])::l ->  (n,[])::(aux l)
-    | [l] ->   [l]
+    | [l] ->        [l]
     | (b,[x])::l -> 
-      (*if x is a negative literal, then it's equivalent to -x xor 1, so we can substitute x for 0 in all instances of the rest of the xnf,
+      (*if x is a negative literal, then it's equivalent to x xor 1, so we can substitute x for 0 in all instances of the rest of the xnf,
         which is equivalent to removing x*)
-      if b then (b,[x])::(aux l) else
+      if not b then (b,[x])::(aux l) else (
+        trace := ("propagating "^(string_of_int x))::!trace;
         (b,[x])::(List.map
                     (fun (b,l) -> (b, List.filter (fun y -> x <> y) l))
                     (aux l))
-
+      )
     | (b,h::not_t)::l -> (
         let foo = aux
             (List.map
@@ -110,7 +111,7 @@ let flatten nb_var trace (l : (bool * int list) list) =
                   positify nb_var (n, List.flatten (List.map (fun x -> if x = h then (bb := b <> !bb; not_t) else [x]) x))
                )
                l) in
-        trace := ("substituting "^(string_of_int h)^" with "^"~("^(string_of_bool b)^","^print_list string_of_int not_t^") in "^(stmt_to_string l)^":\n"^(stmt_to_string foo))::!trace;
+        trace := ("substituting "^(string_of_int h)^" with "^"~("^(string_of_bool b)^","^print_list string_of_int not_t^") in "^(stmt_to_string l))::!trace;
         foo
       ) in
   aux l
@@ -148,44 +149,22 @@ let process (statements: M.statement list) =
     - if there's none, it's sat iff the bool is set to 1*)
 
   let model = Array.make (nb_var+1) false in
-  let rec aux = function
-    | [] -> (true,[])
-    | [b,t] ->
-      let fb = ref b in
-      let t = (List.filter
-                 (fun x ->
-                    if x<0 then
-                      failwith "wtf"
-                    else
-                    if model.(abs x) then begin
-                      fb := not !fb;
-                      false
-                    end else true
-                 ) t) in
-      (!fb,t)
-    | (false,[])::_ ->
-      trace := "Empty clause found"::!trace;
-      failwith "unsat"
-    | (true,[])::l ->
-      aux l
-    | (false,[x])::l ->
-      if x<0 then
-        failwith "something bad happened"
-      else
-        model.(x) <- true;
-      aux l
-    | (_,_::_)::_ ->
-      failwith "something bad happened"
 
+  let rec get_result = function
+    | [] -> true
+    | [(b,l)] ->
+      let bb = ref b in
+      let l = List.filter (fun x -> if model.(x) then (bb := not !bb; false) else true) l in
+      if !bb then true
+      else begin match l with
+        | [] -> false
+        | x::_ -> model.(x) <- true; true
+      end
+    | (false, [x])::l -> model.(x) <- true; get_result l
+    | (true, _)::l -> get_result l
+    | (false, [])::_ -> print_endline "haa"; false
+    | (_,h)::_ -> print_endline (print_list string_of_int h); failwith "cannot happen"
   in
-  try
-    match aux l2  with
-    | (true,[]) -> Ok(model |> to_model ,List.rev !trace)
-    | (false,[]) -> Error(List.rev !trace)
-    | (true,_::_) -> Ok(model |> to_model,List.rev !trace)
-    | (false,h::_) ->
-      model.(h) <- true;
-      Ok(model |> to_model, !trace)
-
-  with
-    _ -> Error (!trace)
+  if get_result l2
+  then Ok(model |> to_model, !trace)
+  else Error(!trace)