Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add solver independent quantifier elimination with ultimate eliminator #462

Draft
wants to merge 79 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
79 commits
Select commit Hold shift + click to select a range
1cc2659
Add UltimateEliminator dependencies to ivy and the classpath and inte…
Nov 13, 2024
e4aa914
add dependencies for Ultimate Eliminator
Anastasia-Gu Nov 27, 2024
6271bf9
add dependencies for Ultimate Eliminator
Anastasia-Gu Nov 27, 2024
349ac26
add dependencies for Ultimate Eliminator
Anastasia-Gu Nov 27, 2024
ed9c398
Add more UltimateEliminator dependencies to ivy and the classpath and…
Dec 4, 2024
bbd1848
Extend UltimateEliminator test example with hints
Dec 4, 2024
6d12d67
added Ultimate Eliminator integration to CVC5 and Z3
Anastasia-Gu Feb 7, 2025
231935a
add Mathsat5QuantifiedFormulaManager;
Anastasia-Gu Feb 11, 2025
2efbf7e
fix ant
Anastasia-Gu Feb 15, 2025
d5eacf6
fix ant
Anastasia-Gu Feb 15, 2025
481ebaa
implement bound variables for Mathsat5QuantifiedFormulaManager
Anastasia-Gu Feb 18, 2025
ec1a17c
implement quantified formula generation for Mathsat5QuantifiedFormula…
Anastasia-Gu Feb 20, 2025
2dae218
remove quantifiedFormula initialization and fix for loop
Anastasia-Gu Feb 23, 2025
5e58542
initial commit for UltimateEliminator support for Yices2 and Bitwuzla
Anastasia-Gu Feb 26, 2025
0d163bc
add UltimateEliminatorWrapper to AbstractQuantifiedFormulaManager
Anastasia-Gu Feb 27, 2025
def1a38
add UltimateEliminatorWrapper
Anastasia-Gu Feb 27, 2025
188bc9e
Improve Mathsat5 quantifier support
Feb 27, 2025
e3d2614
put FormulaManager and mkWithoutQuantifier in AbstractQuantifiedFormu…
Anastasia-Gu Mar 5, 2025
100cb72
format code with ant
Anastasia-Gu Mar 5, 2025
29c1b30
fix mkWithoutQuantifier
Anastasia-Gu Mar 6, 2025
02a7e6c
revert
Anastasia-Gu Mar 6, 2025
d13c401
fix CI errors
Anastasia-Gu Mar 6, 2025
729e37d
fix CI errors
Anastasia-Gu Mar 6, 2025
acaf7da
Rework setup of QuantifierManagerTest so that the setup does not bloc…
Mar 6, 2025
3e318c0
Implement a method for Yices2 that allows the creation of bound varia…
Mar 6, 2025
3d4b036
Rework Yices2 quantifier creation with bound variables
Mar 6, 2025
25be000
Add Yices2 quantifier support in the manager
Mar 6, 2025
5ba98cd
Remove Boolector quantifier support (as it can never be supported)
Mar 6, 2025
f9e4c5a
Remove Boolector from QuantifierManagerTest
Mar 6, 2025
64a70f7
Add bound variables to Yices2 visitor
Mar 6, 2025
9a256e9
Disable quantifier tests that Yices2 can't handle
Mar 6, 2025
a787c54
Add visitor case for Yices2 quantifiers
Mar 6, 2025
d84820f
Use full import list instead of * in Yices2FormulaCreator
Mar 6, 2025
efc25cf
Move Yices2 free variable creation method to native test class and di…
Mar 6, 2025
96aeb4d
Move Yices2 free and bound variable creation method to creator and ca…
Mar 6, 2025
1c96551
Merge branch 'fix_yices2_quantifier' into remove_boolector_quantifiers
Mar 6, 2025
75085ff
Format
Mar 6, 2025
bf75c61
Merge release 5.0.1 with fix for Yices2 quantifiers and Boolector qua…
Mar 6, 2025
6bcc200
add UltimateEliminator support to Princess
Anastasia-Gu Mar 7, 2025
4dd3133
adjust Yices2 to previous changes to AbstractQuantifiedFormulaManager
Anastasia-Gu Mar 7, 2025
0b3175e
fix mkWithoutQuantifier in AbstractQuantifiedFormulaManager
Anastasia-Gu Mar 7, 2025
741b6ca
add some tests and exclude unsupported Solvers
Anastasia-Gu Mar 7, 2025
dbd8f66
implement eliminateQuantifiersUltimateEliminator in AbstractQuantifie…
Anastasia-Gu Mar 8, 2025
347d7ad
improve error handling of eliminateQuantifiers
Anastasia-Gu Mar 9, 2025
9d834c9
add tests for solver-independent quantifier elimination
Anastasia-Gu Mar 9, 2025
7200f60
fix some CI issues
Anastasia-Gu Mar 9, 2025
a4ad348
refactor eliminateQuantifiers to increase readability
Anastasia-Gu Mar 9, 2025
d92ca24
fix warnings
Anastasia-Gu Mar 9, 2025
75bdfc0
revert restriction for dumpFormulaImpl in Mathsat5FormulaManager
Anastasia-Gu Mar 9, 2025
6eae73d
fix CI
Anastasia-Gu Mar 13, 2025
9558318
fix more CI
Anastasia-Gu Mar 13, 2025
0baa28a
fix more more CI
Anastasia-Gu Mar 14, 2025
c5af782
shorten method names for checkstyle
Anastasia-Gu Mar 14, 2025
7374a04
remove Mathsat from tests that require native quantification
Anastasia-Gu Mar 14, 2025
71f443d
remove Mathsat from tests that require native quantification
Anastasia-Gu Mar 14, 2025
4032091
remove Mathsat from more tests that require native quantification
Anastasia-Gu Mar 14, 2025
9bead2b
refactor assume messages for tests where Mathsat5 got removed
Anastasia-Gu Mar 15, 2025
822f945
pulled SolverConcurrencyTest from master
Anastasia-Gu Mar 15, 2025
3207380
format code
Anastasia-Gu Mar 15, 2025
7fcae4b
refactor dependencies
Anastasia-Gu Mar 16, 2025
dd0c425
remove unused method from UltimateEliminatorWrapper
Anastasia-Gu Mar 16, 2025
cdff920
add quantifier elimination tests and refactor method names
Anastasia-Gu Mar 17, 2025
19c675f
remove unused option
Anastasia-Gu Mar 17, 2025
fa7ed3e
remove not thrown Exceptions from method signatures
Anastasia-Gu Mar 17, 2025
3c95681
rename logger componentName for UltimateEliminator
Anastasia-Gu Mar 17, 2025
0e3c875
Merge branch 'master' into add_solver_independent_quantifier_eliminat…
Anastasia-Gu Mar 19, 2025
ec6d411
Merge branch 'refs/heads/master' into add_solver_independent_quantifi…
Anastasia-Gu Mar 20, 2025
c456aea
merge master into branch
Anastasia-Gu Mar 20, 2025
f5a14a6
remove unused IOException
Anastasia-Gu Mar 20, 2025
cf60709
remove MathSAT5 and Yices2 from quantifier tests
Anastasia-Gu Mar 20, 2025
b7bf341
rename ProverOption SOLVER_INDEPENDENT_QUANTIFIER_ELIMINATION_BEFORE …
Anastasia-Gu Mar 20, 2025
e973e5f
updated options and option handling
Anastasia-Gu Mar 24, 2025
763f8e1
fix tests
Anastasia-Gu Mar 24, 2025
613eb07
resolve some comments
Anastasia-Gu Mar 24, 2025
7a1e814
fix CI
Anastasia-Gu Mar 24, 2025
fb403ff
fix CI
Anastasia-Gu Mar 24, 2025
64d7782
fix CI
Anastasia-Gu Mar 24, 2025
9d86ef4
slf4j-nop.jar to classpath to disable failed job from spotbugs
Anastasia-Gu Mar 24, 2025
8f2b80c
Revert "slf4j-nop.jar to classpath to disable failed job from spotbugs"
Anastasia-Gu Mar 24, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
add dependencies for Ultimate Eliminator
Anastasia-Gu committed Nov 27, 2024
commit e4aa91433542e7355b02851376f1a2d37416695d
1 change: 1 addition & 0 deletions .classpath
Original file line number Diff line number Diff line change
@@ -15,6 +15,7 @@ SPDX-License-Identifier: Apache-2.0
<classpathentry kind="lib" path="bin/"/>
<classpathentry kind="lib" path="lib/java/core/guava.jar" sourcepath="lib/java-contrib/guava-sources.jar"/>
<classpathentry kind="lib" path="lib/java/core/ultimate-model-checker-utils.jar" sourcepath="lib/java-contrib/ultimate-model-checker-utils-sources.jar"/>
<classpathentry kind="lib" path="lib/java/core/ultimate-core.jar" sourcepath="lib/java-contrib/ultimate-core-sources.jar"/>
<classpathentry kind="lib" path="lib/java/test/guava-testlib.jar" sourcepath="lib/java-contrib/guava-testlib-sources.jar"/>
<classpathentry kind="lib" path="lib/java/test/truth.jar" sourcepath="lib/java-contrib/truth-sources.jar"/>
<classpathentry kind="lib" path="lib/java/test/junit.jar"/>
25 changes: 11 additions & 14 deletions .idea/JavaSMT.iml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

13 changes: 1 addition & 12 deletions .idea/ant.xml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions lib/ivy.xml
Original file line number Diff line number Diff line change
@@ -149,6 +149,8 @@ SPDX-License-Identifier: Apache-2.0
<dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources"/>
<dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-model-checker-utils"
rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
<dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-core"
rev="2021-10-08-r997cd7c355" conf="core->runtime; contrib->sources"/>

<!-- Princess for our Maven release -->
<dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12" conf="runtime-princess-with-javacup->default; contrib->sources"/>