From bfab2bde219a0cda230fb2f26d89d123918a219f Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 25 Feb 2010 22:32:03 +0000 Subject: [PATCH] Adding Node::getOperator() Removing references to ExprManager from Type, moving Type creation into NodeManager --- src/expr/expr_manager.cpp | 15 +++--- src/expr/expr_manager.h | 7 +-- src/expr/kind_prologue.h | 2 + src/expr/node.h | 68 +++++++++++++++++++++++++ src/expr/node_manager.cpp | 1 - src/expr/node_manager.h | 45 +++++++++++++++++ src/expr/type.cpp | 53 ++++---------------- src/expr/type.h | 68 +++++++++---------------- test/unit/expr/node_black.h | 98 ++++++++++++++++++++++--------------- 9 files changed, 218 insertions(+), 139 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& 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 @@ -222,6 +222,74 @@ template return d_nv->getId(); } + /** + * 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 getOperator() const { + switch(getKind()) { + case kind::APPLY: + /* The operator is the first child. */ + return NodeTemplate (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 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& 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 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& 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 @@ -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("")) { -} - -Type::Type(ExprManager* exprManager, std::string name) : - d_exprManager(exprManager), d_name(name) { +Type::Type() : + d_name(std::string("")) { } 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& argTypes, +FunctionType::FunctionType(const std::vector& 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 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; } @@ -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& argTypes, - const Type* range); - - /** Retrieve the argument types. The vector will be non-empty. */ const std::vector 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& 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& 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; }; /** diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 4731810ea..90358a622 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -18,6 +18,7 @@ //Used in some of the tests #include +#include "expr/expr_manager.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" @@ -30,19 +31,19 @@ using namespace std; class NodeBlack : public CxxTest::TestSuite { private: + NodeManager *d_nodeManager; NodeManagerScope *d_scope; - NodeManager *d_nm; public: void setUp() { - d_nm = new NodeManager(); - d_scope = new NodeManagerScope(d_nm); + d_nodeManager = new NodeManager(); + d_scope = new NodeManagerScope(d_nodeManager); } void tearDown() { delete d_scope; - delete d_nm; + delete d_nodeManager; } bool imp(bool a, bool b) const { @@ -88,12 +89,12 @@ public: void testOperatorEquals() { Node a, b, c; - b = d_nm->mkVar(); + b = d_nodeManager->mkVar(); a = b; c = a; - Node d = d_nm->mkVar(); + Node d = d_nodeManager->mkVar(); TS_ASSERT(a==a); TS_ASSERT(a==b); @@ -128,12 +129,12 @@ public: Node a, b, c; - b = d_nm->mkVar(); + b = d_nodeManager->mkVar(); a = b; c = a; - Node d = d_nm->mkVar(); + Node d = d_nodeManager->mkVar(); /*structed assuming operator == works */ TS_ASSERT(iff(a!=a,!(a==a))); @@ -168,9 +169,9 @@ public: #endif /* CVC4_ASSERTIONS */ //Basic access check - Node tb = d_nm->mkNode(TRUE); - Node eb = d_nm->mkNode(FALSE); - Node cnd = d_nm->mkNode(XOR, tb, eb); + Node tb = d_nodeManager->mkNode(TRUE); + Node eb = d_nodeManager->mkNode(FALSE); + Node cnd = d_nodeManager->mkNode(XOR, tb, eb); Node ite = cnd.iteNode(tb,eb); TS_ASSERT(tb == cnd[0]); @@ -190,7 +191,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nm->mkNode(NOT); + Node c = d_nodeManager->mkNode(NOT); b = c; TS_ASSERT(b==c); @@ -208,14 +209,14 @@ public: */ - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); + Node a = d_nodeManager->mkVar(); + Node b = d_nodeManager->mkVar(); TS_ASSERT(amkNode(NULL_EXPR); - Node d = d_nm->mkNode(NULL_EXPR); + Node c = d_nodeManager->mkNode(NULL_EXPR); + Node d = d_nodeManager->mkNode(NULL_EXPR); TS_ASSERT(!(cmkNode(TRUE); - Node parent = d_nm->mkNode(NOT, child); + Node child = d_nodeManager->mkNode(TRUE); + Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); //Slightly less simple test of DD property. std::vector chain; int N = 500; - Node curr = d_nm->mkNode(NULL_EXPR); + Node curr = d_nodeManager->mkNode(NULL_EXPR); for(int i=0;imkNode(AND,curr); + curr = d_nodeManager->mkNode(AND,curr); } for(int i=0;imkNode(ITE); - Node b = d_nm->mkNode(ITE); + Node a = d_nodeManager->mkNode(ITE); + Node b = d_nodeManager->mkNode(ITE); TS_ASSERT(b.hash() == a.hash()); } @@ -265,8 +266,8 @@ public: void testEqNode() { /*Node eqNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.eqNode(right); @@ -280,7 +281,7 @@ public: void testNotNode() { /* Node notNode() const;*/ - Node child = d_nm->mkNode(TRUE); + Node child = d_nodeManager->mkNode(TRUE); Node parent = child.notNode(); TS_ASSERT(NOT == parent.getKind()); @@ -292,8 +293,8 @@ public: void testAndNode() { /*Node andNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.andNode(right); @@ -308,8 +309,8 @@ public: void testOrNode() { /*Node orNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.orNode(right); @@ -324,9 +325,9 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node cnd = d_nm->mkNode(PLUS); - Node thenBranch = d_nm->mkNode(TRUE); - Node elseBranch = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node cnd = d_nodeManager->mkNode(PLUS); + Node thenBranch = d_nodeManager->mkNode(TRUE); + Node elseBranch = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node ite = cnd.iteNode(thenBranch,elseBranch); @@ -341,8 +342,8 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.iffNode(right); @@ -356,8 +357,8 @@ public: void testImpNode() { /* Node impNode(const Node& right) const; */ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.impNode(right); @@ -370,8 +371,8 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ - Node left = d_nm->mkNode(TRUE); - Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node left = d_nodeManager->mkNode(TRUE); + Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); Node eq = left.xorNode(right); @@ -383,7 +384,7 @@ public: } void testKindSingleton(Kind k) { - Node n = d_nm->mkNode(k); + Node n = d_nodeManager->mkNode(k); TS_ASSERT(k == n.getKind()); } @@ -395,6 +396,25 @@ public: testKindSingleton(ITE); testKindSingleton(SKOLEM); } + + + void testGetOperator() { + const Type* sort = d_nodeManager->mkSort("T"); + const Type* booleanType = d_nodeManager->booleanType(); + const Type* predType = d_nodeManager->mkFunctionType(sort,booleanType); + + Node f = d_nodeManager->mkVar(predType); + Node a = d_nodeManager->mkVar(booleanType); + Node fa = d_nodeManager->mkNode(kind::APPLY,f,a); + + TS_ASSERT( fa.hasOperator() ); + TS_ASSERT( !f.hasOperator() ); + TS_ASSERT( !a.hasOperator() ); + + TS_ASSERT( f == fa.getOperator() ); + TS_ASSERT_THROWS( f.getOperator(), AssertionException ); + TS_ASSERT_THROWS( a.getOperator(), AssertionException ); + } void testNaryExpForSize(Kind k, int N){ NodeBuilder<> nbz(k); -- 2.30.2