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