Do not eliminate variables that are equal to unevaluatable terms (#4267)

When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.

This PR ensures we only eliminate variables when v contains only evaluated operators.

Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.

Fixes #4500.

1 files changed, 7 insertions, 4 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1667e5505..a49903f13 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -43,10 +43,13 @@ std::string TheoryBuiltin::identify() const
 
 void TheoryBuiltin::finishInit()
 {
-  // choice nodes are not evaluated in getModelValue
-  TheoryModel* theoryModel = d_valuation.getModel();
-  Assert(theoryModel != nullptr);
-  theoryModel->setUnevaluatedKind(kind::WITNESS);
+  // Notice that choice is an unevaluated kind belonging to this theory.
+  // However, it should be set as an unevaluated kind where it is used, e.g.
+  // in the quantifiers theory. This ensures that a logic like QF_LIA, which
+  // includes the builtin theory, does not mark any kinds as unevaluated and
+  // hence it is easy to check for illegal eliminations via TheoryModel
+  // (see TheoryModel::isLegalElimination) since there are no unevaluated kinds
+  // present.
 }
 
 }  // namespace builtin