java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Extend MathSAT5 SMTLib2 Dumping for Quantified Formulas or Disallow Quantifiers

Open baierd opened this issue 9 months ago • 0 comments

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.

baierd avatar Mar 03 '25 18:03 baierd