Princess/Ostrich update #518
Conversation
src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java
Show resolved
Hide resolved
|
@daniel-raffler You could ask @PhilippWendler for an SVN account to upload such files directly in the future. Sosy-Ivy has strict rules, e.g., it is append-only and quite strcitly structured, and commits follow a specific pattern. |
… a 0) is still a function (This part breaks if we use just `div` in Princess)
Thanks for your help with the binaries! I already have an account from when CPAchecker still used svn, but last time I tried to upload binaries to the Ivy repository it was still rejected. However, this could just be a problem with my configuration, so I'll try again next time |
The rest still seem to have issues on Princess
Princess no longer rewrites the formula and will now return the correct result
| private static boolean isValue(IFunApp pExpr) { | ||
| if (!pExpr.fun().equals(Rationals.frac()) && !pExpr.fun().equals(Rationals.fromRing())) { | ||
| return false; | ||
| } |
There was a problem hiding this comment.
Does this work for non-rational numbers? I would assume that Intgers are not longer handled here.
There was a problem hiding this comment.
No, it will only detect rational number literals. Other types of literals were handled separately in the visitor and have their own tests. However, since the name was a little confusing I reorganized the code in 8d5fcd1 and all literals are now handled by isValue
Princess will rewrite "floor" as an epsilon term. We'll have to match it in the visitor and restore the original call to get this to work
| requireRationals(); | ||
| requireRationalFloor(); | ||
| // TODO Princess will rewrite floor. Add backtranslation in the visitor | ||
| // TODO Princess will rewrite floor. Add back translation in the visitor |
There was a problem hiding this comment.
No, we do not need to add a precise backwards-mapping. The solver is allowed to rewrite the formula.
There was a problem hiding this comment.
The issue here is that Princess uses quantifiers and we do not handle quantified formulas correctly in some cases.
There was a problem hiding this comment.
Yes, the comment was about quantifiers and/or epsilon terms that Princess likes to introduce for operations like these
| requireRationals(); | ||
| requireRationalFloor(); | ||
| // TODO Princess will rewrite floor. Add backtranslation in the visitor | ||
| // TODO Princess will rewrite floor. Add back translation in the visitor |
There was a problem hiding this comment.
The issue here is that Princess uses quantifiers and we do not handle quantified formulas correctly in some cases.
Hello everyone,
this will update Princesss to version 2025-06-25 and Ostrich to 2.0. Our current version is still from the end of last year and there have been several improvements since then. Specifically, Princess now has special
IFunctions for rational operations like additional or division. The old version would rewrite rational formulas as integer-only formulas, which makes it hard to restore the original formula for the visitor. In Ostrich one of our bugs was closed, andstr_from_codeis now supported.@kfriedberger: Could you please upload the packages from Maven? Here is what I used locally for testing: