From 12a8a7f9a90e45e8313f26af527a52e6dda943d3 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 13 Apr 2010 22:50:07 +0000 Subject: [PATCH] Merging from branches/decl-scopes (r401:411) --- src/expr/Makefile.am | 5 +- src/expr/declaration_scope.cpp | 74 +++++++++++ src/expr/declaration_scope.h | 132 +++++++++++++++++++ src/parser/parser_state.cpp | 16 ++- src/parser/parser_state.h | 16 ++- src/parser/smt/Smt.g | 5 +- test/unit/Makefile.am | 1 + test/unit/expr/declaration_scope_black.h | 158 +++++++++++++++++++++++ test/unit/parser/parser_white.h | 6 + 9 files changed, 398 insertions(+), 15 deletions(-) create mode 100644 src/expr/declaration_scope.cpp create mode 100644 src/expr/declaration_scope.h create mode 100644 test/unit/expr/declaration_scope_black.h diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 1f5e403cc..67970d453 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -24,7 +24,10 @@ libexpr_la_SOURCES = \ @srcdir@/expr.cpp \ type.cpp \ command.h \ - command.cpp + command.cpp \ + declaration_scope.h \ + declaration_scope.cpp + EXTRA_DIST = \ @srcdir@/kind.h \ diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp new file mode 100644 index 000000000..c326817ad --- /dev/null +++ b/src/expr/declaration_scope.cpp @@ -0,0 +1,74 @@ +/********************* */ +/** declaration_scope.cpp + ** Original author: cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Convenience class for scoping variable and type declarations (implementation) + **/ + +#include "declaration_scope.h" +#include "expr.h" +#include "type.h" + +#include "context/cdmap.h" +#include "context/context.h" + +#include + +namespace CVC4 { + +using namespace context; + +DeclarationScope::DeclarationScope() : + d_context(new Context()), + d_exprMap(new (true) CDMap(d_context)), + d_typeMap(new (true) CDMap(d_context)) { +} + +DeclarationScope::~DeclarationScope() { + d_exprMap->deleteSelf(); + delete d_context; +} + +void DeclarationScope::bind(const std::string& name, const Expr& obj) throw () { + d_exprMap->insert(name,obj); +} + +bool DeclarationScope::isBound(const std::string& name) const throw () { + return d_exprMap->find(name) != d_exprMap->end(); +} + +Expr DeclarationScope::lookup(const std::string& name) const throw () { + return (*d_exprMap->find(name)).second; +} + +void DeclarationScope::bindType(const std::string& name, Type* t) throw () { + d_typeMap->insert(name,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 () { + return (*d_typeMap->find(name)).second; +} + + +void DeclarationScope::popScope() throw (ScopeException) { + if( d_context->getLevel() == 0 ) { + throw ScopeException(); + } + d_context->pop(); +} + +void DeclarationScope::pushScope() throw () { + d_context->push(); +} + +} // namespace CVC4 diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h new file mode 100644 index 000000000..e08c25173 --- /dev/null +++ b/src/expr/declaration_scope.h @@ -0,0 +1,132 @@ +/********************* */ +/** context.h + ** Original author: cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Convenience class for scoping variable and type declarations. + **/ + +#ifndef DECLARATION_SCOPE_H_ +#define DECLARATION_SCOPE_H_ + +#include "expr.h" + +#include + +namespace CVC4 { + +class Type; + +namespace context { + +class Context; + +template +class CDMap; + +} //namespace context + +/** A basic hash function for std::string + * TODO: Does this belong somewhere else (like util/)? + */ +struct StringHashFunction { + size_t operator()(const std::string& str) const { + return __gnu_cxx::hash()(str.c_str()); + } +}; + +class CVC4_PUBLIC 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 DeclarationScope { + /** The context manager for the scope maps. */ + context::Context *d_context; + + /** A map for expressions. */ + context::CDMap *d_exprMap; + + /** A map for types. */ + context::CDMap *d_typeMap; + +public: + /** Create a declaration scope. */ + DeclarationScope(); + + /** Destroy a declaration scope. */ + ~DeclarationScope(); + + /** Bind an expression to a name in the current scope level. + * If name is already bound in the current level, then the + * binding is replaced. If name 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 obj the expression to bind to name + */ + void bind(const std::string& name, const Expr& obj) throw (); + + /** Bind a type to a name in the current scope. + * If name is already bound to a type in the current level, + * then the binding is replaced. If name 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 name + */ + void bindType(const std::string& name, Type* t) throw (); + + /** Check whether a name is bound to an expression. + * + * @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 is bound to a type. + * + * @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 name in the current scope. + */ + Expr lookup(const std::string& name) const throw (); + + /** Lookup a bound type. + * + * @param name the identifier to lookup + * @returns the type bound to name in the current scope. + */ + Type* lookupType(const std::string& name) const throw (); + + /** Pop a scope level. Deletes all bindings since the last call to + * pushScope. Calls to pushScope and + * popScope must be "properly nested." I.e., a call to + * popScope is only legal if the number of prior calls to + * pushScope on this DeclarationScope is strictly + * greater than then number of prior calls to popScope. */ + void popScope() throw (ScopeException); + + /** Push a scope level. */ + void pushScope() throw (); +}; + +} // namespace CVC4 + +#endif /* DECLARATION_SCOPE_H_ */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 6cc8f6d9c..5f07b16b7 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -50,7 +50,7 @@ Expr ParserState::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - return d_varTable.getObject(name); + return d_declScope.lookup(name); default: Unhandled(type); @@ -72,7 +72,7 @@ ParserState::getType(const std::string& var_name, Type* ParserState::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); - Type* t = d_sortTable.getObject(name); + Type *t = d_declScope.lookupType(name); return t; } @@ -112,16 +112,18 @@ ParserState::mkVars(const std::vector names, void ParserState::defineVar(const std::string& name, const Expr& val) { Assert(!isDeclared(name)); - d_varTable.bindName(name,val); + d_declScope.bind(name,val); Assert(isDeclared(name)); } +/* void ParserState::undefineVar(const std::string& name) { Assert(isDeclared(name)); - d_varTable.unbindName(name); + d_declScope.unbind(name); Assert(!isDeclared(name)); } +*/ void ParserState::setLogic(const std::string& name) { @@ -137,7 +139,7 @@ ParserState::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ) ; Type* type = d_exprManager->mkSort(name); - d_sortTable.bindName(name, type); + d_declScope.bindType(name, type); Assert( isDeclared(name, SYM_SORT) ) ; return type; } @@ -154,9 +156,9 @@ ParserState::mkSorts(const std::vector& names) { bool ParserState::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: - return d_varTable.isBound(name); + return d_declScope.isBound(name); case SYM_SORT: - return d_sortTable.isBound(name); + return d_declScope.isBoundType(name); default: Unhandled(type); } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 3e0771070..de624e3a0 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -20,6 +20,7 @@ #include +#include "expr/declaration_scope.h" #include "expr/expr.h" #include "expr/kind.h" #include "parser/input.h" @@ -96,11 +97,8 @@ class ParserState { /** The input that we're parsing. */ Input *d_input; - /** The symbol table lookup */ - SymbolTable d_varTable; - - /** The sort table */ - SymbolTable d_sortTable; + /** The symbol table */ + DeclarationScope d_declScope; /** The name of the input file. */ std::string d_filename; @@ -128,6 +126,12 @@ public: return d_input; } + /** Set the declaration scope manager for this input. NOTE: This should only be + * called before parsing begins. Otherwise, previous declarations will be lost. */ + inline void setDeclarationScope(DeclarationScope declScope) { + d_declScope = declScope; + } + /** * Check if we are done -- either the end of input has been reached, or some * error has been encountered. @@ -251,6 +255,8 @@ public: d_input->parseError(msg); } + inline void pushScope() { d_declScope.pushScope(); } + inline void popScope() { d_declScope.popScope(); } }; // class ParserState } // namespace parser diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 160bd321f..25c2fbc89 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -198,10 +198,11 @@ annotatedFormula[CVC4::Expr& expr] (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) annotatedFormula[expr] RPAREN_TOK - { PARSER_STATE->defineVar(name,expr); } + { PARSER_STATE->pushScope(); + PARSER_STATE->defineVar(name,expr); } annotatedFormula[expr] RPAREN_TOK - { PARSER_STATE->undefineVar(name); } + { PARSER_STATE->popScope(); } | /* a variable */ ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3f0816560..a190152d3 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -9,6 +9,7 @@ UNIT_TESTS = \ expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ + expr/declaration_scope_black \ parser/parser_white \ context/context_black \ context/context_white \ diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h new file mode 100644 index 000000000..f93a3fcc8 --- /dev/null +++ b/test/unit/expr/declaration_scope_black.h @@ -0,0 +1,158 @@ +/********************* */ +/** declaration_scope_black.h + ** Original author: cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Black box testing of CVC4::DeclarationScope. + **/ + +#include + +#include +#include + +#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 ); + } +}; diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index d0959cf6f..653e3a1d7 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -261,6 +261,12 @@ public: delete d_exprManager; } + void testBs() { + DeclarationScope declScope; + declScope.bind("foo", d_exprManager->mkVar("foo",d_exprManager->booleanType())); + + } + void testGoodCvc4Inputs() { tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); } -- 2.30.2