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();