Make preregistration safe for uninterpreted constants (#7292)

Work towards addressing #6908.

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 056b0407abb1f4401126385c31d3c87f4f518687..cd974d3e42027eb6c8eae6ff54ad70f7af8dba21 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -287,6 +287,21 @@ void TheoryUF::preRegisterTerm(TNode node)
   case kind::COMBINED_CARDINALITY_CONSTRAINT:
     //do nothing
     break;
+  case kind::UNINTERPRETED_CONSTANT:
+  {
+    // 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.
+    throw LogicException(
+        "An uninterpreted constant was preregistered to the UF theory.");
+  }
+  break;
   default:
     // Variables etc
     d_equalityEngine->addTerm(node);