Option to disable the type hierarchy in the SMT translation

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

This feature request documents the need for an option to omit all type hierarchy related symbols (e.g. u2i/i2u, ...) and axioms from the problem when translating to SMT-LIB. This was also requested in https://git.key-project.org/key/key/-/wikis/KaKeY%202022-03-04, since otherwise MathSAT can not be used for floats.

Background

Quite some effort has been put into the (new/non-legacy) SMT translation to be able to translate the type hierarchy when encoding a sequent to SMT-LIB. However, there are problems:

1. Some SMT solvers (for example MathSAT) do not support quantifiers. While !514 will soon add the possibility to disable handlers individually (in particular the QuantifierHandler) and also to provide a solver-specific preamble, this is not sufficient, as the type hierarchy axiomatisation will also contain quantified formulas.

2. The type hierarchy often misleads or at least increase the solving time in problems that have nothing to do with the type hierarchy.

3. In particular, the embedding of integers and booleans into U (see image below) frequently hinders Z3 from finding a solution.

Additional information

Overview over the current encoding of type hierarchy (implemented by (at)mulbrich and (at)schiffl):

For more information about the encoding technique, see https://doi.org/10.1007/978-3-642-12002-2_26.
The purpose of this image is to demonstrate that the overhead through the type translation can get large. To give an example, for the contraposition example, there are already 16 axioms (most of them with quantifiers) added for the type hierarchy/translation.

---

Information:

• created_at: 2022-03-11T12:42:39.421Z
• updated_at: 2022-03-11T12:42:39.421Z
• closed_at: None (closed_by: )
• milestone: v2.12.0
• user_notes_count: 0