# 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
• • #### Example1 #### Example2 #### 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.