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.

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index e4f281de8d175fef6d8b87ab68b3e6e15252d083..e06a8cb528a717cd91f306a0ab6442c846726e8b 100644 (file)
--- 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 3b95c7e008a690b0cae0a3a278707f853bd6f571..a22e75d91a9aa03ba32ea8714ad5e7049adaae89 100644 (file)
--- 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 4390b3e6e54bc8cb99e88f8dac953af7db5ea3dc..5558b95d4d0661b482ccb4c8c4df62cd29a75753 100644 (file)
--- 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 8247d49404afe2591f111d921ab66d80a81dd10a..ee42a7989ba130a81c0b7f9483fe397f75f29b6b 100644 (file)
--- 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();