Add Ultimate Eliminator as solver independet quantifier elimination option

[baierd]

Ultimate Eliminator is a solver independent quantifier eliminator. By adding it, we could offer (limited) quantifier support for quantifier free solvers, e.h. MathSAT5.
However, we need a layer in JavaSMT that allows us to manipulate the formulas before eliminating the quantifier and then translating the formulas to the final solver. Since Ultimate Eliminator is based in Java, adding should be simple. One possibility of a caching layer would be using Princess, as it supports quantifiers and is always available.

@kfriedberger thoughts?

[kfriedberger]

I am not sure about the best architectural solution here.
However, I doupt the need for a complete intermediate layer.
Thus let me ask a few questions first:

General question:

• Should the user be able to call the new QE in only a few places, e.g., is it called manually? Or should the QE be applied transparently in all possible places, if some specific option is set.
• Which interface does Ultimate Eliminator provide? Does it somehow use an API where the parameters that can be converted forward/backward via FormulaVisitor?

The intermediate layer is unclear:

• Is there really a need for a new intermediate layer?
• Would it only redirect the calls for prover.addAssertion or also every formula construction method? There is potential overhead of traversing every formula several times.
• Would the intermediate layer redirect formula construction to SMTInterpol/Princess only and use another solver as specified by the user.

Possible alternative:

• Would is be sufficient to have one additional method like eliminateQuantifiers: formula -> formula similar to UF elimination (see https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/utils/UfElimination.java)? Then the user needs to call it manually.
• Which solvers do allow/not allow the construction for quantifier-based formulas (without solving them). I assume most solvers already provide this feature in some way, because they can parse SMTLIB2. We might not have implemented this in JavaSMT for all of them.
• Do we need/want the mixture of SMTInterpol/Princess -> Ultimate Eliminator -> concrete solver? This might make debugging quite hard. Having some manually called method that performs some kind of transformation is actually quite similar to the use-case of FormulaTransformation and might be easier for the user to understand and for debugging.

[baierd]

I agree that a solution is not obvious here.

I'd say that all solvers should be able to utilize external quantifier/quantifier elimination, as Ultimate Eliminator seems to yield better results for quantifier elimination in solvers that support it natively in many cases.
A possible solution might be lazily instantiating the quantifier formula, such that the formula fails with an exception if not handled with a elimination call.

While we are at it, since our group tried several quantifier based strategies lately, we should add the possibility for users to choose options in the QuantifedFormulaManager in some way, such that the elimination strategies can be chosen. We might tie this into the addition of Ultimate Eliminator (UE).

The interface of UE is mainly SMT2 files/text. It has a wrapper that allows input via command line, which is really just the same. The components of the wrapper seem to use SMTInterpol by the way! (can be found in the Ultimate repo here.)

We should definitively get in contact with Matthias Heizmann, as he seems to be the maintainer, and they state that they are not decided on an interface yet and are open for suggestions.

[kfriedberger]

Currently, JavaSMT does not use any process-based external tools, but inlcudes them via direct API calls (like JNI).
This has the benefit of not needing to kill external processes. We need to properly investigate their (future?) API and its usage.

Having UE using SMTInterpol can be a benefit for having a known API. However, it also has the issue of packaging SMTInterpol (or its core libraries) as a dependency, because the Ultimate team did until now not manage to separate their own dependencies in a usable way (see their mono-repository at https://github.com/ultimate-pa/ultimate/tree/dev/trunk/source or just ask the CPAchecker developers about LassoRanker conflicting with SMTInterpol in CPAchecker).