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
+++ /dev/null
-/********************* */
-/*! \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 <iterator>
-#include <memory>
-#include <string>
-#include <sstream>
-
-#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 T>
-class CDPtr : public CDO<T*> {
- typedef CDO<T*> super;
-
- // private copy ctor
- CDPtr(const CDPtr<T>& 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<T>(*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<T>& 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<T>& operator=(const CDPtr<T>& 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<T> */
-
-
-/**
- * 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 T, class AllocatorT>
-class CDCircElement {
- typedef CDCircElement<T, AllocatorT> elt_t;
- const T d_t;
- CDPtr<elt_t> d_prev;
- CDPtr<elt_t> d_next;
- friend class CDCircList<T, AllocatorT>;
-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<elt_t>& next() { return d_next; }
- CDPtr<elt_t>& 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 T, class AllocatorT>
-class CDCircList : public ContextObj {
-public:
-
- /** List carrier element type */
- typedef CDCircElement<T, AllocatorT> 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<elt_t> d_head;
- /** The context with which we're associated */
- Context* d_context;
- /** Our allocator */
- typename Allocator::template rebind< CDCircElement<T, AllocatorT> >::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<elt_t>& head() {
- return d_head;
- }
-
- CDPtr<elt_t>& 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<T, AllocatorT>& 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<elt_t> &l1head = head(), &l2head = l.head();
- CDPtr<elt_t> &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<T, AllocatorT>* d_list;
- const elt_t* d_current;
- friend class CDCircList<T, AllocatorT>;
- public:
- iterator(const CDCircList<T, AllocatorT>* 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<T, AllocatorT>&) CVC4_UNUSED;
- CDCircList<T, AllocatorT>& operator=(const CDCircList<T, AllocatorT>&) 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 */
+++ /dev/null
-/********************* */
-/*! \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 <memory>
-
-namespace __gnu_cxx {
- template <class Key> struct hash;
-}/* __gnu_cxx namespace */
-
-namespace CVC4 {
- namespace context {
- template <class T>
- class ContextMemoryAllocator;
-
- template <class T, class Allocator = ContextMemoryAllocator<T> >
- class CDCircList;
- }/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H */
%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"
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 \
mkexpr \
expr_stream.i \
expr_manager.i \
- declaration_scope.i \
+ symbol_table.i \
command.i \
type.i \
kind.i \
* 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<uint64_t, NodeValue*>& 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 */
class AttrHash :
public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
value_type,
- AttrHashStrategy> {
+ AttrHashFunction> {
};/* class AttrHash<> */
/**
class AttrHash<bool> :
protected __gnu_cxx::hash_map<NodeValue*,
uint64_t,
- AttrHashBoolStrategy> {
+ AttrBoolHashFunction> {
/** A "super" type, like in Java, for easy reference below. */
- typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+ typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
/**
* BitAccessor allows us to return a bit "by reference." Of course,
class CDAttrHash :
public context::CDHashMap<std::pair<uint64_t, NodeValue*>,
value_type,
- AttrHashStrategy> {
+ AttrHashFunction> {
public:
CDAttrHash(context::Context* ctxt) :
context::CDHashMap<std::pair<uint64_t, NodeValue*>,
value_type,
- AttrHashStrategy>(ctxt) {
+ AttrHashFunction>(ctxt) {
}
};/* class CDAttrHash<> */
class CDAttrHash<bool> :
protected context::CDHashMap<NodeValue*,
uint64_t,
- AttrHashBoolStrategy> {
+ AttrBoolHashFunction> {
/** A "super" type, like in Java, for easy reference below. */
- typedef context::CDHashMap<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+ typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> super;
/**
* BitAccessor allows us to return a bit "by reference." Of course,
+++ /dev/null
-/********************* */
-/*! \file declaration_scope.cpp
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, ajreynol
- ** 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 Convenience class for scoping variable and type
- ** declarations (implementation).
- **
- ** Convenience class for scoping variable and type declarations
- ** (implementation).
- **/
-
-#include "expr/declaration_scope.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/expr_manager_scope.h"
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "context/context.h"
-
-#include <string>
-#include <utility>
-
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace std;
-
-namespace CVC4 {
-
-DeclarationScope::DeclarationScope() :
- d_context(new Context),
- d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
- d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
- d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
-}
-
-DeclarationScope::~DeclarationScope() {
- d_exprMap->deleteSelf();
- d_typeMap->deleteSelf();
- d_functions->deleteSelf();
- delete d_context;
-}
-
-void DeclarationScope::bind(const std::string& name, Expr obj,
- bool levelZero) throw(AssertionException) {
- CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
- ExprManagerScope ems(obj);
- if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
- else d_exprMap->insert(name, obj);
-}
-
-void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj,
- bool levelZero) throw(AssertionException) {
- CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
- ExprManagerScope ems(obj);
- if(levelZero){
- d_exprMap->insertAtContextLevelZero(name, obj);
- d_functions->insertAtContextLevelZero(obj);
- } else {
- d_exprMap->insert(name, obj);
- d_functions->insert(obj);
- }
-}
-
-bool DeclarationScope::isBound(const std::string& name) const throw() {
- return d_exprMap->find(name) != d_exprMap->end();
-}
-
-bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() {
- CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
- d_exprMap->find(name);
- return found != d_exprMap->end() && d_functions->contains((*found).second);
-}
-
-bool DeclarationScope::isBoundDefinedFunction(Expr func) const throw() {
- return d_functions->contains(func);
-}
-
-Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) {
- return (*d_exprMap->find(name)).second;
-}
-
-void DeclarationScope::bindType(const std::string& name, Type t,
- bool levelZero) throw() {
- if(levelZero){
- d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
- }else{
- d_typeMap->insert(name, make_pair(vector<Type>(), t));
- }
-}
-
-void DeclarationScope::bindType(const std::string& name,
- const std::vector<Type>& params,
- Type t,
- bool levelZero) throw() {
- if(Debug.isOn("sort")) {
- Debug("sort") << "bindType(" << name << ", [";
- if(params.size() > 0) {
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(Debug("sort"), ", ") );
- Debug("sort") << params.back();
- }
- Debug("sort") << "], " << t << ")" << endl;
- }
- if(levelZero){
- d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
- } else {
- d_typeMap->insert(name, make_pair(params, t));
- }
-}
-
-bool DeclarationScope::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) {
- pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
- Assert(p.first.size() == 0,
- "type constructor arity is wrong: "
- "`%s' requires %u parameters but was provided 0",
- name.c_str(), p.first.size());
- return p.second;
-}
-
-Type DeclarationScope::lookupType(const std::string& name,
- const std::vector<Type>& params) const throw(AssertionException) {
- pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
- Assert(p.first.size() == params.size(),
- "type constructor arity is wrong: "
- "`%s' requires %u parameters but was provided %u",
- name.c_str(), p.first.size(), params.size());
- if(p.first.size() == 0) {
- Assert(p.second.isSort());
- return p.second;
- }
- if(p.second.isSortConstructor()) {
- if(Debug.isOn("sort")) {
- Debug("sort") << "instantiating using a sort constructor" << endl;
- Debug("sort") << "have formals [";
- copy( p.first.begin(), p.first.end() - 1,
- ostream_iterator<Type>(Debug("sort"), ", ") );
- Debug("sort") << p.first.back() << "]" << endl
- << "parameters [";
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(Debug("sort"), ", ") );
- Debug("sort") << params.back() << "]" << endl
- << "type ctor " << name << endl
- << "type is " << p.second << endl;
- }
-
- Type instantiation =
- SortConstructorType(p.second).instantiate(params);
-
- Debug("sort") << "instance is " << instantiation << endl;
-
- return instantiation;
- } else if(p.second.isDatatype()) {
- Assert( DatatypeType(p.second).isParametric() );
- return DatatypeType(p.second).instantiate(params);
- } else {
- if(Debug.isOn("sort")) {
- Debug("sort") << "instantiating using a sort substitution" << endl;
- Debug("sort") << "have formals [";
- copy( p.first.begin(), p.first.end() - 1,
- ostream_iterator<Type>(Debug("sort"), ", ") );
- Debug("sort") << p.first.back() << "]" << endl
- << "parameters [";
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(Debug("sort"), ", ") );
- Debug("sort") << params.back() << "]" << endl
- << "type ctor " << name << endl
- << "type is " << p.second << endl;
- }
-
- Type instantiation = p.second.substitute(p.first, params);
-
- Debug("sort") << "instance is " << instantiation << endl;
-
- return instantiation;
- }
-}
-
-size_t DeclarationScope::lookupArity(const std::string& name) {
- pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
- return p.first.size();
-}
-
-void DeclarationScope::popScope() throw(ScopeException) {
- if( d_context->getLevel() == 0 ) {
- throw ScopeException();
- }
- d_context->pop();
-}
-
-void DeclarationScope::pushScope() throw() {
- d_context->push();
-}
-
-size_t DeclarationScope::getLevel() const throw() {
- return d_context->getLevel();
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file declaration_scope.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): ajreynol
- ** 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 Convenience class for scoping variable and type declarations.
- **
- ** Convenience class for scoping variable and type declarations.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__DECLARATION_SCOPE_H
-#define __CVC4__DECLARATION_SCOPE_H
-
-#include <vector>
-#include <utility>
-#include <ext/hash_map>
-
-#include "expr/expr.h"
-#include "util/hash.h"
-
-#include "context/cdhashset_forward.h"
-#include "context/cdhashmap_forward.h"
-
-namespace CVC4 {
-
-class Type;
-
-namespace context {
- class Context;
-}/* CVC4::context namespace */
-
-class CVC4_PUBLIC ScopeException : public Exception {
-};/* class ScopeException */
-
-/**
- * A convenience class for handling scoped declarations. Implements the usual
- * nested scoping rules for declarations, with separate bindings for expressions
- * and types.
- */
-class CVC4_PUBLIC DeclarationScope {
- /** The context manager for the scope maps. */
- context::Context* d_context;
-
- /** A map for expressions. */
- context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
-
- /** A map for types. */
- context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
-
- /** A set of defined functions. */
- context::CDHashSet<Expr, ExprHashFunction> *d_functions;
-
-public:
- /** Create a declaration scope. */
- DeclarationScope();
-
- /** Destroy a declaration scope. */
- ~DeclarationScope();
-
- /**
- * Bind an expression to a name in the current scope level. If
- * <code>name</code> is already bound to an expression in the current
- * level, then the binding is replaced. If <code>name</code> is bound
- * in a previous level, then the binding is "covered" by this one
- * until the current scope is popped. If levelZero is true the name
- * shouldn't be already bound.
- *
- * @param name an identifier
- * @param obj the expression to bind to <code>name</code>
- * @param levelZero set if the binding must be done at level 0
- */
- void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
-
- /**
- * Bind a function body to a name in the current scope. If
- * <code>name</code> is already bound to an expression in the current
- * level, then the binding is replaced. If <code>name</code> is bound
- * in a previous level, then the binding is "covered" by this one
- * until the current scope is popped. Same as bind() but registers
- * this as a function (so that isBoundDefinedFunction() returns true).
- *
- * @param name an identifier
- * @param obj the expression to bind to <code>name</code>
- * @param levelZero set if the binding must be done at level 0
- */
- void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
-
- /**
- * Bind a type to a name in the current scope. If <code>name</code>
- * is already bound to a type in the current level, then the binding
- * is replaced. If <code>name</code> is bound in a previous level,
- * then the binding is "covered" by this one until the current scope
- * is popped.
- *
- * @param name an identifier
- * @param t the type to bind to <code>name</code>
- * @param levelZero set if the binding must be done at level 0
- */
- void bindType(const std::string& name, Type t, bool levelZero = false) throw();
-
- /**
- * Bind a type to a name in the current scope. If <code>name</code>
- * is already bound to a type or type constructor in the current
- * level, then the binding is replaced. If <code>name</code> is
- * bound in a previous level, then the binding is "covered" by this
- * one until the current scope is popped.
- *
- * @param name an identifier
- * @param params the parameters to the type
- * @param t the type to bind to <code>name</code>
- */
- void bindType(const std::string& name,
- const std::vector<Type>& params,
- Type t, bool levelZero = false) throw();
-
- /**
- * Check whether a name is bound to an expression with either bind()
- * or bindDefinedFunction().
- *
- * @param name the identifier to check.
- * @returns true iff name is bound in the current scope.
- */
- bool isBound(const std::string& name) const throw();
-
- /**
- * Check whether a name was bound to a function with bindDefinedFunction().
- */
- bool isBoundDefinedFunction(const std::string& name) const throw();
-
- /**
- * Check whether an Expr was bound to a function (i.e., was the
- * second arg to bindDefinedFunction()).
- */
- bool isBoundDefinedFunction(Expr func) const throw();
-
- /**
- * Check whether a name is bound to a type (or type constructor).
- *
- * @param name the identifier to check.
- * @returns true iff name is bound to a type in the current scope.
- */
- bool isBoundType(const std::string& name) const throw();
-
- /**
- * Lookup a bound expression.
- *
- * @param name the identifier to lookup
- * @returns the expression bound to <code>name</code> in the current scope.
- */
- Expr lookup(const std::string& name) const throw(AssertionException);
-
- /**
- * Lookup a bound type.
- *
- * @param name the type identifier to lookup
- * @returns the type bound to <code>name</code> in the current scope.
- */
- Type lookupType(const std::string& name) const throw(AssertionException);
-
- /**
- * Lookup a bound parameterized type.
- *
- * @param name the type-constructor identifier to lookup
- * @param params the types to use to parameterize the type
- * @returns the type bound to <code>name(<i>params</i>)</code> in
- * the current scope.
- */
- Type lookupType(const std::string& name,
- const std::vector<Type>& params) const throw(AssertionException);
-
- /**
- * Lookup the arity of a bound parameterized type.
- */
- size_t lookupArity(const std::string& name);
-
- /**
- * Pop a scope level. Deletes all bindings since the last call to
- * <code>pushScope</code>. Calls to <code>pushScope</code> and
- * <code>popScope</code> must be "properly nested." I.e., a call to
- * <code>popScope</code> is only legal if the number of prior calls to
- * <code>pushScope</code> on this <code>DeclarationScope</code> is strictly
- * greater than then number of prior calls to <code>popScope</code>. */
- void popScope() throw(ScopeException);
-
- /** Push a scope level. */
- void pushScope() throw();
-
- /** Get the current level of this declaration scope. */
- size_t getLevel() const throw();
-
-};/* class DeclarationScope */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__DECLARATION_SCOPE_H */
+++ /dev/null
-%{
-#include "expr/declaration_scope.h"
-%}
-
-%include "expr/declaration_scope.h"
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 */
/**
* 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) {
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
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:
};
typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValuePoolHashFcn,
+ expr::NodeValuePoolHashFunction,
expr::NodeValuePoolEq> NodeValuePool;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueIDHashFunction,
* 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.
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);
--- /dev/null
+/********************* */
+/*! \file symbol_table.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: bobot, mdeters
+ ** Minor contributors (to current version): ajreynol, dejan
+ ** This file is part of the CVC4 prototype.
+ ** 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)
+ **
+ ** Convenience class for scoping variable and type declarations
+ ** (implementation).
+ **/
+
+#include "expr/symbol_table.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "expr/expr_manager_scope.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/context.h"
+
+#include <string>
+#include <utility>
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
+
+namespace CVC4 {
+
+SymbolTable::SymbolTable() :
+ d_context(new Context),
+ d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
+ d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
+ d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
+}
+
+SymbolTable::~SymbolTable() {
+ d_exprMap->deleteSelf();
+ d_typeMap->deleteSelf();
+ d_functions->deleteSelf();
+ delete d_context;
+}
+
+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);
+ if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
+ else d_exprMap->insert(name, 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);
+ if(levelZero){
+ d_exprMap->insertAtContextLevelZero(name, obj);
+ d_functions->insertAtContextLevelZero(obj);
+ } else {
+ d_exprMap->insert(name, obj);
+ d_functions->insert(obj);
+ }
+}
+
+bool SymbolTable::isBound(const std::string& name) const throw() {
+ return d_exprMap->find(name) != d_exprMap->end();
+}
+
+bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() {
+ CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
+ d_exprMap->find(name);
+ return found != d_exprMap->end() && d_functions->contains((*found).second);
+}
+
+bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
+ return d_functions->contains(func);
+}
+
+Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) {
+ return (*d_exprMap->find(name)).second;
+}
+
+void SymbolTable::bindType(const std::string& name, Type t,
+ bool levelZero) throw() {
+ if(levelZero){
+ d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
+ }else{
+ d_typeMap->insert(name, make_pair(vector<Type>(), t));
+ }
+}
+
+void SymbolTable::bindType(const std::string& name,
+ const std::vector<Type>& params,
+ Type t,
+ bool levelZero) throw() {
+ if(Debug.isOn("sort")) {
+ Debug("sort") << "bindType(" << name << ", [";
+ if(params.size() > 0) {
+ copy( params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << params.back();
+ }
+ Debug("sort") << "], " << t << ")" << endl;
+ }
+ if(levelZero){
+ d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
+ } else {
+ d_typeMap->insert(name, make_pair(params, t));
+ }
+}
+
+bool SymbolTable::isBoundType(const std::string& name) const throw() {
+ return d_typeMap->find(name) != d_typeMap->end();
+}
+
+Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) {
+ pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+ Assert(p.first.size() == 0,
+ "type constructor arity is wrong: "
+ "`%s' requires %u parameters but was provided 0",
+ name.c_str(), p.first.size());
+ return p.second;
+}
+
+Type SymbolTable::lookupType(const std::string& name,
+ const std::vector<Type>& params) const throw(AssertionException) {
+ pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+ Assert(p.first.size() == params.size(),
+ "type constructor arity is wrong: "
+ "`%s' requires %u parameters but was provided %u",
+ name.c_str(), p.first.size(), params.size());
+ if(p.first.size() == 0) {
+ Assert(p.second.isSort());
+ return p.second;
+ }
+ if(p.second.isSortConstructor()) {
+ if(Debug.isOn("sort")) {
+ Debug("sort") << "instantiating using a sort constructor" << endl;
+ Debug("sort") << "have formals [";
+ copy( p.first.begin(), p.first.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << p.first.back() << "]" << endl
+ << "parameters [";
+ copy( params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << params.back() << "]" << endl
+ << "type ctor " << name << endl
+ << "type is " << p.second << endl;
+ }
+
+ Type instantiation =
+ SortConstructorType(p.second).instantiate(params);
+
+ Debug("sort") << "instance is " << instantiation << endl;
+
+ return instantiation;
+ } else if(p.second.isDatatype()) {
+ Assert( DatatypeType(p.second).isParametric() );
+ return DatatypeType(p.second).instantiate(params);
+ } else {
+ if(Debug.isOn("sort")) {
+ Debug("sort") << "instantiating using a sort substitution" << endl;
+ Debug("sort") << "have formals [";
+ copy( p.first.begin(), p.first.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << p.first.back() << "]" << endl
+ << "parameters [";
+ copy( params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << params.back() << "]" << endl
+ << "type ctor " << name << endl
+ << "type is " << p.second << endl;
+ }
+
+ Type instantiation = p.second.substitute(p.first, params);
+
+ Debug("sort") << "instance is " << instantiation << endl;
+
+ return instantiation;
+ }
+}
+
+size_t SymbolTable::lookupArity(const std::string& name) {
+ pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+ return p.first.size();
+}
+
+void SymbolTable::popScope() throw(ScopeException) {
+ if( d_context->getLevel() == 0 ) {
+ throw ScopeException();
+ }
+ d_context->pop();
+}
+
+void SymbolTable::pushScope() throw() {
+ d_context->push();
+}
+
+size_t SymbolTable::getLevel() const throw() {
+ return d_context->getLevel();
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file symbol_table.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): ajreynol, dejan, bobot
+ ** This file is part of the CVC4 prototype.
+ ** 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.
+ **
+ ** Convenience class for scoping variable and type declarations.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SYMBOL_TABLE_H
+#define __CVC4__SYMBOL_TABLE_H
+
+#include <vector>
+#include <utility>
+#include <ext/hash_map>
+
+#include "expr/expr.h"
+#include "util/hash.h"
+
+#include "context/cdhashset_forward.h"
+#include "context/cdhashmap_forward.h"
+
+namespace CVC4 {
+
+class Type;
+
+namespace context {
+ class Context;
+}/* CVC4::context namespace */
+
+class CVC4_PUBLIC ScopeException : public Exception {
+};/* class ScopeException */
+
+/**
+ * A convenience class for handling scoped declarations. Implements the usual
+ * nested scoping rules for declarations, with separate bindings for expressions
+ * and types.
+ */
+class CVC4_PUBLIC SymbolTable {
+ /** The context manager for the scope maps. */
+ context::Context* d_context;
+
+ /** A map for expressions. */
+ context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
+
+ /** A map for types. */
+ context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+
+ /** A set of defined functions. */
+ context::CDHashSet<Expr, ExprHashFunction> *d_functions;
+
+public:
+ /** Create a declaration scope. */
+ SymbolTable();
+
+ /** Destroy a declaration scope. */
+ ~SymbolTable();
+
+ /**
+ * Bind an expression to a name in the current scope level. If
+ * <code>name</code> is already bound to an expression in the current
+ * level, then the binding is replaced. If <code>name</code> is bound
+ * in a previous level, then the binding is "covered" by this one
+ * until the current scope is popped. If levelZero is true the name
+ * shouldn't be already bound.
+ *
+ * @param name an identifier
+ * @param obj the expression to bind to <code>name</code>
+ * @param levelZero set if the binding must be done at level 0
+ */
+ void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+
+ /**
+ * Bind a function body to a name in the current scope. If
+ * <code>name</code> is already bound to an expression in the current
+ * level, then the binding is replaced. If <code>name</code> is bound
+ * in a previous level, then the binding is "covered" by this one
+ * until the current scope is popped. Same as bind() but registers
+ * this as a function (so that isBoundDefinedFunction() returns true).
+ *
+ * @param name an identifier
+ * @param obj the expression to bind to <code>name</code>
+ * @param levelZero set if the binding must be done at level 0
+ */
+ void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type in the current level, then the binding
+ * is replaced. If <code>name</code> is bound in a previous level,
+ * then the binding is "covered" by this one until the current scope
+ * is popped.
+ *
+ * @param name an identifier
+ * @param t the type to bind to <code>name</code>
+ * @param levelZero set if the binding must be done at level 0
+ */
+ void bindType(const std::string& name, Type t, bool levelZero = false) throw();
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type or type constructor in the current
+ * level, then the binding is replaced. If <code>name</code> is
+ * bound in a previous level, then the binding is "covered" by this
+ * one until the current scope is popped.
+ *
+ * @param name an identifier
+ * @param params the parameters to the type
+ * @param t the type to bind to <code>name</code>
+ */
+ void bindType(const std::string& name,
+ const std::vector<Type>& params,
+ Type t, bool levelZero = false) throw();
+
+ /**
+ * Check whether a name is bound to an expression with either bind()
+ * or bindDefinedFunction().
+ *
+ * @param name the identifier to check.
+ * @returns true iff name is bound in the current scope.
+ */
+ bool isBound(const std::string& name) const throw();
+
+ /**
+ * Check whether a name was bound to a function with bindDefinedFunction().
+ */
+ bool isBoundDefinedFunction(const std::string& name) const throw();
+
+ /**
+ * Check whether an Expr was bound to a function (i.e., was the
+ * second arg to bindDefinedFunction()).
+ */
+ bool isBoundDefinedFunction(Expr func) const throw();
+
+ /**
+ * Check whether a name is bound to a type (or type constructor).
+ *
+ * @param name the identifier to check.
+ * @returns true iff name is bound to a type in the current scope.
+ */
+ bool isBoundType(const std::string& name) const throw();
+
+ /**
+ * Lookup a bound expression.
+ *
+ * @param name the identifier to lookup
+ * @returns the expression bound to <code>name</code> in the current scope.
+ */
+ Expr lookup(const std::string& name) const throw(AssertionException);
+
+ /**
+ * Lookup a bound type.
+ *
+ * @param name the type identifier to lookup
+ * @returns the type bound to <code>name</code> in the current scope.
+ */
+ Type lookupType(const std::string& name) const throw(AssertionException);
+
+ /**
+ * Lookup a bound parameterized type.
+ *
+ * @param name the type-constructor identifier to lookup
+ * @param params the types to use to parameterize the type
+ * @returns the type bound to <code>name(<i>params</i>)</code> in
+ * the current scope.
+ */
+ Type lookupType(const std::string& name,
+ const std::vector<Type>& params) const throw(AssertionException);
+
+ /**
+ * Lookup the arity of a bound parameterized type.
+ */
+ size_t lookupArity(const std::string& name);
+
+ /**
+ * Pop a scope level. Deletes all bindings since the last call to
+ * <code>pushScope</code>. Calls to <code>pushScope</code> and
+ * <code>popScope</code> must be "properly nested." I.e., a call to
+ * <code>popScope</code> is only legal if the number of prior calls to
+ * <code>pushScope</code> on this <code>SymbolTable</code> is strictly
+ * greater than then number of prior calls to <code>popScope</code>. */
+ void popScope() throw(ScopeException);
+
+ /** Push a scope level. */
+ void pushScope() throw();
+
+ /** Get the current level of this declaration scope. */
+ size_t getLevel() const throw();
+
+};/* class SymbolTable */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SYMBOL_TABLE_H */
--- /dev/null
+%{
+#include "expr/symbol_table.h"
+%}
+
+%include "expr/symbol_table.h"
std::string id;
std::vector<Type> types;
std::vector< std::pair<std::string, Type> > typeIds;
- DeclarationScope* declScope;
+ //SymbolTable* symtab;
Parser* parser;
lhs = false;
}
* 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) :
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),
switch( type ) {
case SYM_VARIABLE: // Functions share var namespace
- return d_declScope->lookup(name);
+ return d_symtab->lookup(name);
default:
Unhandled(type);
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;
}
const std::vector<Type>& 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. */
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. */
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) );
}
Parser::defineType(const std::string& name,
const std::vector<Type>& params,
const Type& type) {
- d_declScope->bindType(name, params, type);
+ d_symtab->bindType(name, params, type);
Assert( isDeclared(name, SYM_SORT) );
}
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);
}
#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"
* 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;
}
}
- 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.
*/
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();
}
/**
constant SUBRANGE_TYPE \
::CVC4::SubrangeBounds \
- ::CVC4::SubrangeBoundsHashStrategy \
+ ::CVC4::SubrangeBoundsHashFunction \
"util/subrange_bound.h" \
"the type of an integer subrange"
cardinality SUBRANGE_TYPE \
constant CONST_RATIONAL \
::CVC4::Rational \
- ::CVC4::RationalHashStrategy \
+ ::CVC4::RationalHashFunction \
"util/rational.h" \
"a multiple-precision rational constant"
/*! \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
**
** \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"
typedef quad<TNode, TNode, TNode, TNode> 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;
indices = new(true)CTNodeList(c);
stores = new(true)CTNodeList(c);
in_stores = new(true)CTNodeList(c);
-
}
~Info() {
Trace("arrays-info")<<" in_stores ";
printList(in_stores);
}
-};
+};/* class Info */
typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
StatisticsRegistry::registerStat(&d_tableSize);
}
- ~ArrayInfo(){
+ ~ArrayInfo() {
CNodeInfoMap::iterator it = info_map.begin();
for( ; it != info_map.end(); it++ ) {
if((*it).second!= emptyInfo) {
* 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 */
# 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"
constant CONST_BOOLEAN \
bool \
- ::CVC4::BoolHashStrategy \
+ ::CVC4::BoolHashFunction \
"util/bool.h" \
"truth and falsity"
# 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
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
# 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"
constant TYPE_CONSTANT \
::CVC4::TypeConstant \
- ::CVC4::TypeConstantHashStrategy \
+ ::CVC4::TypeConstantHashFunction \
"expr/kind.h" \
"basic types"
operator FUNCTION_TYPE 2: "function 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
constant SUBTYPE_TYPE \
::CVC4::Predicate \
- ::CVC4::PredicateHashStrategy \
+ ::CVC4::PredicateHashFunction \
"util/predicate.h" \
"predicate subtype"
cardinality SUBTYPE_TYPE \
constant BITVECTOR_TYPE \
::CVC4::BitVectorSize \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \
"util/bitvector.h" \
"bit-vector type"
cardinality BITVECTOR_TYPE \
constant CONST_BITVECTOR \
::CVC4::BitVector \
- ::CVC4::BitVectorHashStrategy \
+ ::CVC4::BitVectorHashFunction \
"util/bitvector.h" \
"a fixed-width bit-vector constant"
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"
constant DATATYPE_TYPE \
::CVC4::Datatype \
- "::CVC4::DatatypeHashStrategy" \
+ "::CVC4::DatatypeHashFunction" \
"util/datatype.h" \
"datatype type"
cardinality DATATYPE_TYPE \
"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"
hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
return hash;
}
- };
+ };/* struct ITESimplifier::NodePairHashFunction */
typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
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 */
/**
* 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) {
/**
* 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
/**
* 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 */
/**
/**
* 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 */
};/* struct BitVectorRotateRight */
template <typename T>
-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) {
return os << "[" << bv.bitIndex << "]";
}
-
-
}/* CVC4 namespace */
#endif /* __CVC4__BITVECTOR_H */
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 */
};/* 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.
}
};/* struct StringHashFunction */
-struct StringHashStrategy {
- static size_t hash(const std::string& str) {
- return std::hash<const char*>()(str.c_str());
- }
-};/* struct StringHashStrategy */
-
}/* CVC4 namespace */
#endif /* __CVC4__HASH_H */
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();
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();
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);
}
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 */
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 */
};/* 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);
};/* 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);
};/* 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<size_t>::max();
size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::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;
/**
* 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 */
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 \
context/cdo_black \
context/cdlist_black \
context/cdlist_context_memory_black \
- context/cdcirclist_white \
context/cdmap_black \
context/cdmap_white \
context/cdvector_black \
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-
-#include <vector>
-#include <iostream>
-
-#include <limits.h>
-
-#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<int> l(d_context, ContextMemoryAllocator<int>(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<int> l2(d_context, ContextMemoryAllocator<int>(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<int>::iterator i = l.begin();
- CDCircList<int>::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<int>::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<int>::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<int> 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 */
+++ /dev/null
-/********************* */
-/*! \file declaration_scope_black.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, dejan
- ** 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 Black box testing of CVC4::DeclarationScope.
- **
- ** Black box testing of CVC4::DeclarationScope.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <sstream>
-#include <string>
-
-#include "context/context.h"
-#include "expr/declaration_scope.h"
-#include "expr/expr_manager.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "util/Assert.h"
-#include "util/exception.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace std;
-
-class DeclarationScopeBlack : public CxxTest::TestSuite {
-private:
-
- ExprManager* d_exprManager;
-
-public:
-
- void setUp() {
- try {
- d_exprManager = new ExprManager;
- } catch(Exception e) {
- cerr << "Exception during setUp():" << endl << e;
- throw;
- }
- }
-
- void tearDown() {
- try {
- delete d_exprManager;
- } catch(Exception e) {
- cerr << "Exception during tearDown():" << endl << e;
- throw;
- }
- }
-
- void testBind() {
- DeclarationScope declScope;
- 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 );
- }
-
- void testBind2() {
- DeclarationScope declScope;
- 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 );
- }
-
- void testBind3() {
- DeclarationScope declScope;
- Type booleanType = d_exprManager->booleanType();
- Expr x = d_exprManager->mkVar(booleanType);
- declScope.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 );
- }
-
- void testBind4() {
- DeclarationScope declScope;
- Type booleanType = d_exprManager->booleanType();
- Expr x = d_exprManager->mkVar(booleanType);
- declScope.bind("x",x);
-
- Type t = d_exprManager->mkSort("T");
- // duplicate binding for type is OK
- declScope.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 );
- }
-
- void testBindType() {
- DeclarationScope declScope;
- Type s = d_exprManager->mkSort("S");
- declScope.bindType("S",s);
- TS_ASSERT( declScope.isBoundType("S") );
- TS_ASSERT_EQUALS( declScope.lookupType("S"), s );
- }
-
- void testBindType2() {
- DeclarationScope declScope;
- // 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 );
- }
-
- void testBindType3() {
- DeclarationScope declScope;
- Type s = d_exprManager->mkSort("S");
- declScope.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 );
- }
-
- void testPushScope() {
- DeclarationScope declScope;
- Type booleanType = d_exprManager->booleanType();
- Expr x = d_exprManager->mkVar(booleanType);
- declScope.bind("x",x);
- declScope.pushScope();
-
- TS_ASSERT( declScope.isBound("x") );
- TS_ASSERT_EQUALS( declScope.lookup("x"), x );
-
- Expr y = d_exprManager->mkVar(booleanType);
- declScope.bind("x",y);
-
- TS_ASSERT( declScope.isBound("x") );
- TS_ASSERT_EQUALS( declScope.lookup("x"), y );
-
- declScope.popScope();
- TS_ASSERT( declScope.isBound("x") );
- TS_ASSERT_EQUALS( declScope.lookup("x"), x );
- }
-
- void testBadPop() {
- DeclarationScope declScope;
- // TODO: What kind of exception gets thrown here?
- TS_ASSERT_THROWS( declScope.popScope(), ScopeException );
- }
-};
--- /dev/null
+/********************* */
+/*! \file symbol_table_black.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters, dejan
+ ** 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 Black box testing of CVC4::SymbolTable
+ **
+ ** Black box testing of CVC4::SymbolTable.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <sstream>
+#include <string>
+
+#include "context/context.h"
+#include "expr/symbol_table.h"
+#include "expr/expr_manager.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "util/Assert.h"
+#include "util/exception.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace std;
+
+class SymbolTableBlack : public CxxTest::TestSuite {
+private:
+
+ ExprManager* d_exprManager;
+
+public:
+
+ void setUp() {
+ try {
+ d_exprManager = new ExprManager;
+ } catch(Exception e) {
+ cerr << "Exception during setUp():" << endl << e;
+ throw;
+ }
+ }
+
+ void tearDown() {
+ try {
+ delete d_exprManager;
+ } catch(Exception e) {
+ cerr << "Exception during tearDown():" << endl << e;
+ throw;
+ }
+ }
+
+ void testBind() {
+ SymbolTable symtab;
+ Type booleanType = d_exprManager->booleanType();
+ Expr x = d_exprManager->mkVar(booleanType);
+ symtab.bind("x",x);
+ TS_ASSERT( symtab.isBound("x") );
+ TS_ASSERT_EQUALS( symtab.lookup("x"), x );
+ }
+
+ void testBind2() {
+ SymbolTable symtab;
+ Type booleanType = d_exprManager->booleanType();
+ // var name attribute shouldn't matter
+ Expr y = d_exprManager->mkVar("y", booleanType);
+ symtab.bind("x",y);
+ TS_ASSERT( symtab.isBound("x") );
+ TS_ASSERT_EQUALS( symtab.lookup("x"), y );
+ }
+
+ void testBind3() {
+ SymbolTable symtab;
+ Type booleanType = d_exprManager->booleanType();
+ Expr x = d_exprManager->mkVar(booleanType);
+ symtab.bind("x",x);
+ Expr y = d_exprManager->mkVar(booleanType);
+ // new binding covers old
+ symtab.bind("x",y);
+ TS_ASSERT( symtab.isBound("x") );
+ TS_ASSERT_EQUALS( symtab.lookup("x"), y );
+ }
+
+ void testBind4() {
+ SymbolTable symtab;
+ Type booleanType = d_exprManager->booleanType();
+ Expr x = d_exprManager->mkVar(booleanType);
+ symtab.bind("x",x);
+
+ Type t = d_exprManager->mkSort("T");
+ // duplicate binding for type is OK
+ symtab.bindType("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() {
+ SymbolTable symtab;
+ Type s = d_exprManager->mkSort("S");
+ symtab.bindType("S",s);
+ TS_ASSERT( symtab.isBoundType("S") );
+ TS_ASSERT_EQUALS( symtab.lookupType("S"), s );
+ }
+
+ void testBindType2() {
+ SymbolTable symtab;
+ // type name attribute shouldn't matter
+ Type s = d_exprManager->mkSort("S");
+ symtab.bindType("T",s);
+ TS_ASSERT( symtab.isBoundType("T") );
+ TS_ASSERT_EQUALS( symtab.lookupType("T"), s );
+ }
+
+ void testBindType3() {
+ SymbolTable symtab;
+ Type s = d_exprManager->mkSort("S");
+ symtab.bindType("S",s);
+ Type t = d_exprManager->mkSort("T");
+ // new binding covers old
+ symtab.bindType("S",t);
+ TS_ASSERT( symtab.isBoundType("S") );
+ TS_ASSERT_EQUALS( symtab.lookupType("S"), t );
+ }
+
+ void testPushScope() {
+ SymbolTable symtab;
+ Type booleanType = d_exprManager->booleanType();
+ Expr x = d_exprManager->mkVar(booleanType);
+ symtab.bind("x",x);
+ symtab.pushScope();
+
+ TS_ASSERT( symtab.isBound("x") );
+ TS_ASSERT_EQUALS( symtab.lookup("x"), x );
+
+ Expr y = d_exprManager->mkVar(booleanType);
+ symtab.bind("x",y);
+
+ TS_ASSERT( symtab.isBound("x") );
+ TS_ASSERT_EQUALS( symtab.lookup("x"), y );
+
+ symtab.popScope();
+ TS_ASSERT( symtab.isBound("x") );
+ TS_ASSERT_EQUALS( symtab.lookup("x"), x );
+ }
+
+ void testBadPop() {
+ SymbolTable symtab;
+ // TODO: What kind of exception gets thrown here?
+ TS_ASSERT_THROWS( symtab.popScope(), ScopeException );
+ }
+};/* class SymbolTableBlack */
projects / cvc5.git / commitdiff