From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 25 Feb 2010 22:32:03 +0000 (+0000)
Subject: Adding Node::getOperator()
X-Git-Tag: cvc5-1.0.0~9220
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bfab2bde219a0cda230fb2f26d89d123918a219f;p=cvc5.git

Adding Node::getOperator()
Removing references to ExprManager from Type, moving Type creation into NodeManager
---

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
@@ -222,6 +222,74 @@ template<bool ref_count>
       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<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);