Implement nnf printing

Makefile

@@ -50,7 +50,7 @@ LDXX ?= g++
 OCAMLC := ocamlc.opt
 OCAMLCFLAGS := -I `ocamlfind query ocamlgraph`
 OCAMLOPT := ocamlopt.opt
-OCAMLOPTFLAGS := -cc $(LDXX) -unsafe -inline 100 -I `ocamlfind query ocamlgraph`
+OCAMLOPTFLAGS := -cc $(LDXX) -ccopt -static -unsafe -inline 100 -I `ocamlfind query ocamlgraph`
 
 # No more user input beyond this point.
 

coalg.ml

@@ -37,7 +37,7 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 
 let printUsage () =
   print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
-  print_endline "       <task> in { sat print prov (is »not.(sat ¬f)«) }";
+  print_endline "       <task> in { sat print nnf prov (is »not.(sat ¬f)«) }";
   print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic GML";
   print_endline "                      (or: K)     (or: KD)     (or: CL)       }";
   print_endline "       <flags> = a list of the following items";
@@ -113,6 +113,7 @@ let choiceProvable () =
         else ()
       done
     with End_of_file -> ()
+
 let choicePrint () =
     try
       while true do
@@ -127,6 +128,20 @@ let choicePrint () =
       done
     with End_of_file -> ()
 
+let choiceNNF () =
+    try
+      while true do
+        let input = read_line () in
+        if not (GenAndComp.isEmptyString input) then
+          let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
+          let str = CoAlgFormula.exportFormula f in
+          incr counter;
+          print_string (str ^ "\n");
+          flush stdout;
+        else ()
+      done
+    with End_of_file -> ()
+
 let rec parseFlags arr offs : unit =
     let offs = ref (offs) in
     let getParam () =
@@ -157,6 +172,7 @@ let _ =
     | "sat" -> choiceSat ()
     | "prov" -> choiceProvable ()
     | "print" -> choicePrint ()
+    | "nnf" -> choiceNNF ()
     | _ -> printUsage ()