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