1 /********************* */ 2 /*! \file cddense_set.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief This is an abstraction of a set of unsigned integers. 13 ** 14 ** This is an abstraction of a set of unsigned integers. 15 ** This class is designed to provide constant time insertion, element_of, 16 ** and fast iteration. This is done by storing backing vectors of size greater than 17 ** the maximum key. 18 **/ 19 20 #include "cvc4_private.h" 21 22 #pragma once 23 24 #include <vector> 25 26 #include "context/context.h" 27 #include "context/cdlist_forward.h" 28 #include "context/cdlist.h" 29 30 #include "util/index.h" 31 32 namespace CVC4 { 33 namespace context { 34 35 template <class CleanUp = DefaultCleanUp<Index> > 36 class CDDenseSet { 37 public: 38 typedef Index Element; 39 40 private: 41 42 class RemoveIntCleanup { 43 private: 44 std::vector<bool>& d_set; 45 46 /** 47 * The CleanUp functor. 48 */ 49 CleanUp d_cleanUp; 50 public: RemoveIntCleanup(std::vector<bool> & set,const CleanUp & cleanup)51 RemoveIntCleanup(std::vector<bool>& set, const CleanUp& cleanup) 52 : d_set(set), d_cleanUp(cleanup) 53 {} 54 operator()55 void operator()(Element* p){ 56 d_cleanup(p); 57 58 ArithVar x = *p; 59 Assert(d_set[x]); 60 d_set[x] = false; 61 } 62 }; 63 64 typedef CDList<Element, RemoveIntCleanup> ElementList; 65 ElementList d_list; 66 67 std::vector<bool> d_set; 68 69 public: 70 typedef ElementList::const_iterator const_iterator; 71 72 CDDenseSet(context::Context* c, const CleanUp& cleanup = CleanUp()) d_set()73 : d_set(), d_list(c, true, RemoveIntCleanup(d_set, cleanup)) 74 { } 75 76 /** This cannot be const as garbage collection is done lazily. */ contains(Element x)77 bool contains(Element x) const{ 78 if(x < d_set.size()){ 79 return d_set[x]; 80 }else{ 81 return false; 82 } 83 } 84 insert(Element x)85 void insert(Element x){ 86 Assert(!contains(x)); 87 if(x >= d_set.size()){ 88 d_set.resize(x+1, false); 89 } 90 d_list.push_back(x); 91 d_set[x] = true; 92 } 93 begin()94 const_iterator begin() const { return d_list.begin(); } end()95 const_iterator end() const { return d_list.end(); } 96 97 };/* class CDDenseSet<> */ 98 99 100 }/* CVC4::context namespace */ 101 }/* CVC4 namespace */ 102