From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Oct 2021 21:19:01 +0000 (-0500)
Subject: Make preregistration safe for uninterpreted constants (#7292)
X-Git-Tag: cvc5-1.0.0~1136
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8848b31ec753ba87522fb6e5d76163f2979e73a2;p=cvc5.git

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 056b0407a..cd974d3e4 100644
--- 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);