From f828ad2ff2ad43a30768f20b3f1a44e2f33a92a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Thu, 30 Jan 2014 15:41:38 +0100
Subject: [PATCH] Close the subformula closure by negation
---
CoAlgMisc.ml | 24 +++++++++++++++---------
1 file changed, 15 insertions(+), 9 deletions(-)
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index 30f92b0..3d9c964 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -710,14 +710,18 @@ let ppFormulae nomTbl tbox (s, f) =
raise (C.CoAlgException "Number of sorts must be positive.")
else ();
let nnfAndSimplify f = C.simplify (C.nnf f) in
- let f1 = nnfAndSimplify f in
- let tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
-
- let hcF = C.HcFormula.create true in
- let hcf = C.hc_formula hcF f1 in
- let hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) tbox1 in
+ let f1 = nnfAndSimplify f in
+ let nf1 = nnfAndSimplify (C.NOT f) in
+ let tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
+ let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
+
+ let hcF = C.HcFormula.create true in
+ let hcf = C.hc_formula hcF f1 in
+ let nhcf = C.hc_formula hcF nf1 in
+ let hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) tbox1 in
+ let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
let hcfalse = C.hc_formula hcF C.FALSE in
- let hctrue = C.hc_formula hcF C.TRUE in
+ let hctrue = C.hc_formula hcF C.TRUE in
let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
let atset = C.HcFHt.create 64 in
@@ -726,8 +730,10 @@ let ppFormulae nomTbl tbox (s, f) =
detClosure nomTbl hcF fset atset nomset i hcfalse;
detClosure nomTbl hcF fset atset nomset i hctrue;
done;
- detClosure nomTbl hcF fset atset nomset s hcf;
- List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox;
+ detClosure nomTbl hcF fset atset nomset s hcf;
+ detClosure nomTbl hcF fset atset nomset s nhcf;
+ List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox;
+ List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox;
Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
--
GitLab