summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_manager.cpp15
-rw-r--r--src/expr/expr_manager.h7
-rw-r--r--src/expr/kind_prologue.h2
-rw-r--r--src/expr/node.h68
-rw-r--r--src/expr/node_manager.cpp1
-rw-r--r--src/expr/node_manager.h45
-rw-r--r--src/expr/type.cpp53
-rw-r--r--src/expr/type.h68
-rw-r--r--test/unit/expr/node_black.h98
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<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;
};
/**
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 <vector>
+#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(a<b || b<a);
TS_ASSERT(!(a<b && b<a));
- Node c = d_nm->mkNode(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(!(c<d));
TS_ASSERT(!(d<c));
@@ -228,18 +229,18 @@ public:
*/
//Simple test of descending descendant property
- Node child = d_nm->mkNode(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<Node> chain;
int N = 500;
- Node curr = d_nm->mkNode(NULL_EXPR);
+ Node curr = d_nodeManager->mkNode(NULL_EXPR);
for(int i=0;i<N;i++) {
chain.push_back(curr);
- curr = d_nm->mkNode(AND,curr);
+ curr = d_nodeManager->mkNode(AND,curr);
}
for(int i=0;i<N;i++) {
@@ -254,8 +255,8 @@ public:
void testHash() {
/* Not sure how to test this except survial... */
- Node a = d_nm->mkNode(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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback