[FEATURE] Rewrite S \subseteq T

[konnov]

We now have two implementations of S \subseteq T:

• SetInclusionRule for the default encoding, and
• SetInclusionRuleWithArrays for the arrays encoding.

There is no need for these rules. When S and T are general sets, we can rewrite the S \subseteq T as \A x \in S: x \in T. When S is a general set and T is SUBSET V, we can rewrite S \subseteq SUBSET V as \A x \in S: x \ in V. This will open space for optimizations.

Related to #1103.

[p-offtermatt]

Could you double-check the second part of the issue?
\A x \in S: x \ in V seems like the rewriting for S \in SUBSET V, not for S \subseteq SUBSET V.
A valid rewriting for S \subseteq SUBSET V that avoids expanding SUBSET might be via double quantification: \A X \in S: \A x \in X: x \in V.
But please correct me if I overlooked something!

[Kukovec]

\A x \in S: x \in V <=>
S \subseteq V

S \subseteq SUBSET V <=>
\A x \in S: x \in SUBSET V <=>
\A x \in S: x \subseteq V <=>
\A x \in S: \A y \in x: y \in V

[Kukovec]

Just remember to recursively call rewrite (or transform or w/e):

rewrite(S \subseteq V) = rewrite(\A x \in rewrite(S): x \in rewrite(V))