diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/context | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/Makefile.am | 6 | ||||
-rw-r--r-- | src/context/cdcirclist.h | 418 | ||||
-rw-r--r-- | src/context/cdcirclist_forward.h | 45 | ||||
-rw-r--r-- | src/context/cdlist.h | 9 | ||||
-rw-r--r-- | src/context/cdlist_context_memory.h | 2 | ||||
-rw-r--r-- | src/context/cdlist_forward.h | 2 | ||||
-rw-r--r-- | src/context/cdmap.h | 2 | ||||
-rw-r--r-- | src/context/cdmap_forward.h | 2 | ||||
-rw-r--r-- | src/context/cdo.h | 45 | ||||
-rw-r--r-- | src/context/cdset.h | 2 | ||||
-rw-r--r-- | src/context/cdset_forward.h | 2 | ||||
-rw-r--r-- | src/context/cdvector.h | 2 | ||||
-rw-r--r-- | src/context/context.cpp | 31 | ||||
-rw-r--r-- | src/context/context.h | 4 | ||||
-rw-r--r-- | src/context/context_mm.cpp | 2 | ||||
-rw-r--r-- | src/context/context_mm.h | 7 | ||||
-rw-r--r-- | src/context/stacking_map.h | 162 | ||||
-rw-r--r-- | src/context/stacking_vector.h | 116 |
18 files changed, 816 insertions, 43 deletions
diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 9e349a06b..ca5772d7c 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -18,4 +18,8 @@ libcontext_la_SOURCES = \ cdmap_forward.h \ cdset.h \ cdset_forward.h \ - cdvector.h + cdcirclist.h \ + cdcirclist_forward.h \ + cdvector.h \ + stacking_map.h \ + stacking_vector.h diff --git a/src/context/cdcirclist.h b/src/context/cdcirclist.h new file mode 100644 index 000000000..cc6b60217 --- /dev/null +++ b/src/context/cdcirclist.h @@ -0,0 +1,418 @@ +/********************* */ +/*! \file cdcirclist.h + ** \verbatim + ** Original author: mdeters + ** 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 Context-dependent circular list class + ** + ** Context-dependent circular list class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDCIRCLIST_H +#define __CVC4__CONTEXT__CDCIRCLIST_H + +#include <iterator> +#include <memory> +#include <string> +#include <sstream> + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdcirclist_forward.h" +#include "context/cdo.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +// CDO for pointers in particular, adds * and -> operators +template <class T> +class CDPtr : public CDO<T*> { + typedef CDO<T*> super; + + // private copy ctor + CDPtr(const CDPtr<T>& cdptr) : + super(cdptr) { + } + +public: + + CDPtr(Context* context, T* data = NULL) : + super(context, data) { + } + + CDPtr(bool allocatedInCMM, Context* context, T* data = NULL) : + super(allocatedInCMM, context, data) { + } + + // undesirable to put this here, since CDO<> does it already (?) + virtual ~CDPtr() throw(AssertionException) { this->destroy(); } + + virtual ContextObj* save(ContextMemoryManager* pCMM) { + Debug("context") << "save cdptr " << this << " (value " << super::get() << ")"; + ContextObj* p = new(pCMM) CDPtr<T>(*this); + Debug("context") << " to " << p << std::endl; + return p; + } + + virtual void restore(ContextObj* pContextObj) { + Debug("context") << "restore cdptr " << this << " (using " << pContextObj << ") from " << super::get(); + this->super::restore(pContextObj); + Debug("context") << " to " << super::get() << std::endl; + } + + CDPtr<T>& operator=(T* data) { + Debug("context") << "set " << this << " from " << super::get(); + super::set(data); + Debug("context") << " to " << super::get() << std::endl; + return *this; + } + // assignment is just like using the underlying ptr + CDPtr<T>& operator=(const CDPtr<T>& cdptr) { + return *this = cdptr.get(); + } + + T& operator*() { return *super::get(); } + T* operator->() { return super::get(); } + const T& operator*() const { return *super::get(); } + const T* operator->() const { return super::get(); } +};/* class CDPtr<T> */ + + +/** + * Class representing a single link in a CDCircList<>. + * + * The underlying T object is immutable, only the structure of the + * list is mutable, so only that's backtracked. + */ +template <class T, class AllocatorT> +class CDCircElement { + typedef CDCircElement<T, AllocatorT> elt_t; + const T d_t; + CDPtr<elt_t> d_prev; + CDPtr<elt_t> d_next; + friend class CDCircList<T, AllocatorT>; +public: + CDCircElement(Context* context, const T& t, + elt_t* prev = NULL, elt_t* next = NULL) : + d_t(t), + d_prev(true, context, prev), + d_next(true, context, next) { + } + + CDPtr<elt_t>& next() { return d_next; } + CDPtr<elt_t>& prev() { return d_prev; } + elt_t* next() const { return d_next; } + elt_t* prev() const { return d_prev; } + T element() const { return d_t; } +};/* class CDCircElement<> */ + + +/** + * Generic context-dependent circular list. Items themselves are not + * context dependent, only the forward and backward links. This + * allows two lists to be spliced together in constant time (see + * concat()). The list *structure* is mutable (things can be spliced + * in, removed, added, the list can be cleared, etc.) in a + * context-dependent manner, but the list items are immutable. To + * replace an item A in the list with B, A must be removed and + * B added in the same location. + */ +template <class T, class AllocatorT> +class CDCircList : public ContextObj { +public: + + /** List carrier element type */ + typedef CDCircElement<T, AllocatorT> elt_t; + /** The value type with which this CDCircList<> was instantiated. */ + typedef T value_type; + /** The allocator type with which this CDCircList<> was instantiated. */ + typedef AllocatorT Allocator; + +private: + + /** Head element of the circular list */ + CDPtr<elt_t> d_head; + /** The context with which we're associated */ + Context* d_context; + /** Our allocator */ + typename Allocator::template rebind< CDCircElement<T, AllocatorT> >::other d_allocator; + +public: + + CDCircList(Context* context, const Allocator& alloc = Allocator()) : + ContextObj(context), + d_head(context, NULL), + d_context(context), + d_allocator(alloc) { + } + + CDCircList(bool allocatedInCMM, Context* context, const Allocator& alloc = Allocator()) : + ContextObj(allocatedInCMM, context), + d_head(allocatedInCMM, context, NULL), + d_context(context), + d_allocator(alloc) { + Debug("cdcirclist") << "head " << &d_head << " in cmm ? " << allocatedInCMM << std::endl; + } + + ~CDCircList() throw(AssertionException) { + // by context contract, call destroy() here + destroy(); + } + + void clear() { + d_head = NULL; + } + + bool empty() const { + return d_head == NULL; + } + + CDPtr<elt_t>& head() { + return d_head; + } + + CDPtr<elt_t>& tail() { + return empty() ? d_head : d_head->d_prev; + } + + const elt_t* head() const { + return d_head; + } + + const elt_t* tail() const { + return empty() ? d_head : d_head->d_prev; + } + + T front() const { + Assert(! empty()); + return head()->element(); + } + + T back() const { + Assert(! empty()); + return tail()->element(); + } + + void push_back(const T& t) { + if(Debug.isOn("cdcirclist:paranoid")) { + debugCheck(); + } + // FIXME LEAK! (should alloc in CMM, no?) + elt_t* x = d_allocator.allocate(1); + if(empty()) { + // zero-element case + new(x) elt_t(d_context, t, x, x); + d_head = x; + } else { + // N-element case + new(x) elt_t(d_context, t, d_head->d_prev, d_head); + d_head->d_prev->d_next = x; + d_head->d_prev = x; + } + } + + /** + * Concatenate two lists. This modifies both: afterward, the two + * lists might have different heads, but they will have the same + * elements in the same (circular) order. + */ + void concat(CDCircList<T, AllocatorT>& l) { + Assert(this != &l, "cannot concat a list with itself"); + + if(d_head == NULL) { + d_head = l.d_head; + return; + } else if(l.d_head == NULL) { + l.d_head = d_head; + return; + } + + // splice together the two circular lists + CDPtr<elt_t> &l1head = head(), &l2head = l.head(); + CDPtr<elt_t> &l1tail = tail(), &l2tail = l.tail(); + // l2tail will change underneath us in what's below (because it's + // the same as l2head->prev()), so we have to keep a regular + // pointer to it + elt_t* oldl2tail = l2tail; + + Debug("cdcirclist") << "concat1 " << this << " " << &l << std::endl; + l1tail->next() = l2head; + Debug("cdcirclist") << "concat2" << std::endl; + l2head->prev() = l1tail; + + Debug("cdcirclist") << "concat3" << std::endl; + oldl2tail->next() = l1head; + Debug("cdcirclist") << "concat4" << std::endl; + l1head->prev() = oldl2tail; + Debug("cdcirclist") << "concat5" << std::endl; + } + + class iterator { + const CDCircList<T, AllocatorT>* d_list; + const elt_t* d_current; + friend class CDCircList<T, AllocatorT>; + public: + iterator(const CDCircList<T, AllocatorT>* list, const elt_t* first) : + d_list(list), + d_current(first) { + } + iterator(const iterator& other) : + d_list(other.d_list), + d_current(other.d_current) { + } + + bool operator==(const iterator& other) const { + return d_list == other.d_list && d_current == other.d_current; + } + bool operator!=(const iterator& other) const { + return !(*this == other); + } + iterator& operator++() { + Assert(d_current != NULL, "iterator already off the end"); + if(d_current == d_list->tail()) { + d_current = NULL; + } else { + d_current = d_current->next(); + } + return *this; + } + iterator operator++(int) { + const elt_t* old = d_current; + ++*this; + return iterator(d_list, old); + } + iterator& operator--() { + // undefined to go off the beginning, but don't have a check for that + if(d_current == NULL) { + d_current = d_list->tail(); + } else { + d_current = d_current->prev(); + } + return *this; + } + iterator operator--(int) { + const elt_t* old = d_current; + --*this; + return iterator(d_list, old); + } + T operator*() { + Assert(d_current != NULL, "iterator already off the end"); + return d_current->element(); + } + };/* class CDCircList<>::iterator */ + + // list elements are immutable + typedef iterator const_iterator; + + iterator begin() { + if(Debug.isOn("cdcirclist:paranoid")) { + debugCheck(); + } + return iterator(this, head()); + } + + iterator end() { + if(Debug.isOn("cdcirclist:paranoid")) { + debugCheck(); + } + return iterator(this, NULL); + } + + const_iterator begin() const { + return const_iterator(this, head()); + } + + const_iterator end() const { + return const_iterator(this, NULL); + } + + iterator erase(iterator pos) { + Assert(pos.d_current != NULL); + if(pos.d_current->prev() == pos.d_current) { + // one-elt list + d_head = NULL; + return iterator(this, NULL); + } else { + // N-elt list + if(pos.d_current == d_head) { + // removing list head + elt_t *pHead = head(), *pTail = tail(); + pTail->next() = pHead->next(); + pHead->next()->prev() = pTail; + d_head = pHead->next(); + return iterator(this, d_head); + // can't free old head, because of backtracking + } else { + // not removing list head + const elt_t *elt = pos.d_current; + elt_t *prev = pos.d_current->prev(); + prev->next() = elt->next(); + elt->next()->prev() = prev; + return iterator(this, elt->next()); + // can't free elt, because of backtracking + } + } + } + +private: + + // do not permit copy/assignment + CDCircList(const CDCircList<T, AllocatorT>&) CVC4_UNUSED; + CDCircList<T, AllocatorT>& operator=(const CDCircList<T, AllocatorT>&) CVC4_UNUSED; + +public: + /** Check internal structure and invariants of the list */ + void debugCheck() const { + elt_t* p = d_head; + Debug("cdcirclist") << "this is " << this << std::endl; + if(p == NULL) { + Debug("cdcirclist") << "head[" << &d_head << "] is NULL : " << d_context->getLevel() << std::endl; + // empty list + return; + } + Debug("cdcirclist") << "head[" << &d_head << "] is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << d_context->getLevel() << std::endl;//p->d_t << std::endl; + do { + elt_t* p_last = p; + p = p->d_next; + if(p == NULL) { + Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, next == NULL ******" << std::endl; + break; + } + Debug("cdcirclist") << " p is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << std::endl;//p->d_t << std::endl; + if(p->d_prev != p_last) { + Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, prev != last ******" << std::endl; + } + //Assert(p->d_prev == p_last); + Assert(p != NULL); + } while(p != d_head); + } + +private: + + // Nothing to save; the elements take care of themselves + virtual ContextObj* save(ContextMemoryManager* pCMM) { + Unreachable(); + } + + // Similarly, nothing to restore + virtual void restore(ContextObj* data) { + Unreachable(); + } + +};/* class CDCircList<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDCIRCLIST_H */ diff --git a/src/context/cdcirclist_forward.h b/src/context/cdcirclist_forward.h new file mode 100644 index 000000000..56a39e96f --- /dev/null +++ b/src/context/cdcirclist_forward.h @@ -0,0 +1,45 @@ +/********************* */ +/*! \file cdcirclist_forward.h + ** \verbatim + ** Original author: mdeters + ** 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 a forward declaration header to declare the + ** CDCircList<> template + ** + ** This is a forward declaration header to declare the CDCircList<> + ** template. It's useful if you want to forward-declare CDCircList<> + ** without including the full cdcirclist.h header, for example, in a + ** public header context, or to keep compile times low when only a + ** forward declaration is needed. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H +#define __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H + +#include <memory> + +namespace __gnu_cxx { + template <class Key> struct hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template <class T> + class ContextMemoryAllocator; + + template <class T, class Allocator = ContextMemoryAllocator<T> > + class CDCircList; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H */ diff --git a/src/context/cdlist.h b/src/context/cdlist.h index c999ecadb..dea9f8be7 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -3,17 +3,18 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): barrett, taking + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 Context-dependent list class. + ** \brief Context-dependent list class (only supports append) ** - ** Context-dependent list class. + ** Context-dependent list class. This list only supports appending + ** to the list; on backtrack, the list is simply shortened. **/ #include "cvc4_private.h" diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h index 45a44756d..fcb51fe20 100644 --- a/src/context/cdlist_context_memory.h +++ b/src/context/cdlist_context_memory.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h index a1e50c7c8..90c439085 100644 --- a/src/context/cdlist_forward.h +++ b/src/context/cdlist_forward.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdmap.h b/src/context/cdmap.h index c71459835..3ac99f729 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h index 214d9e700..331d6a93e 100644 --- a/src/context/cdmap_forward.h +++ b/src/context/cdmap_forward.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdo.h b/src/context/cdo.h index f4c4a7e29..025e8e337 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -40,13 +40,29 @@ class CDO : public ContextObj { */ T d_data; +protected: + + /** + * Copy constructor - it's private to ensure it is only used by save(). + * Basic CDO objects, cannot be copied-they have to be unique. + */ + CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {} + + /** + * operator= for CDO is private to ensure CDO object is not copied. + */ + CDO<T>& operator=(const CDO<T>& cdo) CVC4_UNUSED; + /** * Implementation of mandatory ContextObj method save: simply copies the * current data to a copy using the copy constructor. Memory is allocated * using the ContextMemoryManager. */ virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDO<T>(*this); + Debug("context") << "save cdo " << this << " (value " << get() << ")"; + ContextObj* p = new(pCMM) CDO<T>(*this); + Debug("context") << " to " << p << std::endl; + return p; } /** @@ -54,20 +70,11 @@ class CDO : public ContextObj { * saved data back from the saved copy using operator= for T. */ virtual void restore(ContextObj* pContextObj) { + //Debug("context") << "restore cdo " << this << " from " << get(); d_data = ((CDO<T>*) pContextObj)->d_data; + //Debug("context") << " to " << get() << std::endl; } - /** - * Copy constructor - it's private to ensure it is only used by save(). - * Basic CDO objects, cannot be copied-they have to be unique. - */ - CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {} - - /** - * operator= for CDO is private to ensure CDO object is not copied. - */ - CDO<T>& operator=(const CDO<T>& cdo); - public: /** @@ -75,7 +82,8 @@ public: * value of d_data. */ CDO(Context* context) : - ContextObj(context) { + ContextObj(context), + d_data(T()) { } /** @@ -90,7 +98,8 @@ public: * allocating contextual objects with non-standard allocators." */ CDO(bool allocatedInCMM, Context* context) : - ContextObj(allocatedInCMM, context) { + ContextObj(allocatedInCMM, context), + d_data(T()) { } /** @@ -100,7 +109,8 @@ public: * is assigned by the default constructor for T */ CDO(Context* context, const T& data) : - ContextObj(context) { + ContextObj(context), + d_data(T()) { makeCurrent(); d_data = data; } @@ -119,7 +129,8 @@ public: * allocating contextual objects with non-standard allocators." */ CDO(bool allocatedInCMM, Context* context, const T& data) : - ContextObj(allocatedInCMM, context) { + ContextObj(allocatedInCMM, context), + d_data(T()) { makeCurrent(); d_data = data; } diff --git a/src/context/cdset.h b/src/context/cdset.h index 268c3127b..8699d9cf4 100644 --- a/src/context/cdset.h +++ b/src/context/cdset.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdset_forward.h b/src/context/cdset_forward.h index af3c6f85c..2339552a6 100644 --- a/src/context/cdset_forward.h +++ b/src/context/cdset_forward.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdvector.h b/src/context/cdvector.h index cb86d5c4d..49d1b67e9 100644 --- a/src/context/cdvector.h +++ b/src/context/cdvector.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/context.cpp b/src/context/context.cpp index 9b40e9780..2b220d5b4 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -5,7 +5,7 @@ ** Major contributors: barrett ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -78,8 +78,10 @@ void Context::pop() { // Notify the (pre-pop) ContextNotifyObj objects ContextNotifyObj* pCNO = d_pCNOpre; while(pCNO != NULL) { + // pre-store the "next" pointer in case pCNO deletes itself on notify() + ContextNotifyObj* next = pCNO->d_pCNOnext; pCNO->notify(); - pCNO = pCNO->d_pCNOnext; + pCNO = next; } // Grab the top Scope @@ -97,8 +99,10 @@ void Context::pop() { // Notify the (post-pop) ContextNotifyObj objects pCNO = d_pCNOpost; while(pCNO != NULL) { + // pre-store the "next" pointer in case pCNO deletes itself on notify() + ContextNotifyObj* next = pCNO->d_pCNOnext; pCNO->notify(); - pCNO = pCNO->d_pCNOnext; + pCNO = next; } Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to " @@ -135,6 +139,7 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) { void ContextObj::update() throw(AssertionException) { Debug("context") << "before update(" << this << "):" << std::endl + << "context is " << getContext() << std::endl << *getContext() << std::endl; // Call save() to save the information in the current object @@ -203,6 +208,7 @@ ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) { // Assert(d_pScope == d_pScope->getContext()->getBottomScope(), // "Expected bottom scope"); + Debug("context") << "NULL restore object! " << this << std::endl; pContextObjNext = d_pContextObjNext; // Nothing else to do @@ -261,22 +267,28 @@ void ContextObj::destroy() throw(AssertionException) { ContextObj::ContextObj(Context* pContext) : - d_pContextObjRestore(NULL) { + d_pScope(NULL), + d_pContextObjRestore(NULL), + d_pContextObjNext(NULL), + d_ppContextObjPrev(NULL) { Assert(pContext != NULL, "NULL context pointer"); - Debug("context") << "create new ContextObj(" << this << ")" << std::endl; + Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl; d_pScope = pContext->getBottomScope(); d_pScope->addToChain(this); } ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) : - d_pContextObjRestore(NULL) { + d_pScope(NULL), + d_pContextObjRestore(NULL), + d_pContextObjNext(NULL), + d_ppContextObjPrev(NULL) { Assert(pContext != NULL, "NULL context pointer"); - Debug("context") << "create new ContextObj(" << this << ")" << std::endl; + Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl; if(allocatedInCMM) { d_pScope = pContext->getTopScope(); } else { @@ -326,12 +338,15 @@ std::ostream& operator<<(std::ostream& out, std::ostream& operator<<(std::ostream& out, const Scope& scope) throw(AssertionException) { - out << "Scope " << scope.d_level << ":"; + out << "Scope " << scope.d_level << " [" << &scope << "]:"; ContextObj* pContextObj = scope.d_pContextObjList; Assert(pContextObj == NULL || pContextObj->prev() == &scope.d_pContextObjList); while(pContextObj != NULL) { out << " <--> " << pContextObj; + if(pContextObj->d_pScope != &scope) { + out << " XXX bad scope" << std::endl; + } Assert(pContextObj->d_pScope == &scope); Assert(pContextObj->next() == NULL || pContextObj->next()->prev() == &pContextObj->next()); diff --git a/src/context/context.h b/src/context/context.h index 34107ef29..1e69964a0 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: barrett - ** Minor contributors (to current version): taking, dejan + ** Minor contributors (to current version): dejan, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index fde69a149..aea2fe9c2 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 56ef7ab59..66db21424 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -161,10 +161,11 @@ public: }; ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {} - ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.d_mm) {} + template <class U> + ContextMemoryAllocator(const ContextMemoryAllocator<U>& alloc) throw() : d_mm(alloc.getCMM()) {} ~ContextMemoryAllocator() throw() {} - ContextMemoryManager* getCMM() { return d_mm; } + ContextMemoryManager* getCMM() const { return d_mm; } T* address(T& v) const { return &v; } T const* address(T const& v) const { return &v; } size_t max_size() const throw() { diff --git a/src/context/stacking_map.h b/src/context/stacking_map.h new file mode 100644 index 000000000..2dec1845c --- /dev/null +++ b/src/context/stacking_map.h @@ -0,0 +1,162 @@ +/********************* */ +/*! \file stacking_map.h + ** \verbatim + ** Original author: mdeters + ** 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 Backtrackable map using an undo stack + ** + ** Backtrackable map using an undo stack rather than storing items in + ** a CDMap<>. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__STACKING_MAP_H +#define __CVC4__CONTEXT__STACKING_MAP_H + +#include <utility> +#include <vector> +#include <ext/hash_map> + +#include "expr/node.h" +#include "context/cdo.h" + +namespace CVC4 { +namespace context { + +template <class T> +struct StackingMapArgType { + typedef T argtype; +};/* struct StackingMapArgType<T> */ + +template <> +struct StackingMapArgType<Node> { + typedef TNode argtype; +};/* struct StackingMapArgType<Node> */ + + +template <class KeyType, class ValueType, class KeyHash> +struct StackingMapRestoreValue { + typedef typename StackingMapArgType<KeyType>::argtype ArgType; + static void restore(__gnu_cxx::hash_map<KeyType, ValueType, KeyHash>& map, const ArgType& k, const ValueType& v) { + map[k] = v; + } +};/* struct StackingMapRestoreValue<KeyType, ValueType, KeyHash> */ + +template <class KeyType, class KeyHash> +struct StackingMapRestoreValue<KeyType, Node, KeyHash> { + typedef typename StackingMapArgType<KeyType>::argtype ArgType; + static void restore(__gnu_cxx::hash_map<KeyType, Node, KeyHash>& map, const ArgType& k, TNode v) { + if(v.isNull()) { + map.erase(k); + } else { + map[k] = v; + } + } +};/* struct StackingMapRestoreValue<KeyType, Node, KeyHash> */ + +template <class KeyType, class KeyHash> +struct StackingMapRestoreValue<KeyType, TNode, KeyHash> { + typedef typename StackingMapArgType<KeyType>::argtype ArgType; + static void restore(__gnu_cxx::hash_map<KeyType, TNode, KeyHash>& map, const ArgType& k, TNode v) { + if(v.isNull()) { + map.erase(k); + } else { + map[k] = v; + } + } +};/* struct StackingMapRestoreValue<KeyType, TNode, KeyHash> */ + + +template <class KeyType, class ValueType, class KeyHash> +class StackingMap : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef __gnu_cxx::hash_map<KeyType, ValueType, KeyHash> MapType; + + /** + * The type for arguments being passed in. It's the same as + * KeyType, unless KeyType is Node, then it's TNode for efficiency. + */ + typedef typename StackingMapArgType<KeyType>::argtype ArgType; + + /** Our map of keys to their values. */ + MapType d_map; + + /** Our undo stack for changes made to d_map. */ + std::vector<std::pair<ArgType, ValueType> > d_trace; + + /** Our current offset in the d_trace stack (context-dependent). */ + context::CDO<size_t> d_offset; + +public: + typedef typename MapType::const_iterator const_iterator; + + StackingMap(context::Context* ctxt) : + context::ContextNotifyObj(ctxt), + d_offset(ctxt, 0) { + } + + ~StackingMap() throw() { } + + const_iterator find(ArgType n) const { return d_map.find(n); } + const_iterator end() const { return d_map.end(); } + + /** + * Return a key's value in the key-value map. If n is not a key in + * the map, this function returns a default-constructed value. + */ + ValueType operator[](ArgType n) const { + const_iterator it = find(n); + if(it == end()) { + return ValueType(); + } else { + return (*it).second; + } + } + //ValueType& operator[](ArgType n) { return d_map[n]; }// not permitted--bypasses set() logic + + /** + * Set the value in the key-value map for Node n to newValue. + */ + void set(ArgType n, const ValueType& newValue); + + /** + * Called by the Context when a pop occurs. Cancels everything to the + * current context level. Overrides ContextNotifyObj::notify(). + */ + void notify(); + +};/* class StackingMap<> */ + +template <class KeyType, class ValueType, class KeyHash> +void StackingMap<KeyType, ValueType, KeyHash>::set(ArgType n, const ValueType& newValue) { + Trace("sm") << "SM setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl; + ValueType& ref = d_map[n]; + d_trace.push_back(std::make_pair(n, ValueType(ref))); + d_offset = d_trace.size(); + ref = newValue; +} + +template <class KeyType, class ValueType, class KeyHash> +void StackingMap<KeyType, ValueType, KeyHash>::notify() { + Trace("sm") << "SM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; + while(d_offset < d_trace.size()) { + std::pair<ArgType, ValueType> p = d_trace.back(); + StackingMapRestoreValue<KeyType, ValueType, KeyHash>::restore(d_map, p.first, p.second); + d_trace.pop_back(); + } + Trace("sm") << "SM cancelling finished." << std::endl; +} + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /*__CVC4__CONTEXT__STACKING_MAP_H */ diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h new file mode 100644 index 000000000..9987731d4 --- /dev/null +++ b/src/context/stacking_vector.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file stacking_vector.h + ** \verbatim + ** Original author: mdeters + ** 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 Backtrackable vector using an undo stack + ** + ** Backtrackable vector using an undo stack rather than storing items in + ** a CDVector<>. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__STACKING_VECTOR_H +#define __CVC4__CONTEXT__STACKING_VECTOR_H + +#include <utility> +#include <vector> + +#include "context/cdo.h" + +namespace CVC4 { +namespace context { + +template <class T> +class StackingVector : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef std::vector<T> VectorType; + + /** Our map of indices to their values. */ + VectorType d_map; + + /** Our undo stack for changes made to d_map. */ + std::vector<std::pair<size_t, T> > d_trace; + + /** Our current offset in the d_trace stack (context-dependent). */ + context::CDO<size_t> d_offset; + +public: + typedef typename VectorType::const_iterator const_iterator; + + StackingVector(context::Context* ctxt) : + context::ContextNotifyObj(ctxt), + d_offset(ctxt, 0) { + } + + ~StackingVector() throw() { } + + /** + * Return a value from the vector. If n is not a key in + * the map, this function returns a default-constructed T. + */ + T operator[](size_t n) const { + return n < d_map.size() ? d_map[n] : T(); + } + //T& operator[](ArgType n) { return d_map[n]; }// not permitted--bypasses set() logic + + /** + * Set the value in the key-value map for Node n to newValue. + */ + void set(size_t n, const T& newValue); + + /** + * Return the current size of the vector. Note that once a certain + * size is achieved, the size never goes down again, although the + * elements off the old end of the vector will be replaced with + * default-constructed T values. + */ + size_t size() const { + return d_map.size(); + } + + /** + * Called by the Context when a pop occurs. Cancels everything to the + * current context level. Overrides ContextNotifyObj::notify(). + */ + void notify(); + +};/* class StackingVector<> */ + +template <class T> +void StackingVector<T>::set(size_t n, const T& newValue) { + Trace("sv") << "SV setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl; + if(n >= d_map.size()) { + d_map.resize(n + 1); + } + T& ref = d_map[n]; + d_trace.push_back(std::make_pair(n, T(ref))); + d_offset = d_trace.size(); + ref = newValue; +} + +template <class T> +void StackingVector<T>::notify() { + Trace("sv") << "SV cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; + while(d_offset < d_trace.size()) { + std::pair<size_t, T> p = d_trace.back(); + Trace("sv") << "SV cancelling: " << p.first << " back to " << p.second << std::endl; + d_map[p.first] = p.second; + d_trace.pop_back(); + } + Trace("sv") << "SV cancelling finished." << std::endl; +} + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /*__CVC4__CONTEXT__STACKING_VECTOR_H */ |