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.

1 files changed, 6 insertions, 0 deletions

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;