Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

@@ -26,13 +26,22 @@ module Term : Dolmen_dimacs.Term
 
 end
 
-let to_model arr = 
+let to_list arr = 
   let res = ref [] in
   for i = 0 to Array.length arr - 1 do
     if arr.(i) then res := i::!res
   done;
   !res
 
+let to_model arr = 
+  let res = ref [] in
+  for i = 1 to Array.length arr - 1 do
+    if arr.(i) then 
+      res := i::!res
+    else
+      res := (-i)::!res
+  done;
+  List.rev !res
 
 (* Replace every negative variable by it's negation *)
 (* and add or remove 1 to the clause. *)
@@ -50,7 +59,7 @@ let positify nb_var (b,l) =
       aux l
   in 
   aux l;
-  (!one, to_model seen)
+  (!one, to_list seen)
 
 
 module Statement(Term : Dolmen_dimacs.Term with type t = int) : Dolmen_dimacs.Statement
@@ -100,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 b then n else if List.mem h x then not n else 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