Resolve "add horn sat algorithm"

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

project1/bin/horn.ml

-let process clauses = Ok ([List.length clauses]) (*TODO*)
+open Printf
+open Dolmen
+open Lib
+
+(** A data structure to store horn clauses efficiently: *)
+
+(* Clauses are modeled by the number of disjoint false hypothesis and the conlusion *)
+(* and for every variable p, the list of clause where the variable p appear is maintained *)
+(* for example, p1 /\ p2 /\ p2 => p3 is modeled by the clause (2,p3) and the array [| [ref (2,p3)]; [ref (2,p3)]; [] |] *)
+
+(* When the number of false hypothesis of a clause reach zero, the conclusion is propagated: *)
+(* if a variable p is propagated, we can iter the corresponding list and decrease the number of false hypothesis for each clause where p appear *)
+(* if false is propagated, UNSAT has been reached *)
+(* if nothing can be propagated anymore, SAT has been reached *)
+
+module Term : Dolmen_dimacs.Term
+  with type location =  Std.Loc.t
+   and type t = int
+= struct
+
+  type location = Std.Loc.t
+  type t = int
+  let atom ?loc x = let _ = loc in x
+
+end
+
+type stat = Clause of int ref * int option | Vars of stat ref list array ref
+
+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 = stat
+= struct
+
+  type location = Std.Loc.t
+  type term = int
+  type t = stat
+  let vars = ref [||]
+
+  let p_cnf ?loc nb_var _ =
+    let _ = loc in
+    vars := Array.make (nb_var+1) [];
+    Vars vars
+
+  let clause ?loc l =
+
+    let _ = loc
+    and l = remove_duplicates l
+    and len = ref 0
+    and var = ref None in
+
+    List.iter (fun t -> if t < 0 then incr len else var := Some t) l;
+    let clause = Clause (len, !var) in
+    List.iter (fun t -> if t <0 then (!vars).(-t) <- (ref clause) :: (!vars).(-t)) l;
+    clause
+
+end
+
+module M = Dimacs.Make(Std.Loc)(Term)(Statement(Term))
+
+let parse_file = fun x -> snd (M.parse_file x)
+
+let sort_clauses = List.fast_sort ( 
+    fun c1 c2 -> match c1,c2 with
+      | Clause (n1,_), Clause (n2,_) -> compare !n1 !n2
+      | _ -> failwith "cannot happen"
+  )
+
+let to_propagate clauses =
+  match clauses with
+  | [] -> false
+  | Clause (n1,_) :: _ -> !n1 == 0
+  | _ -> failwith "cannot happen"
+
+let propagate vars assignement p =
+  if assignement.(p) == false then (
+    assignement.(p) <- true;
+    List.iter (
+      fun c -> match !c with
+        | Clause (n,_) -> decr n
+        | _ -> failwith "cannot happen"
+    ) vars.(p)
+  )
+
+let get_model assignement =
+  let n = Array.length assignement in
+  let model = ref [] in
+  for i = 1 to n - 1 do
+    let p = n - i in
+    if assignement.(p)
+    then model := p :: !model
+    else model := (- p) :: !model
+  done;
+  !model
+
+(* used for debugging *)
+let print_clauses = List.iter (
+    function
+    | Clause (n, Some p) -> printf "(nb: %d, var: %d) " !n p
+    | Clause (n, None) -> printf "(nb: %d, no var)" !n
+    | _ -> failwith "cannot happen"
+  )
+
+let process statements = match statements with
+  | Vars vars :: clauses ->
+
+    let vars = !vars
+    and clauses = ref clauses
+    and assignement = Array.make (Array.length !vars) false
+    and processing = ref true
+    and unsat = ref false
+    and trace = ref [] in
+
+    while !processing do
+      processing := false;
+      clauses := sort_clauses !clauses;
+
+      while to_propagate !clauses && not !unsat do
+        match !clauses with
+        | Clause (_, Some p) :: l -> (
+            processing := true;
+            clauses := l;
+            trace := ("propagating " ^ string_of_int p) :: !trace;
+            propagate vars assignement p
+          )
+        | Clause (_, None) :: _ -> (
+            trace := "propagating false" :: !trace;
+            unsat := true
+          )
+        | _ -> failwith "cannot happen"
+
+      done
+    done;
+
+    if !unsat then (
+      Error(List.rev !trace)
+    ) else (
+      Ok(get_model assignement, List.rev !trace)
+    )
+
+  | _ -> failwith "cannot happen"