diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-01 16:19:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-01 21:19:01 +0000 |
commit | 8848b31ec753ba87522fb6e5d76163f2979e73a2 (patch) | |
tree | 23d8543a0ce5e90c02dbd9429f1e64a8dc472277 /src/theory/uf | |
parent | 45d127cc4ebaa9c092605266c118288560c1138b (diff) |
Make preregistration safe for uninterpreted constants (#7292)
Work towards addressing #6908.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 15 |
1 files changed, 15 insertions, 0 deletions
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); |