6 files changed, 73 insertions, 33 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 74641513b..6313aa30b 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -124,8 +124,6 @@ namespace theory {
 
 enum TheoryId {
 ${theory_enum}
-  THEORY_QUANTIFIERS,
-  THEORY_REWRITERULES,
   THEORY_LAST
 };
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 0cae68ed0..e113a1e8f 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -2,7 +2,7 @@
 #
 # mkexpr
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2011  The CVC4 Project
+# Copyright (c) 2010-2012  The CVC4 Project
 #
 # The purpose of this script is to create {expr,expr_manager}.{h,cpp}
 # from template files and a list of theory kinds.  Basically it just
@@ -15,7 +15,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2011
+copyright=2010-2012
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -95,6 +95,12 @@ function rewriter {
   check_theory_seen
 }
 
+function instantiator {
+  # instantiator class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function properties {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkkind b/src/expr/mkkind
index abb238f1a..2f361cb63 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -2,7 +2,7 @@
 #
 # mkkind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2011  The CVC4 Project
+# Copyright (c) 2010-2012  The CVC4 Project
 #
 # The purpose of this script is to create kind.h (and also
 # type_properties.h) from a template and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2011
+copyright=2010-2012
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -105,6 +105,12 @@ function theory {
 "
 }
 
+function instantiator {
+  # instantiator class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function properties {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index d84691e14..2e94e41be 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -2,7 +2,7 @@
 #
 # mkmetakind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2011  The CVC4 Project
+# Copyright (c) 2010-2012  The CVC4 Project
 #
 # The purpose of this script is to create metakind.h from a template
 # and a list of theory kinds.
@@ -17,7 +17,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2011
+copyright=2010-2012
 
 cat <<EOF
 /*********************                                                        */
@@ -80,6 +80,12 @@ function theory {
 // #include \"theory/$b/$2\""
 }
 
+function instantiator {
+  # instantiator class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function properties {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/node.h b/src/expr/node.h
index a61944433..e56774d7e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -159,6 +159,14 @@ namespace kind {
   }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
 
+// for hash_maps, hash_sets..
+struct NodeHashFunction {
+  inline size_t operator()(Node node) const;
+};/* struct NodeHashFunction */
+struct TNodeHashFunction {
+  inline size_t operator()(TNode node) const;
+};/* struct TNodeHashFunction */
+
 /**
  * Encapsulation of an NodeValue pointer.  The reference count is
  * maintained in the NodeValue if ref_count is true.
@@ -166,17 +174,6 @@ namespace kind {
  */
 template <bool ref_count>
 class NodeTemplate {
-
-  // for hash_maps, hash_sets..
-  template <bool ref_count1>
-  struct HashFunction {
-    size_t operator()(CVC4::NodeTemplate<ref_count1> node) const {
-      return (size_t) node.getId();
-    }
-  };/* struct HashFunction */
-
-  typedef HashFunction<false> TNodeHashFunction;
-
   /**
    * The NodeValue has access to the private constructors, so that the
    * iterators can can create new nodes.
@@ -233,7 +230,7 @@ class NodeTemplate {
       Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
     }
   }
-
+public:
   /**
    * Cache-aware, recursive version of substitute() used by the public
    * member function with a similar signature.
@@ -904,19 +901,12 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) {
 
 namespace CVC4 {
 
-// for hash_maps, hash_sets..
-struct NodeHashFunction {
-  size_t operator()(CVC4::Node node) const {
-    return (size_t) node.getId();
-  }
-};/* struct NodeHashFunction */
-
-// for hash_maps, hash_sets..
-struct TNodeHashFunction {
-  size_t operator()(CVC4::TNode node) const {
-    return (size_t) node.getId();
-  }
-};/* struct TNodeHashFunction */
+inline size_t NodeHashFunction::operator()(Node node) const {
+  return node.getId();
+}
+inline size_t TNodeHashFunction::operator()(TNode node) const {
+  return node.getId();
+}
 
 struct TNodePairHashFunction {
   size_t operator()(const std::pair<CVC4::TNode, CVC4::TNode>& pair ) const {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 00fe6baa8..e763a1f10 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -362,6 +362,9 @@ public:
   /** Create a skolem constant with the given type. */
   Node mkSkolem(const TypeNode& type);
 
+  /** Create a instantiation constant with the given type. */
+  Node mkInstConstant(const TypeNode& type);
+
   /**
    * Create a constant of type T.  It will have the appropriate
    * CONST_* kind defined for T.
@@ -579,6 +582,15 @@ public:
   /** Get the (singleton) type for sorts. */
   inline TypeNode kindType();
 
+  /** Get the bound var list type. */
+  inline TypeNode boundVarListType();
+
+  /** Get the instantiation pattern type. */
+  inline TypeNode instPatternType();
+
+  /** Get the instantiation pattern type. */
+  inline TypeNode instPatternListType();
+
   /**
    * Get the (singleton) type for builtin operators (that is, the type
    * of the Node returned from Node::getOperator() when the operator
@@ -897,6 +909,21 @@ inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
 }
 
+/** Get the bound var list type. */
+inline TypeNode NodeManager::boundVarListType(){
+  return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
+}
+
+/** Get the instantiation pattern type. */
+inline TypeNode NodeManager::instPatternType(){
+  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
+}
+
+/** Get the instantiation pattern type. */
+inline TypeNode NodeManager::instPatternListType(){
+  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
+}
+
 /** Get the (singleton) type for builtin operators. */
 inline TypeNode NodeManager::builtinOperatorType() {
   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
@@ -1366,6 +1393,13 @@ inline Node NodeManager::mkSkolem(const TypeNode& type) {
   return n;
 }
 
+inline Node NodeManager::mkInstConstant(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   return mkConstInternal<Node, T>(val);