From 6a37fd136eea6ad95aae4e598faee0d47c110343 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 6 Dec 2017 04:45:06 -0800 Subject: [PATCH] Remove CDChunkList (#1414) --- src/Makefile.am | 1 - src/context/cdchunk_list.h | 495 ------------------ src/context/cdlist.h | 1 - src/theory/datatypes/datatypes_sygus.h | 3 +- src/theory/datatypes/theory_datatypes.h | 23 +- src/theory/quantifiers/bounded_integers.h | 1 - src/theory/quantifiers/ce_guided_pbe.h | 1 - src/theory/quantifiers/ce_guided_single_inv.h | 3 +- .../quantifiers/ce_guided_single_inv_sol.h | 1 - src/theory/quantifiers/conjecture_generator.h | 2 - src/theory/quantifiers/equality_infer.h | 7 +- src/theory/quantifiers/quant_conflict_find.h | 5 +- src/theory/quantifiers/rewrite_engine.h | 1 - src/theory/quantifiers/symmetry_breaking.h | 1 - src/theory/quantifiers_engine.h | 6 +- src/theory/sep/theory_sep.h | 10 +- src/theory/sets/theory_sets_rels.h | 5 +- src/theory/strings/theory_strings.h | 13 +- .../strings/theory_strings_preprocess.h | 1 - src/theory/uf/theory_uf_strong_solver.h | 1 - test/regress/regress0/Makefile.am | 1 - test/system/Makefile.am | 1 + test/system/reset_assertions.cpp | 53 ++ test/unit/Makefile.am | 1 - test/unit/context/cdlist_black.h | 8 + .../context/cdlist_context_memory_black.h | 160 ------ 26 files changed, 97 insertions(+), 708 deletions(-) delete mode 100644 src/context/cdchunk_list.h create mode 100644 test/system/reset_assertions.cpp delete mode 100644 test/unit/context/cdlist_context_memory_black.h diff --git a/src/Makefile.am b/src/Makefile.am index 6a21251bd..69e9cd014 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -36,7 +36,6 @@ libcvc4_la_SOURCES = \ git_versioninfo.cpp \ svn_versioninfo.cpp \ context/backtrackable.h \ - context/cdchunk_list.h \ context/cddense_set.h \ context/cdhashmap.h \ context/cdhashmap_forward.h \ diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h deleted file mode 100644 index d13c6ab90..000000000 --- a/src/context/cdchunk_list.h +++ /dev/null @@ -1,495 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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 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 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::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 >. - */ - struct CDChunkListSave : public ContextObj { - ListSegment* d_tail; - size_t d_tailSize, d_size, d_sizeAlloc; - CDChunkListSave(const CDChunkList& 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::CDChunkListSave */ - - /** - * Private copy constructor undefined (no copy permitted). - */ - CDChunkList(const CDChunkList& 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::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(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; - - 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 > */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */ diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 3dab675c3..aeb6567a3 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -419,7 +419,6 @@ public: template class CDList > : public ContextObj { /* CDList is incompatible for use with a ContextMemoryAllocator. - * Consider using CDChunkList instead. * * Explanation: * If ContextMemoryAllocator is used and d_list grows at a deeper context diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 9cfa7355d..099b45fec 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -22,9 +22,9 @@ #include #include -#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" @@ -59,7 +59,6 @@ private: typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDChunkList NodeList; typedef context::CDHashSet NodeSet; IntMap d_testers; IntMap d_is_const; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 5166e118e..3c0a7c7cf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -22,13 +22,13 @@ #include #include -#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 { @@ -40,24 +40,25 @@ namespace quantifiers{ namespace datatypes { class TheoryDatatypes : public Theory { -private: - typedef context::CDChunkList 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 NodeList; + typedef context::CDHashMap NodeIntMap; + typedef context::CDHashMap BoolMap; + typedef context::CDHashMap 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 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& assumptions); + + private: //notification class for equality engine class NotifyClass : public eq::EqualityEngineNotify { TheoryDatatypes& d_dt; diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index a91b04ab3..99d77a8e7 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -23,7 +23,6 @@ #include "context/context.h" #include "context/context_mm.h" -#include "context/cdchunk_list.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h index 8cfed253c..e8bccaac5 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -18,7 +18,6 @@ #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H #include "context/cdhashmap.h" -#include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 33fc7303f..888e078af 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -17,8 +17,7 @@ #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" diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h index 61ade265f..c5f976f02 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h @@ -18,7 +18,6 @@ #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 { diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index a67530556..fa74795c3 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -18,7 +18,6 @@ #define CONJECTURE_GENERATOR_H #include "context/cdhashmap.h" -#include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" #include "theory/type_enumerator.h" @@ -229,7 +228,6 @@ class ConjectureGenerator : public QuantifiersModule friend class SubsEqcIndex; friend class TermGenerator; friend class TermGenEnv; - typedef context::CDChunkList NodeList; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; //this class maintains a congruence closure for *universal* facts diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 5b714c2d3..5a3f2e4d5 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -21,11 +21,10 @@ #include #include -#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" @@ -37,7 +36,7 @@ class EqualityInference { typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDChunkList NodeList; + typedef context::CDList NodeList; typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap; private: context::Context * d_c; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 8a1043ded..f4d0e8e43 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -21,9 +21,9 @@ #include #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 { @@ -191,7 +191,6 @@ class QuantConflictFind : public QuantifiersModule { friend class MatchGen; friend class QuantInfo; - typedef context::CDChunkList NodeList; typedef context::CDHashMap NodeBoolMap; private: context::CDO< bool > d_conflict; diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 5d1918205..d56e7c730 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -18,7 +18,6 @@ #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" diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index 466e6d9a9..091490cec 100644 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -22,7 +22,6 @@ #include #include -#include "context/cdchunk_list.h" #include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 6c7820cef..3cd4e8ef9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -22,8 +22,8 @@ #include #include -#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" @@ -95,8 +95,8 @@ class QuantifiersEngine { friend class quantifiers::QuantConflictFind; friend class inst::InstMatch; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDChunkList NodeList; - typedef context::CDChunkList BoolList; + typedef context::CDList NodeList; + typedef context::CDList BoolList; typedef context::CDHashSet NodeSet; private: /** reference to theory engine object */ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 1786584d4..591a495d0 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -19,13 +19,13 @@ #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 { @@ -35,7 +35,7 @@ class TheoryModel; namespace sep { class TheorySep : public Theory { - typedef context::CDChunkList NodeList; + typedef context::CDList NodeList; typedef context::CDHashSet NodeSet; typedef context::CDHashMap NodeNodeMap; diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index eb97405dc..d6e52a308 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -19,8 +19,8 @@ #include -#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" @@ -46,8 +46,7 @@ public: };/* class TupleTrie */ class TheorySetsRels { - - typedef context::CDChunkList< Node > NodeList; + typedef context::CDList NodeList; typedef context::CDHashSet< Node, NodeHashFunction > NodeSet; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0bdaf7ab5..39ab70e2f 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -19,14 +19,13 @@ #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 #include @@ -49,7 +48,7 @@ struct StringsProxyVarAttributeId {}; typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute; class TheoryStrings : public Theory { - typedef context::CDChunkList NodeList; + typedef context::CDList NodeList; typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 60bfd6fab..41987265e 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -23,7 +23,6 @@ #include "util/hash.h" #include "theory/theory.h" #include "theory/rewriter.h" -#include "context/cdchunk_list.h" #include "context/cdhashmap.h" namespace CVC4 { diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index a7239dba5..0166bd947 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -17,7 +17,6 @@ #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" diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9d049e9d2..80ca1a5ef 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -78,7 +78,6 @@ SMT2_TESTS = \ sqrt2-sort-inf-unk.smt2 \ rec-fun-const-parse-bug.smt2 - # Regression tests for PL inputs CVC_TESTS = \ boolean.cvc \ diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 55a6c2b09..1be242e3d 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -3,6 +3,7 @@ TEST_EXTENSIONS = .class CPLUSPLUS_TESTS = \ boilerplate \ ouroborous \ + reset_assertions \ two_smt_engines \ smt2_compliance \ statistics diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp new file mode 100644 index 000000000..4fed06698 --- /dev/null +++ b/test/system/reset_assertions.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \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 +#include + +#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; +} diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 8c45eeb23..9de940a0d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -34,7 +34,6 @@ UNIT_TESTS += \ context/context_mm_black \ context/cdo_black \ context/cdlist_black \ - context/cdlist_context_memory_black \ context/cdmap_black \ context/cdmap_white \ context/cdvector_black \ diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 8525ef6f3..5015ae002 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -150,4 +150,12 @@ class CDListBlack : public CxxTest::TestSuite { #endif /* CVC4_MEMORY_LIMITING_DISABLED */ } + + void testPopBelowLevelCreated() + { + d_context->push(); + CDList list(d_context); + d_context->popto(0); + list.push_back(42); + } }; diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h deleted file mode 100644 index 654251a0c..000000000 --- a/test/unit/context/cdlist_context_memory_black.h +++ /dev/null @@ -1,160 +0,0 @@ -/********************* */ -/*! \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 - -#include -#include - -#include - -#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 list(d_context, callDestructor, - ContextMemoryAllocator(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::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* list = new (d_context->getCMM()) - CDChunkList(true, d_context, false, - ContextMemoryAllocator(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 listT( - d_context, true, - ContextMemoryAllocator(d_context->getCMM())); - CDChunkList listF( - d_context, false, - ContextMemoryAllocator(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 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 */ - } -}; -- 2.30.2