From 2fda6c574c75fcc85f0d828a0af9435154eb1a96 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Dec 2020 15:55:38 -0600
Subject: [PATCH] Proper expand definitions for sets (#5676)

In the new view, expandDefinitions is used for eliminating partial operators and is not called during solving, and ppRewrite is called during preprocessing.

For sets, choose is a partial operator that should be applied in expand definitions, and in ppRewrite. On the other hand, is_singleton should not be expanded in expandDefinitions since it is not a partial operator, so it should only be handled in ppRewrite.

It also removes some outdated documentation regarding expandDefinitions with universe set, which is now handled by preventing universe set from occurring in solved substitutions.

This is in preparation for refactoring check-model.
---
 src/theory/sets/theory_sets.cpp         |  3 +--
 src/theory/sets/theory_sets.h           |  6 +++++
 src/theory/sets/theory_sets_private.cpp | 11 +++++++++
 src/theory/sets/theory_sets_private.h   | 32 +++----------------------
 4 files changed, 21 insertions(+), 31 deletions(-)

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index e4f281de8..e06a8cb52 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -158,8 +158,7 @@ TrustNode TheorySets::ppRewrite(TNode n)
       throw LogicException(ss.str());
     }
   }
-  // just expand definitions
-  return expandDefinition(n);
+  return d_internal->ppRewrite(n);
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 3b95c7e00..a22e75d91 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -76,7 +76,13 @@ class TheorySets : public Theory
   Node getModelValue(TNode) override;
   std::string identify() const override { return "THEORY_SETS"; }
   void preRegisterTerm(TNode node) override;
+  /**  Expand partial operators (choose) from n. */
   TrustNode expandDefinition(Node n) override;
+  /**
+   * If the sets-ext option is not set and we have an extended operator,
+   * we throw an exception. Additionally, we expand operators like choose
+   * and is_singleton.
+   */
   TrustNode ppRewrite(TNode n) override;
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 4390b3e6e..5558b95d4 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1269,6 +1269,17 @@ TrustNode TheorySetsPrivate::expandDefinition(Node node)
 {
   Debug("sets-proc") << "expandDefinition : " << node << std::endl;
 
+  if (node.getKind()==kind::CHOOSE)
+  {
+    return expandChooseOperator(node);
+  }
+  return TrustNode::null();
+}
+
+TrustNode TheorySetsPrivate::ppRewrite(Node node)
+{
+  Debug("sets-proc") << "ppRewrite : " << node << std::endl;
+
   switch (node.getKind())
   {
     case kind::CHOOSE: return expandChooseOperator(node);
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 8247d4940..ee42a7989 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -167,36 +167,10 @@ class TheorySetsPrivate {
 
   void preRegisterTerm(TNode node);
 
-  /** expandDefinition
-   * If the sets-ext option is not set and we have an extended operator, 
-   * we throw an exception. This function is a no-op otherwise.
-   *
-   * TheorySets uses expandDefinition as an entry point to see if the input
-   * contains extended operators.
-   *
-   * We need to be notified when a universe set occurs in our input,
-   * before preprocessing and simplification takes place. Otherwise the models
-   * may be inaccurate when setsExt is false, here is an example:
-   *
-   * x,y : (Set Int)
-   * x = (as univset (Set Int));
-   * 0 in y;
-   * check-sat;
-   *
-   * If setsExt is enabled, the model value of (as univset (Set Int)) is always accurate.
-   *
-   * If setsExt is not enabled, the following can happen for the above example:
-   * x = (as univset (Set Int)) is made into a model substitution during 
-   * simplification. This means (as univset (Set Int)) is not a term in any assertion, 
-   * and hence we do not throw an exception, nor do we infer that 0 is a member of 
-   * (as univset (Set Int)). We instead report a model where x = {}. The correct behavior 
-   * is to throw an exception that says universe set is not supported when setsExt disabled.
-   * Hence we check for the existence of universe set before simplification here.
-   *
-   * Another option to fix this is to make TheoryModel::getValue more general
-   * so that it makes theory-specific calls to evaluate interpreted symbols.
-   */
+  /** ppRewrite, which expands choose.  */
   TrustNode expandDefinition(Node n);
+  /** ppRewrite, which expands choose and is_singleton.  */
+  TrustNode ppRewrite(Node n);
 
   void presolve();
 
-- 
2.30.2