This is an old revision of the document!
Definition of Set Constraints
Set constraints are a logic used in program analysis. In set constraints, each variable denotes a set of ground terms.
Let be a language of function symbols and constants. We write for an element of . Let be the set of ground terms in language .
Syntax of Set Constraints
\[ \begin{array}{l}
S ::= v | S \cap S | S \cup S | S \setminus S | f(S, ..., S) | f^{-i}(S) \\ F ::= S \subseteq S \mid F \land F
\end{array} \] where
- - set variable
- - standard set operations and relations
- - function symbol
- in , is an integer between 1 and arity of
Semantic
- - set variable, subset of
- - standard set operations and relations
Example1
\[
f(\{a,f(b,b)\},\{b,c\}) = \{ f(a,b),f(a,c),f(f(b,b),b), f(f(b,b),c) \}
\]
Example2
\[
f^{-2}(\{a,f(a,b),f(f(a,a),f(c,c))\}) = \{b,f(c,c)\}
\]
Example3
What is the least solution of constraints \[ \begin{array}{l}
a \subseteq S \\ f(f(S)) \subseteq S
\end{array} \] where is constant and is unary function symbol.
Example4
What is the least solution of constraints \[ \begin{array}{l}
a \subseteq S \\ black(S) \subseteq S \\ red(black(S)) \subseteq S
\end{array} \] where is constant, are unary function symbols.
Example5
Let where
- are constants representing propositional constants
- is unary function symbol representing negation in abstract syntax tree
- are binary function symbols representing in syntax tree
Then the set of ground terms represents propositional formulas.
What does the least solution of these constraints represent (where , are set variables): \[ \begin{array}{l}
a_1 \subseteq P \\ \ldots \\ a_n \subseteq P \\ P \subseteq S \\ not(P) \subseteq S \\ and(S,S) \subseteq S \\ or(S,S) \subseteq S
\end{array} \]
Existence of Solutions
We were able to talk about “the least solution” because previous examples can be rewritten into form \[
(S_1,\ldots,S_n) = F(S_1,\ldots,S_n)
\] where is a -morphism (and therefore monotonic and -continuous). The least solution can therefore be computed by fixpoint iteration (but it may contain infinite sets).
Example
Previous example can be rewritten as \[ \begin{array}{l}
P = P \cup a_1 \cup \ldots a_n \\ S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S)
\end{array} \]