From 1ec1a764f4ebfd7c033fb09a9b4ddceef6f459a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Wed, 29 Jan 2014 02:39:34 +0100
Subject: [PATCH] Implement nnf printing
---
Makefile | 2 +-
coalg.ml | 18 +++++++++++++++++-
2 files changed, 18 insertions(+), 2 deletions(-)
diff --git a/Makefile b/Makefile
index d088200..8451350 100644
--- a/Makefile
+++ b/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.
diff --git a/coalg.ml b/coalg.ml
index 38904c4..745191d 100644
--- a/coalg.ml
+++ b/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 ()
--
GitLab