cd "\`dirname \\"\$0\\"\`"
+if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
+
current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
arch=\${current[0]}
build=\${current[1]}
context_mm.h \
cdo.h \
cdlist.h \
+ cdlist_context_memory.h \
+ cdlist_forward.h \
cdmap.h \
+ cdmap_forward.h \
cdset.h \
+ cdset_forward.h \
cdvector.h
#define __CVC4__CONTEXT__CDLIST_H
#include <iterator>
+#include <memory>
+#include <string>
+#include <sstream>
#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdlist_forward.h"
#include "util/Assert.h"
namespace CVC4 {
namespace context {
/**
- * Generic context-dependent dynamic array. Note that for efficiency, this
- * implementation makes the following assumptions:
+ * Generic context-dependent dynamic array. Note that for efficiency,
+ * this implementation makes the following assumptions:
+ *
* 1. Over time, objects are only added to the list. Objects are only
* removed when a pop restores the list to a previous state.
+ *
* 2. T objects can safely be copied using their copy constructor,
* operator=, and memcpy.
*/
-template <class T>
+template <class T, class AllocatorT>
class CDList : public ContextObj {
+public:
+
+ /** The value type with which this CDList<> was instantiated. */
+ typedef T value_type;
+ /** The allocator type with which this CDList<> was instantiated. */
+ typedef AllocatorT Allocator;
+
+protected:
+
+ static const size_t INITIAL_SIZE = 10;
+ static const size_t GROWTH_FACTOR = 2;
+
/**
* d_list is a dynamic array of objects of type T.
*/
/**
* Number of objects in d_list
*/
- unsigned d_size;
+ size_t d_size;
/**
* Allocated size of d_list.
*/
- unsigned d_sizeAlloc;
-
-protected:
+ size_t d_sizeAlloc;
/**
- * Implementation of mandatory ContextObj method save: simply copies the
- * current size 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.
+ * Our allocator.
*/
- ContextObj* save(ContextMemoryManager* pCMM) {
- return new(pCMM) CDList<T>(*this);
- }
-
- /**
- * 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) {
- if(d_callDestructor) {
- unsigned size = ((CDList<T>*)data)->d_size;
- while(d_size != size) {
- --d_size;
- d_list[d_size].~T();
- }
- } else {
- d_size = ((CDList<T>*)data)->d_size;
- }
- }
-
-private:
+ Allocator d_allocator;
/**
- * Private copy constructor used only by save above. d_list and d_sizeAlloc
- * are not copied: only the base class information and d_size are needed in
- * restore.
+ * Private copy constructor used only by save(). d_list and
+ * d_sizeAlloc are not copied: only the base class information and
+ * d_size are needed in restore.
*/
- CDList(const CDList<T>& l) :
+ CDList(const CDList<T, Allocator>& l) :
ContextObj(l),
d_list(NULL),
- d_callDestructor(l.d_callDestructor),
+ d_callDestructor(false),
d_size(l.d_size),
- d_sizeAlloc(0) {
+ d_sizeAlloc(0),
+ d_allocator(l.d_allocator) {
+ Debug("cdlist") << "copy ctor: " << this
+ << " from " << &l
+ << " size " << d_size << std::endl;
}
/**
void grow() {
if(d_list == NULL) {
// Allocate an initial list if one does not yet exist
- d_sizeAlloc = 10;
- d_list = (T*) malloc(sizeof(T) * d_sizeAlloc);
+ d_sizeAlloc = INITIAL_SIZE;
+ Debug("cdlist") << "initial grow of cdlist " << this
+ << " level " << getContext()->getLevel()
+ << " to " << d_sizeAlloc << std::endl;
+ if(d_sizeAlloc > d_allocator.max_size()) {
+ d_sizeAlloc = d_allocator.max_size();
+ }
+ d_list = d_allocator.allocate(d_sizeAlloc);
if(d_list == NULL) {
throw std::bad_alloc();
}
} else {
// Allocate a new array with double the size
- d_sizeAlloc *= 2;
- T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc);
- if(tmpList == NULL) {
+ size_t newSize = GROWTH_FACTOR * d_sizeAlloc;
+ if(newSize > d_allocator.max_size()) {
+ newSize = d_allocator.max_size();
+ Assert(newSize > d_sizeAlloc,
+ "cannot request larger list due to allocator limits");
+ }
+ T* newList = d_allocator.allocate(newSize);
+ Debug("cdlist") << "2x grow of cdlist " << this
+ << " level " << getContext()->getLevel()
+ << " to " << newSize
+ << " (from " << d_list
+ << " to " << newList << ")" << std::endl;
+ if(newList == NULL) {
throw std::bad_alloc();
}
- d_list = tmpList;
+ std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc);
+ d_allocator.deallocate(d_list, d_sizeAlloc);
+ d_list = newList;
+ d_sizeAlloc = newSize;
+ }
+ }
+
+ /**
+ * Implementation of mandatory ContextObj method save: simply copies
+ * the current size 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) CDList<T, Allocator>(*this);
+ Debug("cdlist") << "save " << this
+ << " at level " << this->getContext()->getLevel()
+ << " size at " << this->d_size
+ << " sizeAlloc at " << this->d_sizeAlloc
+ << " d_list is " << this->d_list
+ << " data:" << data << std::endl;
+ return data;
+ }
+
+ /**
+ * 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("cdlist") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " data == " << data
+ << " call dtor == " << this->d_callDestructor
+ << " d_list == " << this->d_list << std::endl;
+ if(this->d_callDestructor) {
+ const size_t size = ((CDList<T, Allocator>*)data)->d_size;
+ while(this->d_size != size) {
+ --this->d_size;
+ this->d_allocator.destroy(&this->d_list[this->d_size]);
+ }
+ } else {
+ this->d_size = ((CDList<T, Allocator>*)data)->d_size;
}
+ Debug("cdlist") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " size back to " << this->d_size
+ << " sizeAlloc at " << this->d_sizeAlloc << std::endl;
}
public:
+
/**
* Main constructor: d_list starts as NULL, size is 0
*/
- CDList(Context* context, bool callDestructor = true) :
+ CDList(Context* context, bool callDestructor = true,
+ const Allocator& alloc = Allocator()) :
ContextObj(context),
d_list(NULL),
d_callDestructor(callDestructor),
d_size(0),
- d_sizeAlloc(0) {
+ d_sizeAlloc(0),
+ d_allocator(alloc) {
}
/**
* Main constructor: d_list starts as NULL, size is 0
*/
- CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
+ CDList(bool allocatedInCMM, Context* context, bool callDestructor = true,
+ const Allocator& alloc = Allocator()) :
ContextObj(allocatedInCMM, context),
d_list(NULL),
d_callDestructor(callDestructor),
d_size(0),
- d_sizeAlloc(0) {
+ d_sizeAlloc(0),
+ d_allocator(alloc) {
}
/**
* Destructor: delete the list
*/
~CDList() throw(AssertionException) {
- destroy();
+ this->destroy();
- if(d_callDestructor) {
- for(unsigned i = 0; i < d_size; ++i) {
- d_list[i].~T();
+ if(this->d_callDestructor) {
+ for(size_t i = 0; i < this->d_size; ++i) {
+ this->d_allocator.destroy(&this->d_list[i]);
}
}
- free(d_list);
+ this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc);
}
/**
- * Return the current size of (i.e. valid number of objects in) the list
+ * Return the current size of (i.e. valid number of objects in) the
+ * list.
*/
- unsigned size() const {
+ size_t size() const {
return d_size;
}
* Add an item to the end of the list.
*/
void push_back(const T& data) {
+ Debug("cdlist") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": make-current, "
+ << "d_list == " << d_list << std::endl;
makeCurrent();
+ Debug("cdlist") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": grow? " << d_size
+ << " " << d_sizeAlloc << std::endl;
if(d_size == d_sizeAlloc) {
+ Debug("cdlist") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": grow!" << std::endl;
grow();
}
-
- ::new((void*)(d_list + d_size)) T(data);
+ Assert(d_size < d_sizeAlloc);
+
+ Debug("cdlist") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": construct! at " << d_list
+ << "[" << d_size << "] == " << &d_list[d_size]
+ << std::endl;
+ d_allocator.construct(&d_list[d_size], data);
+ Debug("cdlist") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": done..." << std::endl;
++d_size;
+ Debug("cdlist") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": size now " << d_size << std::endl;
}
/**
* Access to the ith item in the list.
*/
- const T& operator[](unsigned i) const {
+ const T& operator[](size_t i) const {
Assert(i < d_size, "index out of bounds in CDList::operator[]");
return d_list[i];
}
}
/**
- * Iterator for CDList class. It has to be const because we don't allow
- * items in the list to be changed. It's a straightforward wrapper around a
- * pointer. Note that for efficiency, we implement only prefix increment and
- * decrement. Also note that it's OK to create an iterator from an empty,
- * uninitialized list, as begin() and end() will have the same value (NULL).
+ * Iterator for CDList class. It has to be const because we don't
+ * allow items in the list to be changed. It's a straightforward
+ * wrapper around a pointer. Note that for efficiency, we implement
+ * only prefix increment and decrement. Also note that it's OK to
+ * create an iterator from an empty, uninitialized list, as begin()
+ * and end() will have the same value (NULL).
*/
class const_iterator {
- T* d_it;
+ T const* d_it;
- const_iterator(T* it) : d_it(it) {}
+ const_iterator(T const* it) : d_it(it) {}
- friend class CDList<T>;
+ friend class CDList<T, Allocator>;
public:
+ // FIXME we support operator--, but do we satisfy all the
+ // requirements of a bidirectional iterator ?
typedef std::input_iterator_tag iterator_category;
typedef T value_type;
typedef ptrdiff_t difference_type;
* Returns an iterator pointing to the first item in the list.
*/
const_iterator begin() const {
- return const_iterator(d_list);
+ return const_iterator(static_cast<T const*>(d_list));
}
/**
* Returns an iterator pointing one past the last item in the list.
*/
const_iterator end() const {
- return const_iterator(d_list + d_size);
+ return const_iterator(static_cast<T const*>(d_list) + d_size);
}
-
-};/* class CDList */
+};/* class CDList<> */
}/* CVC4::context namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file cdlist_context_memory.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 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 specialized for use with a
+ ** context memory allocator.
+ **
+ ** Context-dependent list class specialized for use with a context
+ ** memory allocator.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H
+#define __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H
+
+#include <iterator>
+#include <memory>
+
+#include "context/cdlist_forward.h"
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * Generic context-dependent dynamic array. Like the usual CDList<>,
+ * but allocates all memory from context memory. Elements are kept in
+ * cascading "list segments." Access to elements is not O(1) but
+ * O(log n). As with CDList<>, update is not permitted, only
+ * appending to the end of the list.
+ */
+template <class T>
+class CDList<T, ContextMemoryAllocator<T> > : public ContextObj {
+public:
+
+ /** The value type with which this CDList<> was instantiated. */
+ typedef T value_type;
+ /** The allocator type with which this CDList<> was instantiated. */
+ typedef ContextMemoryAllocator<T> Allocator;
+
+protected:
+
+ static const size_t INITIAL_SEGMENT_SIZE = 10;
+ static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
+
+ /**
+ * ListSegment is itself allocated in Context memory, but it is
+ * never updated; it serves as information about the d_list segment
+ * pointer it contains only.
+ */
+ class ListSegment {
+ ListSegment* d_nextSegment;
+ size_t d_segmentSize;
+ T* d_list;
+ public:
+ ListSegment() :
+ d_nextSegment(NULL),
+ d_segmentSize(0),
+ d_list(NULL) {
+ }
+ void initialize(T* list) {
+ Assert( d_nextSegment == NULL &&
+ d_segmentSize == 0 &&
+ d_list == NULL,
+ "Double-initialization of ListSegment not permitted" );
+ d_list = list;
+ }
+ void linkTo(ListSegment* nextSegment) {
+ Assert( d_nextSegment == NULL,
+ "Double-linking of ListSegment not permitted" );
+ d_nextSegment = nextSegment;
+ }
+ void cutLink() {
+ d_nextSegment = NULL;
+ }
+ ListSegment* getNextSegment() const { return d_nextSegment; }
+ size_t& size() { return d_segmentSize; }
+ size_t size() const { return d_segmentSize; }
+ const T* list() const { return d_list; }
+ T& operator[](size_t i) { return d_list[i]; }
+ const T& operator[](size_t i) const { return d_list[i]; }
+ };/* struct CDList<T, ContextMemoryAllocator<T> >::ListSegment */
+
+ /**
+ * The first segment of list memory.
+ */
+ ListSegment d_headSegment;
+
+ /**
+ * A pointer to the final segment of list memory.
+ */
+ ListSegment* d_tailSegment;
+
+ /**
+ * Whether to call the destructor when items are popped from the
+ * list. True by default, but can be set to false by setting the
+ * second argument in the constructor to false.
+ */
+ bool d_callDestructor;
+
+ /**
+ * Number of objects in list across all segments.
+ */
+ size_t d_size;
+
+ /**
+ * Total allocated size across all segments.
+ */
+ size_t d_totalSizeAlloc;
+
+ /**
+ * Our allocator.
+ */
+ Allocator d_allocator;
+
+ /**
+ * Lightweight save object for CDList<T, ContextMemoryAllocator<T> >.
+ */
+ struct CDListSave : public ContextObj {
+ ListSegment* d_tail;
+ size_t d_tailSize, d_size, d_sizeAlloc;
+ CDListSave(const CDList<T, Allocator>& list, ListSegment* tail,
+ size_t size, size_t sizeAlloc) :
+ ContextObj(list),
+ d_tail(tail),
+ d_tailSize(tail->size()),
+ d_size(size),
+ d_sizeAlloc(sizeAlloc) {
+ }
+ ~CDListSave() {
+ this->destroy();
+ }
+ ContextObj* save(ContextMemoryManager* pCMM) {
+ // This type of object _is_ the save/restore object. It isn't
+ // itself saved or restored.
+ Unreachable();
+ }
+ void restore(ContextObj* data) {
+ // This type of object _is_ the save/restore object. It isn't
+ // itself saved or restored.
+ Unreachable();
+ }
+ };/* struct CDList<T, ContextMemoryAllocator<T> >::CDListSave */
+
+ /**
+ * Private copy constructor undefined (no copy permitted).
+ */
+ CDList(const CDList<T, Allocator>& l);
+
+ /**
+ * Allocate the first list segment.
+ */
+ void allocateHeadSegment() {
+ Assert(d_headSegment.list() == NULL);
+ Assert(d_totalSizeAlloc == 0 && d_size == 0);
+
+ // Allocate an initial list if one does not yet exist
+ size_t newSize = INITIAL_SEGMENT_SIZE;
+ Debug("cdlist:cmm") << "initial grow of cdlist " << this
+ << " level " << getContext()->getLevel()
+ << " to " << newSize << std::endl;
+ if(newSize > d_allocator.max_size()) {
+ newSize = d_allocator.max_size();
+ }
+ T* newList = d_allocator.allocate(newSize);
+ if(newList == NULL) {
+ throw std::bad_alloc();
+ }
+ d_totalSizeAlloc = newSize;
+ d_headSegment.initialize(newList);
+ }
+
+ /**
+ * Allocate a new segment with more space.
+ * Throws bad_alloc if memory allocation fails.
+ */
+ void grow() {
+ Assert(d_totalSizeAlloc == d_size);
+
+ // Allocate a new segment
+ typedef typename Allocator::template rebind<ListSegment>::other
+ SegmentAllocator;
+ ContextMemoryManager* cmm = d_allocator.getCMM();
+ SegmentAllocator segAllocator = SegmentAllocator(cmm);
+ ListSegment* newSegment = segAllocator.allocate(1);
+ if(newSegment == NULL) {
+ throw std::bad_alloc();
+ }
+ segAllocator.construct(newSegment, ListSegment());
+ size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
+ if(newSize > d_allocator.max_size()) {
+ newSize = d_allocator.max_size();
+ }
+ T* newList = d_allocator.allocate(newSize);
+ Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
+ << " level " << getContext()->getLevel()
+ << " to " << newSize
+ << " (from " << d_tailSegment->list()
+ << " to " << newList << ")" << std::endl;
+ if(newList == NULL) {
+ throw std::bad_alloc();
+ }
+ d_tailSegment->linkTo(newSegment);
+ d_tailSegment = newSegment;
+ d_tailSegment->initialize(newList);
+ d_totalSizeAlloc += newSize;
+ }
+
+ /**
+ * Implementation of mandatory ContextObj method save: simply copies the
+ * current size 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) CDListSave(*this, d_tailSegment,
+ d_size, d_totalSizeAlloc);
+ Debug("cdlist:cmm") << "save " << this
+ << " at level " << this->getContext()->getLevel()
+ << " size at " << this->d_size
+ << " totalSizeAlloc at " << this->d_totalSizeAlloc
+ << " data:" << data << std::endl;
+ return data;
+ }
+
+ /**
+ * 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) {
+ CDListSave* save = static_cast<CDListSave*>(data);
+ Debug("cdlist:cmm") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " data == " << data
+ << " call dtor == " << this->d_callDestructor
+ << " d_tail == " << this->d_tailSegment << std::endl;
+ if(this->d_callDestructor) {
+ ListSegment* seg = &d_headSegment;
+ size_t i = save->d_size;
+ while(i >= seg->size()) {
+ i -= seg->size();
+ seg = seg->getNextSegment();
+ }
+ do {
+ while(i < seg->size()) {
+ this->d_allocator.destroy(&(*seg)[i++]);
+ }
+ i = 0;
+ } while((seg = seg->getNextSegment()) != NULL);
+ }
+
+ this->d_size = save->d_size;
+ this->d_tailSegment = save->d_tail;
+ this->d_tailSegment->size() = save->d_tailSize;
+ this->d_tailSegment->cutLink();
+ this->d_totalSizeAlloc = save->d_sizeAlloc;
+ Debug("cdlist:cmm") << "restore " << this
+ << " level " << this->getContext()->getLevel()
+ << " size back to " << this->d_size
+ << " totalSizeAlloc at " << this->d_totalSizeAlloc
+ << std::endl;
+ }
+
+public:
+
+ CDList(Context* context, bool callDestructor, const Allocator& alloc) :
+ ContextObj(context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(alloc) {
+ allocateHeadSegment();
+ }
+
+ CDList(Context* context, bool callDestructor = true) :
+ ContextObj(context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(Allocator(context->getCMM())) {
+ allocateHeadSegment();
+ }
+
+ CDList(bool allocatedInCMM, Context* context, bool callDestructor,
+ const Allocator& alloc) :
+ ContextObj(allocatedInCMM, context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(alloc) {
+ allocateHeadSegment();
+ }
+
+ CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
+ ContextObj(allocatedInCMM, context),
+ d_headSegment(),
+ d_tailSegment(&d_headSegment),
+ d_callDestructor(callDestructor),
+ d_size(0),
+ d_totalSizeAlloc(0),
+ d_allocator(Allocator(context->getCMM())) {
+ allocateHeadSegment();
+ }
+
+ /**
+ * Destructor: delete the list
+ */
+ ~CDList() throw(AssertionException) {
+ this->destroy();
+
+ if(this->d_callDestructor) {
+ for(ListSegment* segment = &d_headSegment;
+ segment != NULL;
+ segment = segment->getNextSegment()) {
+ for(size_t i = 0; i < segment->size(); ++i) {
+ this->d_allocator.destroy(&(*segment)[i]);
+ }
+ }
+ }
+ }
+
+ /**
+ * Return the current size of (i.e. valid number of objects in) the
+ * list.
+ */
+ size_t size() const {
+ return d_size;
+ }
+
+ /**
+ * Return true iff there are no valid objects in the list.
+ */
+ bool empty() const {
+ return d_size == 0;
+ }
+
+ /**
+ * Add an item to the end of the list.
+ */
+ void push_back(const T& data) {
+ Debug("cdlist:cmm") << "push_back " << this
+ << " level " << getContext()->getLevel()
+ << ": make-current, "
+ << "d_list == " << d_tailSegment->list() << std::endl;
+ makeCurrent();
+
+ Debug("cdlist:cmm") << "push_back " << this
+ << " level " << getContext()->getLevel()
+ << ": grow? " << d_size
+ << " size_alloc " << d_totalSizeAlloc
+ << std::endl;
+
+ if(d_size == d_totalSizeAlloc) {
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": grow!\n";
+ grow();
+ }
+ Assert(d_size < d_totalSizeAlloc);
+
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": construct! at [" << d_size << "] == "
+ << &(*d_tailSegment)[d_tailSegment->size()]
+ << std::endl;
+ d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": done..." << std::endl;
+ ++d_tailSegment->size();
+ ++d_size;
+ Debug("cdlist:cmm") << "push_back " << this
+ << " " << getContext()->getLevel()
+ << ": size now " << d_size << std::endl;
+ }
+
+ /**
+ * Access to the ith item in the list.
+ */
+ const T& operator[](size_t i) const {
+ Assert(i < d_size, "index out of bounds in CDList::operator[]");
+ const ListSegment* seg = &d_headSegment;
+ while(i >= seg->size()) {
+ i -= seg->size();
+ seg = seg->getNextSegment();
+ }
+ return (*seg)[i];
+ }
+
+ /**
+ * Returns the most recent item added to the list.
+ */
+ const T& back() const {
+ Assert(d_size > 0, "CDList::back() called on empty list");
+ return (*d_tailSegment)[d_tailSegment->size() - 1];
+ }
+
+ /**
+ * Iterator for CDList class. It has to be const because we don't
+ * allow items in the list to be changed. It's a straightforward
+ * wrapper around a pointer. Note that for efficiency, we implement
+ * only prefix increment and decrement. Also note that it's OK to
+ * create an iterator from an empty, uninitialized list, as begin()
+ * and end() will have the same value (NULL).
+ */
+ class const_iterator {
+ const ListSegment* d_segment;
+ size_t d_index;
+
+ const_iterator(const ListSegment* segment, size_t i) :
+ d_segment(segment),
+ d_index(i) {
+ }
+
+ friend class CDList<T, Allocator>;
+
+ public:
+
+ typedef std::input_iterator_tag iterator_category;
+ typedef T value_type;
+ typedef ptrdiff_t difference_type;
+ typedef const T* pointer;
+ typedef const T& reference;
+
+ const_iterator() : d_segment(NULL), d_index(0) {}
+
+ inline bool operator==(const const_iterator& i) const {
+ return d_segment == i.d_segment && d_index == i.d_index;
+ }
+
+ inline bool operator!=(const const_iterator& i) const {
+ return !(*this == i);
+ }
+
+ inline const T& operator*() const {
+ return (*d_segment)[d_index];
+ }
+
+ /** Prefix increment */
+ const_iterator& operator++() {
+ if(++d_index >= d_segment->size()) {
+ d_segment = d_segment->getNextSegment();
+ d_index = 0;
+ }
+ return *this;
+ }
+
+ /** Postfix increment: returns new iterator with the old value. */
+ const_iterator operator++(int) {
+ const_iterator i = *this;
+ ++(*this);
+ return i;
+ }
+ };/* class CDList<>::const_iterator */
+
+ /**
+ * Returns an iterator pointing to the first item in the list.
+ */
+ const_iterator begin() const {
+ return const_iterator(&d_headSegment, 0);
+ }
+
+ /**
+ * Returns an iterator pointing one past the last item in the list.
+ */
+ const_iterator end() const {
+ return const_iterator(NULL, 0);
+ }
+};/* class CDList<T, ContextMemoryAllocator<T> > */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H */
--- /dev/null
+/********************* */
+/*! \file cdlist_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 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
+ ** CDList<> template
+ **
+ ** This is a forward declaration header to declare the CDList<>
+ ** template. It's useful if you want to forward-declare CDList<>
+ ** without including the full cdlist.h or cdlist_context_memory.h
+ ** header, for example, in a public header context, or to keep
+ ** compile times low when only a forward declaration is needed.
+ **
+ ** Note that all specializations of the template should be listed
+ ** here as well, since different specializations are defined in
+ ** different headers (cdlist.h and cdlist_context_memory.h).
+ ** Explicitly declaring both specializations here ensure that if you
+ ** define one, you'll get an error if you didn't include the correct
+ ** header (avoiding different, incompatible instantiations in
+ ** different compilation units).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDLIST_FORWARD_H
+#define __CVC4__CONTEXT__CDLIST_FORWARD_H
+
+#include <memory>
+
+namespace __gnu_cxx {
+ template <class Key> class hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+ namespace context {
+ template <class T>
+ class ContextMemoryAllocator;
+
+ template <class T, class Allocator = std::allocator<T> >
+ class CDList;
+
+ template <class T>
+ class CDList<T, ContextMemoryAllocator<T> >;
+ }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */
#include <new>
#include "context/context_mm.h"
#include "util/Assert.h"
+#include "util/output.h"
namespace CVC4 {
namespace context {
*/
void newChunk();
- public:
+public:
+
+ /**
+ * Get the maximum allocation size for this memory manager.
+ */
+ static unsigned getMaxAllocationSize() {
+ return chunkSizeBytes;
+ }
/**
* Constructor - creates an initial region and an empty stack
};/* class ContextMemoryManager */
+/**
+ * An STL-like allocator class for allocating from context memory.
+ */
+template <class T>
+class ContextMemoryAllocator {
+ ContextMemoryManager* d_mm;
+
+public:
+
+ typedef size_t size_type;
+ typedef ptrdiff_t difference_type;
+ typedef T* pointer;
+ typedef T const* const_pointer;
+ typedef T& reference;
+ typedef T const& const_reference;
+ typedef T value_type;
+ template <class U> struct rebind {
+ typedef ContextMemoryAllocator<U> other;
+ };
+
+ ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {}
+ ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.d_mm) {}
+ ~ContextMemoryAllocator() throw() {}
+
+ ContextMemoryManager* getCMM() { 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() {
+ return ContextMemoryManager::getMaxAllocationSize() / sizeof(T);
+ }
+ T* allocate(size_t n, const void* = 0) const {
+ return static_cast<T*>(d_mm->newData(n * sizeof(T)));
+ }
+ void deallocate(T* p, size_t n) const {
+ /* no explicit delete */
+ }
+ void construct(T* p, T const& v) const {
+ ::new(reinterpret_cast<void*>(p)) T(v);
+ }
+ void destroy(T* p) const {
+ p->~T();
+ }
+};/* class ContextMemoryAllocator<T> */
+
+template <class T>
+inline bool operator==(const ContextMemoryAllocator<T>& a1,
+ const ContextMemoryAllocator<T>& a2) {
+ return a1.d_mm == a2.d_mm;
+}
+
+template <class T>
+inline bool operator!=(const ContextMemoryAllocator<T>& a1,
+ const ContextMemoryAllocator<T>& a2) {
+ return a1.d_mm != a2.d_mm;
+}
+
}/* CVC4::context namespace */
}/* CVC4 namespace */
}
}
+/**
+ * Cleanup to be performed when a NodeValue zombie is collected, and
+ * it has CONSTANT metakind. This calls the destructor for the underlying
+ * C++ type representing the constant value. See
+ * NodeManager::reclaimZombies() for more information.
+ *
+ * This doesn't support "non-inlined" NodeValues, which shouldn't need this
+ * kind of cleanup.
+ */
+inline void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) {
+ Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
+
+ switch(nv->d_kind) {
+${metakind_constDeleters}
+ default:
+ Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+ }
+}
+
inline unsigned getLowerBoundForKind(::CVC4::Kind k) {
static const unsigned lbs[] = {
0, /* NULL_EXPR */
metakind_compares=
metakind_constHashes=
metakind_constPrinters=
+metakind_constDeleters=
metakind_ubchildren=
metakind_lbchildren=
metakind_operatorKinds=
#line $lineno \"$kf\"
out << nv->getConst< $2 >();
break;
+"
+ cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
+ metakind_constDeleters="${metakind_constDeleters}
+ case kind::$1:
+#line $lineno \"$kf\"
+ std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children));
+ break;
"
}
metakind_compares \
metakind_constHashes \
metakind_constPrinters \
+ metakind_constDeleters \
metakind_ubchildren \
metakind_lbchildren \
metakind_operatorKinds; do
<< " [" << nv->d_id << "]: " << *nv << "\n";
// remove from the pool
- if(nv->getMetaKind() != kind::metakind::VARIABLE) {
+ kind::MetaKind mk = nv->getMetaKind();
+ if(mk != kind::metakind::VARIABLE) {
poolRemove(nv);
}
// decr ref counts of children
nv->decrRefCounts();
+ if(mk == kind::metakind::CONSTANT) {
+ // Destroy (call the destructor for) the C++ type representing
+ // the constant in this NodeValue. This is needed for
+ // e.g. CVC4::Rational, since it has a gmp internal
+ // representation that mallocs memory and should be cleaned
+ // up. (This won't delete a pointer value if used as a
+ // constant, but then, you should probably use a smart-pointer
+ // type for a constant payload.)
+ kind::metakind::deleteNodeValueConstant(nv);
+ }
free(nv);
}
}
class MultNodeBuilder;
class NodeManager;
+namespace expr {
+ class NodeValue;
+}
+
namespace kind {
namespace metakind {
template < ::CVC4::Kind k, bool pool >
struct NodeValueCompare;
struct NodeValueConstPrinter;
+
+ void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
}/* CVC4::kind::metakind namespace */
}/* CVC4::kind namespace */
friend class ::CVC4::NodeManager;
template <Kind k, bool pool>
- friend struct ::CVC4::kind::metakind::NodeValueConstCompare;
+ friend struct ::CVC4::kind::metakind::NodeValueConstCompare;
friend struct ::CVC4::kind::metakind::NodeValueCompare;
friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
+ friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
+
void inc();
void dec();
/* These need to be macros so they can refer to the PARSER macro, which will be defined
* by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
-#undef PARSER_STATE
+#undef PARSER_STATE
#define PARSER_STATE ((Smt*)PARSER->super)
#undef EXPR_MANAGER
#define EXPR_MANAGER PARSER_STATE->getExprManager()
* @return the sequence command containing the whole problem
*/
benchmark returns [CVC4::Command* cmd]
- : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK
+ : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK
{ $cmd = c; }
| EOF { $cmd = 0; }
;
* @return a command corresponding to the attribute
*/
benchAttribute returns [CVC4::Command* smt_command]
-@declarations {
+@declarations {
std::string name;
BenchmarkStatus b_status;
Expr expr;
{ smt_command = new AssertCommand(expr); }
| FORMULA_TOK annotatedFormula[expr]
{ smt_command = new CheckSatCommand(expr); }
- | STATUS_TOK status[b_status]
- { smt_command = new SetBenchmarkStatusCommand(b_status); }
- | EXTRAFUNS_TOK LPAREN_TOK (functionDeclaration)+ RPAREN_TOK
- | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK
- | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK
- | NOTES_TOK STRING_LITERAL
+ | STATUS_TOK status[b_status]
+ { smt_command = new SetBenchmarkStatusCommand(b_status); }
+ | EXTRAFUNS_TOK LPAREN_TOK (functionDeclaration)+ RPAREN_TOK
+ | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK
+ | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK
+ | NOTES_TOK STRING_LITERAL
| annotation
;
std::string name;
std::vector<Expr> args; /* = getExprVector(); */
Expr op; /* Operator expression FIXME: move away kill it */
-}
+}
: /* a built-in operator application */
- LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
+ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
{ if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
It just so happens expr should already by the only argument. */
Assert( expr == args[0] );
- } else if( CVC4::kind::isAssociative(kind) &&
+ } else if( CVC4::kind::isAssociative(kind) &&
args.size() > EXPR_MANAGER->maxArity(kind) ) {
/* Special treatment for associative operators with lots of children */
expr = EXPR_MANAGER->mkAssociative(kind,args);
// Semantic predicate not necessary if parenthesized subexpressions
// are disallowed
- // { isFunction(LT(2)->getText()) }?
- LPAREN_TOK
+ // { isFunction(LT(2)->getText()) }?
+ LPAREN_TOK
parameterizedOperator[op]
annotatedFormulas[args,expr] RPAREN_TOK
// TODO: check arity
{ expr = MK_EXPR(op,args); }
| /* An ite expression */
- LPAREN_TOK ITE_TOK
+ LPAREN_TOK ITE_TOK
annotatedFormula[expr]
- { args.push_back(expr); }
+ { args.push_back(expr); }
annotatedFormula[expr]
- { args.push_back(expr); }
+ { args.push_back(expr); }
annotatedFormula[expr]
- { args.push_back(expr); }
+ { args.push_back(expr); }
RPAREN_TOK
{ expr = MK_EXPR(CVC4::kind::ITE, args); }
| /* a let/flet binding */
- LPAREN_TOK
- (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
+ LPAREN_TOK
+ ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
| FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
annotatedFormula[expr] RPAREN_TOK
{ PARSER_STATE->pushScope();
| NUMERAL_TOK
{ expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
| RATIONAL_TOK
- { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
+ { // FIXME: This doesn't work because an SMT rational is not a
+ // valid GMP rational string
expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
- | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
+ | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
{ expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
// NOTE: Theory constants go here
/* TODO: quantifiers, arithmetic constants */
| /* a variable */
( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- | let_identifier[name,CHECK_DECLARED]
+ | let_identifier[name,CHECK_DECLARED]
| flet_identifier[name,CHECK_DECLARED] )
{ expr = PARSER_STATE->getVariable(name); }
;
/**
- * Matches a sequence of annotated formulas and puts them into the formulas
- * vector.
+ * Matches a sequence of annotated formulas and puts them into the
+ * formulas vector.
* @param formulas the vector to fill with formulas
* @param expr an Expr reference for the elements of the sequence
- */
-/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
+ */
+/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
* time through this rule. */
annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
: ( annotatedFormula[expr] { formulas.push_back(expr); } )+
/**
* Matches an operator.
*/
-parameterizedOperator[CVC4::Expr& op]
+parameterizedOperator[CVC4::Expr& op]
: functionSymbol[op]
| bitVectorOperator[op]
;
bitVectorOperator[CVC4::Expr& op]
: EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']'
{ op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); }
- | REPEAT_TOK '[' n = NUMERAL_TOK ']'
+ | REPEAT_TOK '[' n = NUMERAL_TOK ']'
{ op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
| ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']'
{ op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
| ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']'
{ op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
| ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']'
- { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
+ { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
;
/**
- * Matches a (possibly undeclared) predicate identifier (returning the string).
+ * Matches a (possibly undeclared) predicate identifier (returning the string).
* @param check what kind of check to do with the symbol
*/
predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
* @param check what kind of check to do with the symbol
*/
functionName[std::string& name, CVC4::parser::DeclarationCheck check]
- : identifier[name,check,SYM_VARIABLE]
+ : identifier[name,check,SYM_VARIABLE]
;
/**
}
: functionName[name,CHECK_DECLARED]
{ PARSER_STATE->checkFunction(name);
- fun = PARSER_STATE->getVariable(name); }
+ fun = PARSER_STATE->getVariable(name); }
;
-
+
/**
* Matches an attribute name from the input (:attribute_name).
*/
std::string name;
std::vector<Type> sorts;
}
- : LPAREN_TOK functionName[name,CHECK_UNDECLARED]
+ : LPAREN_TOK functionName[name,CHECK_UNDECLARED]
t = sortSymbol // require at least one sort
{ sorts.push_back(t); }
sortList[sorts] RPAREN_TOK
{ if( sorts.size() == 1 ) {
- Assert( t == sorts[0] );
+ Assert( t == sorts[0] );
} else {
t = EXPR_MANAGER->mkFunctionType(sorts);
}
- PARSER_STATE->mkVar(name, t); }
+ PARSER_STATE->mkVar(name, t); }
;
-
+
/**
* Matches the declaration of a predicate and declares it
*/
{ Type t;
if( p_sorts.empty() ) {
t = EXPR_MANAGER->booleanType();
- } else {
+ } else {
t = EXPR_MANAGER->mkPredicateType(p_sorts);
}
- PARSER_STATE->mkVar(name, t); }
+ PARSER_STATE->mkVar(name, t); }
;
-sortDeclaration
+sortDeclaration
@declarations {
std::string name;
}
{ Debug("parser") << "sort decl: '" << name << "'" << std::endl;
PARSER_STATE->mkSort(name); }
;
-
+
/**
* Matches a sequence of sort symbols and fills them into the given vector.
*/
sortList[std::vector<CVC4::Type>& sorts]
- : ( t = sortSymbol { sorts.push_back(t); })*
+ : ( t = sortSymbol { sorts.push_back(t); })*
;
/**
* Matches the sort symbol, which can be an arbitrary identifier.
* @param check the check to perform on the name
*/
-sortName[std::string& name, CVC4::parser::DeclarationCheck check]
- : identifier[name,check,SYM_SORT]
+sortName[std::string& name, CVC4::parser::DeclarationCheck check]
+ : identifier[name,check,SYM_SORT]
;
sortSymbol returns [CVC4::Type t]
@declarations {
std::string name;
}
- : sortName[name,CHECK_NONE]
+ : sortName[name,CHECK_NONE]
{ $t = PARSER_STATE->getSort(name); }
| BITVECTOR_TOK '[' NUMERAL_TOK ']' {
$t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
* @param type the intended namespace for the identifier
*/
identifier[std::string& id,
- CVC4::parser::DeclarationCheck check,
- CVC4::parser::SymbolType type]
+ CVC4::parser::DeclarationCheck check,
+ CVC4::parser::SymbolType type]
: IDENTIFIER
{ id = AntlrInput::tokenText($IDENTIFIER);
Debug("parser") << "identifier: " << id
* @param check what kinds of check to do on the symbol
*/
let_identifier[std::string& id,
- CVC4::parser::DeclarationCheck check]
+ CVC4::parser::DeclarationCheck check]
: LET_IDENTIFIER
{ id = AntlrInput::tokenText($LET_IDENTIFIER);
Debug("parser") << "let_identifier: " << id
* @param check what kinds of check to do on the symbol
*/
flet_identifier[std::string& id,
- CVC4::parser::DeclarationCheck check]
+ CVC4::parser::DeclarationCheck check]
: FLET_IDENTIFIER
{ id = AntlrInput::tokenText($FLET_IDENTIFIER);
Debug("parser") << "flet_identifier: " << id
TILDE_TOK : '~';
XOR_TOK : 'xor';
-// Bitvector tokens
+// Bitvector tokens
BITVECTOR_TOK : 'BitVec';
BV_TOK : 'bv';
CONCAT_TOK : 'concat';
/**
* Matches an identifier starting with a colon.
*/
-ATTR_IDENTIFIER
+ATTR_IDENTIFIER
: ':' IDENTIFIER
;
LET_IDENTIFIER
: '?' IDENTIFIER
;
-
+
/**
* Matches an identifier starting with a dollar sign.
*/
* Matches a double quoted string literal. Escaping is supported, and escape
* character '\' has to be escaped.
*/
-STRING_LITERAL
+STRING_LITERAL
: '"' (ESCAPE | ~('"'|'\\'))* '"'
;
/**
* Matches the comments and ignores them
*/
-COMMENT
+COMMENT
: ';' (~('\n' | '\r'))* { $channel = HIDDEN;; }
;
* Matches any letter ('a'-'z' and 'A'-'Z').
*/
fragment
-ALPHA
+ALPHA
: 'a'..'z'
| 'A'..'Z'
;
#include "smt/no_such_function_exception.h"
#include "context/context.h"
#include "context/cdlist.h"
+#include "context/cdset.h"
#include "expr/expr.h"
#include "expr/command.h"
#include "expr/node_builder.h"
#include "expr/expr_manager.h"
#include "context/cdmap_forward.h"
#include "context/cdset_forward.h"
+#include "context/cdlist_forward.h"
#include "util/result.h"
#include "util/model.h"
#include "util/sexpr.h"
namespace context {
class Context;
- template <class T> class CDList;
}/* CVC4::context namespace */
namespace prop {
namespace theory {
namespace arith {
-class ArithConstants{
+class ArithConstants {
public:
Rational d_ZERO;
Rational d_ONE;
d_ONE_NODE(nm->mkConst(d_ONE)),
d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
{}
-};
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+ ~ArithConstants() {
+ d_ZERO_NODE = Node::null();
+ d_ONE_NODE = Node::null();
+ d_NEGATIVE_ONE_NODE = Node::null();
+ }
+};/* class ArithConstants */
+
+}/* namespace CVC4::theory::arith */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
template=$1; shift
-theoryof_table_includes=
+theoryof_table_forwards=
theoryof_table_registers=
seen_theory=false
echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
fi
- theoryof_table_includes="${theoryof_table_includes}#include \"theory/$b/$2\"
+ decl=
+ last=
+ num=0
+ for ns in `echo "$1" | sed 's,::, ,g'`; do
+ if [ -n "$last" ]; then
+ decl="${decl}namespace $last { "
+ let ++num
+ fi
+ last="$ns"
+ done
+ decl="${decl}class $last;"
+ while [ $num -gt 0 ]; do
+ decl="${decl} }"
+ let --num
+ done
+
+ theoryof_table_forwards="${theoryof_table_forwards}$decl // #include \"theory/$b/$2\"
"
theoryof_table_registers="${theoryof_table_registers}
/* from $b */
function do_theoryof {
check_theory_seen
- theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = th;
+ theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = (Theory*)th;
"
}
## output
text=$(cat "$template")
-for var in theoryof_table_includes theoryof_table_registers; do
+for var in theoryof_table_forwards theoryof_table_registers; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
** The theory engine.
**/
+#include <vector>
+#include <list>
+
#include "theory/theory_engine.h"
#include "expr/node.h"
#include "expr/attribute.h"
#include "expr/node_builder.h"
#include "smt/options.h"
-#include <vector>
-#include <list>
+#include "theory/builtin/theory_builtin.h"
+#include "theory/booleans/theory_bool.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/morgan/theory_uf_morgan.h"
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arrays/theory_arrays.h"
+#include "theory/bv/theory_bv.h"
using namespace std;
d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
- d_sharedTermManager->registerTheory(d_builtin);
- d_sharedTermManager->registerTheory(d_bool);
- d_sharedTermManager->registerTheory(d_uf);
- d_sharedTermManager->registerTheory(d_arith);
- d_sharedTermManager->registerTheory(d_arrays);
- d_sharedTermManager->registerTheory(d_bv);
-
- d_theoryOfTable.registerTheory(d_builtin);
- d_theoryOfTable.registerTheory(d_bool);
- d_theoryOfTable.registerTheory(d_uf);
- d_theoryOfTable.registerTheory(d_arith);
- d_theoryOfTable.registerTheory(d_arrays);
- d_theoryOfTable.registerTheory(d_bv);
+ d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
+ d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
+ d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
+ d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
+ d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
+ d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
+
+ d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
+ d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
+ d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
+ d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
+ d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
+ d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
}
TheoryEngine::~TheoryEngine() {
#include "expr/node.h"
#include "theory/theory.h"
#include "theory/theoryof_table.h"
-
#include "prop/prop_engine.h"
#include "theory/shared_term_manager.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/tim/theory_uf_tim.h"
-#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
-
#include "util/stats.h"
namespace CVC4 {
d_explanationNode = explanationNode;
++(d_engine->d_statistics.d_statExplanation);
}
- };
-
-
+ };/* class EngineOutputChannel */
EngineOutputChannel d_theoryOut;
/** Pointer to Shared Term Manager */
SharedTermManager* d_sharedTermManager;
- theory::builtin::TheoryBuiltin* d_builtin;
- theory::booleans::TheoryBool* d_bool;
- theory::uf::TheoryUF* d_uf;
- theory::arith::TheoryArith* d_arith;
- theory::arrays::TheoryArrays* d_arrays;
- theory::bv::TheoryBV* d_bv;
+ theory::Theory* d_builtin;
+ theory::Theory* d_bool;
+ theory::Theory* d_uf;
+ theory::Theory* d_arith;
+ theory::Theory* d_arrays;
+ theory::Theory* d_bv;
/**
* Debugging flag to ensure that shutdown() is called before the
#include "expr/kind.h"
#include "util/Assert.h"
-${theoryof_table_includes}
+${theoryof_table_forwards}
namespace CVC4 {
namespace theory {
d_cc(ctxt, &d_ccChannel),
d_unionFind(ctxt),
d_disequalities(ctxt),
- d_disequality(ctxt),
d_conflict(),
d_trueNode(),
d_falseNode(),
- d_trueEqFalseNode(),
- d_activeAssertions(ctxt) {
+ d_trueEqFalseNode() {
NodeManager* nm = NodeManager::currentNM();
TypeNode boolType = nm->booleanType();
d_trueNode = nm->mkVar("TRUE_UF", boolType);
}
TheoryUFMorgan::~TheoryUFMorgan() {
+ d_trueNode = Node::null();
+ d_falseNode = Node::null();
+ d_trueEqFalseNode = Node::null();
}
RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
d_unionFind[a] = b;
- if(Debug.isOn("uf") && find(d_trueNode) == find(d_falseNode)) {
- Debug("uf") << "ok, pay attention now.." << std::endl;
- dump();
- }
-
DiseqLists::iterator deq_i = d_disequalities.find(a);
if(deq_i != d_disequalities.end()) {
// a set of other trees we are already disequal to
DiseqLists::iterator deq_i = d_disequalities.find(of);
DiseqList* deq;
if(deq_i == d_disequalities.end()) {
- deq = new(getContext()->getCMM()) DiseqList(true, getContext());
+ deq = new(getContext()->getCMM()) DiseqList(true, getContext(), false,
+ ContextMemoryAllocator<TNode>(getContext()->getCMM()));
d_disequalities.insertDataFromContextMemory(of, deq);
} else {
deq = (*deq_i).second;
Node assertion = get();
- d_activeAssertions.push_back(assertion);
+ //d_activeAssertions.push_back(assertion);
Debug("uf") << "uf check(): " << assertion << std::endl;
Node b = assertion[0][1];
addDisequality(assertion[0]);
- d_disequality.push_back(assertion[0]);
d_cc.addTerm(a);
d_cc.addTerm(b);
Unhandled(assertion.getKind());
}
+ /*
if(Debug.isOn("uf")) {
dump();
}
+ */
}
Assert(d_conflict.isNull());
Debug("uf") << "uf check() done = " << (done() ? "true" : "false")
<< std::endl;
+ /*
for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
diseqIter != d_disequality.end();
++diseqIter) {
Assert((debugFind(left) == debugFind(right)) ==
d_cc.areCongruent(left, right));
}
+ */
Debug("uf") << "uf: end check(" << level << ")" << std::endl;
}
}
}
+/*
void TheoryUFMorgan::dump() {
if(!Debug.isOn("uf")) {
return;
}
Debug("uf") << "=======================================" << std::endl;
}
+*/
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality.
- **
- ** This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality. It is based on the Nelson-Oppen algorithm given in
- ** "Fast Decision Procedures Based on Congruence Closure"
- ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
- ** This has been extended to work in a context-dependent way.
- ** This interacts heavily with the data-structures given in ecdata.h .
+ ** \brief Implementation of the theory of uninterpreted functions with
+ ** equality
**
+ ** Implementation of the theory of uninterpreted functions with equality,
+ ** based on CVC4's congruence closure module (which is in turn based on
+ ** the Nieuwenhuis and Oliveras paper, Fast Congruence Closure and
+ ** Extensions.
**/
#include "cvc4_private.h"
#include "theory/uf/theory_uf.h"
#include "context/context.h"
-#include "context/cdo.h"
+#include "context/context_mm.h"
#include "context/cdlist.h"
#include "util/congruence_closure.h"
typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind;
UnionFind d_unionFind;
- typedef context::CDList<Node> DiseqList;
+ typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList;
typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists;
/** List of all disequalities this theory has seen. */
DiseqLists d_disequalities;
- context::CDList<Node> d_disequality;
-
Node d_conflict;
Node d_trueNode, d_falseNode, d_trueEqFalseNode;
- context::CDList<Node> d_activeAssertions;
+ //context::CDList<Node> d_activeAssertions;
public:
#include "expr/node_manager.h"
#include "expr/node.h"
+#include "context/context_mm.h"
+#include "context/cdo.h"
#include "context/cdmap.h"
#include "context/cdset.h"
-#include "context/cdlist.h"
+#include "context/cdlist_context_memory.h"
#include "util/exception.h"
namespace CVC4 {
// typedef all of these so that iterators are easy to define
typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap;
- typedef context::CDList<Node> ClassList;
+ typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
- typedef context::CDList<Node> UseList;
+ typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists;
typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap;
UseLists::iterator usei = d_useList.find(of);
UseList* ul;
if(usei == d_useList.end()) {
- ul = new(d_context->getCMM()) UseList(true, d_context);
+ ul = new(d_context->getCMM()) UseList(true, d_context, false,
+ context::ContextMemoryAllocator<TNode>(d_context->getCMM()));
d_useList.insertDataFromContextMemory(of, ul);
} else {
ul = (*usei).second;
ClassLists::iterator cl_bpi = d_classList.find(bp);
ClassList* cl_bp;
if(cl_bpi == d_classList.end()) {
- cl_bp = new(d_context->getCMM()) ClassList(true, d_context);
+ cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false,
+ context::ContextMemoryAllocator<TNode>(d_context->getCMM()));
d_classList.insertDataFromContextMemory(bp, cl_bp);
Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
} else {
+++ /dev/null
-(benchmark NEQ016_size5.smt
-:source {
-CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
- for more information.
-
-This benchmark was obtained by trying to find a finite model of a first-order
-formula (Albert Oliveras).
-}
-:status unsat
-:category { crafted }
-:difficulty { 0 }
-:logic QF_UF
-:extrapreds ((p2 U))
-:extrafuns ((f1 U U U))
-:extrapreds ((p4 U))
-:extrapreds ((p3 U))
-:extrafuns ((c6 U))
-:extrafuns ((c5 U))
-:extrafuns ((c7 U))
-:extrafuns ((c_0 U))
-:extrafuns ((c_1 U))
-:extrafuns ((c_2 U))
-:extrafuns ((c_3 U))
-:extrafuns ((c_4 U))
-:formula
-( and
-( distinct c_0 c_1 c_2 c_3 c_4 )(or (not (p2 c_0)) (not (p2 c_0)) (p4 (f1 c_0 c_0)) (p3 (f1 c_0 c_0)) )(or (not (p2 c_0)) (not (p2 c_1)) (p4 (f1 c_1 c_0)) (p3 (f1 c_1 c_0)) )(or (not (p2 c_0)) (not (p2 c_2)) (p4 (f1 c_2 c_0)) (p3 (f1 c_2 c_0)) )(or (not (p2 c_0)) (not (p2 c_3)) (p4 (f1 c_3 c_0)) (p3 (f1 c_3 c_0)) )(or (not (p2 c_0)) (not (p2 c_4)) (p4 (f1 c_4 c_0)) (p3 (f1 c_4 c_0)) )(or (not (p2 c_1)) (not (p2 c_0)) (p4 (f1 c_0 c_1)) (p3 (f1 c_0 c_1)) )(or (not (p2 c_1)) (not (p2 c_1)) (p4 (f1 c_1 c_1)) (p3 (f1 c_1 c_1)) )(or (not (p2 c_1)) (not (p2 c_2)) (p4 (f1 c_2 c_1)) (p3 (f1 c_2 c_1)) )(or (not (p2 c_1)) (not (p2 c_3)) (p4 (f1 c_3 c_1)) (p3 (f1 c_3 c_1)) )(or (not (p2 c_1)) (not (p2 c_4)) (p4 (f1 c_4 c_1)) (p3 (f1 c_4 c_1)) )(or (not (p2 c_2)) (not (p2 c_0)) (p4 (f1 c_0 c_2)) (p3 (f1 c_0 c_2)) )(or (not (p2 c_2)) (not (p2 c_1)) (p4 (f1 c_1 c_2)) (p3 (f1 c_1 c_2)) )(or (not (p2 c_2)) (not (p2 c_2)) (p4 (f1 c_2 c_2)) (p3 (f1 c_2 c_2)) )(or (not (p2 c_2)) (not (p2 c_3)) (p4 (f1 c_3 c_2)) (p3 (f1 c_3 c_2)) )(or (not (p2 c_2)) (not (p2 c_4)) (p4 (f1 c_4 c_2)) (p3 (f1 c_4 c_2)) )(or (not (p2 c_3)) (not (p2 c_0)) (p4 (f1 c_0 c_3)) (p3 (f1 c_0 c_3)) )(or (not (p2 c_3)) (not (p2 c_1)) (p4 (f1 c_1 c_3)) (p3 (f1 c_1 c_3)) )(or (not (p2 c_3)) (not (p2 c_2)) (p4 (f1 c_2 c_3)) (p3 (f1 c_2 c_3)) )(or (not (p2 c_3)) (not (p2 c_3)) (p4 (f1 c_3 c_3)) (p3 (f1 c_3 c_3)) )(or (not (p2 c_3)) (not (p2 c_4)) (p4 (f1 c_4 c_3)) (p3 (f1 c_4 c_3)) )(or (not (p2 c_4)) (not (p2 c_0)) (p4 (f1 c_0 c_4)) (p3 (f1 c_0 c_4)) )(or (not (p2 c_4)) (not (p2 c_1)) (p4 (f1 c_1 c_4)) (p3 (f1 c_1 c_4)) )(or (not (p2 c_4)) (not (p2 c_2)) (p4 (f1 c_2 c_4)) (p3 (f1 c_2 c_4)) )(or (not (p2 c_4)) (not (p2 c_3)) (p4 (f1 c_3 c_4)) (p3 (f1 c_3 c_4)) )(or (not (p2 c_4)) (not (p2 c_4)) (p4 (f1 c_4 c_4)) (p3 (f1 c_4 c_4)) )(or (not (p2 c_0)) (not (p3 c_0)) )(or (not (p2 c_1)) (not (p3 c_1)) )(or (not (p2 c_2)) (not (p3 c_2)) )(or (not (p2 c_3)) (not (p3 c_3)) )(or (not (p2 c_4)) (not (p3 c_4)) )(or (p4 c_0) (p3 c_0) (p2 c_0) )(or (p4 c_1) (p3 c_1) (p2 c_1) )(or (p4 c_2) (p3 c_2) (p2 c_2) )(or (p4 c_3) (p3 c_3) (p2 c_3) )(or (p4 c_4) (p3 c_4) (p2 c_4) )(p3 c6) (p2 c5) (or (not (p4 c_0)) (not (p4 c_0)) (p2 (f1 c_0 c_0)) )(or (not (p4 c_0)) (not (p4 c_1)) (p2 (f1 c_1 c_0)) )(or (not (p4 c_0)) (not (p4 c_2)) (p2 (f1 c_2 c_0)) )(or (not (p4 c_0)) (not (p4 c_3)) (p2 (f1 c_3 c_0)) )(or (not (p4 c_0)) (not (p4 c_4)) (p2 (f1 c_4 c_0)) )(or (not (p4 c_1)) (not (p4 c_0)) (p2 (f1 c_0 c_1)) )(or (not (p4 c_1)) (not (p4 c_1)) (p2 (f1 c_1 c_1)) )(or (not (p4 c_1)) (not (p4 c_2)) (p2 (f1 c_2 c_1)) )(or (not (p4 c_1)) (not (p4 c_3)) (p2 (f1 c_3 c_1)) )(or (not (p4 c_1)) (not (p4 c_4)) (p2 (f1 c_4 c_1)) )(or (not (p4 c_2)) (not (p4 c_0)) (p2 (f1 c_0 c_2)) )(or (not (p4 c_2)) (not (p4 c_1)) (p2 (f1 c_1 c_2)) )(or (not (p4 c_2)) (not (p4 c_2)) (p2 (f1 c_2 c_2)) )(or (not (p4 c_2)) (not (p4 c_3)) (p2 (f1 c_3 c_2)) )(or (not (p4 c_2)) (not (p4 c_4)) (p2 (f1 c_4 c_2)) )(or (not (p4 c_3)) (not (p4 c_0)) (p2 (f1 c_0 c_3)) )(or (not (p4 c_3)) (not (p4 c_1)) (p2 (f1 c_1 c_3)) )(or (not (p4 c_3)) (not (p4 c_2)) (p2 (f1 c_2 c_3)) )(or (not (p4 c_3)) (not (p4 c_3)) (p2 (f1 c_3 c_3)) )(or (not (p4 c_3)) (not (p4 c_4)) (p2 (f1 c_4 c_3)) )(or (not (p4 c_4)) (not (p4 c_0)) (p2 (f1 c_0 c_4)) )(or (not (p4 c_4)) (not (p4 c_1)) (p2 (f1 c_1 c_4)) )(or (not (p4 c_4)) (not (p4 c_2)) (p2 (f1 c_2 c_4)) )(or (not (p4 c_4)) (not (p4 c_3)) (p2 (f1 c_3 c_4)) )(or (not (p4 c_4)) (not (p4 c_4)) (p2 (f1 c_4 c_4)) )(= (f1 c_0 (f1 c_0 c_0)) (f1 (f1 c_0 c_0) c_0)) (= (f1 c_0 (f1 c_0 c_1)) (f1 (f1 c_0 c_0) c_1)) (= (f1 c_0 (f1 c_0 c_2)) (f1 (f1 c_0 c_0) c_2)) (= (f1 c_0 (f1 c_0 c_3)) (f1 (f1 c_0 c_0) c_3)) (= (f1 c_0 (f1 c_0 c_4)) (f1 (f1 c_0 c_0) c_4)) (= (f1 c_0 (f1 c_1 c_0)) (f1 (f1 c_0 c_1) c_0)) (= (f1 c_0 (f1 c_1 c_1)) (f1 (f1 c_0 c_1) c_1)) (= (f1 c_0 (f1 c_1 c_2)) (f1 (f1 c_0 c_1) c_2)) (= (f1 c_0 (f1 c_1 c_3)) (f1 (f1 c_0 c_1) c_3)) (= (f1 c_0 (f1 c_1 c_4)) (f1 (f1 c_0 c_1) c_4)) (= (f1 c_0 (f1 c_2 c_0)) (f1 (f1 c_0 c_2) c_0)) (= (f1 c_0 (f1 c_2 c_1)) (f1 (f1 c_0 c_2) c_1)) (= (f1 c_0 (f1 c_2 c_2)) (f1 (f1 c_0 c_2) c_2)) (= (f1 c_0 (f1 c_2 c_3)) (f1 (f1 c_0 c_2) c_3)) (= (f1 c_0 (f1 c_2 c_4)) (f1 (f1 c_0 c_2) c_4)) (= (f1 c_0 (f1 c_3 c_0)) (f1 (f1 c_0 c_3) c_0)) (= (f1 c_0 (f1 c_3 c_1)) (f1 (f1 c_0 c_3) c_1)) (= (f1 c_0 (f1 c_3 c_2)) (f1 (f1 c_0 c_3) c_2)) (= (f1 c_0 (f1 c_3 c_3)) (f1 (f1 c_0 c_3) c_3)) (= (f1 c_0 (f1 c_3 c_4)) (f1 (f1 c_0 c_3) c_4)) (= (f1 c_0 (f1 c_4 c_0)) (f1 (f1 c_0 c_4) c_0)) (= (f1 c_0 (f1 c_4 c_1)) (f1 (f1 c_0 c_4) c_1)) (= (f1 c_0 (f1 c_4 c_2)) (f1 (f1 c_0 c_4) c_2)) (= (f1 c_0 (f1 c_4 c_3)) (f1 (f1 c_0 c_4) c_3)) (= (f1 c_0 (f1 c_4 c_4)) (f1 (f1 c_0 c_4) c_4)) (= (f1 c_1 (f1 c_0 c_0)) (f1 (f1 c_1 c_0) c_0)) (= (f1 c_1 (f1 c_0 c_1)) (f1 (f1 c_1 c_0) c_1)) (= (f1 c_1 (f1 c_0 c_2)) (f1 (f1 c_1 c_0) c_2)) (= (f1 c_1 (f1 c_0 c_3)) (f1 (f1 c_1 c_0) c_3)) (= (f1 c_1 (f1 c_0 c_4)) (f1 (f1 c_1 c_0) c_4)) (= (f1 c_1 (f1 c_1 c_0)) (f1 (f1 c_1 c_1) c_0)) (= (f1 c_1 (f1 c_1 c_1)) (f1 (f1 c_1 c_1) c_1)) (= (f1 c_1 (f1 c_1 c_2)) (f1 (f1 c_1 c_1) c_2)) (= (f1 c_1 (f1 c_1 c_3)) (f1 (f1 c_1 c_1) c_3)) (= (f1 c_1 (f1 c_1 c_4)) (f1 (f1 c_1 c_1) c_4)) (= (f1 c_1 (f1 c_2 c_0)) (f1 (f1 c_1 c_2) c_0)) (= (f1 c_1 (f1 c_2 c_1)) (f1 (f1 c_1 c_2) c_1)) (= (f1 c_1 (f1 c_2 c_2)) (f1 (f1 c_1 c_2) c_2)) (= (f1 c_1 (f1 c_2 c_3)) (f1 (f1 c_1 c_2) c_3)) (= (f1 c_1 (f1 c_2 c_4)) (f1 (f1 c_1 c_2) c_4)) (= (f1 c_1 (f1 c_3 c_0)) (f1 (f1 c_1 c_3) c_0)) (= (f1 c_1 (f1 c_3 c_1)) (f1 (f1 c_1 c_3) c_1)) (= (f1 c_1 (f1 c_3 c_2)) (f1 (f1 c_1 c_3) c_2)) (= (f1 c_1 (f1 c_3 c_3)) (f1 (f1 c_1 c_3) c_3)) (= (f1 c_1 (f1 c_3 c_4)) (f1 (f1 c_1 c_3) c_4)) (= (f1 c_1 (f1 c_4 c_0)) (f1 (f1 c_1 c_4) c_0)) (= (f1 c_1 (f1 c_4 c_1)) (f1 (f1 c_1 c_4) c_1)) (= (f1 c_1 (f1 c_4 c_2)) (f1 (f1 c_1 c_4) c_2)) (= (f1 c_1 (f1 c_4 c_3)) (f1 (f1 c_1 c_4) c_3)) (= (f1 c_1 (f1 c_4 c_4)) (f1 (f1 c_1 c_4) c_4)) (= (f1 c_2 (f1 c_0 c_0)) (f1 (f1 c_2 c_0) c_0)) (= (f1 c_2 (f1 c_0 c_1)) (f1 (f1 c_2 c_0) c_1)) (= (f1 c_2 (f1 c_0 c_2)) (f1 (f1 c_2 c_0) c_2)) (= (f1 c_2 (f1 c_0 c_3)) (f1 (f1 c_2 c_0) c_3)) (= (f1 c_2 (f1 c_0 c_4)) (f1 (f1 c_2 c_0) c_4)) (= (f1 c_2 (f1 c_1 c_0)) (f1 (f1 c_2 c_1) c_0)) (= (f1 c_2 (f1 c_1 c_1)) (f1 (f1 c_2 c_1) c_1)) (= (f1 c_2 (f1 c_1 c_2)) (f1 (f1 c_2 c_1) c_2)) (= (f1 c_2 (f1 c_1 c_3)) (f1 (f1 c_2 c_1) c_3)) (= (f1 c_2 (f1 c_1 c_4)) (f1 (f1 c_2 c_1) c_4)) (= (f1 c_2 (f1 c_2 c_0)) (f1 (f1 c_2 c_2) c_0)) (= (f1 c_2 (f1 c_2 c_1)) (f1 (f1 c_2 c_2) c_1)) (= (f1 c_2 (f1 c_2 c_2)) (f1 (f1 c_2 c_2) c_2)) (= (f1 c_2 (f1 c_2 c_3)) (f1 (f1 c_2 c_2) c_3)) (= (f1 c_2 (f1 c_2 c_4)) (f1 (f1 c_2 c_2) c_4)) (= (f1 c_2 (f1 c_3 c_0)) (f1 (f1 c_2 c_3) c_0)) (= (f1 c_2 (f1 c_3 c_1)) (f1 (f1 c_2 c_3) c_1)) (= (f1 c_2 (f1 c_3 c_2)) (f1 (f1 c_2 c_3) c_2)) (= (f1 c_2 (f1 c_3 c_3)) (f1 (f1 c_2 c_3) c_3)) (= (f1 c_2 (f1 c_3 c_4)) (f1 (f1 c_2 c_3) c_4)) (= (f1 c_2 (f1 c_4 c_0)) (f1 (f1 c_2 c_4) c_0)) (= (f1 c_2 (f1 c_4 c_1)) (f1 (f1 c_2 c_4) c_1)) (= (f1 c_2 (f1 c_4 c_2)) (f1 (f1 c_2 c_4) c_2)) (= (f1 c_2 (f1 c_4 c_3)) (f1 (f1 c_2 c_4) c_3)) (= (f1 c_2 (f1 c_4 c_4)) (f1 (f1 c_2 c_4) c_4)) (= (f1 c_3 (f1 c_0 c_0)) (f1 (f1 c_3 c_0) c_0)) (= (f1 c_3 (f1 c_0 c_1)) (f1 (f1 c_3 c_0) c_1)) (= (f1 c_3 (f1 c_0 c_2)) (f1 (f1 c_3 c_0) c_2)) (= (f1 c_3 (f1 c_0 c_3)) (f1 (f1 c_3 c_0) c_3)) (= (f1 c_3 (f1 c_0 c_4)) (f1 (f1 c_3 c_0) c_4)) (= (f1 c_3 (f1 c_1 c_0)) (f1 (f1 c_3 c_1) c_0)) (= (f1 c_3 (f1 c_1 c_1)) (f1 (f1 c_3 c_1) c_1)) (= (f1 c_3 (f1 c_1 c_2)) (f1 (f1 c_3 c_1) c_2)) (= (f1 c_3 (f1 c_1 c_3)) (f1 (f1 c_3 c_1) c_3)) (= (f1 c_3 (f1 c_1 c_4)) (f1 (f1 c_3 c_1) c_4)) (= (f1 c_3 (f1 c_2 c_0)) (f1 (f1 c_3 c_2) c_0)) (= (f1 c_3 (f1 c_2 c_1)) (f1 (f1 c_3 c_2) c_1)) (= (f1 c_3 (f1 c_2 c_2)) (f1 (f1 c_3 c_2) c_2)) (= (f1 c_3 (f1 c_2 c_3)) (f1 (f1 c_3 c_2) c_3)) (= (f1 c_3 (f1 c_2 c_4)) (f1 (f1 c_3 c_2) c_4)) (= (f1 c_3 (f1 c_3 c_0)) (f1 (f1 c_3 c_3) c_0)) (= (f1 c_3 (f1 c_3 c_1)) (f1 (f1 c_3 c_3) c_1)) (= (f1 c_3 (f1 c_3 c_2)) (f1 (f1 c_3 c_3) c_2)) (= (f1 c_3 (f1 c_3 c_3)) (f1 (f1 c_3 c_3) c_3)) (= (f1 c_3 (f1 c_3 c_4)) (f1 (f1 c_3 c_3) c_4)) (= (f1 c_3 (f1 c_4 c_0)) (f1 (f1 c_3 c_4) c_0)) (= (f1 c_3 (f1 c_4 c_1)) (f1 (f1 c_3 c_4) c_1)) (= (f1 c_3 (f1 c_4 c_2)) (f1 (f1 c_3 c_4) c_2)) (= (f1 c_3 (f1 c_4 c_3)) (f1 (f1 c_3 c_4) c_3)) (= (f1 c_3 (f1 c_4 c_4)) (f1 (f1 c_3 c_4) c_4)) (= (f1 c_4 (f1 c_0 c_0)) (f1 (f1 c_4 c_0) c_0)) (= (f1 c_4 (f1 c_0 c_1)) (f1 (f1 c_4 c_0) c_1)) (= (f1 c_4 (f1 c_0 c_2)) (f1 (f1 c_4 c_0) c_2)) (= (f1 c_4 (f1 c_0 c_3)) (f1 (f1 c_4 c_0) c_3)) (= (f1 c_4 (f1 c_0 c_4)) (f1 (f1 c_4 c_0) c_4)) (= (f1 c_4 (f1 c_1 c_0)) (f1 (f1 c_4 c_1) c_0)) (= (f1 c_4 (f1 c_1 c_1)) (f1 (f1 c_4 c_1) c_1)) (= (f1 c_4 (f1 c_1 c_2)) (f1 (f1 c_4 c_1) c_2)) (= (f1 c_4 (f1 c_1 c_3)) (f1 (f1 c_4 c_1) c_3)) (= (f1 c_4 (f1 c_1 c_4)) (f1 (f1 c_4 c_1) c_4)) (= (f1 c_4 (f1 c_2 c_0)) (f1 (f1 c_4 c_2) c_0)) (= (f1 c_4 (f1 c_2 c_1)) (f1 (f1 c_4 c_2) c_1)) (= (f1 c_4 (f1 c_2 c_2)) (f1 (f1 c_4 c_2) c_2)) (= (f1 c_4 (f1 c_2 c_3)) (f1 (f1 c_4 c_2) c_3)) (= (f1 c_4 (f1 c_2 c_4)) (f1 (f1 c_4 c_2) c_4)) (= (f1 c_4 (f1 c_3 c_0)) (f1 (f1 c_4 c_3) c_0)) (= (f1 c_4 (f1 c_3 c_1)) (f1 (f1 c_4 c_3) c_1)) (= (f1 c_4 (f1 c_3 c_2)) (f1 (f1 c_4 c_3) c_2)) (= (f1 c_4 (f1 c_3 c_3)) (f1 (f1 c_4 c_3) c_3)) (= (f1 c_4 (f1 c_3 c_4)) (f1 (f1 c_4 c_3) c_4)) (= (f1 c_4 (f1 c_4 c_0)) (f1 (f1 c_4 c_4) c_0)) (= (f1 c_4 (f1 c_4 c_1)) (f1 (f1 c_4 c_4) c_1)) (= (f1 c_4 (f1 c_4 c_2)) (f1 (f1 c_4 c_4) c_2)) (= (f1 c_4 (f1 c_4 c_3)) (f1 (f1 c_4 c_4) c_3)) (= (f1 c_4 (f1 c_4 c_4)) (f1 (f1 c_4 c_4) c_4)) (or (p2 (f1 c_0 c_0)) (not (p3 c_0)) (not (p3 c_0)) )(or (p2 (f1 c_0 c_1)) (not (p3 c_0)) (not (p3 c_1)) )(or (p2 (f1 c_0 c_2)) (not (p3 c_0)) (not (p3 c_2)) )(or (p2 (f1 c_0 c_3)) (not (p3 c_0)) (not (p3 c_3)) )(or (p2 (f1 c_0 c_4)) (not (p3 c_0)) (not (p3 c_4)) )(or (p2 (f1 c_1 c_0)) (not (p3 c_1)) (not (p3 c_0)) )(or (p2 (f1 c_1 c_1)) (not (p3 c_1)) (not (p3 c_1)) )(or (p2 (f1 c_1 c_2)) (not (p3 c_1)) (not (p3 c_2)) )(or (p2 (f1 c_1 c_3)) (not (p3 c_1)) (not (p3 c_3)) )(or (p2 (f1 c_1 c_4)) (not (p3 c_1)) (not (p3 c_4)) )(or (p2 (f1 c_2 c_0)) (not (p3 c_2)) (not (p3 c_0)) )(or (p2 (f1 c_2 c_1)) (not (p3 c_2)) (not (p3 c_1)) )(or (p2 (f1 c_2 c_2)) (not (p3 c_2)) (not (p3 c_2)) )(or (p2 (f1 c_2 c_3)) (not (p3 c_2)) (not (p3 c_3)) )(or (p2 (f1 c_2 c_4)) (not (p3 c_2)) (not (p3 c_4)) )(or (p2 (f1 c_3 c_0)) (not (p3 c_3)) (not (p3 c_0)) )(or (p2 (f1 c_3 c_1)) (not (p3 c_3)) (not (p3 c_1)) )(or (p2 (f1 c_3 c_2)) (not (p3 c_3)) (not (p3 c_2)) )(or (p2 (f1 c_3 c_3)) (not (p3 c_3)) (not (p3 c_3)) )(or (p2 (f1 c_3 c_4)) (not (p3 c_3)) (not (p3 c_4)) )(or (p2 (f1 c_4 c_0)) (not (p3 c_4)) (not (p3 c_0)) )(or (p2 (f1 c_4 c_1)) (not (p3 c_4)) (not (p3 c_1)) )(or (p2 (f1 c_4 c_2)) (not (p3 c_4)) (not (p3 c_2)) )(or (p2 (f1 c_4 c_3)) (not (p3 c_4)) (not (p3 c_3)) )(or (p2 (f1 c_4 c_4)) (not (p3 c_4)) (not (p3 c_4)) )(p4 c7) (or (not (p4 c_0)) (not (p2 c_0)) )(or (not (p4 c_1)) (not (p2 c_1)) )(or (not (p4 c_2)) (not (p2 c_2)) )(or (not (p4 c_3)) (not (p2 c_3)) )(or (not (p4 c_4)) (not (p2 c_4)) )(or (not (p3 c_0)) (not (p4 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) )(or (not (p3 c_2)) (not (p4 c_2)) )(or (not (p3 c_3)) (not (p4 c_3)) )(or (not (p3 c_4)) (not (p4 c_4)) )(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3)(= (f1 c_0 c_0) c_4))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3)(= (f1 c_0 c_1) c_4))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3)(= (f1 c_0 c_2) c_4))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3)(= (f1 c_0 c_3) c_4))(or (= (f1 c_0 c_4) c_0)(= (f1 c_0 c_4) c_1)(= (f1 c_0 c_4) c_2)(= (f1 c_0 c_4) c_3)(= (f1 c_0 c_4) c_4))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3)(= (f1 c_1 c_0) c_4))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3)(= (f1 c_1 c_1) c_4))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3)(= (f1 c_1 c_2) c_4))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3)(= (f1 c_1 c_3) c_4))(or (= (f1 c_1 c_4) c_0)(= (f1 c_1 c_4) c_1)(= (f1 c_1 c_4) c_2)(= (f1 c_1 c_4) c_3)(= (f1 c_1 c_4) c_4))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3)(= (f1 c_2 c_0) c_4))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3)(= (f1 c_2 c_1) c_4))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3)(= (f1 c_2 c_2) c_4))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3)(= (f1 c_2 c_3) c_4))(or (= (f1 c_2 c_4) c_0)(= (f1 c_2 c_4) c_1)(= (f1 c_2 c_4) c_2)(= (f1 c_2 c_4) c_3)(= (f1 c_2 c_4) c_4))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3)(= (f1 c_3 c_0) c_4))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3)(= (f1 c_3 c_1) c_4))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3)(= (f1 c_3 c_2) c_4))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3)(= (f1 c_3 c_3) c_4))(or (= (f1 c_3 c_4) c_0)(= (f1 c_3 c_4) c_1)(= (f1 c_3 c_4) c_2)(= (f1 c_3 c_4) c_3)(= (f1 c_3 c_4) c_4))(or (= (f1 c_4 c_0) c_0)(= (f1 c_4 c_0) c_1)(= (f1 c_4 c_0) c_2)(= (f1 c_4 c_0) c_3)(= (f1 c_4 c_0) c_4))(or (= (f1 c_4 c_1) c_0)(= (f1 c_4 c_1) c_1)(= (f1 c_4 c_1) c_2)(= (f1 c_4 c_1) c_3)(= (f1 c_4 c_1) c_4))(or (= (f1 c_4 c_2) c_0)(= (f1 c_4 c_2) c_1)(= (f1 c_4 c_2) c_2)(= (f1 c_4 c_2) c_3)(= (f1 c_4 c_2) c_4))(or (= (f1 c_4 c_3) c_0)(= (f1 c_4 c_3) c_1)(= (f1 c_4 c_3) c_2)(= (f1 c_4 c_3) c_3)(= (f1 c_4 c_3) c_4))(or (= (f1 c_4 c_4) c_0)(= (f1 c_4 c_4) c_1)(= (f1 c_4 c_4) c_2)(= (f1 c_4 c_4) c_3)(= (f1 c_4 c_4) c_4))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3)(= c6 c_4))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3)(= c7 c_4))))
C880mul.miter.shuffled-as.sat03-348.smt \
comb2.shuffled-as.sat03-420.smt \
hole10.cvc \
- instance_1151.smt
+ instance_1151.smt \
+ NEQ016_size5.smt
EXTRA_DIST = $(TESTS)
--- /dev/null
+(benchmark NEQ016_size5.smt
+:source {
+CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
+ for more information.
+
+This benchmark was obtained by trying to find a finite model of a first-order
+formula (Albert Oliveras).
+}
+:status unsat
+:category { crafted }
+:difficulty { 0 }
+:logic QF_UF
+:extrapreds ((p2 U))
+:extrafuns ((f1 U U U))
+:extrapreds ((p4 U))
+:extrapreds ((p3 U))
+:extrafuns ((c6 U))
+:extrafuns ((c5 U))
+:extrafuns ((c7 U))
+:extrafuns ((c_0 U))
+:extrafuns ((c_1 U))
+:extrafuns ((c_2 U))
+:extrafuns ((c_3 U))
+:extrafuns ((c_4 U))
+:formula
+( and
+( distinct c_0 c_1 c_2 c_3 c_4 )(or (not (p2 c_0)) (not (p2 c_0)) (p4 (f1 c_0 c_0)) (p3 (f1 c_0 c_0)) )(or (not (p2 c_0)) (not (p2 c_1)) (p4 (f1 c_1 c_0)) (p3 (f1 c_1 c_0)) )(or (not (p2 c_0)) (not (p2 c_2)) (p4 (f1 c_2 c_0)) (p3 (f1 c_2 c_0)) )(or (not (p2 c_0)) (not (p2 c_3)) (p4 (f1 c_3 c_0)) (p3 (f1 c_3 c_0)) )(or (not (p2 c_0)) (not (p2 c_4)) (p4 (f1 c_4 c_0)) (p3 (f1 c_4 c_0)) )(or (not (p2 c_1)) (not (p2 c_0)) (p4 (f1 c_0 c_1)) (p3 (f1 c_0 c_1)) )(or (not (p2 c_1)) (not (p2 c_1)) (p4 (f1 c_1 c_1)) (p3 (f1 c_1 c_1)) )(or (not (p2 c_1)) (not (p2 c_2)) (p4 (f1 c_2 c_1)) (p3 (f1 c_2 c_1)) )(or (not (p2 c_1)) (not (p2 c_3)) (p4 (f1 c_3 c_1)) (p3 (f1 c_3 c_1)) )(or (not (p2 c_1)) (not (p2 c_4)) (p4 (f1 c_4 c_1)) (p3 (f1 c_4 c_1)) )(or (not (p2 c_2)) (not (p2 c_0)) (p4 (f1 c_0 c_2)) (p3 (f1 c_0 c_2)) )(or (not (p2 c_2)) (not (p2 c_1)) (p4 (f1 c_1 c_2)) (p3 (f1 c_1 c_2)) )(or (not (p2 c_2)) (not (p2 c_2)) (p4 (f1 c_2 c_2)) (p3 (f1 c_2 c_2)) )(or (not (p2 c_2)) (not (p2 c_3)) (p4 (f1 c_3 c_2)) (p3 (f1 c_3 c_2)) )(or (not (p2 c_2)) (not (p2 c_4)) (p4 (f1 c_4 c_2)) (p3 (f1 c_4 c_2)) )(or (not (p2 c_3)) (not (p2 c_0)) (p4 (f1 c_0 c_3)) (p3 (f1 c_0 c_3)) )(or (not (p2 c_3)) (not (p2 c_1)) (p4 (f1 c_1 c_3)) (p3 (f1 c_1 c_3)) )(or (not (p2 c_3)) (not (p2 c_2)) (p4 (f1 c_2 c_3)) (p3 (f1 c_2 c_3)) )(or (not (p2 c_3)) (not (p2 c_3)) (p4 (f1 c_3 c_3)) (p3 (f1 c_3 c_3)) )(or (not (p2 c_3)) (not (p2 c_4)) (p4 (f1 c_4 c_3)) (p3 (f1 c_4 c_3)) )(or (not (p2 c_4)) (not (p2 c_0)) (p4 (f1 c_0 c_4)) (p3 (f1 c_0 c_4)) )(or (not (p2 c_4)) (not (p2 c_1)) (p4 (f1 c_1 c_4)) (p3 (f1 c_1 c_4)) )(or (not (p2 c_4)) (not (p2 c_2)) (p4 (f1 c_2 c_4)) (p3 (f1 c_2 c_4)) )(or (not (p2 c_4)) (not (p2 c_3)) (p4 (f1 c_3 c_4)) (p3 (f1 c_3 c_4)) )(or (not (p2 c_4)) (not (p2 c_4)) (p4 (f1 c_4 c_4)) (p3 (f1 c_4 c_4)) )(or (not (p2 c_0)) (not (p3 c_0)) )(or (not (p2 c_1)) (not (p3 c_1)) )(or (not (p2 c_2)) (not (p3 c_2)) )(or (not (p2 c_3)) (not (p3 c_3)) )(or (not (p2 c_4)) (not (p3 c_4)) )(or (p4 c_0) (p3 c_0) (p2 c_0) )(or (p4 c_1) (p3 c_1) (p2 c_1) )(or (p4 c_2) (p3 c_2) (p2 c_2) )(or (p4 c_3) (p3 c_3) (p2 c_3) )(or (p4 c_4) (p3 c_4) (p2 c_4) )(p3 c6) (p2 c5) (or (not (p4 c_0)) (not (p4 c_0)) (p2 (f1 c_0 c_0)) )(or (not (p4 c_0)) (not (p4 c_1)) (p2 (f1 c_1 c_0)) )(or (not (p4 c_0)) (not (p4 c_2)) (p2 (f1 c_2 c_0)) )(or (not (p4 c_0)) (not (p4 c_3)) (p2 (f1 c_3 c_0)) )(or (not (p4 c_0)) (not (p4 c_4)) (p2 (f1 c_4 c_0)) )(or (not (p4 c_1)) (not (p4 c_0)) (p2 (f1 c_0 c_1)) )(or (not (p4 c_1)) (not (p4 c_1)) (p2 (f1 c_1 c_1)) )(or (not (p4 c_1)) (not (p4 c_2)) (p2 (f1 c_2 c_1)) )(or (not (p4 c_1)) (not (p4 c_3)) (p2 (f1 c_3 c_1)) )(or (not (p4 c_1)) (not (p4 c_4)) (p2 (f1 c_4 c_1)) )(or (not (p4 c_2)) (not (p4 c_0)) (p2 (f1 c_0 c_2)) )(or (not (p4 c_2)) (not (p4 c_1)) (p2 (f1 c_1 c_2)) )(or (not (p4 c_2)) (not (p4 c_2)) (p2 (f1 c_2 c_2)) )(or (not (p4 c_2)) (not (p4 c_3)) (p2 (f1 c_3 c_2)) )(or (not (p4 c_2)) (not (p4 c_4)) (p2 (f1 c_4 c_2)) )(or (not (p4 c_3)) (not (p4 c_0)) (p2 (f1 c_0 c_3)) )(or (not (p4 c_3)) (not (p4 c_1)) (p2 (f1 c_1 c_3)) )(or (not (p4 c_3)) (not (p4 c_2)) (p2 (f1 c_2 c_3)) )(or (not (p4 c_3)) (not (p4 c_3)) (p2 (f1 c_3 c_3)) )(or (not (p4 c_3)) (not (p4 c_4)) (p2 (f1 c_4 c_3)) )(or (not (p4 c_4)) (not (p4 c_0)) (p2 (f1 c_0 c_4)) )(or (not (p4 c_4)) (not (p4 c_1)) (p2 (f1 c_1 c_4)) )(or (not (p4 c_4)) (not (p4 c_2)) (p2 (f1 c_2 c_4)) )(or (not (p4 c_4)) (not (p4 c_3)) (p2 (f1 c_3 c_4)) )(or (not (p4 c_4)) (not (p4 c_4)) (p2 (f1 c_4 c_4)) )(= (f1 c_0 (f1 c_0 c_0)) (f1 (f1 c_0 c_0) c_0)) (= (f1 c_0 (f1 c_0 c_1)) (f1 (f1 c_0 c_0) c_1)) (= (f1 c_0 (f1 c_0 c_2)) (f1 (f1 c_0 c_0) c_2)) (= (f1 c_0 (f1 c_0 c_3)) (f1 (f1 c_0 c_0) c_3)) (= (f1 c_0 (f1 c_0 c_4)) (f1 (f1 c_0 c_0) c_4)) (= (f1 c_0 (f1 c_1 c_0)) (f1 (f1 c_0 c_1) c_0)) (= (f1 c_0 (f1 c_1 c_1)) (f1 (f1 c_0 c_1) c_1)) (= (f1 c_0 (f1 c_1 c_2)) (f1 (f1 c_0 c_1) c_2)) (= (f1 c_0 (f1 c_1 c_3)) (f1 (f1 c_0 c_1) c_3)) (= (f1 c_0 (f1 c_1 c_4)) (f1 (f1 c_0 c_1) c_4)) (= (f1 c_0 (f1 c_2 c_0)) (f1 (f1 c_0 c_2) c_0)) (= (f1 c_0 (f1 c_2 c_1)) (f1 (f1 c_0 c_2) c_1)) (= (f1 c_0 (f1 c_2 c_2)) (f1 (f1 c_0 c_2) c_2)) (= (f1 c_0 (f1 c_2 c_3)) (f1 (f1 c_0 c_2) c_3)) (= (f1 c_0 (f1 c_2 c_4)) (f1 (f1 c_0 c_2) c_4)) (= (f1 c_0 (f1 c_3 c_0)) (f1 (f1 c_0 c_3) c_0)) (= (f1 c_0 (f1 c_3 c_1)) (f1 (f1 c_0 c_3) c_1)) (= (f1 c_0 (f1 c_3 c_2)) (f1 (f1 c_0 c_3) c_2)) (= (f1 c_0 (f1 c_3 c_3)) (f1 (f1 c_0 c_3) c_3)) (= (f1 c_0 (f1 c_3 c_4)) (f1 (f1 c_0 c_3) c_4)) (= (f1 c_0 (f1 c_4 c_0)) (f1 (f1 c_0 c_4) c_0)) (= (f1 c_0 (f1 c_4 c_1)) (f1 (f1 c_0 c_4) c_1)) (= (f1 c_0 (f1 c_4 c_2)) (f1 (f1 c_0 c_4) c_2)) (= (f1 c_0 (f1 c_4 c_3)) (f1 (f1 c_0 c_4) c_3)) (= (f1 c_0 (f1 c_4 c_4)) (f1 (f1 c_0 c_4) c_4)) (= (f1 c_1 (f1 c_0 c_0)) (f1 (f1 c_1 c_0) c_0)) (= (f1 c_1 (f1 c_0 c_1)) (f1 (f1 c_1 c_0) c_1)) (= (f1 c_1 (f1 c_0 c_2)) (f1 (f1 c_1 c_0) c_2)) (= (f1 c_1 (f1 c_0 c_3)) (f1 (f1 c_1 c_0) c_3)) (= (f1 c_1 (f1 c_0 c_4)) (f1 (f1 c_1 c_0) c_4)) (= (f1 c_1 (f1 c_1 c_0)) (f1 (f1 c_1 c_1) c_0)) (= (f1 c_1 (f1 c_1 c_1)) (f1 (f1 c_1 c_1) c_1)) (= (f1 c_1 (f1 c_1 c_2)) (f1 (f1 c_1 c_1) c_2)) (= (f1 c_1 (f1 c_1 c_3)) (f1 (f1 c_1 c_1) c_3)) (= (f1 c_1 (f1 c_1 c_4)) (f1 (f1 c_1 c_1) c_4)) (= (f1 c_1 (f1 c_2 c_0)) (f1 (f1 c_1 c_2) c_0)) (= (f1 c_1 (f1 c_2 c_1)) (f1 (f1 c_1 c_2) c_1)) (= (f1 c_1 (f1 c_2 c_2)) (f1 (f1 c_1 c_2) c_2)) (= (f1 c_1 (f1 c_2 c_3)) (f1 (f1 c_1 c_2) c_3)) (= (f1 c_1 (f1 c_2 c_4)) (f1 (f1 c_1 c_2) c_4)) (= (f1 c_1 (f1 c_3 c_0)) (f1 (f1 c_1 c_3) c_0)) (= (f1 c_1 (f1 c_3 c_1)) (f1 (f1 c_1 c_3) c_1)) (= (f1 c_1 (f1 c_3 c_2)) (f1 (f1 c_1 c_3) c_2)) (= (f1 c_1 (f1 c_3 c_3)) (f1 (f1 c_1 c_3) c_3)) (= (f1 c_1 (f1 c_3 c_4)) (f1 (f1 c_1 c_3) c_4)) (= (f1 c_1 (f1 c_4 c_0)) (f1 (f1 c_1 c_4) c_0)) (= (f1 c_1 (f1 c_4 c_1)) (f1 (f1 c_1 c_4) c_1)) (= (f1 c_1 (f1 c_4 c_2)) (f1 (f1 c_1 c_4) c_2)) (= (f1 c_1 (f1 c_4 c_3)) (f1 (f1 c_1 c_4) c_3)) (= (f1 c_1 (f1 c_4 c_4)) (f1 (f1 c_1 c_4) c_4)) (= (f1 c_2 (f1 c_0 c_0)) (f1 (f1 c_2 c_0) c_0)) (= (f1 c_2 (f1 c_0 c_1)) (f1 (f1 c_2 c_0) c_1)) (= (f1 c_2 (f1 c_0 c_2)) (f1 (f1 c_2 c_0) c_2)) (= (f1 c_2 (f1 c_0 c_3)) (f1 (f1 c_2 c_0) c_3)) (= (f1 c_2 (f1 c_0 c_4)) (f1 (f1 c_2 c_0) c_4)) (= (f1 c_2 (f1 c_1 c_0)) (f1 (f1 c_2 c_1) c_0)) (= (f1 c_2 (f1 c_1 c_1)) (f1 (f1 c_2 c_1) c_1)) (= (f1 c_2 (f1 c_1 c_2)) (f1 (f1 c_2 c_1) c_2)) (= (f1 c_2 (f1 c_1 c_3)) (f1 (f1 c_2 c_1) c_3)) (= (f1 c_2 (f1 c_1 c_4)) (f1 (f1 c_2 c_1) c_4)) (= (f1 c_2 (f1 c_2 c_0)) (f1 (f1 c_2 c_2) c_0)) (= (f1 c_2 (f1 c_2 c_1)) (f1 (f1 c_2 c_2) c_1)) (= (f1 c_2 (f1 c_2 c_2)) (f1 (f1 c_2 c_2) c_2)) (= (f1 c_2 (f1 c_2 c_3)) (f1 (f1 c_2 c_2) c_3)) (= (f1 c_2 (f1 c_2 c_4)) (f1 (f1 c_2 c_2) c_4)) (= (f1 c_2 (f1 c_3 c_0)) (f1 (f1 c_2 c_3) c_0)) (= (f1 c_2 (f1 c_3 c_1)) (f1 (f1 c_2 c_3) c_1)) (= (f1 c_2 (f1 c_3 c_2)) (f1 (f1 c_2 c_3) c_2)) (= (f1 c_2 (f1 c_3 c_3)) (f1 (f1 c_2 c_3) c_3)) (= (f1 c_2 (f1 c_3 c_4)) (f1 (f1 c_2 c_3) c_4)) (= (f1 c_2 (f1 c_4 c_0)) (f1 (f1 c_2 c_4) c_0)) (= (f1 c_2 (f1 c_4 c_1)) (f1 (f1 c_2 c_4) c_1)) (= (f1 c_2 (f1 c_4 c_2)) (f1 (f1 c_2 c_4) c_2)) (= (f1 c_2 (f1 c_4 c_3)) (f1 (f1 c_2 c_4) c_3)) (= (f1 c_2 (f1 c_4 c_4)) (f1 (f1 c_2 c_4) c_4)) (= (f1 c_3 (f1 c_0 c_0)) (f1 (f1 c_3 c_0) c_0)) (= (f1 c_3 (f1 c_0 c_1)) (f1 (f1 c_3 c_0) c_1)) (= (f1 c_3 (f1 c_0 c_2)) (f1 (f1 c_3 c_0) c_2)) (= (f1 c_3 (f1 c_0 c_3)) (f1 (f1 c_3 c_0) c_3)) (= (f1 c_3 (f1 c_0 c_4)) (f1 (f1 c_3 c_0) c_4)) (= (f1 c_3 (f1 c_1 c_0)) (f1 (f1 c_3 c_1) c_0)) (= (f1 c_3 (f1 c_1 c_1)) (f1 (f1 c_3 c_1) c_1)) (= (f1 c_3 (f1 c_1 c_2)) (f1 (f1 c_3 c_1) c_2)) (= (f1 c_3 (f1 c_1 c_3)) (f1 (f1 c_3 c_1) c_3)) (= (f1 c_3 (f1 c_1 c_4)) (f1 (f1 c_3 c_1) c_4)) (= (f1 c_3 (f1 c_2 c_0)) (f1 (f1 c_3 c_2) c_0)) (= (f1 c_3 (f1 c_2 c_1)) (f1 (f1 c_3 c_2) c_1)) (= (f1 c_3 (f1 c_2 c_2)) (f1 (f1 c_3 c_2) c_2)) (= (f1 c_3 (f1 c_2 c_3)) (f1 (f1 c_3 c_2) c_3)) (= (f1 c_3 (f1 c_2 c_4)) (f1 (f1 c_3 c_2) c_4)) (= (f1 c_3 (f1 c_3 c_0)) (f1 (f1 c_3 c_3) c_0)) (= (f1 c_3 (f1 c_3 c_1)) (f1 (f1 c_3 c_3) c_1)) (= (f1 c_3 (f1 c_3 c_2)) (f1 (f1 c_3 c_3) c_2)) (= (f1 c_3 (f1 c_3 c_3)) (f1 (f1 c_3 c_3) c_3)) (= (f1 c_3 (f1 c_3 c_4)) (f1 (f1 c_3 c_3) c_4)) (= (f1 c_3 (f1 c_4 c_0)) (f1 (f1 c_3 c_4) c_0)) (= (f1 c_3 (f1 c_4 c_1)) (f1 (f1 c_3 c_4) c_1)) (= (f1 c_3 (f1 c_4 c_2)) (f1 (f1 c_3 c_4) c_2)) (= (f1 c_3 (f1 c_4 c_3)) (f1 (f1 c_3 c_4) c_3)) (= (f1 c_3 (f1 c_4 c_4)) (f1 (f1 c_3 c_4) c_4)) (= (f1 c_4 (f1 c_0 c_0)) (f1 (f1 c_4 c_0) c_0)) (= (f1 c_4 (f1 c_0 c_1)) (f1 (f1 c_4 c_0) c_1)) (= (f1 c_4 (f1 c_0 c_2)) (f1 (f1 c_4 c_0) c_2)) (= (f1 c_4 (f1 c_0 c_3)) (f1 (f1 c_4 c_0) c_3)) (= (f1 c_4 (f1 c_0 c_4)) (f1 (f1 c_4 c_0) c_4)) (= (f1 c_4 (f1 c_1 c_0)) (f1 (f1 c_4 c_1) c_0)) (= (f1 c_4 (f1 c_1 c_1)) (f1 (f1 c_4 c_1) c_1)) (= (f1 c_4 (f1 c_1 c_2)) (f1 (f1 c_4 c_1) c_2)) (= (f1 c_4 (f1 c_1 c_3)) (f1 (f1 c_4 c_1) c_3)) (= (f1 c_4 (f1 c_1 c_4)) (f1 (f1 c_4 c_1) c_4)) (= (f1 c_4 (f1 c_2 c_0)) (f1 (f1 c_4 c_2) c_0)) (= (f1 c_4 (f1 c_2 c_1)) (f1 (f1 c_4 c_2) c_1)) (= (f1 c_4 (f1 c_2 c_2)) (f1 (f1 c_4 c_2) c_2)) (= (f1 c_4 (f1 c_2 c_3)) (f1 (f1 c_4 c_2) c_3)) (= (f1 c_4 (f1 c_2 c_4)) (f1 (f1 c_4 c_2) c_4)) (= (f1 c_4 (f1 c_3 c_0)) (f1 (f1 c_4 c_3) c_0)) (= (f1 c_4 (f1 c_3 c_1)) (f1 (f1 c_4 c_3) c_1)) (= (f1 c_4 (f1 c_3 c_2)) (f1 (f1 c_4 c_3) c_2)) (= (f1 c_4 (f1 c_3 c_3)) (f1 (f1 c_4 c_3) c_3)) (= (f1 c_4 (f1 c_3 c_4)) (f1 (f1 c_4 c_3) c_4)) (= (f1 c_4 (f1 c_4 c_0)) (f1 (f1 c_4 c_4) c_0)) (= (f1 c_4 (f1 c_4 c_1)) (f1 (f1 c_4 c_4) c_1)) (= (f1 c_4 (f1 c_4 c_2)) (f1 (f1 c_4 c_4) c_2)) (= (f1 c_4 (f1 c_4 c_3)) (f1 (f1 c_4 c_4) c_3)) (= (f1 c_4 (f1 c_4 c_4)) (f1 (f1 c_4 c_4) c_4)) (or (p2 (f1 c_0 c_0)) (not (p3 c_0)) (not (p3 c_0)) )(or (p2 (f1 c_0 c_1)) (not (p3 c_0)) (not (p3 c_1)) )(or (p2 (f1 c_0 c_2)) (not (p3 c_0)) (not (p3 c_2)) )(or (p2 (f1 c_0 c_3)) (not (p3 c_0)) (not (p3 c_3)) )(or (p2 (f1 c_0 c_4)) (not (p3 c_0)) (not (p3 c_4)) )(or (p2 (f1 c_1 c_0)) (not (p3 c_1)) (not (p3 c_0)) )(or (p2 (f1 c_1 c_1)) (not (p3 c_1)) (not (p3 c_1)) )(or (p2 (f1 c_1 c_2)) (not (p3 c_1)) (not (p3 c_2)) )(or (p2 (f1 c_1 c_3)) (not (p3 c_1)) (not (p3 c_3)) )(or (p2 (f1 c_1 c_4)) (not (p3 c_1)) (not (p3 c_4)) )(or (p2 (f1 c_2 c_0)) (not (p3 c_2)) (not (p3 c_0)) )(or (p2 (f1 c_2 c_1)) (not (p3 c_2)) (not (p3 c_1)) )(or (p2 (f1 c_2 c_2)) (not (p3 c_2)) (not (p3 c_2)) )(or (p2 (f1 c_2 c_3)) (not (p3 c_2)) (not (p3 c_3)) )(or (p2 (f1 c_2 c_4)) (not (p3 c_2)) (not (p3 c_4)) )(or (p2 (f1 c_3 c_0)) (not (p3 c_3)) (not (p3 c_0)) )(or (p2 (f1 c_3 c_1)) (not (p3 c_3)) (not (p3 c_1)) )(or (p2 (f1 c_3 c_2)) (not (p3 c_3)) (not (p3 c_2)) )(or (p2 (f1 c_3 c_3)) (not (p3 c_3)) (not (p3 c_3)) )(or (p2 (f1 c_3 c_4)) (not (p3 c_3)) (not (p3 c_4)) )(or (p2 (f1 c_4 c_0)) (not (p3 c_4)) (not (p3 c_0)) )(or (p2 (f1 c_4 c_1)) (not (p3 c_4)) (not (p3 c_1)) )(or (p2 (f1 c_4 c_2)) (not (p3 c_4)) (not (p3 c_2)) )(or (p2 (f1 c_4 c_3)) (not (p3 c_4)) (not (p3 c_3)) )(or (p2 (f1 c_4 c_4)) (not (p3 c_4)) (not (p3 c_4)) )(p4 c7) (or (not (p4 c_0)) (not (p2 c_0)) )(or (not (p4 c_1)) (not (p2 c_1)) )(or (not (p4 c_2)) (not (p2 c_2)) )(or (not (p4 c_3)) (not (p2 c_3)) )(or (not (p4 c_4)) (not (p2 c_4)) )(or (not (p3 c_0)) (not (p4 c_0)) )(or (not (p3 c_1)) (not (p4 c_1)) )(or (not (p3 c_2)) (not (p4 c_2)) )(or (not (p3 c_3)) (not (p4 c_3)) )(or (not (p3 c_4)) (not (p4 c_4)) )(or (= (f1 c_0 c_0) c_0)(= (f1 c_0 c_0) c_1)(= (f1 c_0 c_0) c_2)(= (f1 c_0 c_0) c_3)(= (f1 c_0 c_0) c_4))(or (= (f1 c_0 c_1) c_0)(= (f1 c_0 c_1) c_1)(= (f1 c_0 c_1) c_2)(= (f1 c_0 c_1) c_3)(= (f1 c_0 c_1) c_4))(or (= (f1 c_0 c_2) c_0)(= (f1 c_0 c_2) c_1)(= (f1 c_0 c_2) c_2)(= (f1 c_0 c_2) c_3)(= (f1 c_0 c_2) c_4))(or (= (f1 c_0 c_3) c_0)(= (f1 c_0 c_3) c_1)(= (f1 c_0 c_3) c_2)(= (f1 c_0 c_3) c_3)(= (f1 c_0 c_3) c_4))(or (= (f1 c_0 c_4) c_0)(= (f1 c_0 c_4) c_1)(= (f1 c_0 c_4) c_2)(= (f1 c_0 c_4) c_3)(= (f1 c_0 c_4) c_4))(or (= (f1 c_1 c_0) c_0)(= (f1 c_1 c_0) c_1)(= (f1 c_1 c_0) c_2)(= (f1 c_1 c_0) c_3)(= (f1 c_1 c_0) c_4))(or (= (f1 c_1 c_1) c_0)(= (f1 c_1 c_1) c_1)(= (f1 c_1 c_1) c_2)(= (f1 c_1 c_1) c_3)(= (f1 c_1 c_1) c_4))(or (= (f1 c_1 c_2) c_0)(= (f1 c_1 c_2) c_1)(= (f1 c_1 c_2) c_2)(= (f1 c_1 c_2) c_3)(= (f1 c_1 c_2) c_4))(or (= (f1 c_1 c_3) c_0)(= (f1 c_1 c_3) c_1)(= (f1 c_1 c_3) c_2)(= (f1 c_1 c_3) c_3)(= (f1 c_1 c_3) c_4))(or (= (f1 c_1 c_4) c_0)(= (f1 c_1 c_4) c_1)(= (f1 c_1 c_4) c_2)(= (f1 c_1 c_4) c_3)(= (f1 c_1 c_4) c_4))(or (= (f1 c_2 c_0) c_0)(= (f1 c_2 c_0) c_1)(= (f1 c_2 c_0) c_2)(= (f1 c_2 c_0) c_3)(= (f1 c_2 c_0) c_4))(or (= (f1 c_2 c_1) c_0)(= (f1 c_2 c_1) c_1)(= (f1 c_2 c_1) c_2)(= (f1 c_2 c_1) c_3)(= (f1 c_2 c_1) c_4))(or (= (f1 c_2 c_2) c_0)(= (f1 c_2 c_2) c_1)(= (f1 c_2 c_2) c_2)(= (f1 c_2 c_2) c_3)(= (f1 c_2 c_2) c_4))(or (= (f1 c_2 c_3) c_0)(= (f1 c_2 c_3) c_1)(= (f1 c_2 c_3) c_2)(= (f1 c_2 c_3) c_3)(= (f1 c_2 c_3) c_4))(or (= (f1 c_2 c_4) c_0)(= (f1 c_2 c_4) c_1)(= (f1 c_2 c_4) c_2)(= (f1 c_2 c_4) c_3)(= (f1 c_2 c_4) c_4))(or (= (f1 c_3 c_0) c_0)(= (f1 c_3 c_0) c_1)(= (f1 c_3 c_0) c_2)(= (f1 c_3 c_0) c_3)(= (f1 c_3 c_0) c_4))(or (= (f1 c_3 c_1) c_0)(= (f1 c_3 c_1) c_1)(= (f1 c_3 c_1) c_2)(= (f1 c_3 c_1) c_3)(= (f1 c_3 c_1) c_4))(or (= (f1 c_3 c_2) c_0)(= (f1 c_3 c_2) c_1)(= (f1 c_3 c_2) c_2)(= (f1 c_3 c_2) c_3)(= (f1 c_3 c_2) c_4))(or (= (f1 c_3 c_3) c_0)(= (f1 c_3 c_3) c_1)(= (f1 c_3 c_3) c_2)(= (f1 c_3 c_3) c_3)(= (f1 c_3 c_3) c_4))(or (= (f1 c_3 c_4) c_0)(= (f1 c_3 c_4) c_1)(= (f1 c_3 c_4) c_2)(= (f1 c_3 c_4) c_3)(= (f1 c_3 c_4) c_4))(or (= (f1 c_4 c_0) c_0)(= (f1 c_4 c_0) c_1)(= (f1 c_4 c_0) c_2)(= (f1 c_4 c_0) c_3)(= (f1 c_4 c_0) c_4))(or (= (f1 c_4 c_1) c_0)(= (f1 c_4 c_1) c_1)(= (f1 c_4 c_1) c_2)(= (f1 c_4 c_1) c_3)(= (f1 c_4 c_1) c_4))(or (= (f1 c_4 c_2) c_0)(= (f1 c_4 c_2) c_1)(= (f1 c_4 c_2) c_2)(= (f1 c_4 c_2) c_3)(= (f1 c_4 c_2) c_4))(or (= (f1 c_4 c_3) c_0)(= (f1 c_4 c_3) c_1)(= (f1 c_4 c_3) c_2)(= (f1 c_4 c_3) c_3)(= (f1 c_4 c_3) c_4))(or (= (f1 c_4 c_4) c_0)(= (f1 c_4 c_4) c_1)(= (f1 c_4 c_4) c_2)(= (f1 c_4 c_4) c_3)(= (f1 c_4 c_4) c_4))(or (= c6 c_0)(= c6 c_1)(= c6 c_2)(= c6 c_3)(= c6 c_4))(or (= c5 c_0)(= c5 c_1)(= c5 c_2)(= c5 c_3)(= c5 c_4))(or (= c7 c_0)(= c7 c_1)(= c7 c_2)(= c7 c_3)(= c7 c_4))))
context/context_mm_black \
context/cdo_black \
context/cdlist_black \
+ context/cdlist_context_memory_black \
context/cdmap_black \
context/cdmap_white \
context/cdvector_black \
--- /dev/null
+/********************* */
+/*! \file cdlist_context_memory_black.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 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 Black box testing of CVC4::context::CDList<>.
+ **
+ ** Black box testing of CVC4::context::CDList<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+
+#include <limits.h>
+
+#include "memory.h"
+
+#include "context/context.h"
+#include "context/cdlist_context_memory.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4::test;
+
+struct DtorSensitiveObject {
+ bool& d_dtorCalled;
+ DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {}
+ ~DtorSensitiveObject() { d_dtorCalled = true; }
+};
+
+class CDListContextMemoryBlack : public CxxTest::TestSuite {
+private:
+
+ Context* d_context;
+
+public:
+
+ void setUp() {
+ d_context = new Context();
+ }
+
+ void tearDown() {
+ delete d_context;
+ }
+
+ // test at different sizes. this triggers grow() behavior differently.
+ // grow() was completely broken in revision 256
+ void testCDList10() { listTest(10); }
+ void testCDList15() { listTest(15); }
+ void testCDList20() { listTest(20); }
+ void testCDList35() { listTest(35); }
+ void testCDList50() { listTest(50); }
+ void testCDList99() { listTest(99); }
+
+ void listTest(int N) {
+ listTest(N, true);
+ listTest(N, false);
+ }
+
+ void listTest(int N, bool callDestructor) {
+ CDList<int, ContextMemoryAllocator<int> >
+ list(d_context, callDestructor, ContextMemoryAllocator<int>(d_context->getCMM()));
+
+ TS_ASSERT(list.empty());
+ for(int i = 0; i < N; ++i) {
+ TS_ASSERT_EQUALS(list.size(), unsigned(i));
+ list.push_back(i);
+ TS_ASSERT(!list.empty());
+ TS_ASSERT_EQUALS(list.back(), i);
+ int i2 = 0;
+ for(CDList<int, ContextMemoryAllocator<int> >::const_iterator j = list.begin();
+ j != list.end();
+ ++j) {
+ TS_ASSERT_EQUALS(*j, i2++);
+ }
+ }
+ TS_ASSERT_EQUALS(list.size(), unsigned(N));
+
+ for(int i = 0; i < N; ++i) {
+ TS_ASSERT_EQUALS(list[i], i);
+ }
+ }
+
+ void testDtorCalled() {
+ bool shouldRemainFalse = false;
+ bool shouldFlipToTrue = false;
+ bool alsoFlipToTrue = false;
+ bool shouldAlsoRemainFalse = false;
+ bool aThirdFalse = false;
+
+ CDList<DtorSensitiveObject, ContextMemoryAllocator<DtorSensitiveObject> > listT(d_context, true, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
+ CDList<DtorSensitiveObject, ContextMemoryAllocator<DtorSensitiveObject> > listF(d_context, false, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
+
+ DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
+ DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
+ DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue);
+ DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse);
+ DtorSensitiveObject aThirdFalseDSO(aThirdFalse);
+
+ listT.push_back(shouldAlsoRemainFalseDSO);
+ listF.push_back(shouldAlsoRemainFalseDSO);
+
+ d_context->push();
+
+ listT.push_back(shouldFlipToTrueDSO);
+ listT.push_back(alsoFlipToTrueDSO);
+
+ listF.push_back(shouldRemainFalseDSO);
+ listF.push_back(shouldAlsoRemainFalseDSO);
+ listF.push_back(aThirdFalseDSO);
+
+ TS_ASSERT_EQUALS(shouldRemainFalse, false);
+ TS_ASSERT_EQUALS(shouldFlipToTrue, false);
+ TS_ASSERT_EQUALS(alsoFlipToTrue, false);
+ TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
+ TS_ASSERT_EQUALS(aThirdFalse, false);
+
+ d_context->pop();
+
+ TS_ASSERT_EQUALS(shouldRemainFalse, false);
+ TS_ASSERT_EQUALS(shouldFlipToTrue, true);
+ TS_ASSERT_EQUALS(alsoFlipToTrue, true);
+ TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
+ TS_ASSERT_EQUALS(aThirdFalse, false);
+ }
+
+ /* setrlimit() totally broken on Mac OS X */
+ void testOutOfMemory() {
+#ifdef __APPLE__
+
+ TS_WARN("can't run memory tests on Mac OS X");
+
+#else /* __APPLE__ */
+
+ CDList<unsigned, ContextMemoryAllocator<unsigned> > list(d_context);
+ WithLimitedMemory wlm(1);
+
+ TS_ASSERT_THROWS({
+ // We cap it at UINT_MAX, preferring to terminate with a
+ // failure than run indefinitely.
+ for(unsigned i = 0; i < UINT_MAX; ++i) {
+ list.push_back(i);
+ }
+ }, bad_alloc);
+
+#endif /* __APPLE__ */
+ }
+};
projects / cvc5.git / commitdiff