You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
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.
The text was updated successfully, but these errors were encountered: