From d58bba0fbda47b659b6e68e68f94e9c3696c7938 Mon Sep 17 00:00:00 2001
From: Dirk Pattinson <dirk.pattinson@anu.edu.au>
Date: Thu, 5 Feb 2015 13:07:21 +1100
Subject: [PATCH] Removed Negation Normal Form of Choice as Choice is Self-Dual
---
src/lib/CoAlgFormula.ml | 50 ++++++----------------------------------
src/lib/CoAlgFormula.mli | 2 --
src/lib/CoAlgLogics.ml | 2 +-
src/lib/CoAlgMisc.ml | 13 +++++++----
4 files changed, 16 insertions(+), 51 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 46b115d..371895e 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -56,8 +56,7 @@ type formula =
| ID of formula (* modality of the identity functor *)
| NORM of formula * formula (* default implication *)
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
- | CHC of formula * formula
- | CHCN of formula * formula
+ | CHC of formula * formula (* Choice is self-dual *)
| FUS of bool * formula
exception ConversionException of formula
@@ -105,8 +104,7 @@ let rec sizeFormula f =
| NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
| CONST _
| CONSTN _ -> 1
- | CHC (f1, f2)
- | CHCN (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
+ | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
| FUS (_, f1) -> succ (sizeFormula f1)
(** Determines the size of a sorted formula.
@@ -135,7 +133,7 @@ let rec iter func formula =
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
| ID(a) -> proc a
| NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
- | CHC (a,b) | CHCN (a,b) -> (proc a ; proc b)
+ | CHC (a,b) -> (proc a ; proc b)
| FUS (_,a) -> proc a
let rec convert_post func formula = (* run over all subformulas in post order *)
@@ -168,7 +166,6 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
| NORM(a, b) -> NORM(c a, c b)
| NORMN(a, b) -> NORMN(c a, c b)
| CHC (a,b) -> CHC (c a, c b)
- | CHCN (a,b) -> CHCN (c a, c b)
| FUS (s,a) -> FUS (s, c a)) in
func formula
@@ -183,7 +180,7 @@ let convertToK formula = (* tries to convert a formula to a pure K formula *)
| AND _ | OR _
| AP _ | NOT _
| AX _ | EX _
- | CHC _ | CHCN _ | FUS _ -> formula
+ | CHC _ | FUS _ -> formula
| _ -> raise (ConversionException formula)
in
convert_post helper formula
@@ -196,7 +193,7 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula *
| EQU _ | IMP _
| AND _ | OR _
| AP _ | NOT _
- | CHC _ | CHCN _ | FUS _ -> formula
+ | CHC _ | FUS _ -> formula
| AX (r,a) -> MAXEXCEPT (0,r,a)
| EX (r,a) -> MORETHAN (0,r,a)
| _ -> raise (ConversionException formula)
@@ -348,12 +345,6 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb s
| CONSTN s -> Buffer.add_string sb "~=";
Buffer.add_string sb s
- | CHCN (f1, f2) ->
- Buffer.add_string sb "~(";
- exportFormula_buffer sb (negate f1);
- Buffer.add_string sb " + ";
- exportFormula_buffer sb (negate f2);
- Buffer.add_string sb ")"
| FUS (first, f1) ->
Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
prio 4 f1
@@ -437,7 +428,6 @@ let rec exportTatlFormula_buffer sb f =
| CONST _
| CONSTN _
| CHC _
- | CHCN _
| ATLEASTPROB _
| LESSPROBFAIL _
| ID _
@@ -871,8 +861,7 @@ let rec nnfNeg f =
| ID (f1) -> ID (nnfNeg f1)
| NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
| NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
- | CHC (f1, f2) -> CHCN (nnfNeg f1, nnfNeg f2)
- | CHCN (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
+ | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
(** Converts a formula to negation normal form
@@ -951,10 +940,6 @@ and nnf f =
let ft1 = nnf f1 in
let ft2 = nnf f2 in
if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
- | CHCN (f1, f2) ->
- let ft1 = nnf f1 in
- let ft2 = nnf f2 in
- if ft1 == f1 && ft2 == f2 then f else CHCN (ft1, ft2)
| FUS (first, f1) ->
let ft = nnf f1 in
if ft == f1 then f else FUS (first, ft)
@@ -1121,17 +1106,6 @@ let rec simplify f =
if (f1 == ft1) && (f2 == ft2) then f
else CHC (ft1, ft2)
end
- | CHCN (f1, f2) ->
- let ft1 = simplify f1 in
- let ft2 = simplify f2 in
- begin
- match ft1, ft2 with
- | TRUE, TRUE -> TRUE
- | FALSE, FALSE -> FALSE
- | _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
- else CHCN (ft1, ft2)
- end
| FUS (first, f1) ->
let ft = simplify f1 in
begin
@@ -1582,7 +1556,6 @@ and hcFormula_node =
| HCNORM of hcFormula * hcFormula
| HCNORMN of hcFormula * hcFormula
| HCCHC of hcFormula * hcFormula
- | HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
(** Determines whether two formula nodes are structurally equal.
@@ -1615,7 +1588,6 @@ let equal_hcFormula_node f1 f2 =
| HCID f1, HCID f2 -> f1 == f2
| HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
- | HCCHCN (f1a, f1b), HCCHCN (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
(* The rest could be shortened to | _ -> false,
but then the compiler would not warn if the formula type is extended
@@ -1641,7 +1613,6 @@ let equal_hcFormula_node f1 f2 =
| HCNORM _, _
| HCNORMN _, _
| HCCHC _, _
- | HCCHCN _, _
| HCFUS _, _ -> false
(** Computes the hash value of a formula node.
@@ -1665,7 +1636,6 @@ let hash_hcFormula_node f =
| HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
| HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
| HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
- | HCCHCN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 12
| HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
| HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
| HCALLOWS (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
@@ -1702,7 +1672,6 @@ let toFml_hcFormula_node f =
| HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
- | HCCHCN (f1, f2) -> CHCN (f1.HC.fml, f2.HC.fml)
| HCFUS (first, f1) -> FUS (first, f1.HC.fml)
(** Determines the negation (in negation normal form) of a formula node.
@@ -1731,8 +1700,7 @@ let negNde_hcFormula_node f =
| HCID (f1) -> HCID(f1.HC.neg)
| HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
- | HCCHC (f1, f2) -> HCCHCN (f1.HC.neg, f2.HC.neg)
- | HCCHCN (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
+ | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
(** An instantiation of hash-consing for formulae.
@@ -1817,10 +1785,6 @@ let rec hc_formula hcF f =
let tf1 = hc_formula hcF f1 in
let tf2 = hc_formula hcF f2 in
HcFormula.hashcons hcF (HCCHC (tf1, tf2))
- | CHCN (f1, f2) ->
- let tf1 = hc_formula hcF f1 in
- let tf2 = hc_formula hcF f2 in
- HcFormula.hashcons hcF (HCCHCN (tf1, tf2))
| FUS (first, f1) ->
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCFUS (first, tf1))
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 3acba52..3c70e1d 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -40,7 +40,6 @@ type formula =
| NORM of formula * formula (* default implication *)
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
| CHC of formula * formula
- | CHCN of formula * formula
| FUS of bool * formula
exception ConversionException of formula
@@ -146,7 +145,6 @@ and hcFormula_node =
| HCNORM of hcFormula * hcFormula
| HCNORMN of hcFormula * hcFormula
| HCCHC of hcFormula * hcFormula
- | HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 8cdc64f..c7f4a37 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -375,7 +375,7 @@ let mkRule_Const colors sort bs sl : stateExpander =
let allneg = List.length colors = List.length neg in
let twopos = List.length pos > 1 in
let rules = if (clash || allneg || twopos)
- then [( (fun x -> bs), lazylistFromList [] )] (* no backjumping *)
+ then [((fun x -> bs), lazylistFromList [])] (* no backjumping *)
else []
in
lazylistFromList rules
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 783b8ee..33added 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -330,8 +330,13 @@ let queueIsEmpty () =
let queueInsertState state = queueStates := state::!queueStates
+(* original version: breadth-first *)
let queueInsertCore core = queueCores2 := core::!queueCores2
+(* experiment: depth first
+let queueInsertCore core = queueCores1 := core::!queueCores1
+*)
+
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
let queueGetElement () =
@@ -847,8 +852,7 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1;
detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2
- | C.HCCHC (f1, f2)
- | C.HCCHCN (f1, f2) ->
+ | C.HCCHC (f1, f2) ->
if func <> Choice || List.length sortlst <> 2 then
raise (C.CoAlgException "Choice formula is used in wrong sort.")
else ();
@@ -989,7 +993,7 @@ let initTables nomTbl hcF htF htR s f n =
(* idea: hash identifier names *)
| C.HCID (f1) ->
!arrayType.(s).(n) <- IdF;
- !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
| C.HCNORM (f1, f2) ->
!arrayType.(s).(n) <- NormF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
@@ -999,8 +1003,7 @@ let initTables nomTbl hcF htF htR s f n =
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
!arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
(* note that choice is self-dual *)
- | C.HCCHC (f1, f2)
- | C.HCCHCN (f1, f2) ->
+ | C.HCCHC (f1, f2) ->
!arrayType.(s).(n) <- ChcF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
!arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
--
GitLab