-/********************* */
-/*! \file symbol_table.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** 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
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Morgan Deters, Christopher L. Conway
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Convenience class for scoping variable and type declarations.
+ */
-#include <vector>
-#include <utility>
-#include <ext/hash_map>
+#include "cvc5_public.h"
-#include "expr/expr.h"
-#include "util/hash.h"
+#ifndef CVC5__SYMBOL_TABLE_H
+#define CVC5__SYMBOL_TABLE_H
-#include "context/cdhashset_forward.h"
-#include "context/cdhashmap_forward.h"
+#include <memory>
+#include <string>
+#include <vector>
-namespace CVC4 {
+#include "base/exception.h"
+#include "cvc5_export.h"
-class Type;
+namespace cvc5 {
-namespace context {
- class Context;
-}/* CVC4::context namespace */
+namespace api {
+class Solver;
+class Sort;
+class Term;
+} // namespace api
-class CVC4_PUBLIC ScopeException : public Exception {
-};/* class ScopeException */
+class CVC5_EXPORT ScopeException : public Exception
+{
+};
/**
* 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:
+class CVC5_EXPORT SymbolTable
+{
+ public:
/** Create a symbol table. */
SymbolTable();
-
- /** Destroy a symbol table. */
~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.
+ * Bind an expression to a name in the current scope level.
*
- * @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();
-
- /**
- * Bind a function body to a name in the current scope. If
- * <code>name</code> is already bound to an expression in the current
+ * 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. Same as bind() but registers
- * this as a function (so that isBoundDefinedFunction() returns true).
+ * until the current scope is popped.
+ * If levelZero is true the name shouldn't be already bound.
+ *
+ * When doOverload is true:
+ * if <code>name</code> is already bound to an expression in the current
+ * level, then we mark the previous bound expression and obj as overloaded
+ * functions.
*
* @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
+ * @param doOverload set if the binding can overload the function name.
+ *
+ * Returns false if the binding was invalid.
*/
- void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw();
+ bool bind(const std::string& name,
+ api::Term obj,
+ bool levelZero = false,
+ bool doOverload = false);
/**
* Bind a type to a name in the current scope. If <code>name</code>
* @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();
+ void bindType(const std::string& name, api::Sort t, bool levelZero = false);
/**
* Bind a type to a name in the current scope. If <code>name</code>
* locally within the current scope)
*/
void bindType(const std::string& name,
- const std::vector<Type>& params,
- Type t, bool levelZero = false) throw();
+ const std::vector<api::Sort>& params,
+ api::Sort t,
+ bool levelZero = false);
/**
- * Check whether a name is bound to an expression with either bind()
- * or bindDefinedFunction().
+ * Check whether a name is bound to an expression with bind().
*
* @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();
+ bool isBound(const std::string& name) const;
/**
* 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();
+ bool isBoundType(const std::string& name) const;
/**
* Lookup a bound expression.
*
* @param name the identifier to lookup
- * @returns the expression bound to <code>name</code> in the current scope.
+ * @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();
+ api::Term lookup(const std::string& name) const;
/**
* 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();
+ api::Sort lookupType(const std::string& name) const;
/**
* Lookup a bound parameterized 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();
+ api::Sort lookupType(const std::string& name,
+ const std::vector<api::Sort>& params) const;
/**
* 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);
+ * 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();
- /** Push a scope level. */
- void pushScope() throw();
+ /** Push a scope level and increase the scope level by 1. */
+ void pushScope();
/** Get the current level of this symbol table. */
- size_t getLevel() const throw();
+ size_t getLevel() const;
+
+ /** Reset everything. */
+ void reset();
+ /** Reset assertions. */
+ void resetAssertions();
+
+ //------------------------ operator overloading
+ /** is this function overloaded? */
+ bool isOverloadedFunction(api::Term fun) const;
+
+ /** Get overloaded constant for type.
+ * If possible, it returns the defined symbol with name
+ * that has type t. Otherwise returns null expression.
+ */
+ api::Term getOverloadedConstantForType(const std::string& name,
+ api::Sort 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).
+ *
+ * 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.
+ */
+ api::Term getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<api::Sort>& argTypes) const;
+ //------------------------ end operator overloading
-};/* class SymbolTable */
+ private:
+ /** The implementation of the symbol table */
+ class Implementation;
+ std::unique_ptr<Implementation> d_implementation;
+}; /* class SymbolTable */
-}/* CVC4 namespace */
+} // namespace cvc5
-#endif /* __CVC4__SYMBOL_TABLE_H */
+#endif /* CVC5__SYMBOL_TABLE_H */
projects / cvc5.git / blobdiff