Eliminate Existentially Quantified Variables

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).

Web Accessibility