diff options
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/Makefile.am | 3 | ||||
-rw-r--r-- | src/context/cddense_set.h | 103 |
2 files changed, 105 insertions, 1 deletions
diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 13a151ffc..d979a9c16 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -25,4 +25,5 @@ libcontext_la_SOURCES = \ cdvector.h \ cdmaybe.h \ stacking_map.h \ - stacking_vector.h + stacking_vector.h \ + cddense_set.h
\ No newline at end of file diff --git a/src/context/cddense_set.h b/src/context/cddense_set.h new file mode 100644 index 000000000..592925705 --- /dev/null +++ b/src/context/cddense_set.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \file cddense_set.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is an abstraction of a set of unsigned integers. + ** + ** 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 "cvc4_private.h" + +#pragma once + +#include <vector> + +#include "context/context.h" +#include "context/cdlist_forward.h" +#include "context/cdlist.h" + +#include "util/index.h" + +namespace CVC4 { +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<> */ + + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ |