From 5413dcf70eafbc4c473a4c7c429ed2a0f243a56d Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Sun, 7 Feb 2010 17:19:46 +0000 Subject: [PATCH] Documenting type.h/cpp Making Boolean and Kind types singletons --- src/expr/expr_manager.cpp | 12 ++- src/expr/expr_manager.h | 2 - src/expr/type.cpp | 57 ++++++++----- src/expr/type.h | 163 ++++++++++++++++++++++++++++++------ src/parser/antlr_parser.cpp | 58 +++---------- src/parser/antlr_parser.h | 120 +++++++++++++------------- src/parser/smt/smt_parser.g | 7 +- 7 files changed, 256 insertions(+), 163 deletions(-) diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index ee61c14c9..8bd9b21f6 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -31,9 +31,7 @@ using namespace std; namespace CVC4 { ExprManager::ExprManager() - : d_nm(new NodeManager()), - d_booleanType(new BooleanType(this)), - d_kindType(new KindType(this)) { + : d_nm(new NodeManager()) { } ExprManager::~ExprManager() { @@ -41,11 +39,11 @@ ExprManager::~ExprManager() { } const BooleanType* ExprManager::booleanType() { - return d_booleanType; + return BooleanType::getInstance(); } const KindType* ExprManager::kindType() { - return d_kindType; + return KindType::getInstance(); } Expr ExprManager::mkExpr(Kind kind) { @@ -97,14 +95,14 @@ Expr ExprManager::mkExpr(Kind kind, const vector& children) { const FunctionType* ExprManager::mkFunctionType(const Type* domain, const Type* range) { - return new FunctionType(this,domain,range); + return FunctionType::getInstance(this,domain,range); } /** Make a function type with input types from argTypes. */ const FunctionType* ExprManager::mkFunctionType(const std::vector& argTypes, const Type* range) { - return new FunctionType(this,argTypes,range); + return FunctionType::getInstance(this,argTypes,range); } const Type* ExprManager::mkSort(std::string name) { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 41766d64b..1ca707fae 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -108,8 +108,6 @@ public: private: /** The internal node manager */ NodeManager* d_nm; - BooleanType* d_booleanType; - KindType* d_kindType; /** * Returns the internal node manager. This should only be used by internal diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 5052a3b79..d4662d420 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -33,13 +33,12 @@ Type::Type(ExprManager* exprManager, std::string name) : d_exprManager(exprManager), d_name(name) { } -// Type Type::operator=(const Type& t) { -// if( this != &t ) { -// d_name == t.d_name; -// } +Type::Type(std::string name) : + d_name(name) { +} bool Type::operator==(const Type& t) const { - return d_name == t.d_name; + return d_exprManager == t.d_exprManager && d_name == t.d_name; } bool Type::operator!=(const Type& t) const { @@ -54,39 +53,53 @@ std::string Type::getName() const { return d_name; } -// void Type::toStream(std::ostream& out) const { -// out << getName(); -// } +BooleanType BooleanType::s_instance; -BooleanType::BooleanType(ExprManager* exprManager) - : Type(exprManager,std::string("BOOLEAN")) { +BooleanType::BooleanType() : Type(std::string("BOOLEAN")) { } BooleanType::~BooleanType() { } +BooleanType* +BooleanType::getInstance() { + return &s_instance; +} + bool BooleanType::isBoolean() const { return true; } FunctionType::FunctionType(ExprManager* exprManager, - const Type* domain, + const std::vector& argTypes, const Type* range) - : Type(exprManager), d_argTypes(), d_rangeType(range) { - d_argTypes.push_back(domain); + : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) { + Assert( argTypes.size() > 0 ); } // FIXME: What becomes of argument types? FunctionType::~FunctionType() { } -FunctionType::FunctionType(ExprManager* exprManager, - const std::vector& argTypes, - const Type* range) - : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) { +FunctionType* +FunctionType::getInstance(ExprManager* exprManager, + const Type* domain, + const Type* range) { + std::vector argTypes; + argTypes.push_back(domain); + return getInstance(exprManager,argTypes,range); +} + + //FIXME: should be singleton +FunctionType* +FunctionType::getInstance(ExprManager* exprManager, + const std::vector& argTypes, + const Type* range) { Assert( argTypes.size() > 0 ); + return new FunctionType(exprManager,argTypes,range); } + const std::vector FunctionType::getArgTypes() const { return d_argTypes; } @@ -120,8 +133,9 @@ void FunctionType::toStream(std::ostream& out) const { d_rangeType->toStream(out); } -KindType::KindType(ExprManager* exprManager) - : Type(exprManager,std::string("KIND")) { +KindType KindType::s_instance; + +KindType::KindType() : Type(std::string("KIND")) { } KindType::~KindType() { @@ -131,6 +145,11 @@ bool KindType::isKind() const { return true; } +KindType* +KindType::getInstance() { + return &s_instance; +} + SortType::SortType(ExprManager* exprManager,std::string name) : Type(exprManager,name) { } diff --git a/src/expr/type.h b/src/expr/type.h index 87c3d8f5c..e5fda779e 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -27,86 +27,199 @@ class ExprManager; /** * Class encapsulating CVC4 expression types. - * NOTE: This is very much a stub interface!!! I'm putting this here - * so the parser can do some very simple type differentiation, but - * this is obviously hopelessly inadequate. -Chris */ class Type { public: - Type() { }; - Type(ExprManager* const exprManager); - Type(ExprManager* const exprManager, std::string name); - virtual ~Type() { }; - + /** Comparision for equality */ bool operator==(const Type& t) const; + + /** Comparison for disequality */ bool operator!=(const Type& e) const; + /** Get the ExprManager associated with this type. May be NULL for + singleton types. */ ExprManager* getExprManager() const; + /** Get the name of this type. May be empty for composite types. */ std::string getName() const; + /** Is this the boolean type? */ virtual bool isBoolean() const { return false; } + /** Is this a function type? */ virtual bool isFunction() const { return false; } + /** Is this a predicate type? NOTE: all predicate types are also + function types. */ virtual bool isPredicate() const { return false; } + /** Is this a kind type (i.e., the type of a type)? */ virtual bool isKind() const { return false; } + /** Outputs a string representation of this type to the stream. */ virtual void toStream(std::ostream& out) const { out << getName(); } protected: + /** Create a type associated with exprManager. */ + Type(ExprManager* const exprManager); + + /** Create a type associated with exprManager with the given name. */ + Type(ExprManager* const exprManager, std::string name); + + /** Create a type with the given name. */ + Type(std::string name); + + /** Destructor */ + virtual ~Type() { }; + + /** The associated ExprManager */ ExprManager* d_exprManager; + + /** The name of the type (may be empty). */ std::string d_name; }; +/** + * Singleton class encapsulating the boolean type. + */ class BooleanType : public Type { - public: - BooleanType(ExprManager* exprManager); - ~BooleanType(); + +public: + static BooleanType* getInstance(); + + /** Is this the boolean type? (Returns true.) */ bool isBoolean() const; + +private: + /** Create a type associated with exprManager. */ + BooleanType(); + + /** Do-nothing private copy constructor operator, to prevent + copy-construction. */ + BooleanType(const BooleanType&); + + /** Destructor */ + ~BooleanType(); + + /** Do-nothing private assignment operator, to prevent + assignment. */ + BooleanType& operator=(const BooleanType&); + + /** The singleton instance */ + static BooleanType s_instance; }; +/** + * Class encapsulating a function type. + * TODO: Override == to check component types? + */ class FunctionType : public Type { - public: - FunctionType(ExprManager* exprManager, - const Type* domain, - const Type* range); - FunctionType(ExprManager* exprManager, - const std::vector& argTypes, - const Type* range); - ~FunctionType(); + +public: + static FunctionType* getInstance(ExprManager* exprManager, + const Type* domain, + const Type* range); + + static FunctionType* getInstance(ExprManager* exprManager, + const std::vector& argTypes, + const Type* range); + + + /** Retrieve the argument types. The vector will be non-empty. */ const std::vector getArgTypes() const; + + /** Get the range type (i.e., the type of the result). */ const Type* getRangeType() const; + + /** Is this as function type? (Returns true.) */ bool isFunction() const; + + /** Is this as predicate type? (Returns true if range is + boolean.) */ bool isPredicate() const; + + /** Outputs a string representation of this type to the stream, + in the format "D -> R" or "(A, B, C) -> R". */ void toStream(std::ostream& out) const; - private: - std::vector d_argTypes; +private: + + /** Construct a function type associated with exprManager, + given a vector of argument types and the range type. + + @param argTypes a non-empty vector of input types + @param range the result type + */ + FunctionType(ExprManager* exprManager, + const std::vector& argTypes, + const Type* range); + + /** Destructor */ + ~FunctionType(); + + /** The list of input types. */ + const std::vector d_argTypes; + + /** The result type. */ const Type* d_rangeType; + }; + +/** Class encapsulating the kind type (the type of types). + TODO: Should be a singleton per-ExprManager. +*/ class KindType : public Type { - public: - KindType(ExprManager* exprManager); - ~KindType(); + +public: + + /** Create a type associated with exprManager. */ + static KindType* getInstance(); + + /** Is this the kind type? (Returns true.) */ bool isKind() const; + +private: + + /** Create a type associated with exprManager. */ + KindType(); + + /* Do-nothing private copy constructor, to prevent + copy construction. */ + KindType(const KindType&); + + /** Destructor */ + ~KindType(); + + /* Do-nothing private assignment operator, to prevent + assignment. */ + KindType& operator=(const KindType&); + + /** The singleton instance */ + static KindType s_instance; }; +/** Class encapsulating a user-defined sort. + TODO: Should sort be uniquely named per-exprManager and not conflict + with any builtins? */ class SortType : public Type { - public: + +public: + + /** Create a sort associated with exprManager with the given name. */ SortType(ExprManager* exprManager, std::string name); + + /** Destructor */ ~SortType(); }; diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 5a9af8d4a..bd263f72d 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -51,8 +51,7 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : Expr AntlrParser::getSymbol(std::string name, SymbolType type) { Assert( isDeclared(name,type) ); switch( type ) { - case SYM_VARIABLE: // Predicates and functions share var namespace - // case SYM_PREDICATE: + case SYM_VARIABLE: // Functions share var namespace case SYM_FUNCTION: return d_varSymbolTable.getObject(name); default: @@ -68,10 +67,6 @@ Expr AntlrParser::getFunction(std::string name) { return getSymbol(name,SYM_FUNCTION); } -// Expr AntlrParser::getPredicate(std::string name) { -// return getSymbol(name,SYM_PREDICATE); -// } - const Type* AntlrParser::getType(std::string var_name, SymbolType type) { @@ -96,8 +91,7 @@ bool AntlrParser::isFunction(std::string name) { return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction(); } -/* Returns true if name is either a boolean variable OR a function - returning boolean. */ +/* Returns true if name is bound to a function returning boolean. */ bool AntlrParser::isPredicate(std::string name) { return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate(); } @@ -135,45 +129,32 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { return result; } -const FunctionType* +const Type* AntlrParser::functionType(const Type* domainType, const Type* rangeType) { return d_exprManager->mkFunctionType(domainType,rangeType); } -const FunctionType* +const Type* AntlrParser::functionType(const std::vector& argTypes, const Type* rangeType) { Assert( argTypes.size() > 0 ); return d_exprManager->mkFunctionType(argTypes,rangeType); } -const FunctionType* +const Type* AntlrParser::functionType(const std::vector& sorts) { - Assert( sorts.size() > 1 ); - std::vector argTypes(sorts); - const Type* rangeType = argTypes.back(); - argTypes.pop_back(); - return functionType(argTypes,rangeType); -} - -Expr AntlrParser::newFunction(std::string name, - const std::vector& sorts) { Assert( sorts.size() > 0 ); if( sorts.size() == 1 ) { - return mkVar(name, sorts[0]); + return sorts[0]; } else { - return mkVar(name, functionType(sorts)); + std::vector argTypes(sorts); + const Type* rangeType = argTypes.back(); + argTypes.pop_back(); + return functionType(argTypes,rangeType); } } -const std::vector -AntlrParser::newFunctions(const std::vector& names, - const std::vector& sorts) { - const FunctionType* t = functionType(sorts); - return mkVars(names, t); -} - const Type* AntlrParser::predicateType(const std::vector& sorts) { if(sorts.size() == 0) { return d_exprManager->booleanType(); @@ -182,20 +163,6 @@ const Type* AntlrParser::predicateType(const std::vector& sorts) { } } -Expr -AntlrParser::newPredicate(std::string name, - const std::vector& sorts) { - const Type* t = predicateType(sorts); - return mkVar(name, t); -} - -const std::vector -AntlrParser::newPredicates(const std::vector& names, - const std::vector& sorts) { - const Type* t = predicateType(sorts); - return mkVars(names, t); -} - Expr AntlrParser::mkVar(const std::string name, const Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; @@ -301,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { return UINT_MAX; default: - Unhandled("kind in minArity"); + Unhandled("kind in maxArity"); } } @@ -311,8 +278,7 @@ void AntlrParser::setExpressionManager(ExprManager* em) { bool AntlrParser::isDeclared(string name, SymbolType type) { switch(type) { - case SYM_VARIABLE: // Predicates and functions share var namespace - // case SYM_PREDICATE: + case SYM_VARIABLE: // Functions share var namespace case SYM_FUNCTION: return d_varSymbolTable.isBound(name); case SYM_SORT: diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 3cfe4fc5d..76200368c 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -112,8 +112,13 @@ protected: * @return the variable expression */ Expr getVariable(std::string var_name); - Expr getFunction(std::string var_name); - /* Expr getPredicate(std::string var_name); */ + + /** + * Returns a function, given a name and a type. + * @param name the name of the function + * @return the function expression + */ + Expr getFunction(std::string name); /** * Returns a sort, given a name @@ -121,13 +126,11 @@ protected: const Type* getSort(std::string sort_name); /** - * Types of symbols. + * Types of symbols. Used to define namespaces. */ enum SymbolType { /** Variables */ SYM_VARIABLE, - /** Predicates */ - /* SYM_PREDICATE, */ /** Functions */ SYM_FUNCTION, /** Sorts */ @@ -135,23 +138,30 @@ protected: }; /** - * Checks if the variable has been declared. - * @param the variable name + * Checks if a symbol has been declared. + * @param name the symbol name + * @param type the symbol type */ - bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE); + bool isDeclared(std::string name, SymbolType type = SYM_VARIABLE); /** - * Return true if the the declaration policy we want to enforce is true. - * @param varName the symbol to check + * Return true if the the declaration policy we want to enforce holds + * for the given symbol. + * @param name the symbol to check * @oaram check the kind of check to perform + * @param type the type of the symbol * @return true if the check holds */ - bool checkDeclaration(std::string varName, + bool checkDeclaration(std::string name, DeclarationCheck check, SymbolType type = SYM_VARIABLE); - /** Returns the type for the variable with the given name. */ + /** + * Returns the type for the variable with the given name. + * @param name the symbol to lookup + * @param type the (namespace) type of the symbol + */ const Type* getType(std::string var_name, SymbolType type = SYM_VARIABLE); @@ -202,63 +212,39 @@ protected: */ Expr mkExpr(Kind kind, const std::vector& children); - /* Create a new CVC4 variable expression . */ + /** Create a new CVC4 variable expression of the given type. */ Expr mkVar(const std::string name, const Type* type); + /** Create a set of new CVC4 variable expressions of the given + type. */ const std::vector mkVars(const std::vector names, const Type* type); /** Returns a function type over the given domain and range types. */ - const FunctionType* functionType(const Type* domain, const Type* range); - /** Returns a function type over the given types. argTypes must have - at least 1 element. */ - const FunctionType* functionType(const std::vector& argTypes, - const Type* rangeType); - /** Returns a function type over the given types. types must have - at least 2 elements (i.e., a domain and range). */ - const FunctionType* functionType(const std::vector& types); + const Type* functionType(const Type* domain, const Type* range); - /** - * Creates a new function over the given sorts. The function - * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1]. - * @param name the name of the function - * @param sorts the sorts - */ - Expr newFunction(std::string name, - const std::vector& sorts); + /** Returns a function type over the given types. argTypes must be + non-empty. */ + const Type* functionType(const std::vector& argTypes, + const Type* rangeType); - /** - * Creates new functions over the given sorts. Each function has - * arity sorts.size() - 1 and range type sorts[sorts.size() - 1]. - * @param name the name of the function - * @param sorts the sorts + /** + * Returns a function type over the given types. If types has only + * one element, then the type is just types[0]. + * + * @param types a non-empty list of input and output types. */ - const std::vector - newFunctions(const std::vector& names, - const std::vector& sorts); + const Type* functionType(const std::vector& types); - /** Returns a predicate type over the given sorts. sorts must be - non-empty. If sorts has size 1, then the type is just BOOLEAN. */ - const Type* predicateType(const std::vector& sorts); - - /** - * Creates a new predicate (a function with range boolean) over the - * given sorts. The predicate has sorts.size(). - * @param name the name of the predicate - * @param sorts the sorts - */ - Expr newPredicate(std::string name, const std::vector& sorts); + /** + * Returns a predicate type over the given sorts. If sorts is empty, + * then the type is just BOOLEAN. - /** - * Creates new predicates (a function with range boolean) over the - * given sorts. Each predicate will have arity sorts.size(). - * @param p_names the names of the predicates + * @param sorts a list of input types */ - const std::vector - newPredicates(const std::vector& names, - const std::vector& sorts); + const Type* predicateType(const std::vector& sorts); /** * Creates a new sort with the given name. @@ -271,21 +257,29 @@ protected: const std::vector newSorts(const std::vector& names); + /** Is the symbol bound to a boolean variable? */ bool isBoolean(std::string name); + + /** Is the symbol bound to a function? */ bool isFunction(std::string name); + + /** Is the symbol bound to a predicate? */ bool isPredicate(std::string name); + /** Returns the boolean type. */ const BooleanType* booleanType(); + + /** Returns the kind type (i.e., the type of types). */ const KindType* kindType(); - unsigned int minArity(Kind kind); - unsigned int maxArity(Kind kind); + /** Returns the minimum arity of the given kind. */ + static unsigned int minArity(Kind kind); - /** - * Returns the precedence rank of the kind. - */ - static unsigned getPrecedence(Kind kind); + /** Returns the maximum arity of the given kind. */ + static unsigned int maxArity(Kind kind); + /** Returns a string representation of the given object (for + debugging). */ inline std::string toString(DeclarationCheck check) { switch(check) { case CHECK_NONE: return "CHECK_NONE"; @@ -295,6 +289,8 @@ protected: } } + /** Returns a string representation of the given object (for + debugging). */ inline std::string toString(SymbolType type) { switch(type) { case SYM_VARIABLE: return "SYM_VARIABLE"; @@ -319,8 +315,8 @@ private: /** The sort table */ SymbolTable d_sortTable; + /** Lookup a symbol in the given namespace. */ Expr getSymbol(std::string var_name, SymbolType type); - }; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 28101532b..dbc9e1a21 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -259,7 +259,8 @@ functionDeclaration t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN - { newFunction(name, sorts); } + { t = functionType(sorts); + mkVar(name, t); } ; /** @@ -269,9 +270,11 @@ predicateDeclaration { string p_name; std::vector p_sorts; + const Type *t; } : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN - { newPredicate(p_name, p_sorts); } + { t = predicateType(p_sorts); + mkVar(p_name, t); } ; sortDeclaration -- 2.30.2