Adding Node::getOperator()

Removing references to ExprManager from Type, moving Type creation into NodeManager

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;
 };
 
 /**