From af874a5c7a2ff134da0d4c20d06a0626d3e36d9b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
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/sets/theory_sets.cpp         | 38 ++++++++++++++++++++++++++++++-
 src/theory/sets/theory_sets_private.cpp | 40 ---------------------------------
 src/theory/sets/theory_sets_private.h   |  2 --
 3 files changed, 37 insertions(+), 43 deletions(-)

(limited to 'src/theory/sets')

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 8430987f2..b5c2590d5 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -56,6 +56,8 @@ void TheorySets::finishInit()
   TheoryModel* tm = d_valuation.getModel();
   Assert(tm != nullptr);
   tm->setUnevaluatedKind(COMPREHENSION);
+  // choice is used to eliminate witness
+  tm->setUnevaluatedKind(WITNESS);
 }
 
 void TheorySets::addSharedTerm(TNode n) {
@@ -123,7 +125,41 @@ Node TheorySets::expandDefinition(Node n)
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  return d_internal->ppAssert( in, outSubstitutions );
+  Debug("sets-proc") << "ppAssert : " << in << std::endl;
+  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
+
+  // this is based off of Theory::ppAssert
+  if (in.getKind() == kind::EQUAL)
+  {
+    if (in[0].isVar() && isLegalElimination(in[0], in[1]))
+    {
+      // We cannot solve for sets if setsExt is enabled, since universe set
+      // may appear when this option is enabled, and solving for such a set
+      // impacts the semantics of universe set, see
+      // regress0/sets/pre-proc-univ.smt2
+      if (!in[0].getType().isSet() || !options::setsExt())
+      {
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        status = Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+    }
+    else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
+    {
+      if (!in[0].getType().isSet() || !options::setsExt())
+      {
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        status = Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+    }
+    else if (in[0].isConst() && in[1].isConst())
+    {
+      if (in[0] != in[1])
+      {
+        status = Theory::PP_ASSERT_STATUS_CONFLICT;
+      }
+    }
+  }
+  return status;
 }
 
 void TheorySets::presolve() {
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fbf1e6fcf..78f6fa8b5 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1536,46 +1536,6 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
   return chooseSkolem;
 }
 
-Theory::PPAssertStatus TheorySetsPrivate::ppAssert(
-    TNode in, SubstitutionMap& outSubstitutions)
-{
-  Debug("sets-proc") << "ppAssert : " << in << std::endl;
-  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
-
-  // TODO: allow variable elimination for sets when setsExt = true
-
-  // this is based off of Theory::ppAssert
-  if (in.getKind() == kind::EQUAL)
-  {
-    if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
-        && (in[1].getType()).isSubtypeOf(in[0].getType()))
-    {
-      if (!in[0].getType().isSet() || !options::setsExt())
-      {
-        outSubstitutions.addSubstitution(in[0], in[1]);
-        status = Theory::PP_ASSERT_STATUS_SOLVED;
-      }
-    }
-    else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
-             && (in[0].getType()).isSubtypeOf(in[1].getType()))
-    {
-      if (!in[1].getType().isSet() || !options::setsExt())
-      {
-        outSubstitutions.addSubstitution(in[1], in[0]);
-        status = Theory::PP_ASSERT_STATUS_SOLVED;
-      }
-    }
-    else if (in[0].isConst() && in[1].isConst())
-    {
-      if (in[0] != in[1])
-      {
-        status = Theory::PP_ASSERT_STATUS_CONFLICT;
-      }
-    }
-  }
-  return status;
-}
-
 void TheorySetsPrivate::presolve() { d_state.reset(); }
 
 /**************************** eq::NotifyClass *****************************/
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index a7e6f69ee..da42ad1fe 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -210,8 +210,6 @@ class TheorySetsPrivate {
    * so that it makes theory-specific calls to evaluate interpreted symbols.
    */
   Node expandDefinition(Node n);
-
-  Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   
   void presolve();
 
-- 
cgit v1.2.3