3 files changed, 23 insertions, 5 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 86efac2f0..bcf787f6b 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -265,12 +265,19 @@ constant UNINTERPRETED_CONSTANT \
     ::CVC4::UninterpretedConstant \
     ::CVC4::UninterpretedConstantHashFunction \
     "util/uninterpreted_constant.h" \
-    "The kind of nodes representing uninterpreted constants"
+    "The kind of expressions representing uninterpreted constants"
 typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule
 enumerator SORT_TYPE \
     ::CVC4::theory::builtin::UninterpretedSortEnumerator \
     "theory/builtin/type_enumerator.h"
 
+constant ABSTRACT_VALUE \
+    ::CVC4::AbstractValue \
+    ::CVC4::AbstractValueHashFunction \
+    "util/abstract_value.h" \
+    "The kind of expressions representing abstract values (other than uninterpreted sort constants)"
+typerule ABSTRACT_VALUE ::CVC4::theory::builtin::AbstractValueTypeRule
+
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
 # not stored that way.  If you ask for the operator of (EQUAL a b),
@@ -279,7 +286,7 @@ constant BUILTIN \
     ::CVC4::Kind \
     ::CVC4::kind::KindHashFunction \
     "expr/kind.h" \
-    "The kind of nodes representing built-in operators"
+    "The kind of expressions representing built-in operators"
 
 variable FUNCTION "function"
 parameterized APPLY FUNCTION 0: "defined function application"
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index a2e8e8179..3cd2f6282 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -150,6 +150,17 @@ public:
   }
 };/* class UninterpretedConstantTypeRule */
 
+class AbstractValueTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    // An UnknownTypeException means that this node has no type.  For now,
+    // only abstract values are like this.  Assigning them a type in all
+    // cases is difficult, since then the parser and the SmtEngine must be
+    // more tightly coupled.
+    throw UnknownTypeException(n);
+  }
+};/* class AbstractValueTypeRule */
+
 class StringConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index b5f846735..fa4acf3fb 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -2,10 +2,10 @@
 /*! \file substitutions.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: barrett
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing