From af874a5c7a2ff134da0d4c20d06a0626d3e36d9b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 May 2020 21:48:01 -0500 Subject: 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. --- src/theory/arith/theory_arith.h | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/arith/theory_arith.h') diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index f15db32a1..8672f7145 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -58,6 +58,8 @@ public: */ void preRegisterTerm(TNode n) override; + void finishInit() override; + Node expandDefinition(Node node) override; void setMasterEqualityEngine(eq::EqualityEngine* eq) override; -- cgit v1.2.3