ICS (Integrated Canonizer and Solver) is a decision procedure developed at SRI International that efficiently decides formulas in a combination of useful theories. It provides an API that makes it suitable for use in applications with highly dynamic environments such as proof search or symbolic simulation.
ICS decides the satisfiability of formulas in a quantifier-free, first-order theory containing both uninterpreted function symbols and interpreted symbols from a rich combination of datatype theories, including arithmetic, tuples, arrays, and bit-vectors. This theory is particularly interesting for many applications in software and hardware verification.
ICS is capable of deciding the satisfiability/validity of sequences of formulas.
x+2 = y |- f(a[x:=3][y-2]) = f(y-x+1)
f(y-1)-1 = y+1 , f(x)+1 = x-1 , x+1 = y |- false
f(f(x)-f(y)) <> f(z) , y <= x , y >= x+z , z > 0 |- false
Here f is a unary uninterepreted function, a[x:=3] is an array update, and
a <> b represents disequality.
The core of ICS is a recently developed congruence closure procedure for the theory
of equality and disequality with both uninterpreted and interpreted function symbols.
The concepts of canonization and solving have been extended to include inequalities over
arithmetic terms. The theory supported by ICS currently includes:
ics> assert f(f(x)-f(y)) <> f(z).
:ok s1
ics> assert y <= x.
:ok s2
ics> assert y >= x + z.
:ok s3
ics> assert z > 0.
:unsat
{-1 * y + x >=0, z >0,
-1 * z + y + -1 * x >=0}
ICS returns a list of the asserted atoms that participate in demonstrating
the inconsistency.
This sequence of assertions can also placed in a file foo.ics and ICS can be invoked in batch mode as a shell command
$ ics foo.ics
:unsat
{-1 * y + x >=0, z >0,
-1 * z + y + -1 * x >=0}
The SAT solver can also be used interactively as
ics> sat [x > 2 | x < 4 | p] & 2 * x > 6. :sat s5 :model [p |-> :true][-6 + 2 * x > 0]
This sat command returns an assignment for the propositional variable p and a subset of the input literals. Here, satisfying assignments for x are described by means of the constraint -6 + 2 * x > 0.
Verification conditions are usually proved within the context of a large number of assertions derived from the antecedents of implications, conditional tests, and predicate subtype constraints. These contexts must be changed in an incremental manner when assertions are either added or removed. Through the use of functional data structures, ICS allows contexts to be incrementally enriched in a side-effect-free manner.
ICS is implemented in Ocaml, which offers satisfactory run-time performance, efficient garbage collection, and interfaces well with other languages such as C. ICS uses arbitrary precision rational numbers from the GNU multi-precision library GMP. There is a well-defined API for manipulating ICS terms, asserting formulas to the current database, switching between databases, and functions for canonizing terms. This API is packaged as
ICS can be used as a back-end decision procedure in a variety of applications like static analysis, abstract interpretation, extended type checking, symbolic simulation, model checking, and compiler optimization.
Forthcoming versions of ICS will extend its range of theories and capabilities; in particular, the next version of ICS will be complete for integer linear arithmetic and will handle a larger subset of nonlinear real arithmetic.