# Example (for ICS 1.1)

Consider, for example, processing

`f(y-1)-1 = y+1`,
`f(x)+1 = x-1`, and
`x+1 = y`

from top-to-bottom using the interactive mode of ICS.

% ics
ICS: Integrated Canonizer and Solver.
Copyright (c) 2003 SRI International.
Type 'help.' for help about help, and 'Ctrl-d' to exit.
ics> show.
:val

The current logical state of ICS is displayed using the `show` command.
The initial logical state is empty. New facts can be added to the current
logical state using `assert`.
ics> assert f(y - 1) - 1 = y + 1.
:ok s1

This results in a new logical state of name `s1`, which is also the
new current logical state.
The input equality above contains symbols from both the theory of uninterpreted
function symbols, namely `f`, and from the theory of linear arithmetic
(`+`, `-`). In a first step, ICS rewrites this equality in terms
of a conjunction of equalities with terms built up from function symbols in
a single theory. This abstraction step requires the introduction of new
variables, which are of the form `v!i`.
ics> show.
:val
v:[v!1 |-> {v!1, v!4}]
u:[v!3 = f(v!2)]
a:[y = -2 + v!3; v!1 = -1 + v!3; v!2 = -3 + v!3]

This new state consists of a triple of sets of
equalities `v`, `u` and `a`, where
`v` represents equalities between variables,
`u` consists of equalities in the theory of uninterpreted function
symbols, and `a` is a set linear arithmetic equalities.
Here, `v:[v!1 |-> {v!1, v!4}]` denotes the equality `v!1 = v!4`
and `v!1` is considered to be the canonical representative of the
corresponding equivalence class. Equalities in `u` are always of the
form `x = f(y1,...,yn)` with `x`, `y1`,..., `yn`
variables. These equalities are not solved, since `x` might be one of
the `yi`'s. Also, `x` is not necessarily canonical, whereas each
of the `yi` is canonical. In contrast, equalities in interpreted theories
such as linear arithmetic are in solved form and left-hand sides are also canonical.
The number of newly generated variables here heavily depends on the underlying
algorithm and the garbage collection strategy used. Here, we do not use any garbage
collection and thus we do not delete the superfluous variable equality
`v!1 = v!4`.
Now, consider processing the second equation `f(x) + 1 = x - 1`.
ics> assert f(x) + 1 = x - 1.
:ok s2
ics> show.
:val
v:[v!1 |-> {v!1, v!4}; v!6 |-> {v!6, v!7}]
u:[v!3 = f(v!2); v!5 = f(x)]
a:[x = 2 + v!5; y = -2 + v!3; v!1 = -1 + v!3; v!2 = -3 + v!3; v!6 = 1 + v!5]

Now, if `x + 1 = y`, then `v!2 = x`.
In addition, by congruence closure,
`v!3 = v!5`, and therefore `-2 + x = 3 + x`, which is
inconsistent. ICS detects this inconsistency, when asserting the
third equation.
ics> assert x + 1 = y.
:unsat

Back to the main ICS homepage

*Last updated June 20 2002 by
Harald Rueß*