Unify abstract values and uninterpreted constantsabstractVals

This commit unifies abstract values and "uninterpreted constants" into a
single kind. Note that "uninterpreted constants" is a bit of a misnomer
in the context of the new API, since they do not correspond to the
equivalent of a `declare-const` command, but instead are values for
symbols of an uninterpreted sort (and thus special cases of abstract
values). Instead of treating "uninterpreted constants" as a separate
kind, this commit extends abstract values to hold a type (instead of
marking their type via attribute in `NodeManager::mkAbstractValue()`)
and uses the type of the abstract values to determine whether they are a
value for a constant of uninterpreted sort or not. Unifying these
representations simplifies code and brings the terminology more in line
with the SMT-LIB standard.

This commit also updates the APIs to remove support for creating
abstract values and "uninterpreted constants". Users should never create
those. They can only be returned as a value for a term after a
satisfiability check.

Finally, the commit removes code in the parser for parsing abstract
values and updates the code for getting values involving abstract
values. Since the parser does not allow the declaration/definition of
abstract values, and determining whether a symbol is an abstract value
was broken (not all symbols starting with an `@` are abstract values),
the code was effectively dead. Getting values involving "uninterpreted
constants" now no longer requires parsing the string of the values, but
instead, we can use existing API functionality.

45 files changed, 162 insertions, 804 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 778f700c0..3efcf491f 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -54,7 +54,6 @@
 #include "expr/node_manager.h"
 #include "expr/sequence.h"
 #include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/option_exception.h"
@@ -108,7 +107,6 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND},
     {NULL_EXPR, cvc5::Kind::NULL_EXPR},
     /* Builtin ------------------------------------------------------------- */
-    {UNINTERPRETED_CONSTANT, cvc5::Kind::UNINTERPRETED_CONSTANT},
     {ABSTRACT_VALUE, cvc5::Kind::ABSTRACT_VALUE},
     {EQUAL, cvc5::Kind::EQUAL},
     {DISTINCT, cvc5::Kind::DISTINCT},
@@ -387,7 +385,6 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
         {cvc5::Kind::NULL_EXPR, NULL_EXPR},
         /* Builtin --------------------------------------------------------- */
-        {cvc5::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
         {cvc5::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
         {cvc5::Kind::EQUAL, EQUAL},
         {cvc5::Kind::DISTINCT, DISTINCT},
@@ -3103,7 +3100,9 @@ std::string Term::getAbstractValue() const
       << "Term to be an abstract value when calling "
          "getAbstractValue()";
   //////// all checks before this line
-  return d_node->getConst<AbstractValue>().getIndex().toString();
+  std::stringstream ss;
+  ss << d_node->getConst<AbstractValue>();
+  return ss.str();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -3309,31 +3308,6 @@ std::vector<Term> Term::getSequenceValue() const
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Term::isUninterpretedValue() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  //////// all checks before this line
-  return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT;
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-std::pair<Sort, std::int32_t> Term::getUninterpretedValue() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_ARG_CHECK_EXPECTED(
-      d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node)
-      << "Term to be an uninterpreted value when calling "
-         "getUninterpretedValue()";
-  //////// all checks before this line
-  const auto& uc = d_node->getConst<UninterpretedConstant>();
-  return std::make_pair(Sort(d_solver, uc.getType()),
-                        uc.getIndex().toUnsignedInt());
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
   out << t.toString();
@@ -5983,46 +5957,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_SOLVER_CHECK_SORT(sort);
-  //////// all checks before this line
-  return mkValHelper<cvc5::UninterpretedConstant>(
-      cvc5::UninterpretedConstant(*sort.d_type, index));
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkAbstractValue(const std::string& index) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
-
-  cvc5::Integer idx(index, 10);
-  CVC5_API_ARG_CHECK_EXPECTED(idx > 0, index)
-      << "a string representing an integer > 0";
-  //////// all checks before this line
-  return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx)));
-  // do not call getType(), for abstract values, type can not be computed
-  // until it is substituted away
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkAbstractValue(uint64_t index) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
-  //////// all checks before this line
-  return Term(this,
-              getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index))));
-  // do not call getType(), for abstract values, type can not be computed
-  // until it is substituted away
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 5e0f0d834..28d5cb1c9 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1469,19 +1469,6 @@ class CVC5_EXPORT Term
    */
   std::vector<Term> getSequenceValue() const;
 
