git_versioninfo.cpp \
svn_versioninfo.cpp \
context/backtrackable.h \
- context/cdchunk_list.h \
context/cddense_set.h \
context/cdhashmap.h \
context/cdhashmap_forward.h \
+++ /dev/null
-/********************* */
-/*! \file cdchunk_list.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Context-dependent list class designed for use with a
- ** context memory allocator.
- **
- ** Context-dependent list class designed for use with a context
- ** memory allocator.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H
-#define __CVC4__CONTEXT__CDCHUNK_LIST_H
-
-#include <iterator>
-#include <memory>
-
-#include "base/cvc4_assert.h"
-#include "context/context.h"
-#include "context/context_mm.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 by operator[] 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 CDChunkList : public ContextObj {
-public:
-
- /** The value type with which this CDChunkList<> was instantiated. */
- typedef T value_type;
- /** The allocator type with which this CDChunkList<> 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 CDChunkList<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 CDChunkList<T, ContextMemoryAllocator<T> >.
- */
- struct CDChunkListSave : public ContextObj {
- ListSegment* d_tail;
- size_t d_tailSize, d_size, d_sizeAlloc;
- CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail,
- size_t size, size_t sizeAlloc) :
- ContextObj(list),
- d_tail(tail),
- d_tailSize(tail->size()),
- d_size(size),
- d_sizeAlloc(sizeAlloc) {
- }
- ~CDChunkListSave() {
- 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 CDChunkList<T>::CDChunkListSave */
-
- /**
- * Private copy constructor undefined (no copy permitted).
- */
- CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED;
-
- /**
- * 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) CDChunkListSave(*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) {
- CDChunkListSave* save = static_cast<CDChunkListSave*>(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:
-
- CDChunkList(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();
- }
-
- CDChunkList(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();
- }
-
- CDChunkList(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();
- }
-
- CDChunkList(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
- */
- ~CDChunkList() {
- 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 in O(log n).
- */
- const T& operator[](size_t i) const {
- Assert(i < d_size, "index out of bounds in CDChunkList::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, "CDChunkList::back() called on empty list");
- return (*d_tailSegment)[d_tailSegment->size() - 1];
- }
-
- /**
- * Iterator for CDChunkList 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 CDChunkList<T>;
-
- public:
-
- 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_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 CDChunkList<>::const_iterator */
-
- /**
- * Returns an iterator pointing to the first item in the list.
- */
- const_iterator begin() const {
- // This looks curious, but we have to make sure that begin() == end()
- // for an empty list, and begin() == (head,0) for a nonempty one.
- // Since the segment spill-over is implemented in
- // iterator::operator++(), let's reuse it. */
- return ++const_iterator(&d_headSegment, -1);
- }
-
- /**
- * Returns an iterator pointing one past the last item in the list.
- */
- const_iterator end() const {
- return const_iterator(NULL, 0);
- }
-};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */
template <class T, class CleanUp>
class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
/* CDList is incompatible for use with a ContextMemoryAllocator.
- * Consider using CDChunkList<T> instead.
*
* Explanation:
* If ContextMemoryAllocator is used and d_list grows at a deeper context
#include <iostream>
#include <map>
-#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
#include "context/cdo.h"
#include "context/context.h"
#include "expr/datatype.h"
typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDChunkList<Node> NodeList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
IntMap d_testers;
IntMap d_is_const;
#include <iostream>
#include <map>
-#include "context/cdchunk_list.h"
+#include "context/cdlist.h"
+#include "expr/attribute.h"
#include "expr/datatype.h"
#include "theory/datatypes/datatypes_sygus.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "util/hash.h"
-#include "expr/attribute.h"
namespace CVC4 {
namespace theory {
namespace datatypes {
class TheoryDatatypes : public Theory {
-private:
- typedef context::CDChunkList<Node> NodeList;
- typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+ private:
+ typedef context::CDList<Node> NodeList;
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
/** transitive closure to record equivalence/subterm relation. */
- //TransitiveClosureNode d_cycle_check;
+ // TransitiveClosureNode d_cycle_check;
/** has seen cycle */
- context::CDO< bool > d_hasSeenCycle;
+ context::CDO<bool> d_hasSeenCycle;
/** inferences */
NodeList d_infer;
NodeList d_infer_exp;
Node d_true;
Node d_zero;
/** mkAnd */
- Node mkAnd( std::vector< TNode >& assumptions );
-private:
+ Node mkAnd(std::vector<TNode>& assumptions);
+
+ private:
//notification class for equality engine
class NotifyClass : public eq::EqualityEngineNotify {
TheoryDatatypes& d_dt;
#include "context/context.h"
#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
namespace CVC4 {
namespace theory {
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
-#include "context/cdchunk_list.h"
-#include "context/cdhashmap.h"
+#include "context/cdlist.h"
#include "theory/quantifiers/ce_guided_single_inv_sol.h"
#include "theory/quantifiers/inst_match_trie.h"
#include "theory/quantifiers/inst_strategy_cbqi.h"
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
#define CONJECTURE_GENERATOR_H
#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
#include "theory/type_enumerator.h"
friend class SubsEqcIndex;
friend class TermGenerator;
friend class TermGenEnv;
- typedef context::CDChunkList<Node> NodeList;
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
//this class maintains a congruence closure for *universal* facts
#include <map>
#include <vector>
-#include "context/context.h"
-#include "context/context_mm.h"
#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
+#include "context/context.h"
+#include "context/context_mm.h"
#include "theory/theory.h"
{
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDList<Node> NodeList;
typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap;
private:
context::Context * d_c;
#include <vector>
#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
-#include "theory/quantifiers_engine.h"
+#include "context/cdlist.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
{
friend class MatchGen;
friend class QuantInfo;
- typedef context::CDChunkList<Node> NodeList;
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
context::CDO< bool > d_conflict;
#ifndef __CVC4__REWRITE_ENGINE_H
#define __CVC4__REWRITE_ENGINE_H
-#include "context/cdchunk_list.h"
#include "context/context.h"
#include "context/context_mm.h"
#include "theory/quantifiers/trigger.h"
#include <string>
#include <vector>
-#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
#include "context/context.h"
#include "context/context_mm.h"
#include <memory>
#include <unordered_map>
-#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
#include "expr/attribute.h"
#include "options/quantifiers_modes.h"
#include "theory/quantifiers/inst_match.h"
friend class quantifiers::QuantConflictFind;
friend class inst::InstMatch;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDChunkList<Node> NodeList;
- typedef context::CDChunkList<bool> BoolList;
+ typedef context::CDList<Node> NodeList;
+ typedef context::CDList<bool> BoolList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
private:
/** reference to theory engine object */
#ifndef __CVC4__THEORY__SEP__THEORY_SEP_H
#define __CVC4__THEORY__SEP__THEORY_SEP_H
-#include "theory/theory.h"
-#include "util/statistics_registry.h"
-#include "theory/uf/equality_engine.h"
-#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
#include "context/cdqueue.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
namespace sep {
class TheorySep : public Theory {
- typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDList<Node> NodeList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
#include <unordered_set>
-#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
#include "theory/sets/rels_utils.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
};/* class TupleTrie */
class TheorySetsRels {
-
- typedef context::CDChunkList< Node > NodeList;
+ typedef context::CDList<Node> NodeList;
typedef context::CDHashSet< Node, NodeHashFunction > NodeSet;
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/strings/theory_strings_preprocess.h"
-#include "theory/strings/regexp_operation.h"
-
-#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
#include "expr/attribute.h"
+#include "theory/strings/regexp_operation.h"
+#include "theory/strings/theory_strings_preprocess.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
#include <climits>
#include <deque>
typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
class TheoryStrings : public Theory {
- typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDList<Node> NodeList;
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
#include "util/hash.h"
#include "theory/theory.h"
#include "theory/rewriter.h"
-#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
namespace CVC4 {
#ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H
#define __CVC4__THEORY_UF_STRONG_SOLVER_H
-#include "context/cdchunk_list.h"
#include "context/cdhashmap.h"
#include "context/context.h"
#include "context/context_mm.h"
sqrt2-sort-inf-unk.smt2 \
rec-fun-const-parse-bug.smt2
-
# Regression tests for PL inputs
CVC_TESTS = \
boolean.cvc \
CPLUSPLUS_TESTS = \
boilerplate \
ouroborous \
+ reset_assertions \
two_smt_engines \
smt2_compliance \
statistics
--- /dev/null
+/********************* */
+/*! \file reset_assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 A simple test for SmtEngine::resetAssertions()
+ **
+ ** This program indirectly also tests some corner cases w.r.t.
+ ** context-dependent datastructures: resetAssertions() pops the contexts to
+ ** zero but some context-dependent datastructures are created at leevel 1,
+ ** which the datastructure needs to handle properly problematic.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+
+int main()
+{
+ ExprManager em;
+ SmtEngine smt(&em);
+
+ smt.setOption("incremental", SExpr(true));
+
+ Type real = em.realType();
+ Expr x = em.mkVar("x", real);
+ Expr four = em.mkConst(Rational(4));
+ Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four);
+ smt.assertFormula(xEqFour);
+ std::cout << smt.checkSat() << std::endl;
+
+ smt.resetAssertions();
+
+ Type elementType = em.integerType();
+ Type indexType = em.integerType();
+ Type arrayType = em.mkArrayType(indexType, elementType);
+ Expr array = em.mkVar("array", arrayType);
+ Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four);
+ Expr ten = em.mkConst(Rational(10));
+ Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten);
+ smt.assertFormula(arrayAtFour_eq_ten);
+ std::cout << smt.checkSat() << std::endl;
+}
context/context_mm_black \
context/cdo_black \
context/cdlist_black \
- context/cdlist_context_memory_black \
context/cdmap_black \
context/cdmap_white \
context/cdvector_black \
#endif /* CVC4_MEMORY_LIMITING_DISABLED */
}
+
+ void testPopBelowLevelCreated()
+ {
+ d_context->push();
+ CDList<int> list(d_context);
+ d_context->popto(0);
+ list.push_back(42);
+ }
};
+++ /dev/null
-/********************* */
-/*! \file cdlist_context_memory_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Black box testing of CVC4::context::CDList<>.
- **
- ** Black box testing of CVC4::context::CDList<>.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <vector>
-
-#include <limits.h>
-
-#include "memory.h"
-
-#include "context/cdchunk_list.h"
-#include "context/context.h"
-
-using namespace std;
-using namespace CVC4::context;
-
-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 testCDChunkList10() { listTest(10); }
- void testCDChunkList15() { listTest(15); }
- void testCDChunkList20() { listTest(20); }
- void testCDChunkList35() { listTest(35); }
- void testCDChunkList50() { listTest(50); }
- void testCDChunkList99() { listTest(99); }
-
- void listTest(int N) {
- listTest(N, true);
- listTest(N, false);
- }
-
- void listTest(int N, bool callDestructor) {
- CDChunkList<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 (CDChunkList<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 testEmptyIterator() {
- CDChunkList<int>* list = new (d_context->getCMM())
- CDChunkList<int>(true, d_context, false,
- ContextMemoryAllocator<int>(d_context->getCMM()));
- TS_ASSERT_EQUALS(list->begin(), list->end());
- }
-
- void testDtorCalled() {
- bool shouldRemainFalse = false;
- bool shouldFlipToTrue = false;
- bool alsoFlipToTrue = false;
- bool shouldAlsoRemainFalse = false;
- bool aThirdFalse = false;
-
- CDChunkList<DtorSensitiveObject> listT(
- d_context, true,
- ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
- CDChunkList<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);
- }
-
- void testOutOfMemory() {
-#ifdef CVC4_MEMORY_LIMITING_DISABLED
-
- CVC4::test::WarnWithLimitedMemoryDisabledReason();
-
-#else /* CVC4_MEMORY_LIMITING_DISABLED */
-
- CDChunkList<unsigned> list(d_context);
- CVC4::test::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 /* CVC4_MEMORY_LIMITING_DISABLED */
- }
-};
projects / cvc5.git / commitdiff