Resolve "add horn sat algorithm"

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

project1/bin/horn.ml

@@ -13,7 +13,9 @@ open Lib
 (* 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
+module Term : Dolmen_dimacs.Term
+  with type location =  Std.Loc.t
+   and type t = int
 = struct
 
   type location = Std.Loc.t
@@ -24,7 +26,10 @@ 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
+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
@@ -78,9 +83,13 @@ let propagate vars assignement p =
   )
 
 let get_model assignement =
+  let n = Array.length assignement in
   let model = ref [] in
-  for p = 1 to Array.length assignement - 1 do
-    if assignement.(p) then model := p :: !model
+  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
 
@@ -124,10 +133,8 @@ let process statements = match statements with
     done;
 
     if !unsat then (
-      trace := "UNSAT" :: !trace;
       Error(List.rev !trace)
     ) else (
-      trace := "SAT" :: !trace;
       Ok(get_model assignement, List.rev !trace)
     )