-  /**
-   * @return true if the term is a value from an uninterpreted sort.
-   */
-  bool isUninterpretedValue() const;
-  /**
-  bool @return() const;
-   * Asserts isUninterpretedValue().
-   * @return the representation of an uninterpreted value as a pair of its
-  sort and its
-   * index.
-   */
-  std::pair<Sort, int32_t> getUninterpretedValue() const;
-
  protected:
   /**
    * The associated solver object.
@@ -3550,27 +3537,6 @@ class CVC5_EXPORT Solver
   Term mkRoundingMode(RoundingMode rm) const;
 
   /**
-   * Create uninterpreted constant.
-   * @param sort Sort of the constant
-   * @param index Index of the constant
-   */
-  Term mkUninterpretedConst(const Sort& sort, int32_t index) const;
-
-  /**
-   * Create an abstract value constant.
-   * The given index needs to be a positive integer in base 10.
-   * @param index Index of the abstract value
-   */
-  Term mkAbstractValue(const std::string& index) const;
-
-  /**
-   * Create an abstract value constant.
-   * The given index needs to be positive.
-   * @param index Index of the abstract value
-   */
-  Term mkAbstractValue(uint64_t index) const;
-
-  /**
    * Create a floating-point constant.
    * @param exp Size of the exponent
    * @param sig Size of the significand
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 0ff05022f..69daa1720 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -64,18 +64,7 @@ enum CVC5_EXPORT Kind : int32_t
   /* Builtin --------------------------------------------------------------- */
 
   /**
-   * Uninterpreted constant.
-   *
-   * Parameters:
-   *   - 1: Sort of the constant
-   *   - 2: Index of the constant
-   *
-   * Create with:
-   *   - `Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const`
-   */
-  UNINTERPRETED_CONSTANT,
-  /**
-   * Abstract value (other than uninterpreted sort constants).
+   * Abstract value.
    *
    * Parameters:
    *   - 1: Index of the abstract value
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index b0bee500c..ad3111457 100644
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -1118,45 +1118,6 @@ public class Solver implements IPointer
   private native long mkRoundingMode(long pointer, int rm);
 
   /**
-   * Create uninterpreted constant.
-   * @param sort Sort of the constant
-   * @param index Index of the constant
-   */
-  public Term mkUninterpretedConst(Sort sort, int index) throws CVC5ApiException
-  {
-    Utils.validateUnsigned(index, "index");
-    long termPointer = mkUninterpretedConst(pointer, sort.getPointer(), index);
-    return new Term(this, termPointer);
-  }
-
-  private native long mkUninterpretedConst(long pointer, long sortPointer, int index);
-
-  /**
-   * Create an abstract value constant.
-   * @param index Index of the abstract value
-   */
-  public Term mkAbstractValue(String index)
-  {
-    long termPointer = mkAbstractValue(pointer, index);
-    return new Term(this, termPointer);
-  }
-
-  private native long mkAbstractValue(long pointer, String index);
-
-  /**
-   * Create an abstract value constant.
-   * @param index Index of the abstract value
-   */
-  public Term mkAbstractValue(long index) throws CVC5ApiException
-  {
-    Utils.validateUnsigned(index, "index");
-    long termPointer = mkAbstractValue(pointer, index);
-    return new Term(this, termPointer);
-  }
-
-  private native long mkAbstractValue(long pointer, long index);
-
-  /**
    * Create a floating-point constant.
    * @param exp Size of the exponent
    * @param sig Size of the significand
diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java
index e2c719098..7dcf7663a 100644
--- a/src/api/java/cvc5/Term.java
+++ b/src/api/java/cvc5/Term.java
@@ -620,32 +620,6 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
 
   private native long[] getSequenceValue(long pointer);
 
-  /**
-   * @return true if the term is a value from an uninterpreted sort.
-   */
-  public boolean isUninterpretedValue()
-  {
-    return isUninterpretedValue(pointer);
-  }
-
-  private native boolean isUninterpretedValue(long pointer);
-
-  /**
-  boolean @return()
-   * Asserts isUninterpretedValue().
-   * @return the representation of an uninterpreted value as a pair of its
-  sort and its
-   * index.
-   */
-  public Pair<Sort, Integer> getUninterpretedValue()
-  {
-    Pair<Long, Integer> pair = getUninterpretedValue(pointer);
-    Sort sort = new Sort(solver, pair.first);
-    return new Pair<Sort, Integer>(sort, pair.second);
-  }
-
-  private native Pair<Long, Integer> getUninterpretedValue(long pointer);
-
   public class ConstIterator implements Iterator<Term>
   {
     private int currentIndex;
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
index c28ea412f..bcff5ebda 100644
--- a/src/api/java/jni/cvc5_Solver.cpp
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -1277,58 +1277,6 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRoundingMode(JNIEnv* env,
 
 /*
  * Class:     cvc5_Solver
- * Method:    mkUninterpretedConst
- * Signature: (JJI)J
- */
-JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedConst(
-    JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Sort* sort = reinterpret_cast<Sort*>(sortPointer);
-  Term* retPointer =
-      new Term(solver->mkUninterpretedConst(*sort, (int32_t)index));
-  return reinterpret_cast<jlong>(retPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
-/*
- * Class:     cvc5_Solver
- * Method:    mkAbstractValue
- * Signature: (JLjava/lang/String;)J
- */
-JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JLjava_lang_String_2(
-    JNIEnv* env, jobject, jlong pointer, jstring jIndex)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Solver* solver = reinterpret_cast<Solver*>(pointer);
-  const char* s = env->GetStringUTFChars(jIndex, nullptr);
-  std::string cIndex(s);
-  Term* retPointer = new Term(solver->mkAbstractValue(cIndex));
-  env->ReleaseStringUTFChars(jIndex, s);
-  return reinterpret_cast<jlong>(retPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
-/*
- * Class:     cvc5_Solver
- * Method:    mkAbstractValue
- * Signature: (JJ)J
- */
-JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JJ(JNIEnv* env,
-                                                             jobject,
-                                                             jlong pointer,
-                                                             jlong index)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkAbstractValue((uint64_t)index));
-  return reinterpret_cast<jlong>(retPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
-/*
- * Class:     cvc5_Solver
  * Method:    mkFloatingPoint
  * Signature: (JIIJ)J
  */
@@ -2591,4 +2539,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env,
   DatatypeDecl* ret = new DatatypeDecl();
   return reinterpret_cast<jlong>(ret);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
\ No newline at end of file
+}
diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp
index 325a9c744..8e43d0afb 100644
--- a/src/api/java/jni/cvc5_Term.cpp
+++ b/src/api/java/jni/cvc5_Term.cpp
@@ -856,60 +856,6 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSequenceValue(JNIEnv* env,
 
 /*
  * Class:     cvc5_Term
- * Method:    isUninterpretedValue
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL Java_cvc5_Term_isUninterpretedValue(JNIEnv* env,
-                                                               jobject,
-                                                               jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Term* current = reinterpret_cast<Term*>(pointer);
-  return static_cast<jboolean>(current->isUninterpretedValue());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
-/*
- * Class:     cvc5_Term
- * Method:    getUninterpretedValue
- * Signature: (J)Lcvc5/Pair;
- */
-JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env,
-                                                               jobject,
-                                                               jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Term* current = reinterpret_cast<Term*>(pointer);
-  std::pair<Sort, std::int32_t> value = current->getUninterpretedValue();
-
-  Sort* sort = new Sort(value.first);
-  jlong sortPointer = reinterpret_cast<jlong>(sort);
-
-  // Long longObject = new Long(pointer)
-  jclass longClass = env->FindClass("Ljava/lang/Long;");
-  jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
-  jobject longObject = env->NewObject(longClass, longConstructor, sortPointer);
-
-  // Integer integerObject = new Integer(pair.second)
-  jclass integerClass = env->FindClass("Ljava/lang/Integer;");
-  jmethodID integerConstructor =
-      env->GetMethodID(integerClass, "<init>", "(I)V");
-  jobject integerObject = env->NewObject(
-      integerClass, integerConstructor, static_cast<jint>(value.second));
-
-  // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
-  jclass pairClass = env->FindClass("Lcvc5/Pair;");
-  jmethodID pairConstructor = env->GetMethodID(
-      pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
-  jobject pair =
-      env->NewObject(pairClass, pairConstructor, longObject, integerObject);
-
-  return pair;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
-/*
- * Class:     cvc5_Term
  * Method:    iterator
  * Signature: (J)J
  */
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ef9971c20..99747f8b7 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -237,7 +237,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkPosZero(uint32_t exp, uint32_t sig) except +
         Term mkNegZero(uint32_t exp, uint32_t sig) except +
         Term mkRoundingMode(RoundingMode rm) except +
-        Term mkUninterpretedConst(Sort sort, int32_t index) except +
         Term mkAbstractValue(const string& index) except +
         Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except +
         Term mkConst(Sort sort, const string& symbol) except +
@@ -430,8 +429,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         set[Term] getSetValue() except +
         bint isSequenceValue() except +
         vector[Term] getSequenceValue() except +
-        bint isUninterpretedValue() except +
-        pair[Sort, int32_t] getUninterpretedValue() except +
         bint isTupleValue() except +
         vector[Term] getTupleValue() except +
 
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 2a35363ea..c65c8e606 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1345,32 +1345,6 @@ cdef class Solver:
         term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
         return term
 
-    def mkUninterpretedConst(self, Sort sort, int index):
-        """Create uninterpreted constant.
-
-        :param sort: Sort of the constant
-        :param index: Index of the constant
-        """
-        cdef Term term = Term(self)
-        term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
-        return term
-
-    def mkAbstractValue(self, index):
-        """
-        Create an abstract value constant.
-        The given index needs to be positive.
-
-        :param index: Index of the abstract value
-        """
-        cdef Term term = Term(self)
-        try:
-            term.cterm = self.csolver.mkAbstractValue(str(index).encode())
-        except:
-            raise ValueError(
-                "mkAbstractValue expects a str representing a number"
-                " or an int, but got{}".format(index))
-        return term
-
     def mkFloatingPoint(self, int exp, int sig, Term val):
         """Create a floating-point constant.
 
@@ -2642,16 +2616,6 @@ cdef class Term:
             elems.append(term)
         return elems
 
-    def isUninterpretedValue(self):
-        return self.cterm.isUninterpretedValue()
-
-    def getUninterpretedValue(self):
-        cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue()
-        cdef Sort sort = Sort(self.solver)
-        sort.csort = p.first
-        i = p.second
-        return (sort, i)
-
     def isTupleValue(self):
         return self.cterm.isTupleValue()
 
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index e73960676..90a01109d 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -93,8 +93,6 @@ libcvc5_add_sources(
   subs.h
   sygus_datatype.cpp
   sygus_datatype.h
-  uninterpreted_constant.cpp
-  uninterpreted_constant.h
 )
 
 libcvc5_add_sources(GENERATED
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a9e5854b0..60f076057 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1105,9 +1105,7 @@ Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m)
 }
 
 Node NodeManager::mkAbstractValue(const TypeNode& type) {
-  Node n = mkConst(AbstractValue(++d_abstractValueCount));
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
+  Node n = mkConst(AbstractValue(type, ++d_abstractValueCount));
   return n;
 }
 
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
deleted file mode 100644
index ef354568d..000000000
--- a/src/expr/uninterpreted_constant.cpp
+++ /dev/null
@@ -1,97 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andres Noetzli, Andrew Reynolds, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Representation of constants of uninterpreted sorts.
- */
-
-#include "expr/uninterpreted_constant.h"
-
-#include <algorithm>
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "base/check.h"
-#include "expr/type_node.h"
-
-using namespace std;
-
-namespace cvc5 {
-
-UninterpretedConstant::UninterpretedConstant(const TypeNode& type,
-                                             Integer index)
-    : d_type(new TypeNode(type)), d_index(index)
-{
-  //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
-  PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
-}
-
-UninterpretedConstant::~UninterpretedConstant() {}
-
-UninterpretedConstant::UninterpretedConstant(const UninterpretedConstant& other)
-    : d_type(new TypeNode(other.getType())), d_index(other.getIndex())
-{
-}
-
-const TypeNode& UninterpretedConstant::getType() const { return *d_type; }
-const Integer& UninterpretedConstant::getIndex() const { return d_index; }
-bool UninterpretedConstant::operator==(const UninterpretedConstant& uc) const
-{
-  return getType() == uc.getType() && d_index == uc.d_index;
-}
-bool UninterpretedConstant::operator!=(const UninterpretedConstant& uc) const
-{
-  return !(*this == uc);
-}
-
-bool UninterpretedConstant::operator<(const UninterpretedConstant& uc) const
-{
-  return getType() < uc.getType()
-         || (getType() == uc.getType() && d_index < uc.d_index);
-}
-bool UninterpretedConstant::operator<=(const UninterpretedConstant& uc) const
-{
-  return getType() < uc.getType()
-         || (getType() == uc.getType() && d_index <= uc.d_index);
-}
-bool UninterpretedConstant::operator>(const UninterpretedConstant& uc) const
-{
-  return !(*this <= uc);
-}
-bool UninterpretedConstant::operator>=(const UninterpretedConstant& uc) const
-{
-  return !(*this < uc);
-}
-
-std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
-  std::stringstream ss;
-  ss << uc.getType();
-  std::string st(ss.str());
-  // must remove delimiting quotes from the name of the type
-  // this prevents us from printing symbols like |@uc_|T|_n|
-  std::string q("|");
-  size_t pos;
-  while ((pos = st.find(q)) != std::string::npos)
-  {
-    st.replace(pos, 1, "");
-  }
-  return out << "uc_" << st.c_str() << "_" << uc.getIndex();
-}
-
-size_t UninterpretedConstantHashFunction::operator()(
-    const UninterpretedConstant& uc) const
-{
-  return std::hash<TypeNode>()(uc.getType())
-         * IntegerHashFunction()(uc.getIndex());
-}
-
-}  // namespace cvc5
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
deleted file mode 100644
index 4a86ba510..000000000
--- a/src/expr/uninterpreted_constant.h
+++ /dev/null
@@ -1,64 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andres Noetzli, Morgan Deters, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Representation of constants of uninterpreted sorts.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__UNINTERPRETED_CONSTANT_H
-#define CVC5__UNINTERPRETED_CONSTANT_H
-
-#include <iosfwd>
-#include <memory>
-
-#include "util/integer.h"
-
-namespace cvc5 {
-
-class TypeNode;
-
-class UninterpretedConstant
-{
- public:
-  UninterpretedConstant(const TypeNode& type, Integer index);
-  ~UninterpretedConstant();
-
-  UninterpretedConstant(const UninterpretedConstant& other);
-
-  const TypeNode& getType() const;
-  const Integer& getIndex() const;
-  bool operator==(const UninterpretedConstant& uc) const;
-  bool operator!=(const UninterpretedConstant& uc) const;
-  bool operator<(const UninterpretedConstant& uc) const;
-  bool operator<=(const UninterpretedConstant& uc) const;
-  bool operator>(const UninterpretedConstant& uc) const;
-  bool operator>=(const UninterpretedConstant& uc) const;
-
- private:
-  std::unique_ptr<TypeNode> d_type;
-  const Integer d_index;
-}; /* class UninterpretedConstant */
-
-std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc);
-
-/**
- * Hash function for the BitVector constants.
- */
-struct UninterpretedConstantHashFunction
-{
-  size_t operator()(const UninterpretedConstant& uc) const;
-}; /* struct UninterpretedConstantHashFunction */
-
-}  // namespace cvc5
-
-#endif /* CVC5__UNINTERPRETED_CONSTANT_H */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 9f34b5647..ac4935a99 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -751,18 +751,7 @@ void Parser::pushGetValueScope()
     std::vector<api::Term> elements = d_solver->getModelDomainElements(s);
     for (const api::Term& e : elements)
     {
-      // Uninterpreted constants are abstract values, which by SMT-LIB are
-      // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo).
-      // Thus, the element is not printed simply as its name.
-      std::string en = e.toString();
-      size_t index = en.find("(as ");
-      if (index == 0)
-      {
-        index = en.find(" ", 4);
-        en = en.substr(4, index - 4);
-      }
-      Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl;
-      defineVar(en, e);
+      defineVar(e.getAbstractValue(), e);
     }
   }
 }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e1ce29b65..203be81b9 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -325,16 +325,6 @@ bool Smt2::logicIsSet() {
   return d_logicSet;
 }
 
-api::Term Smt2::getExpressionForNameAndType(const std::string& name,
-                                            api::Sort t)
-{
-  if (isAbstractValue(name))
-  {
-    return mkAbstractValue(name);
-  }
-  return Parser::getExpressionForNameAndType(name, t);
-}
-
 bool Smt2::getTesterName(api::Term cons, std::string& name)
 {
   if ((v2_6() || sygus()) && strictModeEnabled())
@@ -832,13 +822,6 @@ bool Smt2::isAbstractValue(const std::string& name)
          && name.find_first_not_of("0123456789", 1) == std::string::npos;
 }
 
-api::Term Smt2::mkAbstractValue(const std::string& name)
-{
-  Assert(isAbstractValue(name));
-  // remove the '@'
-  return d_solver->mkAbstractValue(name.substr(1));
-}
-
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
 {
   Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 8d8f8febe..07cb01423 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -130,12 +130,6 @@ class Smt2 : public Parser
   api::Kind getIndexedOpKind(const std::string& name);
 
   /**
-   * Returns the expression that name should be interpreted as.
-   */
-  api::Term getExpressionForNameAndType(const std::string& name,
-                                        api::Sort t) override;
-
-  /**
    * If we are in a version < 2.6, this updates name to the tester name of cons,
    * e.g. "is-cons".
    */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1da2a3c7b..0d8b69acd 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -32,7 +32,6 @@
 #include "expr/node_manager_attributes.h"
 #include "expr/node_visitor.h"
 #include "expr/sequence.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/bv_options.h"
 #include "options/language.h"
 #include "options/printer_options.h"
@@ -48,6 +47,7 @@
 #include "theory/datatypes/tuple_project_op.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/theory_model.h"
+#include "util/abstract_value.h"
 #include "util/bitvector.h"
 #include "util/divisible.h"
 #include "util/floatingpoint.h"
@@ -323,11 +323,12 @@ void Smt2Printer::toStream(std::ostream& out,
       }
       break;
     }
-    
-    case kind::UNINTERPRETED_CONSTANT: {
-      const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
+
+    case kind::ABSTRACT_VALUE:
+    {
+      const AbstractValue& av = n.getConst<AbstractValue>();
       std::stringstream ss;
-      ss << "(as @" << uc << " " << n.getType() << ")";
+      ss << "(as " << av << " " << n.getType() << ")";
       out << ss.str();
       break;
     }
@@ -524,7 +525,7 @@ void Smt2Printer::toStream(std::ostream& out,
         out << ")";
       }
     }
-    else
+    else if (k != kind::ABSTRACT_VALUE)
     {
       // use type ascription
       out << "(as ";
diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp
index 56cb643db..fd62bf930 100644
--- a/src/smt/abstract_values.cpp
+++ b/src/smt/abstract_values.cpp
@@ -47,10 +47,7 @@ Node AbstractValues::mkAbstractValue(TNode n)
     val = d_nm->mkAbstractValue(n.getType());
     d_abstractValueMap.addSubstitution(val, n);
   }
-  // We are supposed to ascribe types to all abstract values that go out.
-  Node ascription = d_nm->mkConst(AscriptionType(n.getType()));
-  Node retval = d_nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val);
-  return retval;
+  return val;
 }
 
 }  // namespace smt
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index d4a8782b5..a3b51bcd5 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -264,24 +264,14 @@ well-founded SORT_TYPE \
     "::cvc5::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
     "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
 
-constant UNINTERPRETED_CONSTANT \
-    class \
-    UninterpretedConstant \
-    ::cvc5::UninterpretedConstantHashFunction \
-    "expr/uninterpreted_constant.h" \
-    "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)"
-typerule UNINTERPRETED_CONSTANT ::cvc5::theory::builtin::UninterpretedConstantTypeRule
-enumerator SORT_TYPE \
-    ::cvc5::theory::builtin::UninterpretedSortEnumerator \
-    "theory/builtin/type_enumerator.h"
-
 constant ABSTRACT_VALUE \
     class \
     AbstractValue \
     ::cvc5::AbstractValueHashFunction \
     "util/abstract_value.h" \
-    "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)"
+    "the kind of expressions representing abstract values; payload is an instance of the cvc5::AbstractValue class (used in models)"
 typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule
+enumerator SORT_TYPE ::cvc5::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index f3c595720..7064a3142 100644
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -17,18 +17,18 @@
 
 #include "expr/attribute.h"
 #include "expr/skolem_manager.h"
-#include "expr/uninterpreted_constant.h"
+#include "util/abstract_value.h"
 #include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
 namespace builtin {
 
-TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager,
-                                                    TNode n,
-                                                    bool check)
+TypeNode AbstractValueTypeRule::computeType(NodeManager* nodeManager,
+                                            TNode n,
+                                            bool check)
 {
-  return n.getConst<UninterpretedConstant>().getType();
+  return n.getConst<AbstractValue>().getType();
 }
 
 /**
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 54139c433..e966aa5f8 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -91,20 +91,9 @@ class SExprTypeRule {
   }
 };/* class SExprTypeRule */
 
-class UninterpretedConstantTypeRule {
- public:
-  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
-};/* 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---and then, only if they are created
-    // by the user and don't actually correspond to one that the SolverEngine
-    // gave them previously.
-    throw UnknownTypeException(n);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };/* class AbstractValueTypeRule */
 
 class LambdaTypeRule {
diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index 0ef1d3ec7..7c521346c 100644
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -16,6 +16,7 @@
 #include "theory/builtin/type_enumerator.h"
 
 #include "theory/builtin/theory_builtin_rewriter.h"
+#include "util/abstract_value.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 980792f94..81ab2bf5c 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -20,8 +20,8 @@
 
 #include "expr/kind.h"
 #include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
 #include "theory/type_enumerator.h"
+#include "util/abstract_value.h"
 #include "util/integer.h"
 
 namespace cvc5 {
@@ -58,8 +58,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE
     if(isFinished()) {
       throw NoMoreValuesException(getType());
     }
-    return NodeManager::currentNM()->mkConst(
-        UninterpretedConstant(getType(), d_count));
+    return NodeManager::currentNM()->mkConst(AbstractValue(getType(), d_count));
   }
 
   UninterpretedSortEnumerator& operator++() override
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index c446504fd..8c9ef2ec1 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -21,11 +21,11 @@
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/datatypes_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/datatypes/tuple_project_op.h"
+#include "util/abstract_value.h"
 #include "util/rational.h"
 
 using namespace cvc5;
@@ -729,7 +729,7 @@ Node DatatypesRewriter::collectRef(Node n,
       else
       {
         // a loop
-        const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
+        const Integer& i = n.getConst<AbstractValue>().getIndex();
         uint32_t index = i.toUnsignedInt();
         if (index >= sk.size())
         {
@@ -771,7 +771,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc(
     {
       int debruijn = depth - it->second - 1;
       return NodeManager::currentNM()->mkConst(
-          UninterpretedConstant(n.getType(), debruijn));
+          AbstractValue(n.getType(), debruijn));
     }
     std::vector<Node> children;
     bool childChanged = false;
@@ -798,10 +798,9 @@ Node DatatypesRewriter::replaceDebruijn(Node n,
                                         TypeNode orig_tn,
                                         unsigned depth)
 {
-  if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn)
+  if (n.getKind() == kind::ABSTRACT_VALUE && n.getType() == orig_tn)
   {
-    unsigned index =
-        n.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+    unsigned index = n.getConst<AbstractValue>().getIndex().toUnsignedInt();
     if (index == depth)
     {
       return orig;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c892ffc11..370b9cb9e 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -22,7 +22,6 @@
 #include "expr/dtype_cons.h"
 #include "expr/kind.h"
 #include "expr/skolem_manager.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -1293,7 +1292,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
   if( itv!=vmap.end() ){
     int debruijn = depth - 1 - itv->second;
     return NodeManager::currentNM()->mkConst(
-        UninterpretedConstant(n.getType(), debruijn));
+        AbstractValue(n.getType(), debruijn));
   }else if( n.getType().isDatatype() ){
     Node nc = eqc_cons[n];
     if( !nc.isNull() ){
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 39b48ece9..75489f698 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -109,7 +109,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
      if (d_child_enum)
      {
        ret = NodeManager::currentNM()->mkConst(
-           UninterpretedConstant(d_type, d_size_limit));
+           AbstractValue(d_type, d_size_limit));
      }
      else
      {
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 9ea121be4..759c50db0 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -21,7 +21,6 @@
 #include "expr/dtype.h"
 #include "expr/kind.h"
 #include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/quantifiers_options.h"
 #include "theory/type_enumerator.h"
 
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 2d6c3de55..c4aaf0f63 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -42,10 +42,7 @@ EvalResult::EvalResult(const EvalResult& other)
       new (&d_str) String;
       d_str = other.d_str;
       break;
-    case UCONST:
-      new (&d_uc)
-          UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
-      break;
+    case ABSTRACT: new (&d_av) AbstractValue(other.d_av); break;
     case INVALID: break;
   }
 }
@@ -70,10 +67,7 @@ EvalResult& EvalResult::operator=(const EvalResult& other)
         new (&d_str) String;
         d_str = other.d_str;
         break;
-      case UCONST:
-        new (&d_uc)
-            UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
-        break;
+      case ABSTRACT: new (&d_av) AbstractValue(other.d_av); break;
       case INVALID: break;
     }
   }
@@ -99,9 +93,9 @@ EvalResult::~EvalResult()
       d_str.~String();
       break;
     }
-    case UCONST:
+    case ABSTRACT:
     {
-      d_uc.~UninterpretedConstant();
+      d_av.~AbstractValue();
       break;
     }
     default: break;
@@ -117,7 +111,7 @@ Node EvalResult::toNode() const
     case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
     case EvalResult::RATIONAL: return nm->mkConst(d_rat);
     case EvalResult::STRING: return nm->mkConst(d_str);
-    case EvalResult::UCONST: return nm->mkConst(d_uc);
+    case EvalResult::ABSTRACT: return nm->mkConst(d_av);
     default:
     {
       Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
@@ -413,11 +407,10 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(r);
           break;
         }
-        case kind::UNINTERPRETED_CONSTANT:
+        case kind::ABSTRACT_VALUE:
         {
-          const UninterpretedConstant& uc =
-              currNodeVal.getConst<UninterpretedConstant>();
-          results[currNode] = EvalResult(uc);
+          const AbstractValue& av = currNodeVal.getConst<AbstractValue>();
+          results[currNode] = EvalResult(av);
           break;
         }
         case kind::PLUS:
@@ -830,9 +823,9 @@ EvalResult Evaluator::evalInternal(
               results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
               break;
             }
-            case EvalResult::UCONST:
+            case EvalResult::ABSTRACT:
             {
-              results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
+              results[currNode] = EvalResult(lhs.d_av == rhs.d_av);
               break;
             }
 
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 8ccb4561d..33d495aa7 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -26,7 +26,7 @@
 
 #include "base/output.h"
 #include "expr/node.h"
-#include "expr/uninterpreted_constant.h"
+#include "util/abstract_value.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
 #include "util/string.h"
@@ -47,7 +47,7 @@ struct EvalResult
     BITVECTOR,
     RATIONAL,
     STRING,
-    UCONST,
+    ABSTRACT,
     INVALID
   } d_tag;
 
@@ -58,7 +58,7 @@ struct EvalResult
     BitVector d_bv;
     Rational d_rat;
     String d_str;
-    UninterpretedConstant d_uc;
+    AbstractValue d_av;
   };
 
   EvalResult(const EvalResult& other);
@@ -67,7 +67,7 @@ struct EvalResult
   EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
   EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
   EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
-  EvalResult(const UninterpretedConstant& u) : d_tag(UCONST), d_uc(u) {}
+  EvalResult(const AbstractValue& av) : d_tag(ABSTRACT), d_av(av) {}
 
   EvalResult& operator=(const EvalResult& other);
 
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index c9fced3be..a5925631e 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -230,9 +230,12 @@ int TermUtil::getTermDepth( Node n ) {
 bool TermUtil::containsUninterpretedConstant( Node n ) {
   if (!n.hasAttribute(ContainsUConstAttribute()) ){
     bool ret = false;
-    if( n.getKind()==UNINTERPRETED_CONSTANT ){
+    if (n.getKind() == ABSTRACT_VALUE && n.getType().isSort())
+    {
       ret = true;
-    }else{ 
+    }
+    else
+    {
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( containsUninterpretedConstant( n[i] ) ){
           ret = true;
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 33dbe9ffa..de5e21abd 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -16,7 +16,6 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
@@ -25,6 +24,7 @@
 #include "smt/env.h"
 #include "theory/rewriter.h"
 #include "theory/uf/theory_uf_model.h"
+#include "util/abstract_value.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -224,7 +224,7 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue(
     {
       Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
                                    << eqc_m << std::endl;
-      if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
+      if (eqc_m.getKind() == kind::ABSTRACT_VALUE)
       {
         Trace("model-builder-debug") << "*** " << val
                                      << " is excluded datatype for " << eqc
@@ -318,8 +318,7 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue(
                                    << tn << std::endl;
       unsigned card = eqc_usort_count[tn];
       Trace("model-builder-debug") << "  Cardinality is " << card << std::endl;
-      unsigned index =
-          v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+      unsigned index = v.getConst<AbstractValue>().getIndex().toUnsignedInt();
       Trace("model-builder-debug") << "  Index is " << index << std::endl;
       return index > 0 && index >= card;
     }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index cd974d3e4..24ea16c9f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -287,17 +287,16 @@ void TheoryUF::preRegisterTerm(TNode node)
   case kind::COMBINED_CARDINALITY_CONSTRAINT:
     //do nothing
     break;
-  case kind::UNINTERPRETED_CONSTANT:
+  case kind::ABSTRACT_VALUE:
   {
-    // Uninterpreted constants should only appear in models, and should
-    // never appear in constraints. They are unallowed to ever appear in
-    // constraints since the cardinality of an uninterpreted sort may have
-    // an upper bound, e.g. if (forall ((x U) (y U)) (= x y)) holds, then
-    // @uc_U_2 is a ill-formed term, as its existence cannot be assumed.
-    // The parser prevents the user from ever constructing uninterpreted
-    // constants. However, they may be exported via models to API users.
-    // It is thus possible that these uninterpreted constants are asserted
-    // back in constraints, hence this check is necessary.
+    // Abstract values should only appear in models, and should never appear in
+    // constraints. They are unallowed to ever appear in constraints since the
+    // cardinality of an uninterpreted sort may have an upper bound, e.g. if
+    // (forall ((x U) (y U)) (= x y)) holds, then @uc_U_2 is a ill-formed term,
+    // as its existence cannot be assumed.  The parser prevents the user from
+    // ever constructing abstract values. However, they may be exported via
+    // models to API users.  It is thus possible that these abstract values are
+    // asserted back in constraints, hence this check is necessary.
     throw LogicException(
         "An uninterpreted constant was preregistered to the UF theory.");
   }
diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 556ce6eb0..1441b58fb 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -20,21 +20,49 @@
 #include <string>
 
 #include "base/check.h"
+#include "expr/type_node.h"
 
 using namespace std;
 
 namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) {
-  return out << "@" << val.getIndex();
+  return out << "@a" << val.getIndex();
 }
 
-AbstractValue::AbstractValue(Integer index) : d_index(index)
+AbstractValue::AbstractValue(const TypeNode& type, const Integer& index)
+    : d_type(new TypeNode(type)), d_index(index)
 {
-  PrettyCheckArgument(index >= 1,
+  PrettyCheckArgument(index >= 0,
                       index,
-                      "index >= 1 required for abstract value, not `%s'",
+                      "index >= 0 required for abstract value, not `%s'",
                       index.toString().c_str());
 }
 
+AbstractValue::AbstractValue(const AbstractValue& val)
+    : d_type(new TypeNode(*val.d_type)), d_index(val.d_index)
+{
+}
+
+AbstractValue::~AbstractValue() {}
+
+const TypeNode& AbstractValue::getType() const { return *d_type; }
+
+bool AbstractValue::operator==(const AbstractValue& val) const
+{
+  return getType() == val.getType() && d_index == val.d_index;
+}
+
+bool AbstractValue::operator<(const AbstractValue& val) const
+{
+  return getType() < val.getType()
+         || (getType() == val.getType() && d_index < val.d_index);
+}
+
+bool AbstractValue::operator<=(const AbstractValue& val) const
+{
+  return getType() <= val.getType()
+         || (getType() == val.getType() && d_index <= val.d_index);
+}
+
 }  // namespace cvc5
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 2ebc01061..ee3234d69 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -18,40 +18,42 @@
 #pragma once
 
 #include <iosfwd>
+#include <memory>
 
 #include "util/integer.h"
 
 namespace cvc5 {
 
+class TypeNode;
+
 class AbstractValue
 {
-  const Integer d_index;
-
  public:
-  AbstractValue(Integer index);
+  AbstractValue(const TypeNode& type, const Integer& index);
+  AbstractValue(const AbstractValue& val);
+  ~AbstractValue();
 
   const Integer& getIndex() const { return d_index; }
-  bool operator==(const AbstractValue& val) const
-  {
-    return d_index == val.d_index;
-  }
+  const TypeNode& getType() const;
+
+  bool operator==(const AbstractValue& val) const;
   bool operator!=(const AbstractValue& val) const { return !(*this == val); }
-  bool operator<(const AbstractValue& val) const
-  {
-    return d_index < val.d_index;
-  }
-  bool operator<=(const AbstractValue& val) const
-  {
-    return d_index <= val.d_index;
-  }
+  bool operator<(const AbstractValue& val) const;
+  bool operator<=(const AbstractValue& val) const;
   bool operator>(const AbstractValue& val) const { return !(*this <= val); }
   bool operator>=(const AbstractValue& val) const { return !(*this < val); }
+
+ private:
+  /** The type of the abstract value */
+  std::unique_ptr<TypeNode> d_type;
+  /** The index of the abstract value */
+  const Integer d_index;
 }; /* class AbstractValue */
 
 std::ostream& operator<<(std::ostream& out, const AbstractValue& val);
 
 /**
- * Hash function for the BitVector constants.
+ * Hash function for abstract values.
  */
 struct AbstractValueHashFunction
 {
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index db49f8bea..7627bc6e5 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -381,35 +381,6 @@ def test_mk_rounding_mode(solver):
     solver.mkRoundingMode(pycvc5.RoundTowardZero)
 
 
-def test_mk_uninterpreted_const(solver):
-    solver.mkUninterpretedConst(solver.getBooleanSort(), 1)
-    with pytest.raises(RuntimeError):
-        solver.mkUninterpretedConst(pycvc5.Sort(solver), 1)
-    slv = pycvc5.Solver()
-    with pytest.raises(RuntimeError):
-        slv.mkUninterpretedConst(solver.getBooleanSort(), 1)
-
-
-def test_mk_abstract_value(solver):
-    solver.mkAbstractValue("1")
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue("0")
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue("-1")
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue("1.2")
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue("1/2")
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue("asdf")
-
-    solver.mkAbstractValue(1)
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue(-1)
-    with pytest.raises(ValueError):
-        solver.mkAbstractValue(0)
-
-
 def test_mk_floating_point(solver):
     t1 = solver.mkBitVector(8)
     t2 = solver.mkBitVector(4)
diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py
index e65299676..270c826b1 100644
--- a/test/python/unit/api/test_term.py
+++ b/test/python/unit/api/test_term.py
@@ -942,16 +942,17 @@ def test_get_const_array_base(solver):
 
 
 def test_get_abstract_value(solver):
-    v1 = solver.mkAbstractValue(1)
-    v2 = solver.mkAbstractValue("15")
-    v3 = solver.mkAbstractValue("18446744073709551617")
-
-    assert v1.isAbstractValue()
-    assert v2.isAbstractValue()
-    assert v3.isAbstractValue()
-    assert "1" == v1.getAbstractValue()
-    assert "15" == v2.getAbstractValue()
-    assert "18446744073709551617" == v3.getAbstractValue()
+    solver.setOption("produce-models", "true")
+    uSort = solver.mkUninterpretedSort("u")
+    x = solver.mkConst(uSort, "x")
+    y = solver.mkConst(uSort, "y")
+    solver.assertFormula(solver.mkTerm(kinds.Equal, x, y))
+    assert solver.checkSat().isSat()
+    vx = solver.getValue(x)
+    vy = solver.getValue(y)
+    assert vx.isAbstractValue()
+    assert vy.isAbstractValue()
+    assert vx.getAbstractValue() == vy.getAbstractValue()
 
 
 def test_get_tuple(solver):
@@ -1027,18 +1028,6 @@ def test_get_sequence(solver):
     assert [i1, i1, i2] == s5.getSequenceValue()
 
 
-def test_get_uninterpreted_const(solver):
-    s = solver.mkUninterpretedSort("test")
-    t1 = solver.mkUninterpretedConst(s, 3)
-    t2 = solver.mkUninterpretedConst(s, 5)
-
-    assert t1.isUninterpretedValue()
-    assert t2.isUninterpretedValue()
-
-    assert (s, 3) == t1.getUninterpretedValue()
-    assert (s, 5) == t2.getUninterpretedValue()
-
-
 def test_get_floating_point(solver):
     bvval = solver.mkBitVector(16, "0000110000000011", 2)
     fp = solver.mkFloatingPoint(5, 11, bvval)
diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2
index fd7b4a7cc..9f0ad5b9c 100644
--- a/test/regress/regress0/bug421.smt2
+++ b/test/regress/regress0/bug421.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --incremental --abstract-values
 ; EXPECT: sat
-; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
+; EXPECT: ((a (as @a1 (Array Int Int))) (b (as @a2 (Array Int Int))))
 (set-logic QF_AUFLIA)
 (set-option :produce-models true)
 (declare-fun a () (Array Int Int))
diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2
index aed7f7c05..c9e77fa31 100644
--- a/test/regress/regress0/bug421b.smt2
+++ b/test/regress/regress0/bug421b.smt2
@@ -4,7 +4,7 @@
 ;
 ; COMMAND-LINE: --incremental --abstract-values --check-models
 ; EXPECT: sat
-; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
+; EXPECT: ((a (as @a1 (Array Int Int))) (b (as @a2 (Array Int Int))))
 (set-logic QF_AUFLIA)
 (set-option :produce-models true)
 (declare-fun a () (Array Int Int))
diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2
index b6825fe27..ab7615809 100644
--- a/test/regress/regress0/parser/issue6908-get-value-uc.smt2
+++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2
@@ -1,10 +1,10 @@
 ; COMMAND-LINE: --produce-models
 ; EXPECT: sat
-; EXPECT: (((f (as @uc_Foo_0 Foo)) 3))
+; EXPECT: (((f (as @a0 Foo)) 3))
 (set-logic ALL)
 (set-option :produce-models true)
 (declare-sort Foo 0)
 (declare-fun f (Foo) Int)
 (assert (exists ((x Foo)) (= (f x) 3)))
 (check-sat)
-(get-value ((f @uc_Foo_0)))
+(get-value ((f @a0)))
diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java
index d153b8a91..9694510d9 100644
--- a/test/unit/api/java/cvc5/SolverTest.java
+++ b/test/unit/api/java/cvc5/SolverTest.java
@@ -386,35 +386,6 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO));
   }
 
-  @Test void mkUninterpretedConst() throws CVC5ApiException
-  {
-    assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1));
-    Solver slv = new Solver();
-    assertThrows(
-        CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  }
-
-  @Test void mkAbstractValue() throws CVC5ApiException
-  {
-    assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1")));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("0")));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("-1")));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("1.2")));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("1/2"));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("asdf"));
-
-    assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
-    assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
-    assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
-    assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
-    // java does not have specific types for unsigned integers, therefore the two lines below do not
-    // make sense in java. assertDoesNotThrow(() -> d_solver.mkAbstractValue((int)-1));
-    // assertDoesNotThrow(() -> d_solver.mkAbstractValue((long)-1));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(0));
-  }
-
   @Test void mkFloatingPoint() throws CVC5ApiException
   {
     Term t1 = d_solver.mkBitVector(8);
@@ -2342,4 +2313,4 @@ class SolverTest
             + "\"Z\")))",
         projection.toString());
   }
-}
\ No newline at end of file
+}
diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java
index 98f668006..a4b51ab1d 100644
--- a/test/unit/api/java/cvc5/TermTest.java
+++ b/test/unit/api/java/cvc5/TermTest.java
@@ -834,16 +834,17 @@ class TermTest
 
   @Test void getAbstractValue() throws CVC5ApiException
   {
-    Term v1 = d_solver.mkAbstractValue(1);
-    Term v2 = d_solver.mkAbstractValue("15");
-    Term v3 = d_solver.mkAbstractValue("18446744073709551617");
-
-    assertTrue(v1.isAbstractValue());
-    assertTrue(v2.isAbstractValue());
-    assertTrue(v3.isAbstractValue());
-    assertEquals("1", v1.getAbstractValue());
-    assertEquals("15", v2.getAbstractValue());
-    assertEquals("18446744073709551617", v3.getAbstractValue());
+    d_solver.setOption("produce-models", "true");
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkConst(uSort, "x");
+    Term y = d_solver.mkConst(uSort, "y");
+    d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y));
+    assertTrue(d_solver.checkSat().isSat());
+    Term vx = d_solver.getValue(x);
+    Term vy = d_solver.getValue(y);
+    assertEquals(vx.isAbstractValue(), vy.isAbstractValue());
+    assertDoesNotThrow(() -> vx.getAbstractValue());
+    assertDoesNotThrow(() -> vy.getAbstractValue());
   }
 
   @Test void getTuple()
@@ -948,19 +949,6 @@ class TermTest
     assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue()));
   }
 
-  @Test void getUninterpretedConst() throws CVC5ApiException
-  {
-    Sort s = d_solver.mkUninterpretedSort("test");
-    Term t1 = d_solver.mkUninterpretedConst(s, 3);
-    Term t2 = d_solver.mkUninterpretedConst(s, 5);
-
-    assertTrue(t1.isUninterpretedValue());
-    assertTrue(t2.isUninterpretedValue());
-
-    assertEquals(new Pair<Sort, Integer>(s, 3), t1.getUninterpretedValue());
-    assertEquals(new Pair<Sort, Integer>(s, 5), t2.getUninterpretedValue());
-  }
-
   @Test void substitute()
   {
     Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 19113ae13..5669f9803 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -376,33 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode)
   ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
 }
 
-TEST_F(TestApiBlackSolver, mkUninterpretedConst)
-{
-  ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException);
-  Solver slv;
-  ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1),
-               CVC5ApiException);
-}
-
-TEST_F(TestApiBlackSolver, mkAbstractValue)
-{
-  ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
-  ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC5ApiException);
-
-  ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1));
-  ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1));
-  ASSERT_NO_THROW(d_solver.mkAbstractValue((uint64_t)1));
-  ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1));
-  ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1));
-  ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1));
-  ASSERT_THROW(d_solver.mkAbstractValue(0), CVC5ApiException);
-}
-
 TEST_F(TestApiBlackSolver, mkFloatingPoint)
 {
   Term t1 = d_solver.mkBitVector(8);
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 7cfbe2527..3c4493ac6 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -885,16 +885,17 @@ TEST_F(TestApiBlackTerm, getBitVector)
 
 TEST_F(TestApiBlackTerm, getAbstractValue)
 {
-  Term v1 = d_solver.mkAbstractValue(1);
-  Term v2 = d_solver.mkAbstractValue("15");
-  Term v3 = d_solver.mkAbstractValue("18446744073709551617");
-
-  ASSERT_TRUE(v1.isAbstractValue());
-  ASSERT_TRUE(v2.isAbstractValue());
-  ASSERT_TRUE(v3.isAbstractValue());
-  ASSERT_EQ("1", v1.getAbstractValue());
-  ASSERT_EQ("15", v2.getAbstractValue());
-  ASSERT_EQ("18446744073709551617", v3.getAbstractValue());
+  d_solver.setOption("produce-models", "true");
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkConst(uSort, "x");
+  Term y = d_solver.mkConst(uSort, "y");
+  d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y));
+  ASSERT_TRUE(d_solver.checkSat().isSat());
+  Term vx = d_solver.getValue(x);
+  Term vy = d_solver.getValue(y);
+  ASSERT_TRUE(vx.isAbstractValue());
+  ASSERT_TRUE(vy.isAbstractValue());
+  ASSERT_EQ(vx.getAbstractValue(), vy.getAbstractValue());
 }
 
 TEST_F(TestApiBlackTerm, getTuple)
@@ -994,19 +995,6 @@ TEST_F(TestApiBlackTerm, getSequence)
   ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue());
 }
 
-TEST_F(TestApiBlackTerm, getUninterpretedConst)
-{
-  Sort s = d_solver.mkUninterpretedSort("test");
-  Term t1 = d_solver.mkUninterpretedConst(s, 3);
-  Term t2 = d_solver.mkUninterpretedConst(s, 5);
-
-  ASSERT_TRUE(t1.isUninterpretedValue());
-  ASSERT_TRUE(t2.isUninterpretedValue());
-
-  ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue());
-  ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue());
-}
-
 TEST_F(TestApiBlackTerm, substitute)
 {
   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp
index bb7ef871c..f62fd7971 100644
--- a/test/unit/theory/type_enumerator_white.cpp
+++ b/test/unit/theory/type_enumerator_white.cpp
@@ -22,10 +22,10 @@
 #include "expr/dtype.h"
 #include "expr/kind.h"
 #include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/language.h"
 #include "test_smt.h"
 #include "theory/type_enumerator.h"
+#include "util/abstract_value.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
 
@@ -61,13 +61,13 @@ TEST_F(TestTheoryWhiteTypeEnumerator, uf)
   TypeNode sort = d_nodeManager->mkSort("T");
   TypeNode sort2 = d_nodeManager->mkSort("U");
   TypeEnumerator te(sort);
-  ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0)));
+  ASSERT_EQ(*te, d_nodeManager->mkConst(AbstractValue(sort, 0)));
   for (size_t i = 1; i < 100; ++i)
   {
-    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
-    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i)));
-    ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
-    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2)));
+    ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort, i)));
+    ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort2, i)));
+    ASSERT_EQ(*++te, d_nodeManager->mkConst(AbstractValue(sort, i)));
+    ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort, i + 2)));
   }
 }
 
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index 1272926db..d7bc4b412 100644
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -14,8 +14,8 @@
  */
 
 #include "expr/array_store_all.h"
-#include "expr/uninterpreted_constant.h"
 #include "test_smt.h"
+#include "util/abstract_value.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -32,7 +32,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all)
                                            d_nodeManager->realType()),
                 d_nodeManager->mkConst(Rational(9, 2)));
   ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort),
-                d_nodeManager->mkConst(UninterpretedConstant(usort, 0)));
+                d_nodeManager->mkConst(AbstractValue(usort, 0)));
   ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
                                            d_nodeManager->realType()),
                 d_nodeManager->mkConst(Rational(0)));
@@ -44,8 +44,8 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all)
 TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
 {
   ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
-                             d_nodeManager->mkConst(UninterpretedConstant(
-                                 d_nodeManager->mkSort("U"), 0))),
+                             d_nodeManager->mkConst(
+                                 AbstractValue(d_nodeManager->mkSort("U"), 0))),
                IllegalArgumentException);
   ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
                              d_nodeManager->mkConst(Rational(9, 2))),