Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

@@ -81,30 +81,12 @@ let to_list arr =
 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
+    match arr.(i) with
+    | Some(true) -> res := i::!res
+    | _ -> res := (-i)::!res
   done;
   List.rev !res
 
-(* Replace every negative variable by it's negation *)
-(* and add or remove 1 to the clause. *)
-let positify (b, s) =
-  let b2 = ref b in
-  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
    - Once we reach the last big clause, we search through the clause, and we remove all occurences of known variable while flipping the bool each time
@@ -115,21 +97,44 @@ let positify (b, s) =
 let intersect s =
   List.find_map (fun (_, s2) -> S.choose_opt (S.inter s s2))
 
+let contain x s =
+  match S.find_opt x s with
+  | Some _ -> true
+  | None -> false
+
 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
+  let s2 = S.filter (
+      fun x -> match model.(x) with
+        | Some(true) ->
+          b2 := not !b2;
+          false
+        | Some(false) -> false
+        | None -> true) s in
   if !b2 then true
   else (
     match S.choose_opt s2 with
-    | Some(x) -> model.(x) <- true; true
+    | Some(x) -> model.(x) <- Some(true); true
     | None -> false
   )
 
-let get_result trace model (l : (bool * S.t) list) =
+let get_result trace (model : bool option array) (l : (bool * S.t) list) =
+
+  let constraints = ref [] in
 
   let rec aux = function
-    | [] -> true
+
+    | [] -> List.fold_left (fun acc (x, (b,c_x)) ->
+        acc && (
+          let count = S.cardinal (S.filter (fun x -> model.(x) = Some(true)) c_x) in
+          let value = b <> ((count mod 2) = 1) in
+          match model.(x) with
+          | Some(v) when v = value -> false
+          | None -> model.(x) <- Some(not value); true
+          | _ -> true
+        )
+      ) true !constraints
 
     | (false, s)::_ when S.cardinal s = 0 -> false
 
@@ -140,12 +145,13 @@ let get_result trace model (l : (bool * S.t) list) =
     | (false, s)::l when S.cardinal s = 1 ->
       let x = S.choose s in
       trace := ("propagating "^(string_of_int x)^" to true")::!trace;
-      model.(x) <- true;
+      model.(x) <- Some true;
       aux l
 
     | (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;
+      model.(x) <- Some false;
       aux (List.map (fun (b, s2) -> (b, S.remove x s2)) l)
 
     | (b, s)::l ->
@@ -157,7 +163,21 @@ let get_result trace model (l : (bool * S.t) list) =
                     ","^(string_of_set string_of_int s_x)^
                     ") in "^(stmt_to_string l))::!trace;
 
-          aux (List.map (fun (b2, s2) -> positify (b <> b2, S.union s_x (S.remove x s2))) l)
+          constraints := (x,(b,s_x)) :: !constraints;
+
+          aux (List.map (fun (b2, s2) ->
+
+              let b2 =
+                if contain x s2
+                then b = b2
+                else b2 in
+
+              let s3 = S.remove x s2 in
+              let s4 = S.inter s_x s3 in
+              let s5 = S.union (S.diff s3 s4) (S.diff s_x s4) in
+
+              (b2, s5)
+            ) l)
         | None -> resolve trace model (b, s) && aux l
       end
 
@@ -169,12 +189,11 @@ let process = function
 
     let nb_var = S.choose hd in
     let trace : string list ref = ref []
-    and s = List.map positify tl
-    and model = Array.make (nb_var+1) false in
+    and model = Array.make (nb_var+1) None in
 
     trace := ("Formula to test:\n"^(stmt_to_string tl))::!trace;
 
-    if get_result trace model s
+    if get_result trace model tl
     then Ok(model |> to_model, List.rev !trace)
     else Error(List.rev !trace)