#include <ostream>
#include <string>
-#include <utility>
#include <unordered_map>
+#include <utility>
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
// This data structure stores a trie of expressions with
// the same name, and must be distinguished by their argument types.
// It is context-dependent.
-class OverloadedTypeTrie
-{
-public:
- OverloadedTypeTrie(Context * c ) :
- d_overloaded_symbols(new (true) CDHashSet<Expr, ExprHashFunction>(c)) {
- }
- ~OverloadedTypeTrie() {
- d_overloaded_symbols->deleteSelf();
- }
+class OverloadedTypeTrie {
+ public:
+ OverloadedTypeTrie(Context* c)
+ : d_overloaded_symbols(new (true) CDHashSet<Expr, ExprHashFunction>(c)) {}
+ ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
+
/** is this function overloaded? */
bool isOverloadedFunction(Expr fun) const;
-
+
/** Get overloaded constant for type.
* If possible, it returns a defined symbol with name
* that has type t. Otherwise returns null expression.
- */
+ */
Expr getOverloadedConstantForType(const std::string& name, Type t) const;
-
+
/**
* If possible, returns a defined function for a name
* and a vector of expected argument types. Otherwise returns
* null expression.
*/
- Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const;
- /** called when obj is bound to name, and prev_bound_obj was already bound to name
- * Returns false if the binding is invalid.
- */
+ Expr getOverloadedFunctionForTypes(const std::string& name,
+ const std::vector<Type>& argTypes) const;
+ /** called when obj is bound to name, and prev_bound_obj was already bound to
+ * name Returns false if the binding is invalid.
+ */
bool bind(const string& name, Expr prev_bound_obj, Expr obj);
-private:
- /** Marks expression obj with name as overloaded.
+
+ private:
+ /** Marks expression obj with name as overloaded.
* Adds relevant information to the type arg trie data structure.
* It returns false if there is already an expression bound to that name
- * whose type expects the same arguments as the type of obj but is not identical
- * to the type of obj. For example, if we declare :
+ * whose type expects the same arguments as the type of obj but is not
+ * identical to the type of obj. For example, if we declare :
*
* (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
* (declare-fun cons (Int List) List)
*
* cons : constructor_type( Int, List, List )
* cons : function_type( Int, List, List )
- *
+ *
* These are put in the same place in the trie but do not have identical type,
* hence we return false.
- */
+ */
bool markOverloaded(const string& name, Expr obj);
/** the null expression */
Expr d_nullExpr;
// The (context-independent) trie storing that maps expected argument
- // vectors to symbols. All expressions stored in d_symbols are only
+ // vectors to symbols. All expressions stored in d_symbols are only
// interpreted as active if they also appear in the context-dependent
// set d_overloaded_symbols.
class TypeArgTrie {
- public:
+ public:
// children of this node
- std::map< Type, TypeArgTrie > d_children;
+ std::map<Type, TypeArgTrie> d_children;
// symbols at this node
- std::map< Type, Expr > d_symbols;
+ std::map<Type, Expr> d_symbols;
};
- /** for each string with operator overloading, this stores the data structure above. */
- std::unordered_map< std::string, TypeArgTrie > d_overload_type_arg_trie;
+ /** for each string with operator overloading, this stores the data structure
+ * above. */
+ std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
/** The set of overloaded symbols. */
CDHashSet<Expr, ExprHashFunction>* d_overloaded_symbols;
};
bool OverloadedTypeTrie::isOverloadedFunction(Expr fun) const {
- return d_overloaded_symbols->find(fun)!=d_overloaded_symbols->end();
+ return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
}
-Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name, Type t) const {
- std::unordered_map< std::string, TypeArgTrie >::const_iterator it = d_overload_type_arg_trie.find(name);
- if(it!=d_overload_type_arg_trie.end()) {
- std::map< Type, Expr >::const_iterator its = it->second.d_symbols.find(t);
- if(its!=it->second.d_symbols.end()) {
+Expr OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name,
+ Type t) const {
+ std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
+ d_overload_type_arg_trie.find(name);
+ if (it != d_overload_type_arg_trie.end()) {
+ std::map<Type, Expr>::const_iterator its = it->second.d_symbols.find(t);
+ if (its != it->second.d_symbols.end()) {
Expr expr = its->second;
// must be an active symbol
- if(isOverloadedFunction(expr)) {
+ if (isOverloadedFunction(expr)) {
return expr;
}
}
return d_nullExpr;
}
-Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(const std::string& name,
- const std::vector< Type >& argTypes) const {
- std::unordered_map< std::string, TypeArgTrie >::const_iterator it = d_overload_type_arg_trie.find(name);
- if(it!=d_overload_type_arg_trie.end()) {
- const TypeArgTrie * tat = &it->second;
- for(unsigned i=0; i<argTypes.size(); i++) {
- std::map< Type, TypeArgTrie >::const_iterator itc = tat->d_children.find(argTypes[i]);
- if(itc!=tat->d_children.end()) {
+Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<Type>& argTypes) const {
+ std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
+ d_overload_type_arg_trie.find(name);
+ if (it != d_overload_type_arg_trie.end()) {
+ const TypeArgTrie* tat = &it->second;
+ for (unsigned i = 0; i < argTypes.size(); i++) {
+ std::map<Type, TypeArgTrie>::const_iterator itc =
+ tat->d_children.find(argTypes[i]);
+ if (itc != tat->d_children.end()) {
tat = &itc->second;
- }else{
- // no functions match
+ } else {
+ // no functions match
return d_nullExpr;
}
}
// now, we must ensure that there is *only* one active symbol at this node
Expr retExpr;
- for(std::map< Type, Expr >::const_iterator its = tat->d_symbols.begin(); its != tat->d_symbols.end(); ++its) {
+ for (std::map<Type, Expr>::const_iterator its = tat->d_symbols.begin();
+ its != tat->d_symbols.end(); ++its) {
Expr expr = its->second;
- if(isOverloadedFunction(expr)) {
- if(retExpr.isNull()) {
+ if (isOverloadedFunction(expr)) {
+ if (retExpr.isNull()) {
retExpr = expr;
- }else{
+ } else {
// multiple functions match
return d_nullExpr;
}
return d_nullExpr;
}
-bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj, Expr obj) {
+bool OverloadedTypeTrie::bind(const string& name, Expr prev_bound_obj,
+ Expr obj) {
bool retprev = true;
- if(!isOverloadedFunction(prev_bound_obj)) {
+ if (!isOverloadedFunction(prev_bound_obj)) {
// mark previous as overloaded
retprev = markOverloaded(name, prev_bound_obj);
}
// get the argument types
Type t = obj.getType();
Type rangeType = t;
- std::vector< Type > argTypes;
- if(t.isFunction()) {
+ std::vector<Type> argTypes;
+ if (t.isFunction()) {
argTypes = static_cast<FunctionType>(t).getArgTypes();
rangeType = static_cast<FunctionType>(t).getRangeType();
- }else if(t.isConstructor()) {
+ } else if (t.isConstructor()) {
argTypes = static_cast<ConstructorType>(t).getArgTypes();
rangeType = static_cast<ConstructorType>(t).getRangeType();
- }else if(t.isTester()) {
- argTypes.push_back( static_cast<TesterType>(t).getDomain() );
+ } else if (t.isTester()) {
+ argTypes.push_back(static_cast<TesterType>(t).getDomain());
rangeType = static_cast<TesterType>(t).getRangeType();
- }else if(t.isSelector()) {
- argTypes.push_back( static_cast<SelectorType>(t).getDomain() );
+ } else if (t.isSelector()) {
+ argTypes.push_back(static_cast<SelectorType>(t).getDomain());
rangeType = static_cast<SelectorType>(t).getRangeType();
}
// add to the trie
- TypeArgTrie * tat = &d_overload_type_arg_trie[name];
- for(unsigned i=0; i<argTypes.size(); i++) {
+ TypeArgTrie* tat = &d_overload_type_arg_trie[name];
+ for (unsigned i = 0; i < argTypes.size(); i++) {
tat = &(tat->d_children[argTypes[i]]);
}
-
- // types can be identical but vary on the kind of the type, thus we must distinguish based on this
- std::map< Type, Expr >::iterator it = tat->d_symbols.find( rangeType );
- if( it!=tat->d_symbols.end() ){
+
+ // types can be identical but vary on the kind of the type, thus we must
+ // distinguish based on this
+ std::map<Type, Expr>::iterator it = tat->d_symbols.find(rangeType);
+ if (it != tat->d_symbols.end()) {
Expr prev_obj = it->second;
- // if there is already an active function with the same name and expects the same argument types
- if( isOverloadedFunction(prev_obj) ){
- if( prev_obj.getType()==obj.getType() ){
- //types are identical, simply ignore it
+ // if there is already an active function with the same name and expects the
+ // same argument types
+ if (isOverloadedFunction(prev_obj)) {
+ if (prev_obj.getType() == obj.getType()) {
+ // types are identical, simply ignore it
return true;
- }else{
- //otherwise there is no way to distinguish these types, we return an error
+ } else {
+ // otherwise there is no way to distinguish these types, we return an
+ // error
return false;
}
}
}
-
+
// otherwise, update the symbols
d_overloaded_symbols->insert(obj);
tat->d_symbols[rangeType] = obj;
return true;
}
-
class SymbolTable::Implementation {
public:
Implementation()
: d_context(),
d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
d_typeMap(new (true) TypeMap(&d_context)),
- d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)){
+ d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {
d_overload_trie = new OverloadedTypeTrie(&d_context);
}
delete d_overload_trie;
}
- bool bind(const string& name, Expr obj, bool levelZero, bool doOverload) throw();
- bool bindDefinedFunction(const string& name, Expr obj,
- bool levelZero, bool doOverload) throw();
- void bindType(const string& name, Type t, bool levelZero = false) throw();
+ bool bind(const string& name, Expr obj, bool levelZero, bool doOverload);
+ bool bindDefinedFunction(const string& name, Expr obj, bool levelZero,
+ bool doOverload);
+ void bindType(const string& name, Type t, bool levelZero = false);
void bindType(const string& name, const vector<Type>& params, Type t,
- bool levelZero = false) throw();
- bool isBound(const string& name) const throw();
- bool isBoundDefinedFunction(const string& name) const throw();
- bool isBoundDefinedFunction(Expr func) const throw();
- bool isBoundType(const string& name) const throw();
- Expr lookup(const string& name) const throw();
- Type lookupType(const string& name) const throw();
- Type lookupType(const string& name, const vector<Type>& params) const throw();
+ bool levelZero = false);
+ bool isBound(const string& name) const;
+ bool isBoundDefinedFunction(const string& name) const;
+ bool isBoundDefinedFunction(Expr func) const;
+ bool isBoundType(const string& name) const;
+ Expr lookup(const string& name) const;
+ Type lookupType(const string& name) const;
+ Type lookupType(const string& name, const vector<Type>& params) const;
size_t lookupArity(const string& name);
- void popScope() throw(ScopeException);
- void pushScope() throw();
- size_t getLevel() const throw();
+ void popScope();
+ void pushScope();
+ size_t getLevel() const;
void reset();
//------------------------ operator overloading
/** implementation of function from header */
bool isOverloadedFunction(Expr fun) const;
-
+
/** implementation of function from header */
Expr getOverloadedConstantForType(const std::string& name, Type t) const;
-
+
/** implementation of function from header */
- Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const;
+ Expr getOverloadedFunctionForTypes(const std::string& name,
+ const std::vector<Type>& argTypes) const;
//------------------------ end operator overloading
private:
/** The context manager for the scope maps. */
/** A set of defined functions. */
CDHashSet<Expr, ExprHashFunction>* d_functions;
-
+
//------------------------ operator overloading
// the null expression
Expr d_nullExpr;
// overloaded type trie, stores all information regarding overloading
- OverloadedTypeTrie * d_overload_trie;
+ OverloadedTypeTrie* d_overload_trie;
/** bind with overloading
- * This is called whenever obj is bound to name where overloading symbols is allowed.
- * If a symbol is previously bound to that name, it marks both as overloaded.
- * Returns false if the binding was invalid.
- */
+ * This is called whenever obj is bound to name where overloading symbols is
+ * allowed. If a symbol is previously bound to that name, it marks both as
+ * overloaded. Returns false if the binding was invalid.
+ */
bool bindWithOverloading(const string& name, Expr obj);
//------------------------ end operator overloading
}; /* SymbolTable::Implementation */
bool SymbolTable::Implementation::bind(const string& name, Expr obj,
- bool levelZero, bool doOverload) throw() {
+ bool levelZero, bool doOverload) {
PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
ExprManagerScope ems(obj);
if (doOverload) {
- if( !bindWithOverloading(name, obj) ){
+ if (!bindWithOverloading(name, obj)) {
return false;
}
}
}
bool SymbolTable::Implementation::bindDefinedFunction(const string& name,
- Expr obj,
- bool levelZero,
- bool doOverload) throw() {
+ Expr obj, bool levelZero,
+ bool doOverload) {
PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
ExprManagerScope ems(obj);
if (doOverload) {
- if( !bindWithOverloading(name, obj) ){
+ if (!bindWithOverloading(name, obj)) {
return false;
}
}
return true;
}
-bool SymbolTable::Implementation::isBound(const string& name) const throw() {
+bool SymbolTable::Implementation::isBound(const string& name) const {
return d_exprMap->find(name) != d_exprMap->end();
}
bool SymbolTable::Implementation::isBoundDefinedFunction(
- const string& name) const throw() {
+ const string& name) const {
CDHashMap<string, Expr>::iterator found = d_exprMap->find(name);
return found != d_exprMap->end() && d_functions->contains((*found).second);
}
-bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const
- throw() {
+bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const {
return d_functions->contains(func);
}
-Expr SymbolTable::Implementation::lookup(const string& name) const throw() {
+Expr SymbolTable::Implementation::lookup(const string& name) const {
+ Assert(isBound(name));
Expr expr = (*d_exprMap->find(name)).second;
- if(isOverloadedFunction(expr)) {
+ if (isOverloadedFunction(expr)) {
return d_nullExpr;
- }else{
+ } else {
return expr;
}
}
void SymbolTable::Implementation::bindType(const string& name, Type t,
- bool levelZero) throw() {
+ bool levelZero) {
if (levelZero) {
d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
} else {
void SymbolTable::Implementation::bindType(const string& name,
const vector<Type>& params, Type t,
- bool levelZero) throw() {
+ bool levelZero) {
if (Debug.isOn("sort")) {
Debug("sort") << "bindType(" << name << ", [";
if (params.size() > 0) {
}
}
-bool SymbolTable::Implementation::isBoundType(const string& name) const
- throw() {
+bool SymbolTable::Implementation::isBoundType(const string& name) const {
return d_typeMap->find(name) != d_typeMap->end();
}
-Type SymbolTable::Implementation::lookupType(const string& name) const throw() {
+Type SymbolTable::Implementation::lookupType(const string& name) const {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
PrettyCheckArgument(p.first.size() == 0, name,
"type constructor arity is wrong: "
}
Type SymbolTable::Implementation::lookupType(const string& name,
- const vector<Type>& params) const
- throw() {
+ const vector<Type>& params) const {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
PrettyCheckArgument(p.first.size() == params.size(), params,
"type constructor arity is wrong: "
return p.first.size();
}
-void SymbolTable::Implementation::popScope() throw(ScopeException) {
+void SymbolTable::Implementation::popScope() {
if (d_context.getLevel() == 0) {
throw ScopeException();
}
d_context.pop();
}
-void SymbolTable::Implementation::pushScope() throw() { d_context.push(); }
+void SymbolTable::Implementation::pushScope() { d_context.push(); }
-size_t SymbolTable::Implementation::getLevel() const throw() {
+size_t SymbolTable::Implementation::getLevel() const {
return d_context.getLevel();
}
return d_overload_trie->isOverloadedFunction(fun);
}
-Expr SymbolTable::Implementation::getOverloadedConstantForType(const std::string& name, Type t) const {
+Expr SymbolTable::Implementation::getOverloadedConstantForType(
+ const std::string& name, Type t) const {
return d_overload_trie->getOverloadedConstantForType(name, t);
}
-Expr SymbolTable::Implementation::getOverloadedFunctionForTypes(const std::string& name,
- const std::vector< Type >& argTypes) const {
+Expr SymbolTable::Implementation::getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<Type>& argTypes) const {
return d_overload_trie->getOverloadedFunctionForTypes(name, argTypes);
}
-bool SymbolTable::Implementation::bindWithOverloading(const string& name, Expr obj){
+bool SymbolTable::Implementation::bindWithOverloading(const string& name,
+ Expr obj) {
CDHashMap<string, Expr>::const_iterator it = d_exprMap->find(name);
- if(it != d_exprMap->end()) {
+ if (it != d_exprMap->end()) {
const Expr& prev_bound_obj = (*it).second;
- if(prev_bound_obj!=obj) {
+ if (prev_bound_obj != obj) {
return d_overload_trie->bind(name, prev_bound_obj, obj);
}
}
return d_implementation->isOverloadedFunction(fun);
}
-Expr SymbolTable::getOverloadedConstantForType(const std::string& name, Type t) const {
+Expr SymbolTable::getOverloadedConstantForType(const std::string& name,
+ Type t) const {
return d_implementation->getOverloadedConstantForType(name, t);
}
-Expr SymbolTable::getOverloadedFunctionForTypes(const std::string& name,
- const std::vector< Type >& argTypes) const {
+Expr SymbolTable::getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<Type>& argTypes) const {
return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
}
SymbolTable::~SymbolTable() {}
-bool SymbolTable::bind(const string& name, Expr obj, bool levelZero, bool doOverload) throw() {
+bool SymbolTable::bind(const string& name, Expr obj, bool levelZero,
+ bool doOverload) throw() {
return d_implementation->bind(name, obj, levelZero, doOverload);
}
bool SymbolTable::bindDefinedFunction(const string& name, Expr obj,
bool levelZero, bool doOverload) throw() {
- return d_implementation->bindDefinedFunction(name, obj, levelZero, doOverload);
+ return d_implementation->bindDefinedFunction(name, obj, levelZero,
+ doOverload);
}
void SymbolTable::bindType(const string& name, Type t, bool levelZero) throw() {
~SymbolTable();
/**
- * Bind an expression to a name in the current scope level.
+ * Bind an expression to a name in the current scope level.
*
* When doOverload is false:
* 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.
+ * until the current scope is popped.
* If levelZero is true the name shouldn't be already bound.
*
* When doOverload is true:
*
* Returns false if the binding was invalid.
*/
- bool bind(const std::string& name, Expr obj, bool levelZero = false,
+ bool bind(const std::string& name, Expr obj, bool levelZero = false,
bool doOverload = false) throw();
/**
- * Bind a function body to a name in the current scope.
+ * Bind a function body to a name in the current scope.
*
* When doOverload is false:
* 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.
+ * until the current scope is popped.
* If levelZero is true the name shouldn't be already bound.
*
* When doOverload is true:
* level, then we mark the previous bound expression and obj as overloaded
* functions.
*
- * Same as bind() but registers this as a function (so that
+ * Same as bind() but registers this as a function (so that
* isBoundDefinedFunction() returns true).
*
* @param name an identifier
* Returns false if the binding was invalid.
*/
bool bindDefinedFunction(const std::string& name, Expr obj,
- bool levelZero = false,
+ bool levelZero = false,
bool doOverload = false) throw();
/**
* Lookup a bound expression.
*
* @param name the identifier to lookup
- * @returns the unique expression bound to <code>name</code> in the current scope.
- * It returns the null expression if there is not a unique expression bound to
+ * @returns the unique expression bound to <code>name</code> in the current
+ * scope.
+ * It returns the null expression if there is not a unique expression bound to
* <code>name</code> in the current scope (i.e. if there is not exactly one).
*/
Expr lookup(const std::string& name) const throw();
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>. */
+ * Pop a scope level, deletes all bindings since the last call to pushScope,
+ * and decreases the level by 1.
+ *
+ * @throws ScopeException if the scope level is 0.
+ */
void popScope() throw(ScopeException);
- /** Push a scope level. */
+ /** Push a scope level and increase the scope level by 1. */
void pushScope() throw();
/** Get the current level of this symbol table. */
/** Reset everything. */
void reset();
-
+
//------------------------ operator overloading
/** is this function overloaded? */
bool isOverloadedFunction(Expr fun) const;
-
+
/** Get overloaded constant for type.
* If possible, it returns the defined symbol with name
* that has type t. Otherwise returns null expression.
*/
Expr getOverloadedConstantForType(const std::string& name, Type t) const;
-
+
/**
* If possible, returns the unique defined function for a name
* that expects arguments with types "argTypes".
- * For example, if argTypes = ( T1, ..., Tn ), then this may return
- * an expression with type function( T1, ..., Tn ), or constructor( T1, ...., Tn ).
- *
+ * For example, if argTypes = (T1, ..., Tn), then this may return an
+ * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
+ *
* If there is not a unique defined function for the name and argTypes,
* this returns the null expression. This can happen either if there are
* no functions with name and expected argTypes, or alternatively there is
* more than one function with name and expected argTypes.
*/
- Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const;
+ Expr getOverloadedFunctionForTypes(const std::string& name,
+ const std::vector< Type >& argTypes) const;
//------------------------ end operator overloading
-
+
private:
// Copying and assignment have not yet been implemented.
SymbolTable(const SymbolTable&);
projects / cvc5.git / commitdiff