Resolve "add horn sat algorithm"

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

project1/lib/lib.ml

@@ -63,6 +63,58 @@ let print_list print l =
   Buffer.contents buffer
 
 (** naive XOR to cnf formula conversion **)
+type formula = Neg of formula
+             | Or of formula * formula
+             | And of formula * formula
+             | Var of int
+             | Xor of formula * formula
+
+let rec remove_xor form = match form with
+  | Xor (a, b) -> And (Or (a,b), Or (Neg a, Neg b))
+  | Or (a,b) -> Or (remove_xor a, remove_xor b)
+  | And (a,b) -> And (remove_xor a, remove_xor b)
+  | _ -> form
+
+let rec to_cnf = function
+  | Neg (Var i) -> Var (-i)
+  | Neg (And (a,b)) -> to_cnf (Or(to_cnf (Neg a), to_cnf (Neg b)))
+  | Neg (Or (a,b)) -> And(to_cnf (Neg a), to_cnf (Neg b))
+  | Or (And (a,b), c) -> And (to_cnf (Or (a,c)), to_cnf (Or(b,c)))
+  | Or (c,And (a,b)) -> And (to_cnf (Or (a,c)), to_cnf (Or(b,c)))
+  | And (a,b) -> And (to_cnf a, to_cnf b)
+  | Or (a,b) -> to_cnf (Or (to_cnf a, to_cnf b))
+  | Var i -> Var i
+  | _ -> failwith "cannot happen"
+
+let cnf_to_int_list form =
+  let res = ref [] in
+
+  let rec clause c = function
+    | Or (a,b) ->
+      clause c a;
+      clause c b
+    | Var i ->
+      c :=  i :: !c
+    | _ -> failwith "cannot happen"
+  in
+
+  let rec conjonction = function
+    | And (a,b) ->
+      conjonction a;
+      conjonction b
+    | Or (a,b) ->
+      let c = ref [] in
+      clause c a;
+      clause c b;
+      res := !c :: !res
+    | Var i ->
+      res := [i] :: !res
+    | _ -> failwith "cannot happen"
+  in
+
+  conjonction form;
+  !res
+
 module Term : Dolmen_dimacs.Term
   with type location =  Std.Loc.t
    and type t = int
@@ -77,23 +129,33 @@ end
 module Statement(Term : Dolmen_dimacs.Term with type t = int) : Dolmen_dimacs.Statement
   with type location =  Std.Loc.t
    and type term = Term.t
-   and type t = int list
+   and type t = int list list
 = struct
 
   type location = Std.Loc.t
   type term = int
-  type t = int list
+  type t = int list list
 
   let p_cnf ?loc nb_var nb_clause =
     let _ = loc in
-    [nb_var; nb_clause]
+    [[nb_var; nb_clause]]
 
   let clause ?loc l =
     let _ = loc in
-    l
+    cnf_to_int_list (to_cnf (List.fold_left (fun form x -> Xor (form,Var x)) (Var (List.hd l)) (List.tl l)))
 
 end
 
 module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
 
-module S = Set.Make(struct type t = int let compare = compare end)
+let convert_xorsat file =
+  match snd (M.parse_file file) with
+  | [[nb_var; nb_clause]] :: statements ->
+    let oc = open_out "conversion.cnf" in
+    Printf.fprintf oc "p cnf %d %d\n" nb_var nb_clause;
+    List.iter (fun clause ->
+        List.iter (fun x -> Printf.fprintf oc "%d " x) clause;
+        Printf.fprintf oc "\n"
+      ) (List.concat statements);
+    close_out oc
+  | _ -> failwith "cannot happen"