From a7ae917b2f77eb29f8e269052ede873f8dd06b94 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 1 Dec 2015 17:04:04 +0100
Subject: [PATCH] =?UTF-8?q?Implement=20equality=20on=20(HC)=CE=BC/=CE=BD?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/lib/CoAlgFormula.ml | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index eee1f9e..5ce32b0 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1904,6 +1904,9 @@ let equal_hcFormula_node f1 f2 =
| HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
+ | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
+ | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
+ | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
(* The rest could be shortened to | _ -> false,
but then the compiler would not warn if the formula type is extended
and this function is not updated accordingly.*)
@@ -1928,7 +1931,10 @@ let equal_hcFormula_node f1 f2 =
| HCNORM _, _
| HCNORMN _, _
| HCCHC _, _
- | HCFUS _, _ -> false
+ | HCFUS _, _
+ | HCMU _, _
+ | HCNU _, _
+ | HCVAR _, _ -> false
(** Computes the hash value of a formula node.
@param f A formula node.
--
GitLab