ILASP currently supports 4 types of ASP rules: normal rules, choice rules, hard constraints and weak constraints. Each type of rule is outlined in the subsections below. There are many other types of ASP rules supported by ASP solvers such as Clingo, and it is possible that future versions of ILASP may support these.

The following Context-free grammar specifies the literals which are permitted in ILASP.

```
basic_symbol -> [a-z][a-zA-Z0-9_]*
variable -> [A-Z][a-zA-Z0-9_]*
integer -> -?[1-9][0-9]*
bin_op -> '+' | '-' | '*' | '/'
bin_comp -> '<' | '<=' | '=' | '!=' | '>' | '>='
literal -> atom
literal -> 'not ' atom
literal -> term bin_comp term
atom -> basic_symbol
atom -> basic_symbol '(' terms ')'
term -> functional_term
term -> arithmetic_expr
term -> string
functional_term -> basic_symbol
functional_term -> basic_symbol '(' terms ')'
terms -> term
terms -> terms ',' term
arithmetic_expr -> variable
arithmetic_expr -> integer
arithmetic_expr -> arithmetic_expr bin_op arithmetic_expr
arithmetic_expr -> '(' arithmetic_expr ')'
```

A normal rule is of the form:

```
h :- b_1, ..., b_n.
```

where `h`

is an atom and `b_1`

, …, `b_n`

, are literals.

A disjunctive rule is of the form:

```
h_1 ; ... ; h_m :- b_1, ..., b_n.
```

where `h_1`

, …, `h_m`

are atoms and `b_1`

, …, `b_n`

, are literals.

A choice rule is of the form:

```
lb { h_1; ...; h_m } ub :- b_1, ..., b_n.
```

where `lb`

and `ub`

are integers, `h_1`

, …, `h_m`

are atoms and `b_1`

, …, `b_n`

, are literals.

A hard constraint is of the form:

```
:- b_1, ..., b_n.
```

where `b_1`

, …, `b_n`

, are literals.

A weak constraint is of the form:

```
:~ b_1, ..., b_n.[wt@lev,t_1,...,t_m]
```

where `b_1`

, …, `b_n`

, are literals, `wt`

and `lev`

are arithmetic
expressions and `t_1`

, …, `t_m`

are terms.

Consider the following ASP background knowledge for the Sudoku task.

```
cell((1..4,1..4)).
% Note that the '..' notation can be used to define a range of atoms. In
% this case 16 cell atoms are defined.
block((X, Y), tl) :- cell((X, Y)), X < 3, Y < 3.
block((X, Y), tr) :- cell((X, Y)), X > 2, Y < 3.
block((X, Y), bl) :- cell((X, Y)), X < 3, Y > 2.
block((X, Y), br) :- cell((X, Y)), X > 2, Y > 2.
same_row((X1,Y),(X2,Y)) :- X1 != X2, cell((X1,Y)), cell((X2, Y)).
same_col((X,Y1),(X,Y2)) :- Y1 != Y2, cell((X,Y1)), cell((X, Y2)).
same_block(C1,C2) :- block(C1, B), block(C2, B), C1 != C2.
```

The above program defines a `4x4`

Sudoku grid of the form:

```
#-------#-------#
| : | : |
| - + - | - + - |
| : | : |
#-------#-------#
| : | : |
| - + - | - + - |
| : | : |
#-------#-------#
```

It also defines what it means for two distinct cells to be in the same
`row`

, `column`

or `block`

as each other.

From ILASP 3.6.0 onwards, conditional literals are supported, meaning
that any literal `lit`

in the above rules (including atoms in the head
of a rule) can be replaced with `lit : c_1, ..., c_n`

, where `c_1`

, …,
`c_n`

are literals. To denote the end of a literals conditions, `;`

should be used in place of `,`

.