Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

@@ -51,7 +51,7 @@ let parse_file = fun x -> snd (M.parse_file x)
 
 let string_of_set f s =
   let res = ref "" in
-  S.iter (fun x -> res := !res ^f x) s;
+  S.iter (fun x -> res := !res ^ " " ^ f x) s;
   !res
 
 let stmt_to_string =
@@ -80,13 +80,18 @@ let to_model arr =
 (* and add or remove 1 to the clause. *)
 let positify (b, s) =
   let b2 = ref b in
-  let s2 = S.map (
-      fun x ->
-        if x<0 then b2 := not !b2;
-        abs x
-    ) s
-  in
-  (!b2, s2)
+  let occ = Hashtbl.create (S.cardinal s) in
+  S.iter (
+    fun x ->
+      if x<0 then b2 := not !b2;
+      let x = abs x in
+      if Hashtbl.mem occ x
+      then Hashtbl.remove occ x
+      else Hashtbl.add occ (abs x) ();
+  ) s;
+  let s2 = ref S.empty in
+  Hashtbl.iter (fun x _ -> s2 := S.add x !s2) occ;
+  (!b2, !s2)
 
 (* We do as such:
    - add all singleton variables in the model represented as an array
@@ -98,7 +103,8 @@ let positify (b, s) =
 let intersect s =
   List.find_map (fun (_, s2) -> S.choose_opt (S.inter s s2))
 
-let resolve model (b, s) =
+let resolve trace model (b, s) =
+  trace := ("resolving "^(stmt_to_string [(b,s)]))::!trace;
   let b2 = ref b in
   let s2 = S.filter (fun x -> if model.(x) then (b2 := not !b2; false) else true) s in
   if !b2 then true
@@ -117,7 +123,7 @@ let get_result trace model (l : (bool * S.t) list) =
 
     | (true,  s)::l when S.cardinal s = 0 -> aux l
 
-    | [cl] -> resolve model cl
+    | [cl] -> resolve trace model cl
 
     | (false, s)::l when S.cardinal s = 1 ->
       let x = S.choose s in
@@ -125,7 +131,7 @@ let get_result trace model (l : (bool * S.t) list) =
       model.(x) <- true;
       aux l
 
-    | (false, s)::l when S.cardinal s = 1 ->
+    | (true, s)::l when S.cardinal s = 1 ->
       let x = S.choose s in
       trace := ("propagating "^(string_of_int x)^" to false in "^(stmt_to_string l))::!trace;
       aux (List.map (fun (b, s2) -> (b, S.remove x s2)) l)
@@ -140,7 +146,7 @@ let get_result trace model (l : (bool * S.t) list) =
                     ") in "^(stmt_to_string l))::!trace;
 
           aux (List.map (fun (b2, s2) -> positify (b <> b2, S.union s_x (S.remove x s2))) l)
-        | None -> resolve model (b, s) && aux l
+        | None -> resolve trace model (b, s) && aux l
       end
 
   in aux l
@@ -159,7 +165,7 @@ let process = function
        "\nPositified formula:\n"^(stmt_to_string s)) :: !trace;
 
     if get_result trace model s
-    then Ok(model |> to_model, !trace)
-    else Error(!trace)
+    then Ok(model |> to_model, List.rev !trace)
+    else Error(List.rev !trace)
 
   | _ -> failwith "cannot happen"