From: Matthew Sotoudeh <masotoudeh@ucdavis.edu>
Date: Fri, 7 Jan 2022 20:12:18 +0000 (-0800)
Subject: Remove CDDenseSet data structure (#7890)
X-Git-Tag: cvc5-1.0.0~583
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2092b9a3f73762253dbf0e237a198dc989292acb;p=cvc5.git

Remove CDDenseSet data structure (#7890)

It was not used anywhere, and does not appear to build under, at least,
GCC/9.1.0.

Signed-off-by: Matthew Sotoudeh <sotoudeh@stanford.edu>
---

diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt
index 482dc6acc..19e603646 100644
--- a/src/context/CMakeLists.txt
+++ b/src/context/CMakeLists.txt
@@ -14,7 +14,6 @@
 ##
 
 set(LIBCONTEXT_SOURCES
-  cddense_set.h
   cdhashmap.h
   cdhashmap_forward.h
   cdhashset.h
diff --git a/src/context/cddense_set.h b/src/context/cddense_set.h
deleted file mode 100644
index 16e98eb95..000000000
--- a/src/context/cddense_set.h
+++ /dev/null
@@ -1,99 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- * This is an abstraction of a set of unsigned integers.
- *
- * This class is designed to provide constant time insertion, element_of,
- * and fast iteration. This is done by storing backing vectors of size greater
- * than the maximum key.
- */
-
-#include "cvc5_private.h"
-
-#pragma once
-
-#include <vector>
-
-#include "context/context.h"
-#include "context/cdlist_forward.h"
-#include "context/cdlist.h"
-
-#include "util/index.h"
-
-namespace cvc5 {
-namespace context {
-
-template <class CleanUp = DefaultCleanUp<Index> >
-class CDDenseSet {
-public:
-  typedef Index Element;
-
-private:
-
-  class RemoveIntCleanup {
-  private:
-    std::vector<bool>& d_set;
-
-    /**
-     * The CleanUp functor.
-     */
-    CleanUp d_cleanUp;
-  public:
-    RemoveIntCleanup(std::vector<bool>& set, const CleanUp& cleanup)
-      : d_set(set), d_cleanUp(cleanup)
-    {}
-
-    void operator()(Element* p){
-      d_cleanup(p);
-
-      ArithVar x = *p;
-      Assert(d_set[x]);
-      d_set[x] = false;
-    }
-  };
-
-  typedef CDList<Element, RemoveIntCleanup> ElementList;
-  ElementList d_list;
-
-  std::vector<bool> d_set;
-
-public:
-  typedef ElementList::const_iterator const_iterator;
-
-  CDDenseSet(context::Context* c, const CleanUp& cleanup = CleanUp())
-    : d_set(), d_list(c, true, RemoveIntCleanup(d_set, cleanup))
-  { }
-
-  /** This cannot be const as garbage collection is done lazily. */
-  bool contains(Element x) const{
-    if(x < d_set.size()){
-      return d_set[x];
-    }else{
-      return false;
-    }
-  }
-
-  void insert(Element x){
-    Assert(!contains(x));
-    if(x >= d_set.size()){
-      d_set.resize(x+1, false);
-    }
-    d_list.push_back(x);
-    d_set[x] = true;
-  }
-
-  const_iterator begin() const { return d_list.begin(); }
-  const_iterator end() const { return d_list.end(); }
-
-};/* class CDDenseSet<> */
-
-}  // namespace context
-}  // namespace cvc5