diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-25 22:32:03 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-25 22:32:03 +0000 |
commit | bfab2bde219a0cda230fb2f26d89d123918a219f (patch) | |
tree | ea051051a3b7821127500926593b310bbf5b744a /src/expr | |
parent | 175741488a4dd986ad69ee644617ff735b855031 (diff) |
Adding Node::getOperator()
Removing references to ExprManager from Type, moving Type creation into NodeManager
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager.cpp | 15 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 7 | ||||
-rw-r--r-- | src/expr/kind_prologue.h | 2 | ||||
-rw-r--r-- | src/expr/node.h | 68 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 1 | ||||
-rw-r--r-- | src/expr/node_manager.h | 45 | ||||
-rw-r--r-- | src/expr/type.cpp | 53 | ||||
-rw-r--r-- | src/expr/type.h | 68 |
8 files changed, 159 insertions, 100 deletions
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 6e1be2e09..993bf3483 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -38,14 +38,14 @@ ExprManager::~ExprManager() { delete d_nodeManager; } -const BooleanType* ExprManager::booleanType() { +const BooleanType* ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); - return BooleanType::getInstance(); + d_nodeManager->booleanType(); } -const KindType* ExprManager::kindType() { +const KindType* ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); - return KindType::getInstance(); + d_nodeManager->kindType(); } Expr ExprManager::mkExpr(Kind kind) { @@ -106,7 +106,7 @@ const FunctionType* ExprManager::mkFunctionType(const Type* domain, const Type* range) { NodeManagerScope nms(d_nodeManager); - return FunctionType::getInstance(this, domain, range); + return d_nodeManager->mkFunctionType(domain,range); } /** Make a function type with input types from argTypes. */ @@ -114,13 +114,12 @@ const FunctionType* ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) { NodeManagerScope nms(d_nodeManager); - return FunctionType::getInstance(this, argTypes, range); + return d_nodeManager->mkFunctionType(argTypes,range); } const Type* ExprManager::mkSort(const std::string& name) { - // FIXME: Sorts should be unique per-ExprManager NodeManagerScope nms(d_nodeManager); - return new SortType(this, name); + return d_nodeManager->mkSort(name); } Expr ExprManager::mkVar(const Type* type, const std::string& name) { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 319a5d318..3ea1b581a 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -46,10 +46,11 @@ public: */ ~ExprManager(); - /** Get the type for booleans. */ - const BooleanType* booleanType(); + /** Get the type for booleans */ + const BooleanType* booleanType() const; + /** Get the type for sorts. */ - const KindType* kindType(); + const KindType* kindType() const; /** * Make a unary expression of a given kind (TRUE, FALSE,...). diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h index 08468385b..32a96dcd9 100644 --- a/src/expr/kind_prologue.h +++ b/src/expr/kind_prologue.h @@ -27,3 +27,5 @@ enum Kind_t { UNDEFINED_KIND = -1, /** Null Kind */ NULL_EXPR, + /** The kind of nodes representing built-in operators */ + BUILTIN, diff --git a/src/expr/node.h b/src/expr/node.h index 474a175b1..06f368583 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -223,6 +223,74 @@ template<bool ref_count> } /** + * Returns a node representing the operator of this expression. + * If this is an APPLY, then the operator will be a functional term. + * Otherwise, it will be a node with kind BUILTIN + */ + inline NodeTemplate<true> getOperator() const { + switch(getKind()) { + case kind::APPLY: + /* The operator is the first child. */ + return NodeTemplate<true> (d_nv->d_children[0]); + + case kind::EQUAL: + case kind::ITE: + case kind::TUPLE: + case kind::NOT: + case kind::AND: + case kind::IFF: + case kind::IMPLIES: + case kind::OR: + case kind::XOR: + case kind::PLUS: + /* Should return a BUILTIN node. */ + Unimplemented("getOperator() on non-APPLY kind: " + getKind()); + break; + + case kind::FALSE: + case kind::TRUE: + case kind::SKOLEM: + case kind::VARIABLE: + IllegalArgument(*this,"getOperator() called on kind with no operator"); + break; + + default: + Unhandled(getKind()); + } + + NodeTemplate<true> n; // NULL Node for default return + return n; + } + + /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */ + inline bool hasOperator() const { + switch(getKind()) { + case kind::APPLY: + case kind::EQUAL: + case kind::ITE: + case kind::TUPLE: + case kind::FALSE: + case kind::TRUE: + case kind::NOT: + case kind::AND: + case kind::IFF: + case kind::IMPLIES: + case kind::OR: + case kind::XOR: + case kind::PLUS: + return true; + + case kind::SKOLEM: + case kind::VARIABLE: + return false; + + default: + Unhandled(getKind()); + } + + } + + /** * Returns the type of this node. * @return the type */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index b11361827..5b5dfafa9 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -30,5 +30,4 @@ NodeValue* NodeManager::poolLookup(NodeValue* nv) const { return *find; } } - }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index a200a6d77..9d2b0947e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -114,6 +114,28 @@ public: const AttrKind&, const typename AttrKind::value_type& value); + + /** Get the type for booleans. */ + inline const BooleanType* booleanType() const { + return BooleanType::getInstance(); + } + + /** Get the type for sorts. */ + inline const KindType* kindType() const { + return KindType::getInstance(); + } + + /** Make a function type from domain to range. */ + inline const FunctionType* + mkFunctionType(const Type* domain, const Type* range); + + /** Make a function type with input types from argTypes. */ + inline const FunctionType* + mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range); + + /** Make a new sort with the given name. */ + inline const Type* mkSort(const std::string& name); + inline const Type* getType(TNode n); }; @@ -159,6 +181,29 @@ inline void NodeManager::setAttribute(TNode n, d_attrManager.setAttribute(n, AttrKind(), value); } +/** Make a function type from domain to range. + * TODO: Function types should be unique for this manager. */ +const FunctionType* +NodeManager::mkFunctionType(const Type* domain, + const Type* range) { + std::vector<const Type*> argTypes; + argTypes.push_back(domain); + return new FunctionType(argTypes, range); +} + +/** Make a function type with input types from argTypes. + * TODO: Function types should be unique for this manager. */ +const FunctionType* +NodeManager::mkFunctionType(const std::vector<const Type*>& argTypes, + const Type* range) { + Assert( argTypes.size() > 0 ); + return new FunctionType(argTypes, range); +} + +const Type* +NodeManager::mkSort(const std::string& name) { + return new SortType(name); +} inline const Type* NodeManager::getType(TNode n) { return getAttribute(n, CVC4::expr::TypeAttr()); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 368a3fe44..4bdda6810 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -13,7 +13,7 @@ ** Implementation of expression types **/ -#include "expr/expr_manager.h" +#include "expr/node_manager.h" #include "expr/type.h" #include "util/Assert.h" #include <string> @@ -25,30 +25,14 @@ std::ostream& operator<<(std::ostream& out, const Type& e) { return out; } -Type::Type(ExprManager* exprManager) : - d_exprManager(exprManager), d_name(std::string("<undefined>")) { -} - -Type::Type(ExprManager* exprManager, std::string name) : - d_exprManager(exprManager), d_name(name) { +Type::Type() : + d_name(std::string("<undefined>")) { } Type::Type(std::string name) : d_name(name) { } -bool Type::operator==(const Type& t) const { - return d_exprManager == t.d_exprManager && d_name == t.d_name; -} - -bool Type::operator!=(const Type& t) const { - return !(*this == t); -} - -ExprManager* Type::getExprManager() const { - return d_exprManager; -} - std::string Type::getName() const { return d_name; } @@ -70,10 +54,10 @@ bool BooleanType::isBoolean() const { return true; } -FunctionType::FunctionType(ExprManager* exprManager, - const std::vector<const Type*>& argTypes, +FunctionType::FunctionType(const std::vector<const Type*>& argTypes, const Type* range) - : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) { + : d_argTypes(argTypes), + d_rangeType(range) { Assert( argTypes.size() > 0 ); } @@ -81,25 +65,6 @@ FunctionType::FunctionType(ExprManager* exprManager, FunctionType::~FunctionType() { } -FunctionType* -FunctionType::getInstance(ExprManager* exprManager, - const Type* domain, - const Type* range) { - std::vector<const Type*> argTypes; - argTypes.push_back(domain); - return getInstance(exprManager,argTypes,range); -} - - //FIXME: should be singleton -FunctionType* -FunctionType::getInstance(ExprManager* exprManager, - const std::vector<const Type*>& argTypes, - const Type* range) { - Assert( argTypes.size() > 0 ); - return new FunctionType(exprManager,argTypes,range); -} - - const std::vector<const Type*> FunctionType::getArgTypes() const { return d_argTypes; } @@ -113,7 +78,7 @@ bool FunctionType::isFunction() const { } bool FunctionType::isPredicate() const { - return d_rangeType == d_exprManager->booleanType(); + return d_rangeType->isBoolean(); } void FunctionType::toStream(std::ostream& out) const { @@ -150,8 +115,8 @@ KindType::getInstance() { return &s_instance; } -SortType::SortType(ExprManager* exprManager,std::string name) - : Type(exprManager,name) { +SortType::SortType(std::string name) + : Type(name) { } SortType::~SortType() { diff --git a/src/expr/type.h b/src/expr/type.h index fd485602e..77994eec5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -23,7 +23,7 @@ namespace CVC4 { -class ExprManager; +class NodeManager; /** * Class encapsulating CVC4 expression types. @@ -36,10 +36,6 @@ public: /** 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; @@ -70,11 +66,8 @@ public: } 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 an un-named type. */ + Type(); /** Create a type with the given name. */ Type(std::string name); @@ -82,9 +75,6 @@ protected: /** Destructor */ virtual ~Type() { }; - /** The associated ExprManager */ - ExprManager* d_exprManager; - /** The name of the type (may be empty). */ std::string d_name; }; @@ -95,13 +85,13 @@ protected: class BooleanType : public Type { public: - static BooleanType* getInstance(); - /** Is this the boolean type? (Returns true.) */ bool isBoolean() const; + static BooleanType* getInstance(); private: - /** Create a type associated with exprManager. */ + + /** Create a type associated with nodeManager. */ BooleanType(); /** Do-nothing private copy constructor operator, to prevent @@ -126,15 +116,6 @@ private: class FunctionType : public Type { public: - static FunctionType* getInstance(ExprManager* exprManager, - const Type* domain, - const Type* range); - - static FunctionType* getInstance(ExprManager* exprManager, - const std::vector<const Type*>& argTypes, - const Type* range); - - /** Retrieve the argument types. The vector will be non-empty. */ const std::vector<const Type*> getArgTypes() const; @@ -154,14 +135,13 @@ public: 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<const Type*>& argTypes, + /** Construct a function type associated with nodeManager, + * 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(const std::vector<const Type*>& argTypes, const Type* range); /** Destructor */ @@ -173,25 +153,23 @@ private: /** The result type. */ const Type* d_rangeType; + friend class NodeManager; }; /** Class encapsulating the kind type (the type of types). - TODO: Should be a singleton per-ExprManager. */ class KindType : public Type { public: - - /** Create a type associated with exprManager. */ - static KindType* getInstance(); - /** Is this the kind type? (Returns true.) */ bool isKind() const; + /** Get an instance of the kind type. */ + static KindType* getInstance(); + private: - /** Create a type associated with exprManager. */ KindType(); /* Do-nothing private copy constructor, to prevent @@ -210,17 +188,19 @@ private: }; /** Class encapsulating a user-defined sort. - TODO: Should sort be uniquely named per-exprManager and not conflict + TODO: Should sort be uniquely named per-nodeManager and not conflict with any builtins? */ class SortType : public Type { public: - - /** Create a sort associated with exprManager with the given name. */ - SortType(ExprManager* exprManager, std::string name); - /** Destructor */ ~SortType(); + +private: + /** Create a sort with the given name. */ + SortType(std::string name); + + friend class NodeManager; }; /** |