Resolve "add horn sat algorithm"

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

project1/bin/xor.ml

@@ -125,22 +125,24 @@ let get_result trace (model : bool option array) (l : (bool * S.t) list) =
 
   let rec aux = function
 
-    | [] -> 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
+    | [] ->
+      trace := ("checking constraints "^(print_list (fun (x,(b,s)) -> (string_of_int x)^"<>"^(stmt_to_string [(b,s)])) !constraints))::!trace;
+      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
 
     | (true,  s)::l when S.cardinal s = 0 -> aux l
 
-    | [cl] -> resolve trace model cl
+    | [cl] -> resolve trace model cl && aux []
 
     | (false, s)::l when S.cardinal s = 1 ->
       let x = S.choose s in
@@ -167,16 +169,15 @@ let get_result trace (model : bool option array) (l : (bool * S.t) list) =
 
           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)
+              if contain x s2
+              then
+                let b3 = (b = 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
+                (b3, s5)
+              else
+                (b2, s2)
             ) l)
         | None -> resolve trace model (b, s) && aux l
       end