From ff4dc78690ef8573ca7f3d904f2037820b07637c Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 16 Nov 2015 23:29:34 +0100
Subject: [PATCH] =?UTF-8?q?implement=20nnf=20for=20=CE=BC-Calculus?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/lib/CoAlgFormula.ml | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 39e1ee6..b9e097d 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1004,6 +1004,7 @@ let rec nnfNeg f =
| TRUE -> FALSE
| FALSE -> TRUE
| AP _ -> NOT f
+ | VAR _ -> f
| NOT f1 -> nnf f1
| AT (s, f1) -> AT (s, nnfNeg f1)
| OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
@@ -1027,6 +1028,8 @@ let rec nnfNeg f =
| NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
| CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
+ | MU (s, f1) -> NU(s, nnfNeg f1)
+ | NU (s, f1) -> MU(s, nnfNeg f1)
| AF _
| EF _
| AG _
@@ -1048,7 +1051,8 @@ and nnf f =
| AP _
| NOT (AP _)
| CONST _
- | CONSTN _ -> f
+ | CONSTN _
+ | VAR _ -> f
| NOT f1 -> nnfNeg f1
| AT (s, f1) ->
let ft1 = nnf f1 in
@@ -1113,7 +1117,12 @@ and nnf f =
| FUS (first, f1) ->
let ft = nnf f1 in
if ft == f1 then f else FUS (first, ft)
-
+ | MU (s, f1) ->
+ let ft = nnf f1 in
+ if ft == f1 then f else MU (s, ft)
+ | NU (s, f1) ->
+ let ft = nnf f1 in
+ if ft == f1 then f else NU (s, ft)
| AF _
| EF _
| AG _
--
GitLab