From b0deae79d8bae5051a85dc15e43e7b83bc8cf9ab Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 7 Aug 2012 18:38:49 +0000 Subject: [PATCH] Some items from the CVC4 public interface review: * rename DeclarationScope to SymbolTable * rename all HashStrategy -> HashFunction (which we often have anyways) * remove CDCircList (no one is currently using it) --- src/context/Makefile.am | 4 +- src/context/cdcirclist.h | 418 ------------------ src/context/cdcirclist_forward.h | 45 -- src/cvc4.i | 2 +- src/expr/Makefile.am | 6 +- src/expr/attribute_internals.h | 22 +- src/expr/declaration_scope.i | 5 - src/expr/kind_template.h | 14 +- src/expr/mkmetakind | 4 +- src/expr/node_manager.h | 2 +- src/expr/node_value.h | 6 +- ...declaration_scope.cpp => symbol_table.cpp} | 46 +- .../{declaration_scope.h => symbol_table.h} | 22 +- src/expr/symbol_table.i | 5 + src/parser/cvc/Cvc.g | 10 +- src/parser/parser.cpp | 28 +- src/parser/parser.h | 26 +- src/theory/arith/kinds | 4 +- src/theory/arrays/array_info.h | 37 +- src/theory/arrays/kinds | 2 +- src/theory/booleans/kinds | 2 +- src/theory/builtin/kinds | 12 +- src/theory/bv/kinds | 18 +- src/theory/datatypes/kinds | 4 +- src/theory/ite_simplifier.h | 2 +- src/util/array_store_all.h | 8 +- src/util/ascription_type.h | 6 +- src/util/bitvector.h | 28 +- src/util/bool.h | 6 +- src/util/datatype.h | 11 - src/util/hash.h | 6 - src/util/integer_cln_imp.h | 6 +- src/util/integer_gmp_imp.h | 6 +- src/util/predicate.cpp | 2 +- src/util/predicate.h | 8 +- src/util/rational_cln_imp.h | 6 +- src/util/rational_gmp_imp.h | 6 +- src/util/subrange_bound.h | 6 +- src/util/uninterpreted_constant.h | 8 +- test/unit/Makefile.am | 3 +- test/unit/context/cdcirclist_white.h | 223 ---------- ...ion_scope_black.h => symbol_table_black.h} | 104 ++--- 42 files changed, 230 insertions(+), 959 deletions(-) delete mode 100644 src/context/cdcirclist.h delete mode 100644 src/context/cdcirclist_forward.h delete mode 100644 src/expr/declaration_scope.i rename src/expr/{declaration_scope.cpp => symbol_table.cpp} (80%) rename src/expr/{declaration_scope.h => symbol_table.h} (93%) create mode 100644 src/expr/symbol_table.i delete mode 100644 test/unit/context/cdcirclist_white.h rename test/unit/expr/{declaration_scope_black.h => symbol_table_black.h} (55%) diff --git a/src/context/Makefile.am b/src/context/Makefile.am index d979a9c16..e7f1dc68b 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -20,10 +20,8 @@ libcontext_la_SOURCES = \ cdhashmap_forward.h \ cdhashset.h \ cdhashset_forward.h \ - cdcirclist.h \ - cdcirclist_forward.h \ cdvector.h \ cdmaybe.h \ stacking_map.h \ stacking_vector.h \ - cddense_set.h \ No newline at end of file + cddense_set.h diff --git a/src/context/cdcirclist.h b/src/context/cdcirclist.h deleted file mode 100644 index cc6b60217..000000000 --- a/src/context/cdcirclist.h +++ /dev/null @@ -1,418 +0,0 @@ -/********************* */ -/*! \file cdcirclist.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Context-dependent circular list class - ** - ** Context-dependent circular list class. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__CDCIRCLIST_H -#define __CVC4__CONTEXT__CDCIRCLIST_H - -#include -#include -#include -#include - -#include "context/context.h" -#include "context/context_mm.h" -#include "context/cdcirclist_forward.h" -#include "context/cdo.h" -#include "util/Assert.h" - -namespace CVC4 { -namespace context { - -// CDO for pointers in particular, adds * and -> operators -template -class CDPtr : public CDO { - typedef CDO super; - - // private copy ctor - CDPtr(const CDPtr& cdptr) : - super(cdptr) { - } - -public: - - CDPtr(Context* context, T* data = NULL) : - super(context, data) { - } - - CDPtr(bool allocatedInCMM, Context* context, T* data = NULL) : - super(allocatedInCMM, context, data) { - } - - // undesirable to put this here, since CDO<> does it already (?) - virtual ~CDPtr() throw(AssertionException) { this->destroy(); } - - virtual ContextObj* save(ContextMemoryManager* pCMM) { - Debug("context") << "save cdptr " << this << " (value " << super::get() << ")"; - ContextObj* p = new(pCMM) CDPtr(*this); - Debug("context") << " to " << p << std::endl; - return p; - } - - virtual void restore(ContextObj* pContextObj) { - Debug("context") << "restore cdptr " << this << " (using " << pContextObj << ") from " << super::get(); - this->super::restore(pContextObj); - Debug("context") << " to " << super::get() << std::endl; - } - - CDPtr& operator=(T* data) { - Debug("context") << "set " << this << " from " << super::get(); - super::set(data); - Debug("context") << " to " << super::get() << std::endl; - return *this; - } - // assignment is just like using the underlying ptr - CDPtr& operator=(const CDPtr& cdptr) { - return *this = cdptr.get(); - } - - T& operator*() { return *super::get(); } - T* operator->() { return super::get(); } - const T& operator*() const { return *super::get(); } - const T* operator->() const { return super::get(); } -};/* class CDPtr */ - - -/** - * Class representing a single link in a CDCircList<>. - * - * The underlying T object is immutable, only the structure of the - * list is mutable, so only that's backtracked. - */ -template -class CDCircElement { - typedef CDCircElement elt_t; - const T d_t; - CDPtr d_prev; - CDPtr d_next; - friend class CDCircList; -public: - CDCircElement(Context* context, const T& t, - elt_t* prev = NULL, elt_t* next = NULL) : - d_t(t), - d_prev(true, context, prev), - d_next(true, context, next) { - } - - CDPtr& next() { return d_next; } - CDPtr& prev() { return d_prev; } - elt_t* next() const { return d_next; } - elt_t* prev() const { return d_prev; } - T element() const { return d_t; } -};/* class CDCircElement<> */ - - -/** - * Generic context-dependent circular list. Items themselves are not - * context dependent, only the forward and backward links. This - * allows two lists to be spliced together in constant time (see - * concat()). The list *structure* is mutable (things can be spliced - * in, removed, added, the list can be cleared, etc.) in a - * context-dependent manner, but the list items are immutable. To - * replace an item A in the list with B, A must be removed and - * B added in the same location. - */ -template -class CDCircList : public ContextObj { -public: - - /** List carrier element type */ - typedef CDCircElement elt_t; - /** The value type with which this CDCircList<> was instantiated. */ - typedef T value_type; - /** The allocator type with which this CDCircList<> was instantiated. */ - typedef AllocatorT Allocator; - -private: - - /** Head element of the circular list */ - CDPtr d_head; - /** The context with which we're associated */ - Context* d_context; - /** Our allocator */ - typename Allocator::template rebind< CDCircElement >::other d_allocator; - -public: - - CDCircList(Context* context, const Allocator& alloc = Allocator()) : - ContextObj(context), - d_head(context, NULL), - d_context(context), - d_allocator(alloc) { - } - - CDCircList(bool allocatedInCMM, Context* context, const Allocator& alloc = Allocator()) : - ContextObj(allocatedInCMM, context), - d_head(allocatedInCMM, context, NULL), - d_context(context), - d_allocator(alloc) { - Debug("cdcirclist") << "head " << &d_head << " in cmm ? " << allocatedInCMM << std::endl; - } - - ~CDCircList() throw(AssertionException) { - // by context contract, call destroy() here - destroy(); - } - - void clear() { - d_head = NULL; - } - - bool empty() const { - return d_head == NULL; - } - - CDPtr& head() { - return d_head; - } - - CDPtr& tail() { - return empty() ? d_head : d_head->d_prev; - } - - const elt_t* head() const { - return d_head; - } - - const elt_t* tail() const { - return empty() ? d_head : d_head->d_prev; - } - - T front() const { - Assert(! empty()); - return head()->element(); - } - - T back() const { - Assert(! empty()); - return tail()->element(); - } - - void push_back(const T& t) { - if(Debug.isOn("cdcirclist:paranoid")) { - debugCheck(); - } - // FIXME LEAK! (should alloc in CMM, no?) - elt_t* x = d_allocator.allocate(1); - if(empty()) { - // zero-element case - new(x) elt_t(d_context, t, x, x); - d_head = x; - } else { - // N-element case - new(x) elt_t(d_context, t, d_head->d_prev, d_head); - d_head->d_prev->d_next = x; - d_head->d_prev = x; - } - } - - /** - * Concatenate two lists. This modifies both: afterward, the two - * lists might have different heads, but they will have the same - * elements in the same (circular) order. - */ - void concat(CDCircList& l) { - Assert(this != &l, "cannot concat a list with itself"); - - if(d_head == NULL) { - d_head = l.d_head; - return; - } else if(l.d_head == NULL) { - l.d_head = d_head; - return; - } - - // splice together the two circular lists - CDPtr &l1head = head(), &l2head = l.head(); - CDPtr &l1tail = tail(), &l2tail = l.tail(); - // l2tail will change underneath us in what's below (because it's - // the same as l2head->prev()), so we have to keep a regular - // pointer to it - elt_t* oldl2tail = l2tail; - - Debug("cdcirclist") << "concat1 " << this << " " << &l << std::endl; - l1tail->next() = l2head; - Debug("cdcirclist") << "concat2" << std::endl; - l2head->prev() = l1tail; - - Debug("cdcirclist") << "concat3" << std::endl; - oldl2tail->next() = l1head; - Debug("cdcirclist") << "concat4" << std::endl; - l1head->prev() = oldl2tail; - Debug("cdcirclist") << "concat5" << std::endl; - } - - class iterator { - const CDCircList* d_list; - const elt_t* d_current; - friend class CDCircList; - public: - iterator(const CDCircList* list, const elt_t* first) : - d_list(list), - d_current(first) { - } - iterator(const iterator& other) : - d_list(other.d_list), - d_current(other.d_current) { - } - - bool operator==(const iterator& other) const { - return d_list == other.d_list && d_current == other.d_current; - } - bool operator!=(const iterator& other) const { - return !(*this == other); - } - iterator& operator++() { - Assert(d_current != NULL, "iterator already off the end"); - if(d_current == d_list->tail()) { - d_current = NULL; - } else { - d_current = d_current->next(); - } - return *this; - } - iterator operator++(int) { - const elt_t* old = d_current; - ++*this; - return iterator(d_list, old); - } - iterator& operator--() { - // undefined to go off the beginning, but don't have a check for that - if(d_current == NULL) { - d_current = d_list->tail(); - } else { - d_current = d_current->prev(); - } - return *this; - } - iterator operator--(int) { - const elt_t* old = d_current; - --*this; - return iterator(d_list, old); - } - T operator*() { - Assert(d_current != NULL, "iterator already off the end"); - return d_current->element(); - } - };/* class CDCircList<>::iterator */ - - // list elements are immutable - typedef iterator const_iterator; - - iterator begin() { - if(Debug.isOn("cdcirclist:paranoid")) { - debugCheck(); - } - return iterator(this, head()); - } - - iterator end() { - if(Debug.isOn("cdcirclist:paranoid")) { - debugCheck(); - } - return iterator(this, NULL); - } - - const_iterator begin() const { - return const_iterator(this, head()); - } - - const_iterator end() const { - return const_iterator(this, NULL); - } - - iterator erase(iterator pos) { - Assert(pos.d_current != NULL); - if(pos.d_current->prev() == pos.d_current) { - // one-elt list - d_head = NULL; - return iterator(this, NULL); - } else { - // N-elt list - if(pos.d_current == d_head) { - // removing list head - elt_t *pHead = head(), *pTail = tail(); - pTail->next() = pHead->next(); - pHead->next()->prev() = pTail; - d_head = pHead->next(); - return iterator(this, d_head); - // can't free old head, because of backtracking - } else { - // not removing list head - const elt_t *elt = pos.d_current; - elt_t *prev = pos.d_current->prev(); - prev->next() = elt->next(); - elt->next()->prev() = prev; - return iterator(this, elt->next()); - // can't free elt, because of backtracking - } - } - } - -private: - - // do not permit copy/assignment - CDCircList(const CDCircList&) CVC4_UNUSED; - CDCircList& operator=(const CDCircList&) CVC4_UNUSED; - -public: - /** Check internal structure and invariants of the list */ - void debugCheck() const { - elt_t* p = d_head; - Debug("cdcirclist") << "this is " << this << std::endl; - if(p == NULL) { - Debug("cdcirclist") << "head[" << &d_head << "] is NULL : " << d_context->getLevel() << std::endl; - // empty list - return; - } - Debug("cdcirclist") << "head[" << &d_head << "] is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << d_context->getLevel() << std::endl;//p->d_t << std::endl; - do { - elt_t* p_last = p; - p = p->d_next; - if(p == NULL) { - Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, next == NULL ******" << std::endl; - break; - } - Debug("cdcirclist") << " p is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << std::endl;//p->d_t << std::endl; - if(p->d_prev != p_last) { - Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, prev != last ******" << std::endl; - } - //Assert(p->d_prev == p_last); - Assert(p != NULL); - } while(p != d_head); - } - -private: - - // Nothing to save; the elements take care of themselves - virtual ContextObj* save(ContextMemoryManager* pCMM) { - Unreachable(); - } - - // Similarly, nothing to restore - virtual void restore(ContextObj* data) { - Unreachable(); - } - -};/* class CDCircList<> */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDCIRCLIST_H */ diff --git a/src/context/cdcirclist_forward.h b/src/context/cdcirclist_forward.h deleted file mode 100644 index 56a39e96f..000000000 --- a/src/context/cdcirclist_forward.h +++ /dev/null @@ -1,45 +0,0 @@ -/********************* */ -/*! \file cdcirclist_forward.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This is a forward declaration header to declare the - ** CDCircList<> template - ** - ** This is a forward declaration header to declare the CDCircList<> - ** template. It's useful if you want to forward-declare CDCircList<> - ** without including the full cdcirclist.h header, for example, in a - ** public header context, or to keep compile times low when only a - ** forward declaration is needed. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H -#define __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H - -#include - -namespace __gnu_cxx { - template struct hash; -}/* __gnu_cxx namespace */ - -namespace CVC4 { - namespace context { - template - class ContextMemoryAllocator; - - template > - class CDCircList; - }/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H */ diff --git a/src/cvc4.i b/src/cvc4.i index 08b2c509f..a4d5e1986 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -112,7 +112,7 @@ using namespace CVC4; %include "expr/kind.i" %include "expr/expr.i" %include "expr/command.i" -%include "expr/declaration_scope.i" +%include "expr/symbol_table.i" %include "expr/expr_manager.i" %include "expr/expr_stream.i" diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 38cb8250c..b581e8919 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -24,8 +24,8 @@ libexpr_la_SOURCES = \ node_value.cpp \ command.h \ command.cpp \ - declaration_scope.h \ - declaration_scope.cpp \ + symbol_table.h \ + symbol_table.cpp \ expr_manager_scope.h \ node_self_iterator.h \ variable_type_map.h \ @@ -62,7 +62,7 @@ EXTRA_DIST = \ mkexpr \ expr_stream.i \ expr_manager.i \ - declaration_scope.i \ + symbol_table.i \ command.i \ type.i \ kind.i \ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 70535cf1c..a963b9f55 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -40,23 +40,23 @@ namespace attr { * A hash function for attribute table keys. Attribute table keys are * pairs, (unique-attribute-id, Node). */ -struct AttrHashStrategy { +struct AttrHashFunction { enum { LARGE_PRIME = 32452843ul }; std::size_t operator()(const std::pair& p) const { return p.first * LARGE_PRIME + p.second->getId(); } -}; +};/* struct AttrHashFunction */ /** * A hash function for boolean-valued attribute table keys; here we * don't have to store a pair as the key, because we use a known bit * in [0..63] for each attribute */ -struct AttrHashBoolStrategy { +struct AttrBoolHashFunction { std::size_t operator()(NodeValue* nv) const { return (size_t)nv->getId(); } -}; +};/* struct AttrBoolHashFunction */ }/* CVC4::expr::attr namespace */ @@ -156,7 +156,7 @@ template class AttrHash : public __gnu_cxx::hash_map, value_type, - AttrHashStrategy> { + AttrHashFunction> { };/* class AttrHash<> */ /** @@ -167,10 +167,10 @@ template <> class AttrHash : protected __gnu_cxx::hash_map { + AttrBoolHashFunction> { /** A "super" type, like in Java, for easy reference below. */ - typedef __gnu_cxx::hash_map super; + typedef __gnu_cxx::hash_map super; /** * BitAccessor allows us to return a bit "by reference." Of course, @@ -367,12 +367,12 @@ template class CDAttrHash : public context::CDHashMap, value_type, - AttrHashStrategy> { + AttrHashFunction> { public: CDAttrHash(context::Context* ctxt) : context::CDHashMap, value_type, - AttrHashStrategy>(ctxt) { + AttrHashFunction>(ctxt) { } };/* class CDAttrHash<> */ @@ -384,10 +384,10 @@ template <> class CDAttrHash : protected context::CDHashMap { + AttrBoolHashFunction> { /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDHashMap super; + typedef context::CDHashMap super; /** * BitAccessor allows us to return a bit "by reference." Of course, diff --git a/src/expr/declaration_scope.i b/src/expr/declaration_scope.i deleted file mode 100644 index e32c4ee4f..000000000 --- a/src/expr/declaration_scope.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "expr/declaration_scope.h" -%} - -%include "expr/declaration_scope.h" diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 6313aa30b..1acbed978 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -87,9 +87,11 @@ inline std::string kindToString(::CVC4::Kind k) { return ss.str(); } -struct KindHashStrategy { - static inline size_t hash(::CVC4::Kind k) { return k; } -};/* struct KindHashStrategy */ +struct KindHashFunction { + inline size_t operator()(::CVC4::Kind k) const { + return k; + } +};/* struct KindHashFunction */ }/* CVC4::kind namespace */ @@ -104,11 +106,11 @@ ${type_constant_list} /** * We hash the constants with their values. */ -struct TypeConstantHashStrategy { - static inline size_t hash(TypeConstant tc) { +struct TypeConstantHashFunction { + inline size_t operator()(TypeConstant tc) const { return tc; } -};/* struct BoolHashStrategy */ +};/* struct TypeConstantHashFunction */ inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { switch(typeConstant) { diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 5608d2972..647c1af8e 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -193,7 +193,7 @@ function constant { fi fi if ! expr "$3" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2 + echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFunction)" >&2 fi if [ -n "$4" ]; then @@ -252,7 +252,7 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { metakind_constHashes="${metakind_constHashes} case kind::$1: #line $lineno \"$kf\" - return $3::hash(nv->getConst< $2 >()); + return $3()(nv->getConst< $2 >()); " metakind_constPrinters="${metakind_constPrinters} case kind::$1: diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ce6a91483..682a48bda 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -75,7 +75,7 @@ class NodeManager { }; typedef __gnu_cxx::hash_set NodeValuePool; typedef __gnu_cxx::hash_set >::difference_type p, * PERFORMING for other uses! NodeValue::poolHash() will lead to * collisions for all VARIABLEs. */ -struct NodeValuePoolHashFcn { +struct NodeValuePoolHashFunction { inline size_t operator()(const NodeValue* nv) const { return (size_t) nv->poolHash(); } -};/* struct NodeValuePoolHashFcn */ +};/* struct NodeValuePoolHashFunction */ /** * For hash_maps, hash_sets, etc. @@ -371,7 +371,7 @@ struct NodeValueIDHashFunction { inline size_t operator()(const NodeValue* nv) const { return (size_t) nv->getId(); } -};/* struct NodeValueIDHashFcn */ +};/* struct NodeValueIDHashFunction */ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv); diff --git a/src/expr/declaration_scope.cpp b/src/expr/symbol_table.cpp similarity index 80% rename from src/expr/declaration_scope.cpp rename to src/expr/symbol_table.cpp index 6038fadab..c9234b5e0 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/symbol_table.cpp @@ -1,24 +1,24 @@ /********************* */ -/*! \file declaration_scope.cpp +/*! \file symbol_table.cpp ** \verbatim ** Original author: cconway - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan, ajreynol + ** Major contributors: bobot, mdeters + ** Minor contributors (to current version): ajreynol, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** ** \brief Convenience class for scoping variable and type - ** declarations (implementation). + ** declarations (implementation) ** ** Convenience class for scoping variable and type declarations ** (implementation). **/ -#include "expr/declaration_scope.h" +#include "expr/symbol_table.h" #include "expr/expr.h" #include "expr/type.h" #include "expr/expr_manager_scope.h" @@ -35,21 +35,21 @@ using namespace std; namespace CVC4 { -DeclarationScope::DeclarationScope() : +SymbolTable::SymbolTable() : d_context(new Context), d_exprMap(new(true) CDHashMap(d_context)), d_typeMap(new(true) CDHashMap, Type>, StringHashFunction>(d_context)), d_functions(new(true) CDHashSet(d_context)) { } -DeclarationScope::~DeclarationScope() { +SymbolTable::~SymbolTable() { d_exprMap->deleteSelf(); d_typeMap->deleteSelf(); d_functions->deleteSelf(); delete d_context; } -void DeclarationScope::bind(const std::string& name, Expr obj, +void SymbolTable::bind(const std::string& name, Expr obj, bool levelZero) throw(AssertionException) { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); @@ -57,7 +57,7 @@ void DeclarationScope::bind(const std::string& name, Expr obj, else d_exprMap->insert(name, obj); } -void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj, +void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj, bool levelZero) throw(AssertionException) { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); @@ -70,25 +70,25 @@ void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj, } } -bool DeclarationScope::isBound(const std::string& name) const throw() { +bool SymbolTable::isBound(const std::string& name) const throw() { return d_exprMap->find(name) != d_exprMap->end(); } -bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() { +bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() { CDHashMap::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } -bool DeclarationScope::isBoundDefinedFunction(Expr func) const throw() { +bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() { return d_functions->contains(func); } -Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) { +Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) { return (*d_exprMap->find(name)).second; } -void DeclarationScope::bindType(const std::string& name, Type t, +void SymbolTable::bindType(const std::string& name, Type t, bool levelZero) throw() { if(levelZero){ d_typeMap->insertAtContextLevelZero(name, make_pair(vector(), t)); @@ -97,7 +97,7 @@ void DeclarationScope::bindType(const std::string& name, Type t, } } -void DeclarationScope::bindType(const std::string& name, +void SymbolTable::bindType(const std::string& name, const std::vector& params, Type t, bool levelZero) throw() { @@ -117,11 +117,11 @@ void DeclarationScope::bindType(const std::string& name, } } -bool DeclarationScope::isBoundType(const std::string& name) const throw() { +bool SymbolTable::isBoundType(const std::string& name) const throw() { return d_typeMap->find(name) != d_typeMap->end(); } -Type DeclarationScope::lookupType(const std::string& name) const throw(AssertionException) { +Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) { pair, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == 0, "type constructor arity is wrong: " @@ -130,7 +130,7 @@ Type DeclarationScope::lookupType(const std::string& name) const throw(Assertion return p.second; } -Type DeclarationScope::lookupType(const std::string& name, +Type SymbolTable::lookupType(const std::string& name, const std::vector& params) const throw(AssertionException) { pair, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == params.size(), @@ -188,23 +188,23 @@ Type DeclarationScope::lookupType(const std::string& name, } } -size_t DeclarationScope::lookupArity(const std::string& name) { +size_t SymbolTable::lookupArity(const std::string& name) { pair, Type> p = (*d_typeMap->find(name)).second; return p.first.size(); } -void DeclarationScope::popScope() throw(ScopeException) { +void SymbolTable::popScope() throw(ScopeException) { if( d_context->getLevel() == 0 ) { throw ScopeException(); } d_context->pop(); } -void DeclarationScope::pushScope() throw() { +void SymbolTable::pushScope() throw() { d_context->push(); } -size_t DeclarationScope::getLevel() const throw() { +size_t SymbolTable::getLevel() const throw() { return d_context->getLevel(); } diff --git a/src/expr/declaration_scope.h b/src/expr/symbol_table.h similarity index 93% rename from src/expr/declaration_scope.h rename to src/expr/symbol_table.h index 8695d9287..ee04b17fd 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/symbol_table.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file declaration_scope.h +/*! \file symbol_table.h ** \verbatim ** Original author: cconway ** Major contributors: mdeters - ** Minor contributors (to current version): ajreynol + ** Minor contributors (to current version): ajreynol, dejan, bobot ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__DECLARATION_SCOPE_H -#define __CVC4__DECLARATION_SCOPE_H +#ifndef __CVC4__SYMBOL_TABLE_H +#define __CVC4__SYMBOL_TABLE_H #include #include @@ -47,7 +47,7 @@ class CVC4_PUBLIC ScopeException : public Exception { * nested scoping rules for declarations, with separate bindings for expressions * and types. */ -class CVC4_PUBLIC DeclarationScope { +class CVC4_PUBLIC SymbolTable { /** The context manager for the scope maps. */ context::Context* d_context; @@ -62,10 +62,10 @@ class CVC4_PUBLIC DeclarationScope { public: /** Create a declaration scope. */ - DeclarationScope(); + SymbolTable(); /** Destroy a declaration scope. */ - ~DeclarationScope(); + ~SymbolTable(); /** * Bind an expression to a name in the current scope level. If @@ -188,7 +188,7 @@ public: * pushScope. Calls to pushScope and * popScope must be "properly nested." I.e., a call to * popScope is only legal if the number of prior calls to - * pushScope on this DeclarationScope is strictly + * pushScope on this SymbolTable is strictly * greater than then number of prior calls to popScope. */ void popScope() throw(ScopeException); @@ -198,8 +198,8 @@ public: /** Get the current level of this declaration scope. */ size_t getLevel() const throw(); -};/* class DeclarationScope */ +};/* class SymbolTable */ }/* CVC4 namespace */ -#endif /* __CVC4__DECLARATION_SCOPE_H */ +#endif /* __CVC4__SYMBOL_TABLE_H */ diff --git a/src/expr/symbol_table.i b/src/expr/symbol_table.i new file mode 100644 index 000000000..7e5579c49 --- /dev/null +++ b/src/expr/symbol_table.i @@ -0,0 +1,5 @@ +%{ +#include "expr/symbol_table.h" +%} + +%include "expr/symbol_table.h" diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index bbeee4f7f..1a85f45c3 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1057,7 +1057,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, std::string id; std::vector types; std::vector< std::pair > typeIds; - DeclarationScope* declScope; + //SymbolTable* symtab; Parser* parser; lhs = false; } @@ -1097,11 +1097,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, * declared in the outer context. What follows isn't quite right, * though, since type aliases and function definitions should be * retained in the set of current declarations. */ - { /*declScope = PARSER_STATE->getDeclarationScope(); - PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ } + { /*symtab = PARSER_STATE->getSymbolTable(); + PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ } formula[f] ( COMMA formula[f2] )? RPAREN - { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope(); - PARSER_STATE->useDeclarationsFrom(declScope); + { /*SymbolTable* old = PARSER_STATE->getSymbolTable(); + PARSER_STATE->useDeclarationsFrom(symtab); delete old;*/ t = f2.isNull() ? EXPR_MANAGER->mkPredicateSubtype(f) : diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 44148a7f1..29db640c7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -43,8 +43,8 @@ namespace parser { Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : d_exprManager(exprManager), d_input(input), - d_declScopeAllocated(), - d_declScope(&d_declScopeAllocated), + d_symtabAllocated(), + d_symtab(&d_symtabAllocated), d_anonymousFunctionCount(0), d_done(false), d_checksEnabled(true), @@ -60,7 +60,7 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - return d_declScope->lookup(name); + return d_symtab->lookup(name); default: Unhandled(type); @@ -87,7 +87,7 @@ Type Parser::getType(const std::string& var_name, Type Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope->lookupType(name); + Type t = d_symtab->lookupType(name); return t; } @@ -95,14 +95,14 @@ Type Parser::getSort(const std::string& name, const std::vector& params) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope->lookupType(name, params); + Type t = d_symtab->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name){ checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(sort_name, SYM_SORT) ); - return d_declScope->lookupArity(sort_name); + return d_symtab->lookupArity(sort_name); } /* Returns true if name is bound to a boolean variable. */ @@ -125,14 +125,14 @@ bool Parser::isFunctionLike(const std::string& name) { bool Parser::isDefinedFunction(const std::string& name) { // more permissive in type than isFunction(), because defined // functions can be zero-ary and declared functions cannot. - return d_declScope->isBoundDefinedFunction(name); + return d_symtab->isBoundDefinedFunction(name); } /* Returns true if the Expr is a defined function. */ bool Parser::isDefinedFunction(Expr func) { // more permissive in type than isFunction(), because defined // functions can be zero-ary and declared functions cannot. - return d_declScope->isBoundDefinedFunction(func); + return d_symtab->isBoundDefinedFunction(func); } /* Returns true if name is bound to a function returning boolean. */ @@ -179,20 +179,20 @@ Parser::mkVars(const std::vector names, void Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) { - d_declScope->bind(name, val, levelZero); + d_symtab->bind(name, val, levelZero); Assert( isDeclared(name) ); } void Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) { - d_declScope->bindDefinedFunction(name, val, levelZero); + d_symtab->bindDefinedFunction(name, val, levelZero); Assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { - d_declScope->bindType(name, type); + d_symtab->bindType(name, type); Assert( isDeclared(name, SYM_SORT) ); } @@ -200,7 +200,7 @@ void Parser::defineType(const std::string& name, const std::vector& params, const Type& type) { - d_declScope->bindType(name, params, type); + d_symtab->bindType(name, params, type); Assert( isDeclared(name, SYM_SORT) ); } @@ -369,9 +369,9 @@ DatatypeType Parser::mkTupleType(const std::vector& types) { bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: - return d_declScope->isBound(name); + return d_symtab->isBound(name); case SYM_SORT: - return d_declScope->isBoundType(name); + return d_symtab->isBoundType(name); default: Unhandled(type); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 635dd6b6c..f3210ae29 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -28,7 +28,7 @@ #include "parser/input.h" #include "parser/parser_exception.h" #include "expr/expr.h" -#include "expr/declaration_scope.h" +#include "expr/symbol_table.h" #include "expr/kind.h" #include "expr/expr_stream.h" @@ -117,15 +117,15 @@ class CVC4_PUBLIC Parser { * The declaration scope that is "owned" by this parser. May or * may not be the current declaration scope in use. */ - DeclarationScope d_declScopeAllocated; + SymbolTable d_symtabAllocated; /** * This current symbol table used by this parser. Initially points - * to d_declScopeAllocated, but can be changed (making this parser + * to d_symtabAllocated, but can be changed (making this parser * delegate its definitions and lookups to another parser). * See useDeclarationsFrom(). */ - DeclarationScope* d_declScope; + SymbolTable* d_symtab; /** How many anonymous functions we've created. */ size_t d_anonymousFunctionCount; @@ -493,8 +493,8 @@ public: } } - inline void pushScope() { d_declScope->pushScope(); } - inline void popScope() { d_declScope->popScope(); } + inline void pushScope() { d_symtab->pushScope(); } + inline void popScope() { d_symtab->popScope(); } /** * Set the current symbol table used by this parser. @@ -523,25 +523,25 @@ public: */ inline void useDeclarationsFrom(Parser* parser) { if(parser == NULL) { - d_declScope = &d_declScopeAllocated; + d_symtab = &d_symtabAllocated; } else { - d_declScope = parser->d_declScope; + d_symtab = parser->d_symtab; } } - inline void useDeclarationsFrom(DeclarationScope* scope) { - d_declScope = scope; + inline void useDeclarationsFrom(SymbolTable* symtab) { + d_symtab = symtab; } - inline DeclarationScope* getDeclarationScope() const { - return d_declScope; + inline SymbolTable* getSymbolTable() const { + return d_symtab; } /** * Gets the current declaration level. */ inline size_t getDeclarationLevel() const throw() { - return d_declScope->getLevel(); + return d_symtab->getLevel(); } /** diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 7883bd92b..b9fac6e20 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -38,7 +38,7 @@ sort INTEGER_TYPE \ constant SUBRANGE_TYPE \ ::CVC4::SubrangeBounds \ - ::CVC4::SubrangeBoundsHashStrategy \ + ::CVC4::SubrangeBoundsHashFunction \ "util/subrange_bound.h" \ "the type of an integer subrange" cardinality SUBRANGE_TYPE \ @@ -51,7 +51,7 @@ well-founded SUBRANGE_TYPE \ constant CONST_RATIONAL \ ::CVC4::Rational \ - ::CVC4::RationalHashStrategy \ + ::CVC4::RationalHashFunction \ "util/rational.h" \ "a multiple-precision rational constant" diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index b34232b8f..e847a238d 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -2,28 +2,10 @@ /*! \file array_info.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan, barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/*! \file array_info.h - ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -31,14 +13,13 @@ ** ** \brief Contains additional classes to store context dependent information ** for each term of type array - ** - ** **/ #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H + #include "util/backtrackable.h" #include "context/cdlist.h" #include "context/cdhashmap.h" @@ -58,7 +39,7 @@ typedef context::CDList CTNodeList; typedef quad RowLemmaType; struct RowLemmaTypeHashFunction { - size_t operator()(const RowLemmaType& q ) const { + size_t operator()(const RowLemmaType& q) const { TNode n1 = q.first; TNode n2 = q.second; TNode n3 = q.third; @@ -92,7 +73,6 @@ public: indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); - } ~Info() { @@ -115,7 +95,7 @@ public: Trace("arrays-info")<<" in_stores "; printList(in_stores); } -}; +};/* class Info */ typedef __gnu_cxx::hash_map CNodeInfoMap; @@ -202,7 +182,7 @@ public: StatisticsRegistry::registerStat(&d_tableSize); } - ~ArrayInfo(){ + ~ArrayInfo() { CNodeInfoMap::iterator it = info_map.begin(); for( ; it != info_map.end(); it++ ) { if((*it).second!= emptyInfo) { @@ -255,8 +235,7 @@ public: * a should be the canonical representative of b */ void mergeInfo(const TNode a, const TNode b); -}; - +};/* class ArrayInfo */ }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 7386ec5c2..ef237e351 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -32,7 +32,7 @@ operator STORE 3 "array store" # storeall t e is \all i in indexType(t) <= e constant STORE_ALL \ ::CVC4::ArrayStoreAll \ - ::CVC4::ArrayStoreAllHashStrategy \ + ::CVC4::ArrayStoreAllHashFunction \ "util/array_store_all.h" \ "array store-all" diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 92a9a937f..4d748ca59 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -20,7 +20,7 @@ sort BOOLEAN_TYPE \ constant CONST_BOOLEAN \ bool \ - ::CVC4::BoolHashStrategy \ + ::CVC4::BoolHashFunction \ "util/bool.h" \ "truth and falsity" diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 57baa82cd..6bb175db3 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -122,7 +122,7 @@ # to define it. Hasher is a hash functor type defined like this: # # struct MyHashFcn { -# static size_t hash(const T& val); +# size_t operator()(const T& val) const; # }; # # For consistency, constants taking a non-void payload should @@ -267,7 +267,7 @@ well-founded SORT_TYPE \ constant UNINTERPRETED_CONSTANT \ ::CVC4::UninterpretedConstant \ - ::CVC4::UninterpretedConstantHashStrategy \ + ::CVC4::UninterpretedConstantHashFunction \ "util/uninterpreted_constant.h" \ "The kind of nodes representing uninterpreted constants" typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule @@ -281,7 +281,7 @@ enumerator SORT_TYPE \ # you'll get a special, singleton (BUILTIN EQUAL) Node. constant BUILTIN \ ::CVC4::Kind \ - ::CVC4::kind::KindHashStrategy \ + ::CVC4::kind::KindHashFunction \ "expr/kind.h" \ "The kind of nodes representing built-in operators" @@ -296,7 +296,7 @@ operator TUPLE 2: "a tuple" constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ - ::CVC4::TypeConstantHashStrategy \ + ::CVC4::TypeConstantHashFunction \ "expr/kind.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" @@ -325,7 +325,7 @@ sort STRING_TYPE \ "String type" constant CONST_STRING \ ::std::string \ - ::CVC4::StringHashStrategy \ + ::CVC4::StringHashFunction \ "util/hash.h" \ "a string of characters" typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule @@ -337,7 +337,7 @@ typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ - ::CVC4::PredicateHashStrategy \ + ::CVC4::PredicateHashFunction \ "util/predicate.h" \ "predicate subtype" cardinality SUBTYPE_TYPE \ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 36e27c66c..765f6bc59 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -14,7 +14,7 @@ rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" constant BITVECTOR_TYPE \ ::CVC4::BitVectorSize \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ + "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" cardinality BITVECTOR_TYPE \ @@ -23,7 +23,7 @@ cardinality BITVECTOR_TYPE \ constant CONST_BITVECTOR \ ::CVC4::BitVector \ - ::CVC4::BitVectorHashStrategy \ + ::CVC4::BitVectorHashFunction \ "util/bitvector.h" \ "a fixed-width bit-vector constant" @@ -63,43 +63,43 @@ operator BITVECTOR_SGE 2 "signed greater than or equal" constant BITVECTOR_BITOF_OP \ ::CVC4::BitVectorBitOf \ - ::CVC4::BitVectorBitOfHashStrategy \ + ::CVC4::BitVectorBitOfHashFunction \ "util/bitvector.h" \ "operator for the bit-vector boolean bit extract" constant BITVECTOR_EXTRACT_OP \ ::CVC4::BitVectorExtract \ - ::CVC4::BitVectorExtractHashStrategy \ + ::CVC4::BitVectorExtractHashFunction \ "util/bitvector.h" \ "operator for the bit-vector extract" constant BITVECTOR_REPEAT_OP \ ::CVC4::BitVectorRepeat \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRepeat >" \ + "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \ "util/bitvector.h" \ "operator for the bit-vector repeat" constant BITVECTOR_ZERO_EXTEND_OP \ ::CVC4::BitVectorZeroExtend \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorZeroExtend >" \ + "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \ "util/bitvector.h" \ "operator for the bit-vector zero-extend" constant BITVECTOR_SIGN_EXTEND_OP \ ::CVC4::BitVectorSignExtend \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSignExtend >" \ + "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \ "util/bitvector.h" \ "operator for the bit-vector sign-extend" constant BITVECTOR_ROTATE_LEFT_OP \ ::CVC4::BitVectorRotateLeft \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateLeft >" \ + "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \ "util/bitvector.h" \ "operator for the bit-vector rotate left" constant BITVECTOR_ROTATE_RIGHT_OP \ ::CVC4::BitVectorRotateRight \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \ + "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \ "util/bitvector.h" \ "operator for the bit-vector rotate right" diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index e66cc3454..58c8fb5d2 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -44,7 +44,7 @@ parameterized APPLY_TESTER TESTER_TYPE 1: "tester application" constant DATATYPE_TYPE \ ::CVC4::Datatype \ - "::CVC4::DatatypeHashStrategy" \ + "::CVC4::DatatypeHashFunction" \ "util/datatype.h" \ "datatype type" cardinality DATATYPE_TYPE \ @@ -72,7 +72,7 @@ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ "type ascription, for datatype constructor applications" constant ASCRIPTION_TYPE \ ::CVC4::AscriptionType \ - ::CVC4::AscriptionTypeHashStrategy \ + ::CVC4::AscriptionTypeHashFunction \ "util/ascription_type.h" \ "a type parameter for type ascription" diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index fb42909e0..cba5c7051 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -69,7 +69,7 @@ class ITESimplifier { hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2); return hash; } - }; + };/* struct ITESimplifier::NodePairHashFunction */ typedef std::hash_map NodePairMap; diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h index 834eec2c3..277422ecf 100644 --- a/src/util/array_store_all.h +++ b/src/util/array_store_all.h @@ -88,12 +88,12 @@ public: std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC; /** - * Hash function for the BitVector constants. + * Hash function for the ArrayStoreAll constants. */ -struct CVC4_PUBLIC ArrayStoreAllHashStrategy { - static inline size_t hash(const ArrayStoreAll& asa) { +struct CVC4_PUBLIC ArrayStoreAllHashFunction { + inline size_t operator()(const ArrayStoreAll& asa) const { return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); } -};/* struct ArrayStoreAllHashStrategy */ +};/* struct ArrayStoreAllHashFunction */ }/* CVC4 namespace */ diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h index 81289572c..579746332 100644 --- a/src/util/ascription_type.h +++ b/src/util/ascription_type.h @@ -48,11 +48,11 @@ public: /** * A hash strategy for type ascription operators. */ -struct CVC4_PUBLIC AscriptionTypeHashStrategy { - static inline size_t hash(const AscriptionType& at) { +struct CVC4_PUBLIC AscriptionTypeHashFunction { + inline size_t operator()(const AscriptionType& at) const { return TypeHashFunction()(at.getType()); } -};/* struct AscriptionTypeHashStrategy */ +};/* struct AscriptionTypeHashFunction */ /** An output routine for AscriptionTypes */ inline std::ostream& operator<<(std::ostream& out, AscriptionType at) { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 5d0c301d4..185bb55d9 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -375,11 +375,11 @@ inline BitVector::BitVector(const std::string& num, unsigned base) { /** * Hash function for the BitVector constants. */ -struct CVC4_PUBLIC BitVectorHashStrategy { - static inline size_t hash(const BitVector& bv) { +struct CVC4_PUBLIC BitVectorHashFunction { + inline size_t operator()(const BitVector& bv) const { return bv.hash(); } -};/* struct BitVectorHashStrategy */ +};/* struct BitVectorHashFunction */ /** * The structure representing the extraction operation for bit-vectors. The @@ -403,14 +403,13 @@ struct CVC4_PUBLIC BitVectorExtract { /** * Hash function for the BitVectorExtract objects. */ -class CVC4_PUBLIC BitVectorExtractHashStrategy { -public: - static size_t hash(const BitVectorExtract& extract) { +struct CVC4_PUBLIC BitVectorExtractHashFunction { + size_t operator()(const BitVectorExtract& extract) const { size_t hash = extract.low; hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2); return hash; } -};/* class BitVectorExtractHashStrategy */ +};/* struct BitVectorExtractHashFunction */ /** @@ -430,12 +429,11 @@ struct CVC4_PUBLIC BitVectorBitOf { /** * Hash function for the BitVectorBitOf objects. */ -class CVC4_PUBLIC BitVectorBitOfHashStrategy { -public: - static size_t hash(const BitVectorBitOf& b) { +struct CVC4_PUBLIC BitVectorBitOfHashFunction { + size_t operator()(const BitVectorBitOf& b) const { return b.bitIndex; } -};/* class BitVectorBitOfHashStrategy */ +};/* struct BitVectorBitOfHashFunction */ @@ -482,11 +480,11 @@ struct CVC4_PUBLIC BitVectorRotateRight { };/* struct BitVectorRotateRight */ template -struct CVC4_PUBLIC UnsignedHashStrategy { - static inline size_t hash(const T& x) { +struct CVC4_PUBLIC UnsignedHashFunction { + inline size_t operator()(const T& x) const { return (size_t)x; } -};/* struct UnsignedHashStrategy */ +};/* struct UnsignedHashFunction */ inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) { @@ -503,8 +501,6 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) { return os << "[" << bv.bitIndex << "]"; } - - }/* CVC4 namespace */ #endif /* __CVC4__BITVECTOR_H */ diff --git a/src/util/bool.h b/src/util/bool.h index a4d33ca61..9985395e3 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -29,11 +29,11 @@ namespace CVC4 { -struct BoolHashStrategy { - static inline size_t hash(bool b) { +struct BoolHashFunction { + inline size_t operator()(bool b) const { return b; } -};/* struct BoolHashStrategy */ +};/* struct BoolHashFunction */ }/* CVC4 namespace */ diff --git a/src/util/datatype.h b/src/util/datatype.h index b701073c7..c7631ae7b 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -559,17 +559,6 @@ public: };/* class Datatype */ -/** - * A hash strategy for Datatypes. Needed because Datatypes are used - * as the constant payload in CONSTANT-kinded TypeNodes (for - * DATATYPE_TYPE expressions). - */ -struct CVC4_PUBLIC DatatypeHashStrategy { - static inline size_t hash(const Datatype& dt) { - return StringHashFunction()(dt.getName()); - } -};/* struct DatatypeHashStrategy */ - /** * A hash function for Datatypes. Needed to store them in hash sets * and hash maps. diff --git a/src/util/hash.h b/src/util/hash.h index 6fb20dab0..2420b7acd 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -54,12 +54,6 @@ struct StringHashFunction { } };/* struct StringHashFunction */ -struct StringHashStrategy { - static size_t hash(const std::string& str) { - return std::hash()(str.c_str()); - } -};/* struct StringHashStrategy */ - }/* CVC4 namespace */ #endif /* __CVC4__HASH_H */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 43b77df6a..71d6d5b6d 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -460,11 +460,11 @@ public: friend class CVC4::Rational; };/* class Integer */ -struct IntegerHashStrategy { - static inline size_t hash(const CVC4::Integer& i) { +struct IntegerHashFunction { + inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); } -};/* struct IntegerHashStrategy */ +};/* struct IntegerHashFunction */ inline std::ostream& operator<<(std::ostream& os, const Integer& n) { return os << n.toString(); diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index dfd6c0599..ea7967023 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -418,11 +418,11 @@ public: friend class CVC4::Rational; };/* class Integer */ -struct IntegerHashStrategy { - static inline size_t hash(const CVC4::Integer& i) { +struct IntegerHashFunction { + inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); } -};/* struct IntegerHashStrategy */ +};/* struct IntegerHashFunction */ inline std::ostream& operator<<(std::ostream& os, const Integer& n) { return os << n.toString(); diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp index 1868f557d..748e818c3 100644 --- a/src/util/predicate.cpp +++ b/src/util/predicate.cpp @@ -49,7 +49,7 @@ operator<<(std::ostream& out, const Predicate& p) { return out; } -size_t PredicateHashStrategy::hash(const Predicate& p) { +size_t PredicateHashFunction::operator()(const Predicate& p) const { ExprHashFunction h; return h(p.d_witness) * 5039 + h(p.d_predicate); } diff --git a/src/util/predicate.h b/src/util/predicate.h index 94a685177..18e0b8b70 100644 --- a/src/util/predicate.h +++ b/src/util/predicate.h @@ -31,9 +31,9 @@ class Predicate; std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC; -struct CVC4_PUBLIC PredicateHashStrategy { - static size_t hash(const Predicate& p); -};/* class PredicateHashStrategy */ +struct CVC4_PUBLIC PredicateHashFunction { + size_t operator()(const Predicate& p) const; +};/* class PredicateHashFunction */ }/* CVC4 namespace */ @@ -55,7 +55,7 @@ public: bool operator==(const Predicate& p) const; friend std::ostream& operator<<(std::ostream& out, const Predicate& p); - friend size_t PredicateHashStrategy::hash(const Predicate& p); + friend size_t PredicateHashFunction::operator()(const Predicate& p) const; };/* class Predicate */ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index ea9f7d055..258060e02 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -314,11 +314,11 @@ public: };/* class Rational */ -struct RationalHashStrategy { - static inline size_t hash(const CVC4::Rational& r) { +struct RationalHashFunction { + inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); } -};/* struct RationalHashStrategy */ +};/* struct RationalHashFunction */ CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index ed9c57a80..22f1e91b2 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -296,11 +296,11 @@ public: };/* class Rational */ -struct RationalHashStrategy { - static inline size_t hash(const CVC4::Rational& r) { +struct RationalHashFunction { + inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); } -};/* struct RationalHashStrategy */ +};/* struct RationalHashFunction */ CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 063e59a0f..5de17106d 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -230,15 +230,15 @@ public: };/* class SubrangeBounds */ -struct CVC4_PUBLIC SubrangeBoundsHashStrategy { - static inline size_t hash(const SubrangeBounds& bounds) { +struct CVC4_PUBLIC SubrangeBoundsHashFunction { + inline size_t operator()(const SubrangeBounds& bounds) const { // We use Integer::hash() rather than Integer::getUnsignedLong() // because the latter might overflow and throw an exception size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits::max(); size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits::max(); return l + 0x9e3779b9 + (u << 6) + (u >> 2); } -};/* struct SubrangeBoundsHashStrategy */ +};/* struct SubrangeBoundsHashFunction */ inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC; diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h index 418b8d333..792da178e 100644 --- a/src/util/uninterpreted_constant.h +++ b/src/util/uninterpreted_constant.h @@ -77,10 +77,10 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC /** * Hash function for the BitVector constants. */ -struct CVC4_PUBLIC UninterpretedConstantHashStrategy { - static inline size_t hash(const UninterpretedConstant& uc) { - return TypeHashFunction()(uc.getType()) * IntegerHashStrategy::hash(uc.getIndex()); +struct CVC4_PUBLIC UninterpretedConstantHashFunction { + inline size_t operator()(const UninterpretedConstant& uc) const { + return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex()); } -};/* struct UninterpretedConstantHashStrategy */ +};/* struct UninterpretedConstantHashFunction */ }/* CVC4 namespace */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 88d21cac5..470fdac3d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -17,7 +17,7 @@ UNIT_TESTS = \ expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ - expr/declaration_scope_black \ + expr/symbol_table_black \ expr/node_self_iterator_black \ expr/type_cardinality_public \ expr/type_node_white \ @@ -30,7 +30,6 @@ UNIT_TESTS = \ context/cdo_black \ context/cdlist_black \ context/cdlist_context_memory_black \ - context/cdcirclist_white \ context/cdmap_black \ context/cdmap_white \ context/cdvector_black \ diff --git a/test/unit/context/cdcirclist_white.h b/test/unit/context/cdcirclist_white.h deleted file mode 100644 index b03a850a8..000000000 --- a/test/unit/context/cdcirclist_white.h +++ /dev/null @@ -1,223 +0,0 @@ -/********************* */ -/*! \file cdcirclist_white.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief White box testing of CVC4::context::CDCircList<>. - ** - ** White box testing of CVC4::context::CDCircList<>. - **/ - -#include - -#include -#include - -#include - -#include "context/context.h" -#include "context/cdcirclist.h" - -#include "util/output.h" - -using namespace std; -using namespace CVC4::context; -using namespace CVC4; - -class CDCircListWhite : public CxxTest::TestSuite { -private: - - Context* d_context; - -public: - - void setUp() { - d_context = new Context(); - } - - void tearDown() { - delete d_context; - } - - void testSimple() { - //Debug.on("cdcirclist"); - CDCircList l(d_context, ContextMemoryAllocator(d_context->getCMM())); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - d_context->push(); - { - TS_ASSERT(l.empty()); - l.push_back(1); - TS_ASSERT(!l.empty()); - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 1); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - l.push_back(2); - TS_ASSERT(!l.empty()); - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 2); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - l.push_back(3); - TS_ASSERT(!l.empty()); - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 3); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( l.concat(l), AssertionException ); -#endif /* CVC4_ASSERTIONS */ - - CDCircList l2(d_context, ContextMemoryAllocator(d_context->getCMM())); - l2.push_back(4); - l2.push_back(5); - l2.push_back(6); - TS_ASSERT_EQUALS(l2.front(), 4); - TS_ASSERT_EQUALS(l2.back(), 6); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - - d_context->push(); - { - l.concat(l2); - - TS_ASSERT_EQUALS(l.front(), 1); - TS_ASSERT_EQUALS(l.back(), 6); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - - TS_ASSERT_EQUALS(l2.front(), 4); - TS_ASSERT_EQUALS(l2.back(), 3); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - - d_context->push(); - { - CDCircList::iterator i = l.begin(); - CDCircList::iterator j = l.begin(); - TS_ASSERT_EQUALS(i, j); - TS_ASSERT_EQUALS(i++, j); - TS_ASSERT_EQUALS(i, ++j); - TS_ASSERT_EQUALS(l.erase(l.begin()), i); - - i = l.begin(); - TS_ASSERT_EQUALS(i, j); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(i, l.begin()); TS_ASSERT_EQUALS(i, j); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - } - d_context->pop(); - - CDCircList::iterator i = l.begin(); - TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(i, l.begin()); - - i = l2.begin(); - TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(i, l2.begin()); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - } - d_context->pop(); - - TS_ASSERT(! l.empty()); - TS_ASSERT(! l2.empty()); - - CDCircList::iterator i = l.begin(); - TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end()); - TS_ASSERT_EQUALS(i, l.begin()); - - i = l2.begin(); - TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end()); - TS_ASSERT_EQUALS(i, l2.begin()); - - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); - } - d_context->pop(); - - TS_ASSERT(l.empty()); - TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); - } - - void testCDPtr() { - int* x = (int*)0x12345678; - int* y = (int*)0x87654321; - CDPtr p(d_context, NULL); - TS_ASSERT(p == NULL); - d_context->push(); - TS_ASSERT(p == NULL); - d_context->push(); - TS_ASSERT(p == NULL); - p = x; - TS_ASSERT(p == x); - d_context->push(); - TS_ASSERT(p == x); - p = y; - TS_ASSERT(p == y); - d_context->pop(); - TS_ASSERT(p == x); - d_context->pop(); - TS_ASSERT(p == NULL); - d_context->pop(); - TS_ASSERT(p == NULL); - } - -};/* class CDCircListWhite */ diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/symbol_table_black.h similarity index 55% rename from test/unit/expr/declaration_scope_black.h rename to test/unit/expr/symbol_table_black.h index bde04157c..89fbf42e8 100644 --- a/test/unit/expr/declaration_scope_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file declaration_scope_black.h +/*! \file symbol_table_black.h ** \verbatim ** Original author: cconway ** Major contributors: none @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Black box testing of CVC4::DeclarationScope. + ** \brief Black box testing of CVC4::SymbolTable ** - ** Black box testing of CVC4::DeclarationScope. + ** Black box testing of CVC4::SymbolTable. **/ #include @@ -22,7 +22,7 @@ #include #include "context/context.h" -#include "expr/declaration_scope.h" +#include "expr/symbol_table.h" #include "expr/expr_manager.h" #include "expr/expr.h" #include "expr/type.h" @@ -34,7 +34,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace std; -class DeclarationScopeBlack : public CxxTest::TestSuite { +class SymbolTableBlack : public CxxTest::TestSuite { private: ExprManager* d_exprManager; @@ -60,104 +60,104 @@ public: } void testBind() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + symtab.bind("x",x); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); } void testBind2() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); // var name attribute shouldn't matter Expr y = d_exprManager->mkVar("y", booleanType); - declScope.bind("x",y); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + symtab.bind("x",y); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), y ); } void testBind3() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); + symtab.bind("x",x); Expr y = d_exprManager->mkVar(booleanType); // new binding covers old - declScope.bind("x",y); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + symtab.bind("x",y); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), y ); } void testBind4() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); + symtab.bind("x",x); Type t = d_exprManager->mkSort("T"); // duplicate binding for type is OK - declScope.bindType("x",t); + symtab.bindType("x",t); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); - TS_ASSERT( declScope.isBoundType("x") ); - TS_ASSERT_EQUALS( declScope.lookupType("x"), t ); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); + TS_ASSERT( symtab.isBoundType("x") ); + TS_ASSERT_EQUALS( symtab.lookupType("x"), t ); } void testBindType() { - DeclarationScope declScope; + SymbolTable symtab; Type s = d_exprManager->mkSort("S"); - declScope.bindType("S",s); - TS_ASSERT( declScope.isBoundType("S") ); - TS_ASSERT_EQUALS( declScope.lookupType("S"), s ); + symtab.bindType("S",s); + TS_ASSERT( symtab.isBoundType("S") ); + TS_ASSERT_EQUALS( symtab.lookupType("S"), s ); } void testBindType2() { - DeclarationScope declScope; + SymbolTable symtab; // type name attribute shouldn't matter Type s = d_exprManager->mkSort("S"); - declScope.bindType("T",s); - TS_ASSERT( declScope.isBoundType("T") ); - TS_ASSERT_EQUALS( declScope.lookupType("T"), s ); + symtab.bindType("T",s); + TS_ASSERT( symtab.isBoundType("T") ); + TS_ASSERT_EQUALS( symtab.lookupType("T"), s ); } void testBindType3() { - DeclarationScope declScope; + SymbolTable symtab; Type s = d_exprManager->mkSort("S"); - declScope.bindType("S",s); + symtab.bindType("S",s); Type t = d_exprManager->mkSort("T"); // new binding covers old - declScope.bindType("S",t); - TS_ASSERT( declScope.isBoundType("S") ); - TS_ASSERT_EQUALS( declScope.lookupType("S"), t ); + symtab.bindType("S",t); + TS_ASSERT( symtab.isBoundType("S") ); + TS_ASSERT_EQUALS( symtab.lookupType("S"), t ); } void testPushScope() { - DeclarationScope declScope; + SymbolTable symtab; Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); - declScope.bind("x",x); - declScope.pushScope(); + symtab.bind("x",x); + symtab.pushScope(); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); Expr y = d_exprManager->mkVar(booleanType); - declScope.bind("x",y); + symtab.bind("x",y); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), y ); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), y ); - declScope.popScope(); - TS_ASSERT( declScope.isBound("x") ); - TS_ASSERT_EQUALS( declScope.lookup("x"), x ); + symtab.popScope(); + TS_ASSERT( symtab.isBound("x") ); + TS_ASSERT_EQUALS( symtab.lookup("x"), x ); } void testBadPop() { - DeclarationScope declScope; + SymbolTable symtab; // TODO: What kind of exception gets thrown here? - TS_ASSERT_THROWS( declScope.popScope(), ScopeException ); + TS_ASSERT_THROWS( symtab.popScope(), ScopeException ); } -}; +};/* class SymbolTableBlack */ -- 2.30.2