Eliminator

Ultimate Eliminator is a tool that takes as an input a formula that may contain quantifiers and tries to find a logically equivalent formula without quantifiers. We call this task quantifier elimination.

Quantified formulas are notoriously difficult to solve and several state-of-the-art SMT solvers support only quantifier-free formulas. Several algorithms that are used in the Ultimate Automizer software verifier produce quantified formulas. In order to make these formulas fit for a larger number of SMT solvers and algorithms that require quantifier-free formulas the developers of Ultimate Automizer implemented several simple techniques that try to eliminate quantifiers. For example, one of these algorithms replaces a formula of the form ∃x.φ(x) ∧ x = t by the formula φ(t).

Our motivation for developing Ultimate Eliminator was to make these quantifier elimination techniques accessible to users that want to eliminate quantifiers.

The current version of Ultimate Eliminator is only a prototype that should demonstrate the power of Ultimate's quantifier elimination techniques. This tool is a user interface that takes SMT-LIB~2.6 compatible input tries to eliminate quantifiers in this input and passes the modified input to a user defined SMT-LIB 2.6 compatible solver. I.e., it is a wrapper for an SMT solver that give this solver capabilities to handle quantified formulas.

Web Interface

Ultimate Eliminator is available via a web interface. In this web interface Ultimate Eliminator wraps the SMTInterpol SMT solver.

Input/Output Format

Currently, Ultimate Eliminator is only a wrapper for SMT solvers. We also want to make the quantifier elimination directly accessible to users but have not yet decided for an interface. Current ideas are a new eliminate-quantifiers SMT command or the possibility to pass a formula via the command line. If you would like to use Ultimate Eliminator we are open to other ideas as well. Please contact Matthias Heizmann.

Source Code

The source code of Ultimate Eliminator and all quantifier elimination techniques is available at GitHub..