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ß