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, 17 insertions, 1 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index c777f164f..366a943ef 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -248,8 +248,24 @@ class Theory {
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
-public:
+  /** is legal elimination
+   *
+   * Returns true if x -> val is a legal elimination of variable x. This is
+   * useful for ppAssert, when x = val is an entailed equality. This function
+   * determines whether indeed x can be eliminated from the problem via the
+   * substituion x -> val.
+   *
+   * The following criteria imply that x -> val is *not* a legal elimination:
+   * (1) If x is contained in val,
+   * (2) If the type of val is not a subtype of the type of x,
+   * (3) If val contains an operator that cannot be evaluated, and produceModels
+   * is true. For example, x -> sqrt(2) is not a legal elimination if we
+   * are producing models. This is because we care about the value of x, and
+   * its value must be computed (approximated) by the non-linear solver.
+   */
+  bool isLegalElimination(TNode x, TNode val);
 
+ public:
   /**
    * Return the ID of the theory responsible for the given type.
    */