Add solver independent quantifier elimination with ultimate eliminator by Anastasia-Gu · Pull Request #462 · sosy-lab/java-smt

Anastasia-Gu · 2025-03-20T22:22:20Z

Added dependencies for UltimateEliminator in ivy.xml
Integrated classes needed for UltimateEliminator in JavaSMT
Created UltimateEliminatorWrapper class and equipped with a utility class UltimateEliminatorParser
Created options in QuantifiedFormulaManager
Added a Mathsat5QuantifiedFormulaManager
Implemented the method EliminateQuantifiersUltimateEliminator in AbtractQuantifiedFormulaManager
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)
Tests

…llij

… intellij

format code add missing UltimateEliminator dependencies

…Manager

…laManager

…k most solvers (now 152 tests run over all solvers compared to 89 before)

…bles for quantifiers

This reverts commit 9d86ef4.

src/org/sosy_lab/java_smt/api/QuantifiedFormulaManager.java

baierd · 2025-04-02T08:19:47Z

@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?

kfriedberger · 2025-04-02T09:04:45Z

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:

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

…the delegates

baierd · 2025-04-07T15:31:56Z

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!

PhilippWendler · 2025-04-08T05:49:04Z

@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).

…verride it in Mathsat5QuantifiedFormulaManager

…antifierCreationMethod

…r_elimination_with_ultimate_eliminator' into add_solver_independent_quantifier_elimination_with_ultimate_eliminator # Conflicts: # src/org/sosy_lab/java_smt/delegate/debugging/DebuggingQuantifiedFormulaManager.java # src/org/sosy_lab/java_smt/delegate/statistics/StatisticsQuantifiedFormulaManager.java # src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedQuantifiedFormulaManager.java

baierd

Your test classes test the options for quantifier creation and elimination explicitly. However, you could add a second or even third parameter to the parameterized test setup of SolverBasedTest0.ParameterizedSolverBasedTest0 (by extending it with a subclass or two). Then you could automatically check ALL option combinations with all solvers.

Also, please extend the documentation of the methods in the AbstractQuantifiedFormulaManager that deal with the interaction of UE with the solvers. They have very little to none currently.

baierd · 2025-04-10T12:41:18Z

src/org/sosy_lab/java_smt/basicimpl/AbstractQuantifiedFormulaManager.java

