Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

@@ -109,11 +109,11 @@ let flatten nb_var trace (l : (bool * int list) list) =
             (List.map
               (fun (n,x) -> 
                   positify nb_var
-                  ((if List.mem h x then b else false) <> n,
+                  ((if List.mem h x then not b else false) <> n,
                   List.flatten (List.map (fun x -> if x = h then 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))::!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;
         trace := "found:"::!trace;
         trace := (stmt_to_string foo)::!trace;
         foo