summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/context/cddense_set.h4
-rw-r--r--src/context/cdlist.h459
-rw-r--r--src/context/cdlist_forward.h8
-rw-r--r--src/context/cdqueue.h38
-rw-r--r--src/context/default_clean_up.h34
-rw-r--r--src/theory/arith/constraint.h18
-rw-r--r--src/theory/arith/partial_model.cpp10
-rw-r--r--src/theory/arith/partial_model.h4
-rw-r--r--src/theory/assertion.h4
-rw-r--r--test/unit/context/cdlist_black.h30
11 files changed, 232 insertions, 378 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e56379f0c..2334989b2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -33,6 +33,7 @@ libcvc4_add_sources(
context/context.h
context/context_mm.cpp
context/context_mm.h
+ context/default_clean_up.h
decision/decision_attributes.h
decision/decision_engine.cpp
decision/decision_engine.h
diff --git a/src/context/cddense_set.h b/src/context/cddense_set.h
index a59a32592..c5f3149e9 100644
--- a/src/context/cddense_set.h
+++ b/src/context/cddense_set.h
@@ -23,9 +23,9 @@
#include <vector>
-#include "context/context.h"
-#include "context/cdlist_forward.h"
#include "context/cdlist.h"
+#include "context/context.h"
+#include "context/default_clean_up.h"
#include "util/index.h"
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index cb5e552ac..aba1c49e0 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -22,219 +22,68 @@
#include <iterator>
#include <memory>
-#include <string>
#include <sstream>
+#include <string>
+#include <vector>
#include "base/check.h"
#include "context/cdlist_forward.h"
#include "context/context.h"
#include "context/context_mm.h"
+#include "context/default_clean_up.h"
namespace CVC4 {
namespace context {
/**
- * 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.
+ * Generic context-dependent dynamic array. Note that for efficiency, this
+ * implementation makes the following assumption: Over time, objects are only
+ * added to the list. Objects are only removed when a pop restores the list to
+ * a previous state.
*/
-template <class T, class CleanUpT, class AllocatorT>
-class CDList : public ContextObj {
-public:
-
+template <class T, class CleanUpT, class Allocator>
+class CDList : public ContextObj
+{
+ public:
/** The value type with which this CDList<> was instantiated. */
- typedef T value_type;
+ using value_type = T;
/** The cleanup type with which this CDList<> was instantiated. */
- typedef CleanUpT CleanUp;
-
- /** The allocator type with which this CDList<> was instantiated. */
- typedef AllocatorT Allocator;
-
-protected:
+ using CleanUp = CleanUpT;
/**
- * d_list is a dynamic array of objects of type T.
+ * `std::vector<T>::operator[] const` returns an
+ * std::vector<T>::const_reference, which does not necessarily have to be a
+ * `const T&`. Specifically, in the case of `std::vector<bool>`, the type is
+ * specialized to be just a simple `bool`. For our `operator[] const`, we use
+ * the same type.
*/
- T* d_list;
+ using ConstReference = typename std::vector<T>::const_reference;
/**
- * Number of objects in d_list
+ * Instead of implementing our own iterators, we just use the iterators of
+ * the underlying `std::vector<T>`.
*/
- size_t d_size;
-
-private:
-
- static const size_t INITIAL_SIZE = 10;
- static const size_t GROWTH_FACTOR = 2;
+ using const_iterator = typename std::vector<T>::const_iterator;
+ using iterator = typename std::vector<T>::const_iterator;
/**
- * 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;
-
- /**
- * Allocated size of d_list.
- */
- size_t d_sizeAlloc;
-
- /**
- * The CleanUp functor.
- */
- CleanUp d_cleanUp;
-
- /**
- * Our allocator.
- */
- Allocator d_allocator;
-
-protected:
- /**
- * 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& l) :
- ContextObj(l),
- d_list(NULL),
- d_size(l.d_size),
- d_callDestructor(false),
- d_sizeAlloc(0),
- d_cleanUp(l.d_cleanUp),
- d_allocator(l.d_allocator) {
- Debug("cdlist") << "copy ctor: " << this
- << " from " << &l
- << " size " << d_size << std::endl;
- }
- CDList& operator=(const CDList& l) = delete;
-
-private:
- /**
- * Reallocate the array with more space.
- * Throws bad_alloc if memory allocation fails.
- */
- void grow() {
- if(d_list == NULL) {
- // Allocate an initial list if one does not yet exist
- 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
- 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();
- }
- 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) override
- {
- ContextObj* data = new(pCMM) CDList<T, CleanUp, 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;
- }
-
-protected:
- /**
- * Implementation of mandatory ContextObj method restore: simply
- * restores the previous size. Note that the list pointer and the
- * allocated size are not changed.
- */
- void restore(ContextObj* data) override
- {
- Debug("cdlist") << "restore " << this << " level "
- << this->getContext()->getLevel() << " data == " << data
- << " call dtor == " << this->d_callDestructor
- << " d_list == " << this->d_list << std::endl;
- truncateList(((CDList<T, CleanUp, 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;
- }
-
- /**
- * Given a size parameter smaller than d_size, truncateList()
- * removes the elements from the end of the list until d_size equals size.
+ * Main constructor: d_list starts with size 0
*
- * WARNING! You should only use this function when you know what you are doing.
- * This is a primitive operation with strange context dependent behavior!
- * It is up to the user of the function to ensure that the saved d_size values
- * at lower context levels are less than or equal to size.
- */
- void truncateList(const size_t size){
- Assert(size <= d_size);
- if(d_callDestructor) {
- while(d_size != size) {
- --d_size;
- d_cleanUp(&d_list[d_size]);
- d_allocator.destroy(&d_list[d_size]);
- }
- } else {
- d_size = size;
- }
- }
-
-
-public:
-
- /**
- * Main constructor: d_list starts as NULL, size is 0
+ * Optionally, a cleanup callback can be specified, which is called on every
+ * element that gets removed during a pop. The callback is only used when
+ * callCleanup is true. Note: the destructor of the elements in the list is
+ * called regardless of whether callCleanup is true or false.
*/
CDList(Context* context,
- bool callDestructor = true,
- const CleanUp& cleanup = CleanUp(),
- const Allocator& alloc = Allocator()) :
- ContextObj(context),
- d_list(NULL),
- d_size(0),
- d_callDestructor(callDestructor),
- d_sizeAlloc(0),
- d_cleanUp(cleanup),
- d_allocator(alloc) {
+ bool callCleanup = true,
+ const CleanUp& cleanup = CleanUp())
+ : ContextObj(context),
+ d_list(),
+ d_size(0),
+ d_callCleanup(callCleanup),
+ d_cleanUp(cleanup)
+ {
}
/**
@@ -243,60 +92,34 @@ public:
~CDList() {
this->destroy();
- if(this->d_callDestructor) {
+ if (this->d_callCleanup)
+ {
truncateList(0);
}
-
- this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc);
}
/**
* Return the current size of (i.e. valid number of objects in) the
* list.
*/
- size_t size() const {
- return d_size;
- }
+ size_t size() const { return d_list.size(); }
/**
* Return true iff there are no valid objects in the list.
*/
- bool empty() const {
- return d_size == 0;
- }
+ bool empty() const { return d_list.empty(); }
/**
* 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;
+ Debug("cdlist") << "push_back " << this << " " << getContext()->getLevel()
+ << ": make-current" << 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();
- }
- 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_list.push_back(data);
++d_size;
+
Debug("cdlist") << "push_back " << this
<< " " << getContext()->getLevel()
<< ": size now " << d_size << std::endl;
@@ -305,7 +128,8 @@ public:
/**
* Access to the ith item in the list.
*/
- const T& operator[](size_t i) const {
+ ConstReference operator[](size_t i) const
+ {
Assert(i < d_size) << "index out of bounds in CDList::operator[]";
return d_list[i];
}
@@ -313,127 +137,122 @@ public:
/**
* Returns the most recent item added to the list.
*/
- const T& back() const {
+ ConstReference back() const
+ {
Assert(d_size > 0) << "CDList::back() called on empty list";
return d_list[d_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).
+ * Returns an iterator pointing to the first item in the list.
*/
- class const_iterator {
- T const* d_it;
-
- const_iterator(T const* it) : d_it(it) {}
-
- friend class CDList<T, CleanUp, 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 std::ptrdiff_t difference_type;
- typedef const T* pointer;
- typedef const T& reference;
-
- const_iterator() : d_it(NULL) {}
-
- inline bool operator==(const const_iterator& i) const {
- return d_it == i.d_it;
- }
-
- inline bool operator!=(const const_iterator& i) const {
- return d_it != i.d_it;
- }
-
- inline const T& operator*() const {
- return *d_it;
- }
+ const_iterator begin() const { return d_list.begin(); }
- inline const T* operator->() const { return d_it; }
-
- /** Prefix increment */
- const_iterator& operator++() {
- ++d_it;
- return *this;
- }
-
- /** Prefix decrement */
- const_iterator& operator--() { --d_it; return *this; }
-
- /** operator+ */
- const_iterator operator+(long signed int off) const {
- return const_iterator(d_it + off);
- }
-
- // Postfix operations on iterators: requires a Proxy object to
- // hold the intermediate value for dereferencing
- class Proxy {
- const T* d_t;
+ /**
+ * Returns an iterator pointing one past the last item in the list.
+ */
+ const_iterator end() const { return d_list.end(); }
- public:
+ protected:
+ /**
+ * Private copy constructor used only by save(). d_list is not copied: only
+ * the base class information and d_size are needed in restore.
+ */
+ CDList(const CDList& l)
+ : ContextObj(l),
+ d_size(l.d_size),
+ d_callCleanup(false),
+ d_cleanUp(l.d_cleanUp)
+ {
+ Debug("cdlist") << "copy ctor: " << this << " from " << &l << " size "
+ << d_size << std::endl;
+ }
+ CDList& operator=(const CDList& l) = delete;
+ /**
+ * Implementation of mandatory ContextObj method restore: simply
+ * restores the previous size. Note that the list pointer and the
+ * allocated size are not changed.
+ */
- Proxy(const T& p): d_t(&p) {}
+ void restore(ContextObj* data) override
+ {
+ Debug("cdlist") << "restore " << this << " level "
+ << this->getContext()->getLevel() << " data == " << data
+ << " call dtor == " << this->d_callCleanup << std::endl;
+ truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size);
+ Debug("cdlist") << "restore " << this << " level "
+ << this->getContext()->getLevel() << " size back to "
+ << this->d_size << std::endl;
+ }
- T& operator*() {
- return *d_t;
+ /**
+ * Given a size parameter smaller than d_size, truncateList()
+ * removes the elements from the end of the list until d_size equals size.
+ *
+ * WARNING! You should only use this function when you know what you are
+ * doing. This is a primitive operation with strange context dependent
+ * behavior! It is up to the user of the function to ensure that the saved
+ * d_size values at lower context levels are less than or equal to size.
+ */
+ void truncateList(const size_t size)
+ {
+ Assert(size <= d_size);
+ if (d_callCleanup)
+ {
+ while (d_size != size)
+ {
+ --d_size;
+ typename std::vector<T>::reference elem = d_list[d_size];
+ d_cleanUp(elem);
}
- };/* class CDList<>::const_iterator::Proxy */
-
- /** Postfix increment: returns Proxy with the old value. */
- Proxy operator++(int) {
- Proxy e(*(*this));
- ++(*this);
- return e;
}
-
- /** Postfix decrement: returns Proxy with the old value. */
- Proxy operator--(int) {
- Proxy e(*(*this));
- --(*this);
- return e;
+ else
+ {
+ d_size = size;
}
+ d_list.erase(d_list.begin() + d_size, d_list.end());
+ }
- };/* class CDList<>::const_iterator */
- typedef const_iterator iterator;
+ /**
+ * d_list is a vector of objects of type T.
+ */
+ std::vector<T> d_list;
/**
- * Returns an iterator pointing to the first item in the list.
+ * Number of objects in d_list
*/
- const_iterator begin() const {
- return const_iterator(static_cast<T const*>(d_list));
- }
+ size_t d_size;
+ private:
/**
- * Returns an iterator pointing one past the last item in the list.
+ * 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.
*/
- const_iterator end() const {
- return const_iterator(static_cast<T const*>(d_list) + d_size);
- }
-};/* class CDList<> */
+ bool d_callCleanup;
-template <class T, class CleanUp>
-class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
- /* CDList is incompatible for use with a ContextMemoryAllocator.
- *
- * Explanation:
- * If ContextMemoryAllocator is used and d_list grows at a deeper context
- * level the reallocated will be reallocated in a context memory region that
- * can be destroyed on pop. To support this, a full copy of d_list would have
- * to be made. As this is unacceptable for performance in other situations, we
- * do not do this.
+ /**
+ * The CleanUp functor.
+ */
+ CleanUp d_cleanUp;
+
+ /**
+ * 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) override
+ {
+ ContextObj* data = new (pCMM) CDList<T, CleanUp, Allocator>(*this);
+ Debug("cdlist") << "save " << this << " at level "
+ << this->getContext()->getLevel() << " size at "
+ << this->d_size << " data:" << data << std::endl;
+ return data;
+ }
- static_assert(sizeof(T) == 0,
- "Cannot create a CDList with a ContextMemoryAllocator.");
-};
+}; /* class CDList<> */
}/* CVC4::context namespace */
}/* CVC4 namespace */
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index 1caeea985..668d2a8c3 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -34,17 +34,13 @@
#include <memory>
+#include "context/default_clean_up.h"
+
/// \cond internals
namespace CVC4 {
namespace context {
-template <class T>
-class DefaultCleanUp {
-public:
- inline void operator()(T* t CVC4_UNUSED) const{}
-};
-
template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
class CDList;
diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h
index b28fcc3d3..32b3562ae 100644
--- a/src/context/cdqueue.h
+++ b/src/context/cdqueue.h
@@ -66,13 +66,11 @@ protected:
// We save the d_size in d_lastsave and we should never destruct below this
// indices before the corresponding restore.
d_lastsave = ParentType::d_size;
- Debug("cdqueue") << "save " << this
- << " at level " << this->getContext()->getLevel()
- << " size at " << this->d_size
- << " iter at " << this->d_iter
- << " lastsave at " << this->d_lastsave
- << " d_list is " << this->d_list
- << " data:" << data << std::endl;
+ Debug("cdqueue") << "save " << this << " at level "
+ << this->getContext()->getLevel() << " size at "
+ << this->d_size << " iter at " << this->d_iter
+ << " lastsave at " << this->d_lastsave << " d_list is "
+ << this->d_list.data() << " data:" << data << std::endl;
return data;
}
@@ -94,19 +92,19 @@ protected:
public:
/** Creates a new CDQueue associated with the current context. */
- CDQueue(Context* context,
- bool callDestructor = true,
- const CleanUp& cleanup = CleanUp(),
- const Allocator& alloc = Allocator())
- : ParentType(context, callDestructor, cleanup, alloc),
- d_iter(0),
- d_lastsave(0)
- {}
-
- /** Returns true if the queue is empty in the current context. */
- bool empty() const{
- Assert(d_iter <= ParentType::d_size);
- return d_iter == ParentType::d_size;
+ CDQueue(Context* context,
+ bool callCleanup = true,
+ const CleanUp& cleanup = CleanUp(),
+ const Allocator& alloc = Allocator())
+ : ParentType(context, callCleanup, cleanup), d_iter(0), d_lastsave(0)
+ {
+ }
+
+ /** Returns true if the queue is empty in the current context. */
+ bool empty() const
+ {
+ Assert(d_iter <= ParentType::d_size);
+ return d_iter == ParentType::d_size;
}
/** Returns the number of elements that have not been dequeued in the context. */
diff --git a/src/context/default_clean_up.h b/src/context/default_clean_up.h
new file mode 100644
index 000000000..4f6c6a9c3
--- /dev/null
+++ b/src/context/default_clean_up.h
@@ -0,0 +1,34 @@
+/********************* */
+/*! \file default_clean_up.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The default CleanUp class that does nothing.
+ **
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__CONTEXT__DEFAULT_CLEAN_UP_H
+#define CVC4__CONTEXT__DEFAULT_CLEAN_UP_H
+
+namespace CVC4 {
+namespace context {
+
+template <class T>
+class DefaultCleanUp
+{
+ public:
+ void operator()(typename std::vector<T>::reference CVC4_UNUSED) const {}
+};
+
+} // namespace context
+} // namespace CVC4
+
+#endif /* __CVC4__CONTEXT__DEFAULT_CLEAN_UP_H */
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 952879182..6241dd88a 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -780,16 +780,15 @@ class Constraint {
class ConstraintRuleCleanup
{
public:
- inline void operator()(ConstraintRule* crp)
+ inline void operator()(ConstraintRule& crp)
{
- Assert(crp != NULL);
- ConstraintP constraint = crp->d_constraint;
+ ConstraintP constraint = crp.d_constraint;
Assert(constraint->d_crid != ConstraintRuleIdSentinel);
constraint->d_crid = ConstraintRuleIdSentinel;
ARITH_PROOF({
- if (crp->d_farkasCoefficients != RationalVectorCPSentinel)
+ if (crp.d_farkasCoefficients != RationalVectorCPSentinel)
{
- delete crp->d_farkasCoefficients;
+ delete crp.d_farkasCoefficients;
}
});
}
@@ -798,9 +797,8 @@ class Constraint {
class CanBePropagatedCleanup
{
public:
- inline void operator()(ConstraintP* p)
+ inline void operator()(ConstraintP& constraint)
{
- ConstraintP constraint = *p;
Assert(constraint->d_canBePropagated);
constraint->d_canBePropagated = false;
}
@@ -809,9 +807,8 @@ class Constraint {
class AssertionOrderCleanup
{
public:
- inline void operator()(ConstraintP* p)
+ inline void operator()(ConstraintP& constraint)
{
- ConstraintP constraint = *p;
Assert(constraint->assertedToTheTheory());
constraint->d_assertionOrder = AssertionOrderSentinel;
constraint->d_witness = TNode::null();
@@ -822,9 +819,8 @@ class Constraint {
class SplitCleanup
{
public:
- inline void operator()(ConstraintP* p)
+ inline void operator()(ConstraintP& constraint)
{
- ConstraintP constraint = *p;
Assert(constraint->d_split);
constraint->d_split = false;
}
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index bf86c7e86..2bf3a3d84 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -673,15 +673,17 @@ bool ArithVariables::inMaps(ArithVar x) const{
ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
: d_pm(pm)
{}
-void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
- d_pm->popLowerBound(p);
+void ArithVariables::LowerBoundCleanUp::operator()(AVCPair& p)
+{
+ d_pm->popLowerBound(&p);
}
ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
: d_pm(pm)
{}
-void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){
- d_pm->popUpperBound(p);
+void ArithVariables::UpperBoundCleanUp::operator()(AVCPair& p)
+{
+ d_pm->popUpperBound(&p);
}
}/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 1606be73b..fcdce44c3 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -202,7 +202,7 @@ private:
ArithVariables* d_pm;
public:
LowerBoundCleanUp(ArithVariables* pm);
- void operator()(AVCPair* restore);
+ void operator()(AVCPair& restore);
};
class UpperBoundCleanUp {
@@ -210,7 +210,7 @@ private:
ArithVariables* d_pm;
public:
UpperBoundCleanUp(ArithVariables* pm);
- void operator()(AVCPair* restore);
+ void operator()(AVCPair& restore);
};
typedef context::CDList<AVCPair, LowerBoundCleanUp> LBReverts;
diff --git a/src/theory/assertion.h b/src/theory/assertion.h
index 1445ffd7b..d0e58d0a7 100644
--- a/src/theory/assertion.h
+++ b/src/theory/assertion.h
@@ -28,10 +28,10 @@ namespace theory {
/** Information about an assertion for the theories. */
struct Assertion {
/** The assertion expression. */
- const Node d_assertion;
+ Node d_assertion;
/** Has this assertion been preregistered with this theory. */
- const bool d_isPreregistered;
+ bool d_isPreregistered;
Assertion(TNode assertion, bool isPreregistered)
: d_assertion(assertion), d_isPreregistered(isPreregistered)
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 845bc72c4..6f935a6a2 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -29,10 +29,18 @@ using namespace std;
using namespace CVC4::context;
using namespace CVC4;
-struct DtorSensitiveObject {
- bool& d_dtorCalled;
- DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {}
- ~DtorSensitiveObject() { d_dtorCalled = true; }
+struct TestObject
+{
+ bool* d_cleanupCalled;
+ TestObject(bool* cleanupCalled) : d_cleanupCalled(cleanupCalled) {}
+};
+
+class TestCleanup
+{
+ private:
+ public:
+ TestCleanup() {}
+ void operator()(TestObject& o) { (*o.d_cleanupCalled) = true; }
};
class CDListBlack : public CxxTest::TestSuite {
@@ -86,14 +94,14 @@ class CDListBlack : public CxxTest::TestSuite {
bool shouldAlsoRemainFalse = false;
bool aThirdFalse = false;
- CDList<DtorSensitiveObject> listT(d_context, true);
- CDList<DtorSensitiveObject> listF(d_context, false);
+ CDList<TestObject, TestCleanup> listT(d_context, true, TestCleanup());
+ CDList<TestObject, TestCleanup> listF(d_context, false, TestCleanup());
- DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
- DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
- DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue);
- DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse);
- DtorSensitiveObject aThirdFalseDSO(aThirdFalse);
+ TestObject shouldRemainFalseDSO(&shouldRemainFalse);
+ TestObject shouldFlipToTrueDSO(&shouldFlipToTrue);
+ TestObject alsoFlipToTrueDSO(&alsoFlipToTrue);
+ TestObject shouldAlsoRemainFalseDSO(&shouldAlsoRemainFalse);
+ TestObject aThirdFalseDSO(&aThirdFalse);
listT.push_back(shouldAlsoRemainFalseDSO);
listF.push_back(shouldAlsoRemainFalseDSO);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback