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

Published 20 hours ago • verified publisher icon sosy-lab

Add solver independent quantifier elimination with ultimate eliminator

Open Anastasia-Gu opened this issue 8 months ago • 4 comments

  1. Added dependencies for UltimateEliminator in ivy.xml
  2. Integrated classes needed for UltimateEliminator in JavaSMT
  3. Created UltimateEliminatorWrapper class and equipped with a utility class UltimateEliminatorParser
  4. Created options in QuantifiedFormulaManager
  5. Added a Mathsat5QuantifiedFormulaManager
  6. Implemented the method EliminateQuantifiersUltimateEliminator in AbtractQuantifiedFormulaManager
  7. Implemented eliminateQuantifierBeforeMakingFormula in AbtractQuantifiedFormulaManager for when quantifier elimination is done before the native solver gets the formula. (To get the right formula information: with visitor get the name and type of bound variables)
  8. Tests

Anastasia-Gu avatar Mar 20 '25 22:03 Anastasia-Gu

@kfriedberger @PhilippWendler we have 3 warnings from Spotbugs that are empty in this PR. Do you happen to know the reason for this or how to find out?

baierd avatar Apr 02 '25 08:04 baierd

image

  • UrF = Unread Field
  • UwF = Unwritten Field

Please check the code for unused fields or variables.

I also would like to have better Spotbugs messages. I assume this topic is more general and applies to more project at SoSy-Lab. I have not yet checked in CPAchecker or VCloud, whether SpotBugs prints so minimal errors there, too.

UPDATE: Spotbugs at CPAchecker seems to provide better errror messages: image

TODO: Check whether JavaSMT uses the latest version of SpotBugs (no, it does not) and has set all required options for it?

kfriedberger avatar Apr 02 '25 09:04 kfriedberger

Thanks for the help! I guess we are currently not synced to the java project template of SoSy. I'm gonna update it this week!

baierd avatar Apr 07 '25 15:04 baierd

@kfriedberger @PhilippWendler we have 3 warnings from Spotbugs that are empty in this PR. Do you happen to know the reason for this or how to find out?

This is a known SpotBugs bug and fixed in version 4.9.0 (from January).

PhilippWendler avatar Apr 08 '25 05:04 PhilippWendler

Results of running this branch in CPAchecker using Newton refinement in Predicate Abstraction look good and perform on-par and sometimes better than native QE. (I can't upload for some reason)

baierd avatar Jul 21 '25 13:07 baierd

Note: we will postpone this branch until we are up-to-date with Java21 to avoid problems and utilize BV and FP support in SMTInterpol.

baierd avatar Jul 21 '25 13:07 baierd