Hackeython Working Group: SMT Translation without Type Embedding

Shepard: Wolfram

Motivation

SMT solvers only use a "flat" type hierarchy without subtypes. In contrast to that, KeY has a type hierarchy, where everything (in particular int and bool) is a subtype of any. To reflect this, in our SMT translation an embedding is used (more information can be found in #1703):

However, the use of these embedding functions (u2i, i2u, u2b, b2i) sometimes seems to confuse the solver.

Idea

The idea of this working group is to provide an option to disable the type embedding (and maybe also the translation of the type hierarchy). However, we have to make sure that this translation stays is sound, so we need to discuss when we are allowed to translate integers from KeY directly to the SMT Ints.

Further SMT related bugs/features that we might look into

• Support the modulo operator in the SMT translation.
• Select the next open goal after applying the SMT result (should be consistent with behavior when closing a branch via taclets).
• Caching of SMT solver results: If the SMT input did not change (same content sent to SMT solver again), we could remember the result from last time. This is particularly useful if you have large timeouts.
• Catch exceptions (StreamClosedException) when running SMT solvers (in particular CVC4 and sometimes cvc5).