Resolve "add horn sat algorithm"

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

project1/bin/horn.ml

@@ -78,8 +78,6 @@ let propagate vars assignement p =
   )
 
 let get_model assignement =
-
-  print_string "aaearaez";
   let model = ref [] in
   for p = 1 to Array.length assignement - 1 do
     if assignement.(p) then model := p :: !model
@@ -104,14 +102,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 +114,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