A key operation supported by the Omega test is the
elimination of existentially quantified variables. For example,
the Omega test will transform
to
.
This operation can be viewed as shadow casting: if
is a set of constraints on
,
and
that
describes a dodecahedron,
is a set of constraints on
and
that describe
the shadow of the dodecahedron.
Elimination of an existentially quantified integer variable may create
nonconvex constraints.
The Omega test uses two techniques to represent nonconvex
constraints. Some nonconvex constraints
can be described by a convex set of constraints and a set
of stride constraints
(e.g., 3 divides
and 2 divides
).
We use
to denote ``
divides
''.
For example,
is transformed
by the Omega test to
.
In some cases, this method is not sufficient and the Omega
produces a set of constraints in
disjunctive normal form (this is referred to as splintering).