summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/Makefile.am5
-rw-r--r--src/expr/declaration_scope.cpp74
-rw-r--r--src/expr/declaration_scope.h132
-rw-r--r--src/parser/parser_state.cpp16
-rw-r--r--src/parser/parser_state.h16
-rw-r--r--src/parser/smt/Smt.g5
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/expr/declaration_scope_black.h158
-rw-r--r--test/unit/parser/parser_white.h6
9 files changed, 398 insertions, 15 deletions
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 <string>
+
+namespace CVC4 {
+
+using namespace context;
+
+DeclarationScope::DeclarationScope() :
+ d_context(new Context()),
+ d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)),
+ d_typeMap(new (true) CDMap<std::string,Type*,StringHashFunction>(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 <ext/hash_map>
+
+namespace CVC4 {
+
+class Type;
+
+namespace context {
+
+class Context;
+
+template <class Key, class Data, class HashFcn>
+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<const char*>()(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<std::string,Expr,StringHashFunction> *d_exprMap;
+
+ /** A map for types. */
+ context::CDMap<std::string,Type*,StringHashFunction> *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 <code>name</code> is already bound 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 obj the expression to bind to <code>name</code>
+ */
+ void bind(const std::string& name, const Expr& obj) throw ();
+
+ /** 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>
+ */
+ 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 <code>name</code> 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 <code>name</code> in the current scope.
+ */
+ Type* lookupType(const std::string& name) const throw ();
+
+ /** 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 ();
+};
+
+} // 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<std::string> 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<std::string>& 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 <string>
+#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<Expr> d_varTable;
-
- /** The sort table */
- SymbolTable<Type*> 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 <em>only</me> 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 <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 );
+ }
+};
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback