From 87d5082f799ecdbcd10cf7974d562989a7dda999 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 4 Nov 2015 19:16:13 +0100
Subject: [PATCH] =?UTF-8?q?Add=20=CE=BC-constructors=20for=20hcFormula?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
CTL is assumed to be eliminated before the hash-consing step
---
src/lib/CoAlgFormula.ml | 6 ++++++
src/lib/CoAlgFormula.mli | 3 +++
2 files changed, 9 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 8b68635..422a926 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1644,6 +1644,9 @@ let const_fusion first f1 = FUS (first, f1)
(** Hash-consed formulae, which are in negation normal form,
such that structural and physical equality coincide.
+
+ Also CTL has been replaced by the equivalent μ-Calculus
+ constructs
*)
type hcFormula = (hcFormula_node, formula) HC.hash_consed
and hcFormula_node =
@@ -1669,6 +1672,9 @@ and hcFormula_node =
| HCNORMN of hcFormula * hcFormula
| HCCHC of hcFormula * hcFormula
| HCFUS of bool * hcFormula
+ | HCMU of string * hcFormula
+ | HCNU of string * hcFormula
+ | HCVAR of string
(** Determines whether two formula nodes are structurally equal.
@param f1 The first formula node.
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 3397ba4..c807b4e 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -155,6 +155,9 @@ and hcFormula_node =
| HCNORMN of hcFormula * hcFormula
| HCCHC of hcFormula * hcFormula
| HCFUS of bool * hcFormula
+ | HCMU of string * hcFormula
+ | HCNU of string * hcFormula
+ | HCVAR of string
module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
--
GitLab