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.

1 files changed, 9 insertions, 10 deletions

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.");
   }