+    return fmgr.orElseThrow();
+  }
+
+  public void setFmgr(AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> pFmgr) {


Why not simply set it in the AbstractFormulaManagers constructor for existing QuantifiedFormulaManagers?
Then its in the same package and can be package-private.
This would also prevent other developers from forgetting.

baierd · 2025-04-10T12:42:29Z

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5QuantifiedFormulaManager.java

+  @Override
+  protected String dumpFormula(BooleanFormula bf) {
+    return ((Mathsat5FormulaManager) getFmgr())
+        .dumpFormulaImplExt(extractInfo(bf), "qFormulaNameMathsat5");


Why not out the implementation of dumpFormulaImplExt here?

baierd · 2025-04-10T12:43:39Z

src/org/sosy_lab/java_smt/test/ultimate/UltimateEliminatorWrapper.java

+   * Simplifies and try to remove the quantifiers from the given term using the UltimateEliminator.
+   */
  public Term simplify(Term pTerm) {
    return ultimateEliminator.simplify(pTerm);


UE has lots of options that allow different types of simplifications.
Do we have a way of changing those?

As far as I understand it, we currently do not. As we would have to Override the "simplify" method in the UltimateEliminator source code to do so. I tried creating a class that extends UltimateEliminator to override the method, however, it ended with accessibility issues
See: https://github.com/ultimate-pa/ultimate/blob/0ed21c286de111155dccfbaf80bfbc5906a6435f/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/UltimateEliminator.java#L268

baierd · 2025-04-10T12:49:46Z

src/org/sosy_lab/java_smt/basicimpl/AbstractQuantifiedFormulaManager.java

+        try {
          return wrap(eliminateQuantifiers(extractInfo(pF)));
-        } else {
+        } catch (Exception e1) {


Please never plainly catch Exception. Always catch named exceptions only.

baierd · 2025-04-10T12:51:07Z

src/org/sosy_lab/java_smt/basicimpl/AbstractQuantifiedFormulaManager.java

+        }
+
+      case ULTIMATE_ELIMINATOR_FALLBACK_ON_FAILURE:
+        try {


You are repeating the try-catch blocks quite a lot. You could extract them into a method.

…nd tests

add Level.WARNING instead of null to logger

baierd · 2025-07-21T13:32:29Z

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 · 2025-07-21T13:33:21Z

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 and others added 30 commits November 13, 2024 16:57

Add UltimateEliminator dependencies to ivy and the classpath and inte…

1cc2659

…llij

add dependencies for Ultimate Eliminator

e4aa914

add dependencies for Ultimate Eliminator

6271bf9

add dependencies for Ultimate Eliminator

349ac26

Add more UltimateEliminator dependencies to ivy and the classpath and…

ed9c398

… intellij

Extend UltimateEliminator test example with hints

bbd1848

added Ultimate Eliminator integration to CVC5 and Z3

6d12d67

add Mathsat5QuantifiedFormulaManager;

231935a

format code add missing UltimateEliminator dependencies

fix ant

2efbf7e

fix ant

d5eacf6

implement bound variables for Mathsat5QuantifiedFormulaManager

481ebaa

implement quantified formula generation for Mathsat5QuantifiedFormula…

ec1a17c

…Manager

remove quantifiedFormula initialization and fix for loop

2dae218

initial commit for UltimateEliminator support for Yices2 and Bitwuzla

5e58542

add UltimateEliminatorWrapper to AbstractQuantifiedFormulaManager

0d163bc

add UltimateEliminatorWrapper

def1a38

Improve Mathsat5 quantifier support

188bc9e

put FormulaManager and mkWithoutQuantifier in AbstractQuantifiedFormu…

e3d2614

…laManager

format code with ant

100cb72

fix mkWithoutQuantifier

29c1b30

revert

02a7e6c

fix CI errors

d13c401

fix CI errors

729e37d

Rework setup of QuantifierManagerTest so that the setup does not bloc…

acaf7da

…k most solvers (now 152 tests run over all solvers compared to 89 before)

Implement a method for Yices2 that allows the creation of bound varia…

3e318c0

…bles for quantifiers

Rework Yices2 quantifier creation with bound variables

3d4b036

Add Yices2 quantifier support in the manager

25be000

Remove Boolector quantifier support (as it can never be supported)

5ba98cd

Remove Boolector from QuantifierManagerTest

f9e4c5a

Add bound variables to Yices2 visitor

64a70f7

Anastasia-Gu added 4 commits March 24, 2025 03:56

fix CI

fb403ff

fix CI

64d7782

slf4j-nop.jar to classpath to disable failed job from spotbugs

9d86ef4

Revert "slf4j-nop.jar to classpath to disable failed job from spotbugs"

8f2b80c

This reverts commit 9d86ef4.

baierd requested changes Apr 1, 2025

View reviewed changes

src/org/sosy_lab/java_smt/api/QuantifiedFormulaManager.java Outdated Show resolved Hide resolved

baierd added 3 commits April 3, 2025 17:11

Remove Boolector quantifier support (as it can never be supported)

db28834

Remove Boolector from quantified tests

0baae82

Use the delegate to set the options for quantified formula manger in …

7e5766d

…the delegates

Anastasia-Gu added 8 commits April 8, 2025 17:52

extend AbstractQuantifiedFormulaManager with dumpFormula method and o…

2b4b834

…verride it in Mathsat5QuantifiedFormulaManager

add documentation

90cf638

replace usage of ProverOption with QuantifierEliminationMethod and Qu…

b081df7

…antifierCreationMethod

remove unused code

1af6a9f

fix pipeline issues

e7d00d8

fix more pipeline issues

389a2a1

fix even more pipeline issues

dba7e59

baierd requested changes Apr 10, 2025

View reviewed changes

Anastasia-Gu added 7 commits April 10, 2025 18:46

move dumpFormulaImplExt to Mathsat5QuantifiedFormulaManager

61107bb

set qfmgr's fmgr in AbstractFormulaManagers constructor

2dd9c77

extract repeated try-catch blocks to methods

b7f9cde

add documentation

4e72016

extract repeated try-catch blocks for formula creation to a method

c9cd36a

add null and empty checks to eliminateQuantifierBeforeMakingFormula a…

de43b95

…nd tests

remove logic from msat_to_smtlib2_ext

e97a9ef

add Level.WARNING instead of null to logger

Conversation

Anastasia-Gu commented Mar 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

baierd commented Apr 2, 2025

Uh oh!

kfriedberger commented Apr 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

baierd commented Apr 7, 2025

Uh oh!

PhilippWendler commented Apr 8, 2025

Uh oh!

baierd left a comment

Choose a reason for hiding this comment

Uh oh!

baierd Apr 10, 2025

Choose a reason for hiding this comment

Uh oh!

baierd Apr 10, 2025

Choose a reason for hiding this comment

Uh oh!

baierd Apr 10, 2025

Choose a reason for hiding this comment

Uh oh!

Anastasia-Gu Apr 10, 2025

Choose a reason for hiding this comment

Uh oh!

baierd Apr 10, 2025

Choose a reason for hiding this comment

Uh oh!

baierd Apr 10, 2025

Choose a reason for hiding this comment

Uh oh!

baierd commented Jul 21, 2025

Uh oh!

baierd commented Jul 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

4 participants

Anastasia-Gu commented Mar 20, 2025 •

edited

Loading

kfriedberger commented Apr 2, 2025 •

edited

Loading