From eff3ff0cd8cfb6d6b92733ae7ae724fc012c82f9 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 10 May 2016 03:07:10 +0200
Subject: [PATCH] =?UTF-8?q?make=20HashConsing=20accept=20=C2=ACVar=20?=
=?UTF-8?q?=E2=89=A1=20Var?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/lib/HashConsing.ml | 15 +++++++++++----
1 file changed, 11 insertions(+), 4 deletions(-)
diff --git a/src/lib/HashConsing.ml b/src/lib/HashConsing.ml
index a7e88de..6b75c0b 100644
--- a/src/lib/HashConsing.ml
+++ b/src/lib/HashConsing.ml
@@ -208,11 +208,18 @@ module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
let ndeN = H.negNde nde in
let hkeyN = realhash ndeN in
let fmlN = H.toFml ndeN in
- let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
- nd.neg <- ndN;
let idxN = hkeyN mod ds in
- data.(idxN) <- ndN :: data.(idxN);
- hc.size <- osize + 2;
+ let bucketN = data.(idxN) in
+ try begin
+ find ndeN bucketN;
+ hc.size <- succ osize;
+ end
+ with Not_found ->
+ let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
+ nd.neg <- ndN;
+ let idxN = hkeyN mod ds in
+ data.(idxN) <- ndN :: data.(idxN);
+ hc.size <- osize + 2
else hc.size <- succ osize;
if hc.size > ds lsl 1 then resize hc else ();
nd
--
GitLab