java-smt
java-smt copied to clipboard
Extend MathSAT5 SMTLib2 Dumping for Quantified Formulas or Disallow Quantifiers
MathSAT5 can create quantified formulas, but not solve them. However, they can be dumped with msat_to_smtlib2_ext() and msat_to_smtlib2_term().
msat_to_smtlib2_ext() exports a full SMTLib2 program, while msat_to_smtlib2_term() exports only the formula given, without definitions.
Once we support quantification in our API (see #297 ), we need to discuss if we want to switch to one of the methods above for dumping, add an option to switch to one of them, or not publicly expose the quantification API for MathSAT.