Quantifier support for MathSAT

[PhilippWendler]

The MathSAT API contains methods for quantifiers, but it seems that JavaSMT does not expose them. This should be added in order to not hide solver features from users of JavaSMT. We might also want to try the quantifier support in CPAchecker.

[kfriedberger]

Quote from the official MathSAT website:

Release Notes for v5.6.0: Added support for quantifiers in the front-end only. This means that it is now possible to use the MathSAT API to parse/create/manipulate/print formulas involving quantified variables. The solver still works only on quantifier-free input though. For more details, see the new API functions msat_make_exists, msat_make_forall, msat_make_variable, msat_existentially_quantify, msat_term_is_exists, msat_term_is_forall, msat_term_is_variable.

There has not yet been an official statement about backend support for quantifiers. Thus, I would not make too much promises here. We can at least support building quantified formulas with a QuantifiedFormulaManager and then check solver support when solving the query.

[PhilippWendler]

Ok, I wasn't aware of this. If one can do nothing with these formulas, I am not sure whether it is better to have the API or not.