Skip to content

Princess/Ostrich update #518

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.

Sign up for GitHub

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

Merged
merged 16 commits into from
Sep 14, 2025
+123 −141
Merged

Princess/Ostrich update #518

Changes from 1 commit
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
c84ca3e
Princess: Update Princess to version 2025-06-25 and Ostrich to 2.0
daniel-raffler Sep 5, 2025
fec5a61
Princess: Use total definition for division where a/0 is allowed
daniel-raffler Sep 5, 2025
61f810d
Princess: Remove extra parentheses
daniel-raffler Sep 6, 2025
11d1c9b
Princess: Add a comment about divWithSpecialZero
daniel-raffler Sep 6, 2025
1e3ef7e
Princess: Remove Princess from the blacklist in the testDivisionByZer…
daniel-raffler Sep 6, 2025
2c14481
Princess: Add another case to the testDivisionByZero to check that (/…
daniel-raffler Sep 6, 2025
f87a843
Princess: Enable one of the tests for codepoints in string theory
daniel-raffler Sep 6, 2025
3141539
Princess: Update a test in FormulaClassifierTest
daniel-raffler Sep 6, 2025
ccc8cbe
Princess: Use variables to make the test for zero division more general
daniel-raffler Sep 7, 2025
8d5fcd1
Princess: Handle all constant values for the visitor in isValue()
daniel-raffler Sep 7, 2025
ed02e9b
Princess: Add support for `floor` operation
daniel-raffler Sep 8, 2025
2347d94
Princess: Fix imports
daniel-raffler Sep 8, 2025
a58cc80
Princess: Fix the broken test
daniel-raffler Sep 8, 2025
4f81e8d
Princess: disable collection of model constraints if model generation…
kfriedberger Sep 14, 2025
b832ae2
fix CheckStyle warning
kfriedberger Sep 14, 2025
ae36c38
Merge remote-tracking branch 'origin/master' into princess-2025-06-25
kfriedberger Sep 14, 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
4 changes: 2 additions & 2 deletions src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,11 +126,11 @@ public void forallFloorIsLessThanValueTest() throws SolverException, Interrupted
public void visitFloorTest() {
requireRationals();
requireRationalFloor();
// TODO Princess will rewrite floor. Add backtranslation in the visitor
// TODO Princess will rewrite floor. Add back translation in the visitor
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, we do not need to add a precise backwards-mapping. The solver is allowed to rewrite the formula.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The issue here is that Princess uses quantifiers and we do not handle quantified formulas correctly in some cases.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, the comment was about quantifiers and/or epsilon terms that Princess likes to introduce for operations like these

assume()
.withMessage("We don't support \"floor\" in the Princess visitor")
.that(solverToUse())
.isEqualTo(Solvers.PRINCESS);
.isNotEqualTo(Solvers.PRINCESS);

IntegerFormula f = rmgr.floor(rmgr.makeVariable("v"));
assertThat(mgr.extractVariables(f)).hasSize(1);
Expand Down