From 8848b31ec753ba87522fb6e5d76163f2979e73a2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Oct 2021 16:19:01 -0500 Subject: [PATCH] Make preregistration safe for uninterpreted constants (#7292) Work towards addressing #6908. --- src/theory/uf/theory_uf.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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); -- 2.30.2