# LARA

## 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

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

#### Example3

What is the least solution of constraints

where is constant and is unary function symbol.

#### Example4

What is the least solution of constraints

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):

## Existence of Solutions

We were able to talk about “the least solution” because previous examples can be rewritten into form

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

Is every set expression in set constraints monotonic?

## Conditional Constraints

Let us simplify this expression:

Consider conditional constraints of the form

We can transform it into

for some binary function symbol . Thus, we can introduce such conditional constraints without changing expressive power or decidability.