Back translation for Princess rewrites

[daniel-raffler]

Hello everyone,
this PR aims to address some of the issues that came up while working on the tracing delegate. Specifically, Princess will often rewrite formulas for operations like multiplication, divison or floor using quantifiers and epsilon terms. As an example let's take the formula RationalFormulaManager.floor(RationalFormulamanager.makeNumber(0.5)). Here Princess will produce the following expression:

EPS EX (((_1 = EPS EX EX EX ((((_0 = Rat_frac(1, 2)) & (_1 = mul(_3, _2))) & (_2 = _4)) & (((_0 + -1 * _1) >= 0) & (((_1 + -1 * (_0 + -1 * \if ((_2 >= 0)) \then (_2) \else (-1 * _2))) + -1) >= 0)))) & (_0 = Rat_denom)) & ((_0 + -1) >= 0))

While the expression is logically equivalent, and solvers are allowed to make some rewrites, such a fundamental transformation makes is quite hard to understand the meaning of the term. More importantly, it will cause crashes in our visitor as epsilon terms are not supported by JavaSMT. Because of this many formulas in Princess currently can't be visited.

In this PR we try to fix the problem by translating Princess formulas back to their original operations. This is done by using pattern matching in the visitor: We first create a set of patterns by evaluating operations like floor or division on some generic arguments, f.ex RationalFormulaManager.floor(a) or RationalFormlaManager.divide(a, b) where a, b are variables. Then we match those patterns against the current formula in the visitor. If they can be unified the substitution is then used to recover the original arguments for the operation. We then visit the operation with the recovered arguments and skip any quantifiers or epsilon terms that Princess has created

The number of patterns that are needed is relatively small and currently looks like this:

    ImmutableList.of(
        // Rational.divide
        buildPattern(
            PrincessRationalDivisionDeclaration.INSTANCE,
            ImmutableList.of(symbolReal1, toReal(symbolInt2)),
            true),
        buildPattern(
            PrincessRationalDivisionDeclaration.INSTANCE,
            ImmutableList.of(symbolReal1, symbolReal2)),

        // Rational.floor
        buildPattern(PrincessRationalFloorDeclaration.INSTANCE, ImmutableList.of(symbolReal1)),

        // Integer.divide
        buildPattern(
            PrincessIntegerDivisionDeclaration.INSTANCE,
            ImmutableList.of(IExpression.i(2), symbolInt2),
            true),
        buildPattern(
            PrincessIntegerDivisionDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(2))),
        buildPattern(
            PrincessIntegerDivisionDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(2).unary_$minus())),
        buildPattern(
            PrincessIntegerDivisionDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(3)),
            true),
        buildPattern(
            PrincessIntegerDivisionDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()),
            true),

        // Integer.modulo
        buildPattern(
            PrincessIntegerModuloDeclaration.INSTANCE, ImmutableList.of(symbolInt1, symbolInt2)),
        buildPattern(
            PrincessIntegerModuloDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(2))),
        buildPattern(
            PrincessIntegerModuloDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(2).unary_$minus()),
            true),
        buildPattern(
            PrincessIntegerModuloDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(3)),
            true),
        buildPattern(
            PrincessIntegerModuloDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()),
            true),

        // Integer.modularCongruence
        buildPattern(
            PrincessModularCongruenceDeclaration.INSTANCE,
            ImmutableList.of(symbolInt1, symbolInt2, IExpression.i(3)),
            true));

Note that for some operations we need several patterns to cover all cases. We should make sure that these patterns are indeed always enough to match the terms that Princess returns. However, from my experience the transformation that Princess applies is relatively static and the solver doesn't try to optimize these terms any further.

We could alternatively still ask the Princess developers to handle the back translation for us. However, I haven't opened an issue about this yet.