# Introduction

Decision procedures are at the core of many industrial-strength verification systems such as PVS. When used in such embedded contexts, decision procedures must handle a rich combination of theories involving booleans, arithmetic, and other commonly used datatypes, and provide an application programmer interface (API) for managing and manipulating large assertional contexts.

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:
• Equality and disequality.
• Rational and (incomplete) integer linear arithmetic.
• Tuples and projections from tuples.
• Coproducts. Together with tuples, coproducts are used to build up ground datatype terms.
• Boolean constants.
• S-expressions builtup from car, cdr, and cons.
• Functional arrays.
• Combinatory logic with case-splitting.
• Bitvector terms include constants, concatenation, extraction.
• There are also (incomplete) extensions to handle nonlinear multiplication.
The list of interpreted theories above is open-ended in the sense that new theories can be added to ICS as long as they are canonizable and algebraically solvable. The modular design of ICS---both the underlying algorithms and their implementation---supports such extensions. ICS decides propositional satisfiability problems with literals drawn from the combination of theories as described above. The underlying verification engine combines the ICS core capabilities with a state-of-the-art propositional SAT solver using the paradigm of lazy theorem proving. For example, using the ICS interactor, the validity of such propositional formulas is demonstrated as follows. (| is disjunction, & is conjunction, and brackets are used for grouping). ICS can be invoked as a shell command or used interactively. For example, the unsatisfiability of the third formula above, for example, can be demonstrated using the ICS interactor, with the following sequence of assertions.
```  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

• a C shared-object library,
• an Ocaml object module,
• a CommonLisp foreign-function interface, and
• an interactor

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.

Back to the main ICS homepage