From 508e3c33ea80958101e7e5cfb80d603147812adc Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 6 Nov 2015 22:38:11 +0100
Subject: [PATCH] Add pattern-matching for hcFormula where obvious
Add all obvious cases for hcFormula
---
src/lib/CoAlgFormula.ml | 15 ++++++++++++++-
1 file changed, 14 insertions(+), 1 deletion(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 63e59e9..edf5ba9 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1783,7 +1783,8 @@ let hash_hcFormula_node f =
| HCTRUE -> 0
| HCFALSE -> 1
| HCAP s
- | HCNOT s -> base * Hashtbl.hash s + 1
+ | HCNOT s
+ | HCVAR s -> base * Hashtbl.hash s + 1
| HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
| HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
| HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
@@ -1802,6 +1803,8 @@ let hash_hcFormula_node f =
| HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
| HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
| HCID (f1) -> base * f1.HC.hkey + 20
+ | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
+ | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
(** Determines the "real" formula of a formula node.
@param f A formula node.
@@ -1812,6 +1815,7 @@ let toFml_hcFormula_node f =
| HCTRUE -> TRUE
| HCFALSE -> FALSE
| HCAP s -> AP s
+ | HCVAR s -> VAR s
| HCNOT s -> NOT (AP s)
| HCAT (s, f1) -> AT (s, f1.HC.fml)
| HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
@@ -1831,6 +1835,8 @@ let toFml_hcFormula_node f =
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
| HCFUS (first, f1) -> FUS (first, f1.HC.fml)
+ | HCMU (var, f1) -> MU (var, f1.HC.fml)
+ | HCNU (var, f1) -> NU (var, f1.HC.fml)
(** Determines the negation (in negation normal form) of a formula node.
@param f A formula node.
@@ -1885,6 +1891,7 @@ let rec hc_formula hcF f =
| TRUE -> HcFormula.hashcons hcF HCTRUE
| FALSE -> HcFormula.hashcons hcF HCFALSE
| AP s -> HcFormula.hashcons hcF (HCAP s)
+ | VAR s -> HcFormula.hashcons hcF (HCVAR s)
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
| AT (s, f1) ->
let tf1 = hc_formula hcF f1 in
@@ -1946,6 +1953,12 @@ let rec hc_formula hcF f =
| FUS (first, f1) ->
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCFUS (first, tf1))
+ | MU (var, f1) ->
+ let tf1 = hc_formula hcF f1 in
+ HcFormula.hashcons hcF (HCMU (var, tf1))
+ | NU (var, f1) ->
+ let tf1 = hc_formula hcF f1 in
+ HcFormula.hashcons hcF (HCNU (var, tf1))
| AF _
| EF _
| AG _
--
GitLab