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,11 +83,13 @@ let propagate vars assignement p =
   )
 
 let get_model assignement =
-
-  print_string "aaearaez";
+  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
 
@@ -104,14 +111,10 @@ let process statements = match statements with
     and unsat = ref false
     and trace = ref [] in
 
-    print_clauses !clauses;
-
     while !processing do
       processing := false;
       clauses := sort_clauses !clauses;
 
-      print_clauses !clauses;
-
       while to_propagate !clauses && not !unsat do
         match !clauses with
         | Clause (_, Some p) :: l -> (
@@ -120,7 +123,6 @@ let process statements = match statements with
             trace := ("propagating " ^ string_of_int p) :: !trace;
             propagate vars assignement p
           )
-        (* UNSAT *)
         | Clause (_, None) :: _ -> (
             trace := "propagating false" :: !trace;
             unsat := true
@@ -131,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)
     )