cdlist_forward.h \
cdqueue.h \
cdtrail_queue.h \
+ cdtrail_hashmap.h \
+ cdtrail_hashmap_forward.h \
+ cdinsert_hashmap.h \
+ cdinsert_hashmap_forward.h \
cdhashmap.h \
cdhashmap_forward.h \
cdhashset.h \
** and operator== for the key class. For key types that don't have a
** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
**
+ ** See also:
+ ** CDInsertHashMap : An "insert-once" CD hash map.
+ ** CDTrailHashMap : A lightweight CD hash map with poor iteration
+ ** characteristics and some quirks in usage.
+ **
** Internal documentation:
**
- ** CDMap<> is something of a work in progress at present (26 May
+ ** CDHashMap<> is something of a work in progress at present (26 May
** 2010), due to some recent discoveries of problems with its
** internal state. Here are some notes on the internal use of
** CDOhash_maps that may be useful in figuring out this mess:
**
- ** So you have a CDMap<>.
+ ** So you have a CDHashMap<>.
**
** You insert some (key,value) pairs. Each allocates a CDOhash_map<>
** and goes on a doubly-linked list headed by map.d_first and
** map pointer at level 0, and a non-NULL map pointer in the
** current context level. (Remember that for later.)
**
- ** When a key is associated to a new value in a CDMap, its
+ ** When a key is associated to a new value in a CDHashMap, its
** associated CDOhash_map calls makeCurrent(), then sets the new
** value. The save object is also a CDOhash_map (allocated in context
** memory).
** obliterate() removes it from the map and frees the CDOhash_map's
** memory.
**
- ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()).
+ ** Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
** This first calls destroy(), as per ContextObj contract, but
** cdhashmapdoesn't save/restore itself, so that does nothing at the
- ** CDMap-level. Then it empties the trash. Then, for each
+ ** CDHashMap-level. Then it empties the trash. Then, for each
** element in the map, it marks it as being "part of a complete
** map destruction", which essentially short-circuits
** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
** it. Finally it asserts that the trash is empty (which it
** should be, since restore() was short-circuited).
**
- ** Fifth, you might clear() the CDMap. This does exactly the
- ** same as CDMap::~CDMap(), except that it doesn't call destroy()
+ ** Fifth, you might clear() the CDHashMap. This does exactly the
+ ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
** on itself.
**
- ** CDMap::emptyTrash() simply goes through and calls
+ ** CDHashMap::emptyTrash() simply goes through and calls
** ->deleteSelf() on all elements in the trash.
** ContextObj::deleteSelf() calls the CDOhash_map destructor, then
** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map()
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDMAP_H
-#define __CVC4__CONTEXT__CDMAP_H
+#ifndef __CVC4__CONTEXT__CDHASHMAP_H
+#define __CVC4__CONTEXT__CDHASHMAP_H
#include <vector>
#include <iterator>
d_next->d_prev = d_prev;
d_prev->d_next = d_next;
if(d_noTrash) {
- Debug("gc") << "CDMap<> no-trash " << this << std::endl;
+ Debug("gc") << "CDHashMap<> no-trash " << this << std::endl;
} else {
- Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
+ Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
//this->deleteSelf();
d_map->d_trash.push_back(this);
}
// "Initializing" map insertion: this entry will never be
// removed from the map, it's inserted at level 0 as an
// "initializing" element. See
- // CDMap<>::insertAtContextLevelZero().
+ // CDHashMap<>::insertAtContextLevelZero().
d_data = data;
} else {
// Normal map insertion: first makeCurrent(), then set the data
}
/**
- * Version of insert() for CDMap<> that inserts data value d at
+ * Version of insert() for CDHashMap<> that inserts data value d at
* context level zero. This is a special escape hatch for inserting
* "initializing" data into the map. Imagine something happens at a
* deep context level L that causes insertion into a map, such that
const std::pair<const Key, Data>& operator*() const {
return *d_pair;
}
- };/* class CDMap<>::iterator::Proxy */
+ };/* class CDHashMap<>::iterator::Proxy */
// Actual postfix increment: returns Proxy with the old value.
// Now, an expression like *i++ will return the current *i, and
++(*this);
return e;
}
- };/* class CDMap<>::iterator */
+ };/* class CDHashMap<>::iterator */
typedef iterator const_iterator;
return const_cast<const CDHashMap*>(this)->find(k);
}
-};/* class CDMap<> */
+};/* class CDHashMap<> */
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDMAP_H */
+#endif /* __CVC4__CONTEXT__CDHashMAP_H */
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief This is a forward declaration header to declare the CDMap<>
+ ** \brief This is a forward declaration header to declare the CDHashMap<>
** template
**
- ** This is a forward declaration header to declare the CDMap<>
- ** template. It's useful if you want to forward-declare CDMap<>
- ** without including the full cdmap.h header, for example, in a
+ ** This is a forward declaration header to declare the CDHashMap<>
+ ** template. It's useful if you want to forward-declare CDHashMap<>
+ ** without including the full cdhashmap.h header, for example, in a
** public header context.
**
- ** For CDMap<> in particular, it's difficult to forward-declare it
+ ** For CDHashMap<> in particular, it's difficult to forward-declare it
** yourself, because it has a default template argument.
**/
#include "cvc4_public.h"
-#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
-#define __CVC4__CONTEXT__CDMAP_FORWARD_H
+#ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
+#define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
/// \cond internals
/// \endcond
-#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
+#endif /* __CVC4__CONTEXT__CDHASHMAP_FORWARD_H */
#define __CVC4__CONTEXT__CDSET_H
#include "context/context.h"
-#include "context/cdhashset_forward.h"
-#include "context/cdhashmap.h"
+#include "context/cdinsert_hashmap.h"
#include "util/cvc4_assert.h"
namespace CVC4 {
namespace context {
template <class V, class HashFcn>
-class CDHashSet : protected CDHashMap<V, V, HashFcn> {
- typedef CDHashMap<V, V, HashFcn> super;
+class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
+ typedef CDInsertHashMap<V, bool, HashFcn> super;
public:
return super::size();
}
- size_t count(const V& v) const {
- return super::count(v);
- }
-
bool insert(const V& v) {
- return super::insert(v, v);
- }
-
- void insertAtContextLevelZero(const V& v) {
- return super::insertAtContextLevelZero(v, v);
+ return super::insert_safe(v, true);
}
bool contains(const V& v) {
- return find(v) != end();
+ return super::contains(v);
}
- // FIXME: no erase(), too much hassle to implement efficiently...
-
- class iterator {
- typename super::iterator d_it;
+ class const_iterator {
+ typename super::const_iterator d_it;
public:
- iterator(const typename super::iterator& it) : d_it(it) {}
- iterator(const iterator& it) : d_it(it.d_it) {}
+ const_iterator(const typename super::const_iterator& it) : d_it(it) {}
+ const_iterator(const const_iterator& it) : d_it(it.d_it) {}
// Default constructor
- iterator() {}
+ const_iterator() {}
// (Dis)equality
- bool operator==(const iterator& i) const {
+ bool operator==(const const_iterator& i) const {
return d_it == i.d_it;
}
- bool operator!=(const iterator& i) const {
+ bool operator!=(const const_iterator& i) const {
return d_it != i.d_it;
}
}
// Prefix increment
- iterator& operator++() {
+ const_iterator& operator++() {
++d_it;
return *this;
}
}
};/* class CDSet<>::iterator */
- typedef iterator const_iterator;
-
const_iterator begin() const {
- return iterator(super::begin());
+ return const_iterator(super::begin());
}
const_iterator end() const {
- return iterator(super::end());
+ return const_iterator(super::end());
}
const_iterator find(const V& v) const {
- return iterator(super::find(v));
+ return const_iterator(super::find(v));
+ }
+
+ typedef typename super::key_iterator key_iterator;
+ key_iterator key_begin() const {
+ return super::key_begin();
+ }
+ key_iterator key_end() const {
+ return super::key_end();
+ }
+
+ void insertAtContextLevelZero(const V& v) {
+ return super::insertAtContextLevelZero(v, true);
}
};/* class CDSet */
--- /dev/null
+/********************* */
+/*! \file cdinsert_hashmap.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-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent insert only hashmap built using trail of edits
+ **
+ ** Context-dependent hashmap that only allows for one insertion per element.
+ ** This can be viewed as a highly restricted version of CDHashMap.
+ ** It is significantly lighter in memory usage than CDHashMap.
+ **
+ ** See also:
+ ** CDTrailHashMap : A lightweight CD hash map with poor iteration
+ ** characteristics and some quirks in usage.
+ ** CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
+ **
+ ** Notes:
+ ** - To iterate efficiently over the elements use the key_iterators.
+ ** - operator[] is only supported as a const derefence (must succeed).
+ ** - insert(k) must always work.
+ ** - Use insert_safe if you want to check if the element has been inserted
+ ** and only insert if it has not yet been.
+ ** - Does not accept TNodes as keys.
+ ** - Supports insertAtContextLevelZero() if the element is not in the map.
+ **/
+
+
+#include "cvc4_private.h"
+
+#include "context/context.h"
+#include "context/cdinsert_hashmap_forward.h"
+#include <utility>
+#include <ext/hash_map>
+#include <deque>
+#include "util/cvc4_assert.h"
+#include "util/output.h"
+
+#include "expr/node.h"
+#include <boost/static_assert.hpp>
+
+#pragma once
+
+namespace CVC4 {
+namespace context {
+
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class InsertHashMap {
+private:
+ typedef std::deque<Key> KeyVec;
+ /** A list of the keys in the map maintained as a stack. */
+ KeyVec d_keys;
+
+ typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap;
+ /** The hash_map used for element lookup. */
+ HashMap d_hashMap;
+
+public:
+ /**
+ * An iterator over a list of keys.
+ * Use this to efficiently iterate over the elements.
+ * (See std::deque<>::iterator).
+ */
+ typedef typename KeyVec::const_iterator key_iterator;
+
+ /**An iterator over the elements in the hash_map. */
+ typedef typename HashMap::const_iterator const_iterator;
+
+
+ /**
+ * Returns an iterator to the begining of the HashMap.
+ * Acts like a hash_map::const_iterator.
+ */
+ const_iterator begin() const{
+ return d_hashMap.begin();
+ }
+ /**
+ * Returns an iterator to the end of the HashMap.
+ * Acts like a hash_map::const_iterator.
+ */
+ const_iterator end() const{
+ return d_hashMap.end();
+ }
+
+ /**
+ * Returns an iterator to the Key k of the map.
+ * See hash_map::find()
+ */
+ const_iterator find(const Key& k) const{
+ return d_hashMap.find(k);
+ }
+
+ /** Returns an iterator to the start of the set of keys. */
+ key_iterator key_begin() const{
+ return d_keys.begin();
+ }
+ /** Returns an iterator to the end of the set of keys. */
+ key_iterator key_end() const{
+ return d_keys.end();
+ }
+
+ /** Returns true if the map is empty. */
+ bool empty() const { return d_keys.empty(); }
+ /** Returns the number of elements in the map. */
+ size_t size() const { return d_keys.size(); }
+
+ /** Returns true if k is a mapped key. */
+ bool contains(const Key& k) const {
+ return find(k) != end();
+ }
+
+ /**
+ * Returns a reference the data mapped by k.
+ * This must succeed.
+ */
+ const Data& operator[](const Key& k) const {
+ const_iterator ci = find(k);
+ Assert(ci != end());
+ return (*ci).second;
+ }
+
+ /**
+ * Inserts an element into the map, and pushes its key to the front
+ * of the stack. The key inserted must be not be currently mapped.
+ */
+ void push_front(const Key& k, const Data& d){
+ Assert(!contains(k));
+ d_hashMap.insert(std::make_pair(k, d));
+ d_keys.push_front(k);
+ }
+
+ /**
+ * Inserts an element into the map, and pushes its key onto the
+ * back on the stack. The key inserted must be not be currently mapped.
+ */
+ void push_back(const Key& k, const Data& d){
+ Assert(!contains(k));
+ d_hashMap.insert(std::make_pair(k, d));
+ d_keys.push_back(k);
+ }
+
+ /**
+ * Pops the key at the front of the list off and removes its key from the map.
+ */
+ void pop_front(){
+ Assert(!empty());
+ const Key& front = d_keys.front();
+ d_hashMap.erase(front);
+
+ Debug("TrailHashMap") <<"TrailHashMap pop_front " << size() << std::endl;
+ d_keys.pop_front();
+ }
+
+ /**
+ * Pops the key at the back of the stack off and removes its key from the map.
+ */
+ void pop_back(){
+ Assert(!empty());
+ const Key& back = d_keys.back();
+ d_hashMap.erase(back);
+
+ Debug("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl;
+ d_keys.pop_back();
+ }
+
+ /**
+ * Pops the back of the stack until the size is below s.
+ */
+ void pop_to_size(size_t s){
+ while(size() > s){
+ pop_back();
+ }
+ }
+};/* class TrailHashMap<> */
+
+template <class Key, class Data, class HashFcn >
+class CDInsertHashMap : public ContextObj {
+private:
+ typedef InsertHashMap<Key, Data, HashFcn> IHM;
+
+ /** An InsertHashMap that backs all of the data. */
+ IHM* d_insertMap;
+
+ /** For restores, we need to keep track of the previous size. */
+ size_t d_size;
+
+ /**
+ * To support insertAtContextLevelZero() and restores,
+ * we have called d_insertMap->d_pushFront().
+ */
+ size_t d_pushFronts;
+
+ /**
+ * Private copy constructor used only by save(). d_insertMap is
+ * not copied: only the base class information and
+ * d_size and d_pushFronts are needed in restore.
+ */
+ CDInsertHashMap(const CDInsertHashMap<Key, Data, HashFcn>& l) :
+ ContextObj(l),
+ d_insertMap(NULL),
+ d_size(l.d_size),
+ d_pushFronts(l.d_pushFronts)
+ {
+ Debug("CDInsertHashMap") << "copy ctor: " << this
+ << " from " << &l
+ << " size " << d_size << std::endl;
+ }
+
+ /**
+ * Implementation of mandatory ContextObj method save: simply copies
+ * the current size information to a copy using the copy constructor (the
+ * pointer and the allocated size are *not* copied as they are not
+ * restored on a pop). The saved information is allocated using the
+ * ContextMemoryManager.
+ */
+ ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
+ Debug("CDInsertHashMap") << "save " << this
+ << " at level " << this->getContext()->getLevel()
+ << " size at " << this->d_size
+ << " d_list is " << this->d_insertMap
+ << " data:" << data << std::endl;
+ return data;
+ }
+protected:
+ /**
+ * Implementation of mandatory ContextObj method restore:
+ * restore to the previous size taking into account the number
+ * of new pushFront calls have happened since saving.
+ * The d_insertMap is untouched and d_pushFronts is also kept.
+ */
+ void restore(ContextObj* data) {
+ Debug("CDInsertHashMap") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " data == " << data
+ << " d_insertMap == " << this->d_insertMap << std::endl;
+ size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
+ size_t oldPushFronts = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
+ Assert(oldPushFronts <= d_pushFronts);
+
+ // The size to restore to.
+ size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
+ d_insertMap->pop_to_size(restoreSize);
+ d_size = restoreSize;
+ Assert(d_insertMap->size() == d_size);
+ Debug("CDInsertHashMap") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " size back to " << this->d_size << std::endl;
+ }
+public:
+
+ /**
+ * Main constructor: d_insertMap starts as an empty map, with the size is 0
+ */
+ CDInsertHashMap(Context* context) :
+ ContextObj(context),
+ d_insertMap(new IHM()),
+ d_size(0),
+ d_pushFronts(0){
+ Assert(d_insertMap->size() == d_size);
+ }
+
+ /**
+ * Destructor: delete the d_insertMap
+ */
+ ~CDInsertHashMap() throw(AssertionException) {
+ this->destroy();
+ delete d_insertMap;
+ }
+
+ /** An iterator over the elements in the hash_map. */
+ typedef typename IHM::const_iterator const_iterator;
+
+ /**
+ * An iterator over a list of keys.
+ * Use this to efficiently iterate over the elements.
+ * (See std::deque<>::iterator).
+ */
+ typedef typename IHM::key_iterator key_iterator;
+
+ /** Returns true if the map is empty in the current context. */
+ bool empty() const{
+ return d_size == 0;
+ }
+
+ /** Returns true the size of the map in the current context. */
+ size_t size() const {
+ return d_size;
+ }
+
+ /**
+ * Inserts an element into the map.
+ * The key inserted must be not be currently mapped.
+ * This is implemented using d_insertMap.push_back().
+ */
+ void insert(const Key& k, const Data& d){
+ makeCurrent();
+ ++d_size;
+ d_insertMap->push_back(k, d);
+ Assert(d_insertMap->size() == d_size);
+ }
+
+ /**
+ * Checks if the key k is mapped already.
+ * If it is, this returns false.
+ * Otherwise it is inserted and this returns true.
+ */
+ bool insert_safe(const Key& k, const Data& d){
+ if(contains(k)){
+ return false;
+ }else{
+ insert(k,d);
+ return true;
+ }
+ }
+
+ /**
+ * Version of insert() for CDMap<> that inserts data value d at
+ * context level zero.
+ *
+ * It is an error to insertAtContextLevelZero()
+ * a key that already is in the map.
+ */
+ void insertAtContextLevelZero(const Key& k, const Data& d){
+ makeCurrent();
+ ++d_size;
+ ++d_pushFronts;
+ d_insertMap->push_front(k, d);
+ }
+
+ /** Returns true if k is a mapped key in the context. */
+ bool contains(const Key& k) const {
+ return d_insertMap->contains(k);
+ }
+
+ /**
+ * Returns a reference the data mapped by k.
+ * k must be in the map in this context.
+ */
+ const Data& operator[](const Key& k) const {
+ return (*d_insertMap)[k];
+ }
+
+ /**
+ * Returns a const_iterator to the value_type if k is a mapped key in
+ * the context.
+ */
+ const_iterator find(const Key& k) const {
+ return d_insertMap->find(k);
+ }
+
+ /**
+ * Returns an iterator to the begining of the map.
+ * Acts like a hash_map::const_iterator.
+ */
+ const_iterator begin() const{
+ return d_insertMap->begin();
+ }
+
+ /**
+ * Returns an iterator to the end of the map.
+ * Acts like a hash_map::const_iterator.
+ */
+ const_iterator end() const{
+ return d_insertMap->end();
+ }
+
+ /** Returns an iterator to the start of the set of keys. */
+ key_iterator key_begin() const{
+ return d_insertMap->key_begin();
+ }
+ /** Returns an iterator to the end of the set of keys. */
+ key_iterator key_end() const{
+ return d_insertMap->key_end();
+ }
+};/* class CDInsertHashMap<> */
+
+
+template <class Data, class HashFcn>
+class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
+ /* CDInsertHashMap is challenging to get working with TNode.
+ * Consider using CDHashMap<TNode,...> instead.
+ *
+ * Explanation:
+ * CDInsertHashMap uses keys for deallocation.
+ * If the key is a TNode and the backing (the hard node reference)
+ * for the key in another data structure removes the key at the same context
+ * the ref count could drop to 0. The key would then not be eligible to be
+ * hashed. Getting the order right with a guarentee is to hard.
+ */
+
+ BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+};
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file cdinsert_hashmap_forward.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-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the CDInsertHashMap<>
+ ** template
+ **
+ ** This is a forward declaration header to declare the CDInsertHashMap<>
+ ** template. It's useful if you want to forward-declare CDInsertHashMap<>
+ ** without including the full cdinsert_hashmap.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDInsertHashMap<> in particular, it's difficult to forward-declare it
+ ** yourself, because it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace __gnu_cxx {
+ template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+ namespace context {
+ template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+ class CDInsertHashMap;
+ }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
--- /dev/null
+/********************* */
+/*! \file cdtrail_hashmap.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-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent hashmap built using trail of elements
+ **
+ ** Context-dependent hashmap that explicitly keeps track of its edit history.
+ ** This is similar in functionality to CDHashMap with fewer capabilites and
+ ** slight changes in the interface. It has the advantage of being lighter in
+ ** memory usage.
+ **
+ ** See also:
+ ** CDInsertHashMap : An "insert-once" CD hash map.
+ ** CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
+ **
+ ** Notes:
+ ** - To iterate efficiently over the elements use the key_iterators.
+ ** - operator[] is only supported as a const derefence (must succeed).
+ ** - Insertions to the map are done with respect to a context.
+ ** - Insertions can be done in two manors either with insert() or
+ ** insert_no_overwrite().
+ ** - insert(k,d) inserts the key data pair into the hashtable and returns a
+ ** false if it overwrote the previous value.
+ ** - insert_no_overwrite(k,d) inserts key data pair into the hashtable only
+ ** if the value is not already there. It returns true, if an element was
+ ** added. This conditionally extends the trail length if it returns true.
+ ** - inserts are compacting. If there is another insert to the same key
+ ** at the same context, the memory is reused.
+ ** - Iterating over const_iterators has amortized time proportional to
+ ** O(trail length). (If this needs to be improved, please bug Tim.)
+ ** - contains() and operator[] are slightly faster than using stl style
+ ** iterator comparisons: find(), end(), etc.
+ **/
+
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "context/context.h"
+#include "context/cdtrail_hashmap_forward.h"
+#include <utility>
+#include <ext/hash_map>
+#include <deque>
+#include "util/cvc4_assert.h"
+#include "util/output.h"
+
+#include "expr/node.h"
+#include <boost/static_assert.hpp>
+
+
+namespace CVC4 {
+namespace context {
+
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class TrailHashMap {
+public:
+ /** A pair of Key and Data that mirrors hash_map::value_type. */
+ typedef std::pair<Key, Data> value_type;
+
+private:
+
+ /** The trail information from an insert. */
+ struct KDT {
+ /** The Key Data pair. */
+ value_type d_kd;
+
+ /**
+ * The previous trail entry with the same key.
+ * On a pop, this is the element to revert to.
+ * This value is a self loop if there is no previous entry.
+ */
+ size_t d_prevKey;
+
+ /** The whether the trail element is current. */
+ bool d_current;
+
+ KDT(const Key& key, const Data& data, size_t prev, bool cur = true):
+ d_kd(std::make_pair(key, data)), d_prevKey(prev), d_current(cur){ }
+ KDT(){}
+ };
+
+ typedef std::deque<KDT> KDTVec;
+ typedef typename KDTVec::const_iterator KDTVec_const_iterator;
+ /** The trail of elements. */
+ KDTVec d_kdts;
+
+
+ typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap;
+ typedef typename PositionMap::iterator PM_iterator;
+ typedef typename PositionMap::const_iterator PM_const_iterator;
+
+ /** A map of keys to their positions in the trail. */
+ PositionMap d_posMap;
+
+
+ /** The number of unique keys in the map. */
+ size_t d_uniqueKeys;
+
+ /** Internal utility class. NonConstant find on the position map.*/
+ inline PM_iterator ncfind(const Key& k) {
+ return d_posMap.find(k);
+ }
+
+ /** Internal utility class. Position Map Find.*/
+ inline PM_const_iterator pmfind(const Key& k) const{
+ return d_posMap.find(k);
+ }
+ /** Internal utility class. Position Map End.*/
+ inline PM_const_iterator pmend() const{
+ return d_posMap.end();
+ }
+
+ /** This is true if the previous entry in the trail points at itself.*/
+ inline bool selfLoop(size_t pos, const KDT& kdt) const {
+ return pos == kdt.d_prevKey;
+ }
+
+public:
+ /**
+ * Constant iterator for TrailHashMap.
+ * Only supports forward iteration.
+ * This always points at the end or a current element in the trail.
+ * This is done by iterating over the trail.
+ */
+ class const_iterator {
+ private:
+ /** A vector iterator. */
+ KDTVec_const_iterator d_it;
+
+ /** A pointer to the end of the vector.*/
+ KDTVec_const_iterator d_end;
+
+ /** Move the iterator to the end or the next current element.*/
+ void findCurrent(){
+ while(d_it != d_end && !(*d_it).d_current){
+ ++d_it;
+ }
+ }
+
+ public:
+
+ /** Constructs an iterator for a TrailHashMap. */
+ const_iterator(KDTVec_const_iterator it, KDTVec_const_iterator end) :
+ d_it(it),
+ d_end(end){
+ findCurrent();
+ }
+
+ /** Copy constructor for an iterator for a TrailHashMap. */
+ const_iterator(const const_iterator& other) :
+ d_it(other.d_it), d_end(other.d_end){
+ // Do not need to findCurrent()
+ }
+
+ /** Returns true if the iterators are the same. */
+ inline bool operator==(const const_iterator& other) const {
+ return d_it == other.d_it;
+ }
+
+ /** Returns true if the iterators are the same. */
+ inline bool operator!=(const const_iterator& other) const {
+ return d_it != other.d_it;
+ }
+
+ /** Returns a pair<Key,Data>. */
+ inline const value_type& operator*() const {
+ return (*d_it).d_kd;
+ }
+
+ /** Prefix increment */
+ const_iterator& operator++() {
+ ++d_it;
+ findCurrent();
+ return *this;
+ }
+ };
+
+ /** Returns a beginning iterator.*/
+ inline const_iterator begin() const{
+ return const_iterator(d_kdts.begin(), d_kdts.end());
+ }
+
+ /** Returns an end iterator.*/
+ inline const_iterator end() const{
+ return const_iterator(d_kdts.end(), d_kdts.end());
+ }
+
+ /** Returns true if the trail is empty.*/
+ inline bool empty() const { return d_kdts.empty(); }
+
+ /** Returns the size of the trail.*/
+ inline size_t trailSize() const { return d_kdts.size(); }
+
+ /** Returns the number of unique keys in the map.*/
+ inline size_t uniqueKeys() const { return d_uniqueKeys; }
+
+ /** Returns true if the key is in the map.*/
+ inline bool contains(const Key& k) const {
+ return pmfind(k) != pmend();
+ }
+
+ /**
+ * Returns a NON const reference to an element in the Map.
+ * k must be a key in the Map.
+ * DO NOT USE THIS UNLESS YOU ARE CONFIDENT THE CHANGES MAKE SENSE.
+ */
+ Data& lookup(const Key& k){
+ Assert(contains(k));
+ PM_iterator ci = ncfind(k);
+ KDT& kdt = d_kdts[(*ci).second];
+ return kdt.d_kd.second;
+ }
+
+ /**
+ * Returns a const reference to an element mapped by a Key k.
+ * k must be a key in the Map.
+ */
+ const Data& operator[](const Key& k) const {
+ PM_const_iterator pci = pmfind(k);
+ Assert(pci != pmend());
+ return d_kdts[(*pci).second].d_kd.second;
+ }
+
+ /**
+ * If the key k is in the map, this returns a const_iterator pointing at this
+ * element. Otherwise, this returns end().
+ */
+ const_iterator find(const Key& k) const {
+ PM_const_iterator pci = pmfind(k);
+ if(pci == pmend()){
+ return end();
+ }else{
+ size_t pos = (*pci).second;
+ return const_iterator(d_kdts.begin() + pos, d_kdts.end());
+ }
+ }
+
+ /**
+ * Similar to contains, but includes a notion of trail position.
+ * Returns <true, true> if contains(k) and the current position of k
+ * in the map is greater than or equal to pos.
+ * Returns <true, false> if it contains(k) but not the previous condition.
+ * Returns <false, false> if it does not contains(k).
+ */
+ std::pair<bool, bool> hasAfter(const Key& k, size_t pos) {
+ PM_iterator it = ncfind(k);
+ if(it != d_posMap.end()){
+ return std::make_pair(true, (*it).second >= pos );
+ }
+ return std::make_pair(false, false);
+ }
+
+ /**
+ * Inserts an element unconditionally.
+ * Always increases the trail size.
+ * Returns true if the key count increased.
+ */
+ bool push_back(const Key& k, const Data& d){
+ std::pair<bool, bool> res = compacting_push_back(k, d, trailSize());
+ return res.first;
+ }
+
+ /**
+ * This inserts an element into the trail.
+ * This insert can reuse the same trail element if the postion of the element
+ * is >= threshold.
+ *
+ * Return values:
+ * If pair<bool, bool> res = compacting_push_back(..),
+ * then res.first is true if this is a new unique key, and
+ * res.second is true if the trail length increased.
+ *
+ */
+ std::pair<bool, bool> compacting_push_back(const Key& k, const Data& d, size_t threshold){
+ size_t backPos = d_kdts.size();
+ std::pair<PM_iterator, bool> res = d_posMap.insert(std::make_pair(k, backPos));
+ if(!res.second){
+ size_t& prevPosInPM = (*res.first).second;
+
+ Assert(d_kdts[prevPosInPM].d_current);
+
+ if(prevPosInPM < threshold){
+ d_kdts.push_back(KDT(k,d, prevPosInPM));
+ d_kdts[prevPosInPM].d_current = false;
+ prevPosInPM = backPos;
+
+ return std::make_pair(false, true);
+ }else{
+ d_kdts[prevPosInPM].d_kd.second = d;
+ return std::make_pair(false, false);
+ }
+ }else{
+ d_kdts.push_back(KDT(k,d, backPos));
+ ++d_uniqueKeys;
+ return std::make_pair(true, true);
+ }
+ }
+
+ /**
+ * Inserts an element if the key is not already in the map.
+ * Returns true if the element was inserted.
+ */
+ bool insert_no_overwrite(const Key& k, const Data& d){
+ size_t backPos = d_kdts.size();
+ std::pair<PM_iterator, bool> res = d_posMap.insert(std::make_pair(k, backPos));
+ if(res.second){
+ d_kdts.push_back(KDT(k,d, backPos));
+ ++d_uniqueKeys;
+ }
+ Debug("TrailHashMap") <<"TrailHashMap insert" << k << " d " << d << " " << backPos << std::endl;
+ return res.second;
+ }
+
+ /** Pops the element at the back of the trail. */
+ void pop_back(){
+ Assert(!empty());
+ const KDT& back = d_kdts.back();
+ const Key& k = back.d_kd.first;
+ if(selfLoop(trailSize()-1, back)){
+ d_posMap.erase(k);
+ --d_uniqueKeys;
+ Debug("TrailHashMap") <<"TrailHashMap pop_back erase " << trailSize() <<" " << std::endl;
+
+ }else{
+ Debug("TrailHashMap") <<"TrailHashMap reset " << trailSize() <<" " << " " << back.d_prevKey << std::endl;
+ d_posMap[k] = back.d_prevKey;
+ d_kdts[back.d_prevKey].d_current = true;
+ }
+ d_kdts.pop_back();
+ }
+
+ /** Pops the element at the back of the trail until the trailSize is <= s. */
+ void pop_to_size(size_t s){
+ while(trailSize() > s){
+ pop_back();
+ }
+ }
+};/* class TrailHashMap<> */
+
+template <class Key, class Data, class HashFcn >
+class CDTrailHashMap : public ContextObj {
+private:
+ /** A short name for the templatized TrailMap that backs the CDTrailMap. */
+ typedef TrailHashMap<Key, Data, HashFcn> THM;
+
+ /** The trail map that backs the CDTrailMap. */
+ THM* d_trailMap;
+public:
+ /** Iterator for the CDTrailHashMap. */
+ typedef typename THM::const_iterator const_iterator;
+
+ /** Return value of operator* on a const_iterator (pair<Key,Data>).*/
+ typedef typename THM::value_type value_type;
+
+private:
+ /**
+ * The length of the trail in the current context.
+ * This is used to support reverting.
+ */
+ size_t d_trailSize;
+
+ /**
+ * The length of the trail immediately after the previous makeCurrent().
+ * This is used to support compacting inserts.
+ */
+ size_t d_prevTrailSize;
+
+ /**
+ * Private copy constructor used only by save(). d_trailMap is not copied:
+ * only the base class information, d_trailSize, and d_prevTrailSize
+ * are needed in restore.
+ */
+ CDTrailHashMap(const CDTrailHashMap<Key, Data, HashFcn>& l) :
+ ContextObj(l),
+ d_trailMap(NULL),
+ d_trailSize(l.d_trailSize),
+ d_prevTrailSize(l.d_prevTrailSize){
+ Debug("CDTrailHashMap") << "copy ctor: " << this
+ << " from " << &l
+ << " size " << d_trailSize << std::endl;
+ }
+
+ /**
+ * Implementation of mandatory ContextObj method save: simply copies
+ * the current sizes to a copy using the copy constructor,
+ * The saved information is allocated using the ContextMemoryManager.
+ */
+ ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* data = new(pCMM) CDTrailHashMap<Key, Data, HashFcn>(*this);
+ Debug("CDTrailHashMap") << "save " << this
+ << " at level " << this->getContext()->getLevel()
+ << " size at " << this->d_trailSize
+ << " d_list is " << this->d_trailMap
+ << " data:" << data << std::endl;
+ return data;
+ }
+protected:
+ /**
+ * Implementation of mandatory ContextObj method restore: simply
+ * restores the previous size. Note that the list pointer and the
+ * allocated size are not changed.
+ */
+ void restore(ContextObj* data) {
+ Debug("CDTrailHashMap") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " data == " << data
+ << " d_trailMap == " << this->d_trailMap << std::endl;
+ size_t oldSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_trailSize;
+ d_trailMap->pop_to_size(oldSize);
+ d_trailSize = oldSize;
+ Assert(d_trailMap->trailSize() == d_trailSize);
+
+ d_prevTrailSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_prevTrailSize;
+ Debug("CDTrailHashMap") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " size back to " << this->d_trailSize << std::endl;
+ }
+
+ /**
+ * We need to save the d_trailSize immediately after a successful makeCurrent.
+ * So this version needs to be used everywhere instead of maekCurrent()
+ * internally.
+ */
+ void internalMakeCurrent () {
+ if(!isCurrent()){
+ makeCurrent();
+ d_prevTrailSize = d_trailSize;
+ }
+ }
+
+public:
+
+ /**
+ * Main constructor: d_trailMap starts as an empty map, with the sizes are 0
+ */
+ CDTrailHashMap(Context* context) :
+ ContextObj(context),
+ d_trailMap(new THM()),
+ d_trailSize(0),
+ d_prevTrailSize(0){
+ Assert(d_trailMap->trailSize() == d_trailSize);
+ }
+
+ /**
+ * Destructor: delete the map
+ */
+ ~CDTrailHashMap() throw(AssertionException) {
+ this->destroy();
+ delete d_trailMap;
+ }
+
+ /** Returns true if the map is empty in the current context. */
+ bool empty() const{
+ return d_trailSize == 0;
+ }
+
+ /** Returns true the size of the map in the current context. */
+ size_t size() const {
+ return d_trailMap->uniqueKeys();
+ }
+
+ /**
+ * Inserts an element into the map.
+ * This always succeeds.
+ * Returns true if the key is new.
+ */
+ bool insert(const Key& k, const Data& d){
+ internalMakeCurrent();
+ std::pair<bool, bool> res = d_trailMap->compacting_push_back(k, d, d_prevTrailSize);
+ if(res.second){
+ ++d_trailSize;
+ }
+ Assert(d_trailMap->trailSize() == d_trailSize);
+ return res.first;
+ }
+
+ /**
+ * Inserts an element into the map if the key is not already there.
+ * This has no side effects if the insert does not happen.
+ * Returns true if the element was inserted.
+ */
+ bool insert_no_overwrite(const Key& k, const Data& d){
+ bool res = d_trailMap->insert_no_overwrite(k, d);
+ if(res){
+ internalMakeCurrent();
+ ++d_trailSize;
+ }
+ Assert(d_trailMap->trailSize() == d_trailSize);
+ return res;
+ }
+
+ /** Returns true if k is a mapped key in the context. */
+ bool contains(const Key& k) const {
+ return d_trailMap->contains(k);
+ }
+
+ /**
+ * Returns a reference the data mapped by k.
+ * k must be in the map in this context.
+ */
+ const Data& operator[](const Key& k) const {
+ return (*d_trailMap)[k];
+ }
+ /*
+// While the following code "works", I wonder if it is not better to disable it?
+// Non-const operator[] has strange semantics for a context-dependent
+// data structure.
+ Data& operator[](const Key& k) {
+ internalMakeCurrent();
+ std::pair<bool, bool> res = d_trailMap->hasAfter(k, d_prevTrailSize);
+ if(!res.first){
+ std::pair<bool, bool> res = d_trailMap->compacting_push_back(k, Data(), d_prevTrailSize);
+ if(res.second){
+ ++d_trailSize;
+ }
+ }else if(!res.second){
+ std::pair<bool, bool> res = d_trailMap->compacting_push_back(k, (*d_trailMap)[k], d_prevTrailSize);
+ if(res.second){
+ ++d_trailSize;
+ }
+ }
+ return d_trailMap->lookup(k);
+ }
+ */
+
+ /**
+ * Returns a const_iterator to the value_type if k is a mapped key in
+ * the context.
+ */
+ const_iterator find(const Key& k) const {
+ return d_trailMap->find(k);
+ }
+
+ /** Returns an iterator to the begining of the map. */
+ const_iterator begin() const{
+ return d_trailMap->begin();
+ }
+ /** Returns an iterator to the end of the map. */
+ const_iterator end() const{
+ return d_trailMap->end();
+ }
+
+};/* class CDTrailHashMap<> */
+
+template <class Data, class HashFcn>
+class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
+ /* CDTrailHashMap is challenging to get working with TNode.
+ * Consider using CDHashMap<TNode,...> instead.
+ *
+ * Explanation:
+ * CDTrailHashMap uses keys during deallocation.
+ * If the key is a TNode and the backing (the hard node reference)
+ * for the key in another data structure removes the key at the same context
+ * the ref count could drop to 0. The key would then not be eligible to be
+ * hashed. Getting the order right with a guarentee is to hard.
+ */
+
+ BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+};
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file cdtrail_hashmap_forward.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-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the
+ ** CDTrailHashMap<> template
+ **
+ ** This is a forward declaration header to declare the CDTrailHashMap<>
+ ** template. It's useful if you want to forward-declare CDTrailHashMap<>
+ ** without including the full cdtrail_hash_map.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDTrailHashMap<> in particular, it's difficult to forward-declare it
+ ** yourself, because it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace __gnu_cxx {
+ template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+ namespace context {
+ template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+ class CDTrailHashMap;
+ }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
// being 'justified' is monotonic with respect to decisions
- typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
+ typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
JustifiedSet d_justified;
context::CDO<unsigned> d_prvsIndex;
d_visited.clear();
if(Trace.isOn("justified")) {
- for(JustifiedSet::iterator i = d_justified.begin();
- i != d_justified.end(); ++i) {
+ for(JustifiedSet::key_iterator i = d_justified.key_begin();
+ i != d_justified.key_end(); ++i) {
TNode n = *i;
SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
d_decisionEngine->getSatLiteral(n) : -1;
typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
// being 'justified' is monotonic with respect to decisions
- context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+ context::CDHashSet<Node, NodeHashFunction> d_justified;
context::CDO<unsigned> d_prvsIndex;
IntStat d_helfulness;
Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
if(hasLiteral(n)) {
SatLiteral lit = getLiteral(n);
- LiteralToNodeMap::iterator i = d_literalToNodeMap.find(lit);
- if(i == d_literalToNodeMap.end()) {
+ if(!d_literalToNodeMap.contains(lit)){
// Store backward-mappings
- d_literalToNodeMap[lit] = n;
- d_literalToNodeMap[~lit] = n.notNode();
+ d_literalToNodeMap.insert(lit, n);
+ d_literalToNodeMap.insert(~lit, n.notNode());
}
return;
}
lit = toCNF(n, false);
// Store backward-mappings
- d_literalToNodeMap[lit] = n;
- d_literalToNodeMap[~lit] = n.notNode();
+ // These may already exist
+ d_literalToNodeMap.insert_safe(lit, n);
+ d_literalToNodeMap.insert_safe(~lit, n.notNode());
} else {
// We have a theory atom or variable.
lit = convertAtom(n);
} else {
lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
}
- d_nodeToLiteralMap[node] = lit;
- d_nodeToLiteralMap[node.notNode()] = ~lit;
+ d_nodeToLiteralMap.insert(node, lit);
+ d_nodeToLiteralMap.insert(node.notNode(), ~lit);
} else {
lit = getLiteral(node);
}
if ( theoryLiteral || d_fullLitToNodeMap ||
( CVC4_USE_REPLAY && options::replayLog() != NULL ) ||
(Dump.isOn("clauses")) ) {
- d_literalToNodeMap[lit] = node;
- d_literalToNodeMap[~lit] = node.notNode();
+
+ d_literalToNodeMap.insert_safe(lit, node);
+ d_literalToNodeMap.insert_safe(~lit, node.notNode());
}
// If a theory literal, we pre-register it
TNode CnfStream::getNode(const SatLiteral& literal) {
Debug("cnf") << "getNode(" << literal << ")" << endl;
- LiteralToNodeMap::iterator find = d_literalToNodeMap.find(literal);
- Assert(find != d_literalToNodeMap.end());
- Assert(d_nodeToLiteralMap.find((*find).second) != d_nodeToLiteralMap.end());
- Debug("cnf") << "getNode(" << literal << ") => " << (*find).second << endl;
- return (*find).second;
+ Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl;
+ return d_literalToNodeMap[literal];
}
void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
}
SatLiteral CnfStream::getLiteral(TNode node) {
- NodeToLiteralMap::iterator find = d_nodeToLiteralMap.find(node);
Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
- Assert(find != d_nodeToLiteralMap.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
- SatLiteral literal = (*find).second;
+ Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
+ SatLiteral literal = d_nodeToLiteralMap[node];
Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
return literal;
}
#include "prop/theory_proxy.h"
#include "prop/registrar.h"
#include "context/cdlist.h"
+#include "context/cdinsert_hashmap.h"
#include <ext/hash_map>
public:
/** Cache of what nodes have been registered to a literal. */
- typedef context::CDHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap;
+ typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction> LiteralToNodeMap;
/** Cache of what literals have been registered to a node. */
- typedef context::CDHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap;
+ typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction> NodeToLiteralMap;
protected:
break;
case CONST_RATIONAL:
// Mark constants as minmax
- d_minMap[n] = n.getConst<Rational>();
- d_maxMap[n] = n.getConst<Rational>();
+ d_minMap.insert(n, n.getConst<Rational>());
+ d_maxMap.insert(n, n.getConst<Rational>());
break;
case OR: {
// Look for things like "x = 0 OR x = 1" (that are defTrue) and
DeltaRational min = std::min(first, second);
CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
if (minFind == d_minMap.end() || (*minFind).second < min) {
- d_minMap[n] = min;
+ d_minMap.insert(n, min);
Node nGeqMin;
if (min.getInfinitesimalPart() == 0) {
nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
DeltaRational max = std::max(first, second);
CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
- d_maxMap[n] = max;
+ d_maxMap.insert(n, max);
Node nLeqMax;
if (max.getInfinitesimalPart() == 0) {
nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
/* fall through */
case kind::LEQ:
if (maxFind == d_maxMap.end() || (*maxFind).second > bound) {
- d_maxMap[n[0]] = bound;
+ d_maxMap.insert(n[0], bound);
Debug("arith::static") << "adding bound " << n << endl;
}
break;
/* fall through */
case kind::GEQ:
if (minFind == d_minMap.end() || (*minFind).second < bound) {
- d_minMap[n[0]] = bound;
+ d_minMap.insert(n[0], bound);
Debug("arith::static") << "adding bound " << n << endl;
}
break;
#include "context/context.h"
#include "context/cdlist.h"
-#include "context/cdhashmap.h"
+#include "context/cdtrail_hashmap.h"
#include <set>
namespace CVC4 {
* (=> _ (= x c))
* where c is a constant.
*/
- //typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
+ typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
// The domain is an implicit list OR(x, OR(y, ..., FALSE ))
// or FALSE
CDNodeToNodeListMap d_miplibTrick;
/**
* Map from a node to it's minimum and maximum.
*/
- //typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
- typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
+ typedef context::CDTrailHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
CDNodeToMinMaxMap d_minMap;
CDNodeToMinMaxMap d_maxMap;
if(assertion != reAssertion){
Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " << reAssertion << endl;
Assert(constraint != NullConstraint);
- d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint;
+ d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
}
}
#include "context/context.h"
#include "context/cdlist.h"
#include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
#include "context/cdqueue.h"
#include "expr/node.h"
* A superset of all of the assertions that currently are not the literal for
* their constraint do not match constraint literals. Not just the witnesses.
*/
- context::CDHashMap<TNode, Constraint, TNodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
+ context::CDInsertHashMap<Node, Constraint, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
/**
* (For the moment) the type hierarchy goes as:
void TheoryArrays::computeCareGraph()
{
if (d_sharedArrays.size() > 0) {
- context::CDHashSet<TNode, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+ CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end();
for (; it1 != iend; ++it1) {
for (it2 = it1, ++it2; it2 != iend; ++it2) {
if ((*it1).getType() != (*it2).getType()) {
void TheoryArrays::queueRowLemma(RowLemmaType lem)
{
- if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+ if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
return;
}
TNode a = lem.first;
for (unsigned count = 0; count < sz; ++count) {
RowLemmaType l = d_RowQueue.front();
d_RowQueue.pop();
- if (d_RowAlreadyAdded.count(l) != 0) {
+ if (d_RowAlreadyAdded.contains(l)) {
continue;
}
context::CDQueue<RowLemmaType> d_RowQueue;
context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
- context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays;
- context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
+ typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+ CDNodeSet d_sharedArrays;
+ CDNodeSet d_sharedOther;
context::CDO<bool> d_sharedTerms;
context::CDList<TNode> d_reads;
std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
/** Nodes that have been attached already (computed forward edges for) */
// All the nodes we've visited so far
- context::CDHashSet<TNode, TNodeHashFunction> d_seen;
+ context::CDHashSet<Node, NodeHashFunction> d_seen;
/**
* Assignment status of each node.
context::Context* d_context;
/** Context dependent set of atoms we already propagated */
- context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
- context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
+ context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
+ context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
BitblastSolver d_bitblastSolver;
EqualitySolver d_equalitySolver;
AlreadyNotifiedMap d_alreadyNotifiedMap;
/** The registered equalities for propagation */
- typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet;
+ typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
RegisteredEqualitiesSet d_registeredEqualities;
private:
* context-dependent set of those theory-propagable literals that
* have been propagated.
*/
- context::CDHashSet<TNode, TNodeHashFunction> d_hasPropagated;
+ context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
/**
* Statistics for a particular theory.
projects / cvc5.git / commitdiff