Next: Verify Implications Up: The Omega Test Previous: Verify the Existence

Remove Redundant Constraints

In the normal operation of the Omega test, we eliminate any constraint that is made redundant by any other single constraint (e.g., is made redundant by ). Upon request, we can use more aggressive techniques to eliminate redundant constraints. We use incomplete tests that can flag a constraint as definitely redundant or definitely not redundant, and a backup complete test. This capability is used when verifying implications and simplifying formulas involving negation.