diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-07 18:38:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-07 18:38:49 +0000 |
commit | b0deae79d8bae5051a85dc15e43e7b83bc8cf9ab (patch) | |
tree | d73fa7f9fb37077853f824dcecd2a1b8e4d22837 /src/expr | |
parent | ea5acaba821790dd240db779f2340fbe5fce0b8e (diff) |
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)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 6 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 22 | ||||
-rw-r--r-- | src/expr/declaration_scope.i | 5 | ||||
-rw-r--r-- | src/expr/kind_template.h | 14 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 | ||||
-rw-r--r-- | src/expr/node_value.h | 6 | ||||
-rw-r--r-- | src/expr/symbol_table.cpp (renamed from src/expr/declaration_scope.cpp) | 46 | ||||
-rw-r--r-- | src/expr/symbol_table.h (renamed from src/expr/declaration_scope.h) | 22 | ||||
-rw-r--r-- | src/expr/symbol_table.i | 5 |
10 files changed, 67 insertions, 65 deletions
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<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 */ @@ -156,7 +156,7 @@ template <class value_type> class AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, value_type, - AttrHashStrategy> { + AttrHashFunction> { };/* class AttrHash<> */ /** @@ -167,10 +167,10 @@ template <> 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, @@ -367,12 +367,12 @@ template <class value_type> 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<> */ @@ -384,10 +384,10 @@ template <> 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, 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<expr::NodeValue*, - expr::NodeValuePoolHashFcn, + expr::NodeValuePoolHashFunction, expr::NodeValuePoolEq> NodeValuePool; typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueIDHashFunction, diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 657fabeb5..ae3c6beda 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -358,11 +358,11 @@ operator+(NodeValue::iterator<NodeTemplate<false> >::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 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<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() { +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<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() { +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<Type>(), 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<Type>& 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<vector<Type>, 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<Type>& params) const throw(AssertionException) { pair<vector<Type>, 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<vector<Type>, 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 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 <vector> #include <utility> @@ -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: * <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 + * <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); @@ -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" |