Add support for Strings and Rationals to the Princess backend

[daniel-raffler]

Hello everyone, the goal of this pull request is to add two more theories for strings and rational numbers to the Princess backend. It is a continuation of the work that went into https://github.com/sosy-lab/java-smt/pull/257. Some of the issues that blocked us from merging it back then have since been resolved, and at least the rational formula manager is actually starting to look pretty good now. Here is a comparison between Princess and some other solvers when running BMC on the ReachSafety-Floats task with option cpa.predicate.encodeFloatAs=RATIONAL set to test the rational formula manager:

It's a bit harder to evaluate how well the String manager is working now. The Ostrich team has been very helpful and they quickly fixed a couple of bugs that we've reported. However, since CPAchecker doesn't use String theory there is no easy way of trying it out.

Linked issues:

Princess (Rationals)

• https://github.com/uuverifiers/princess/issues/7
• https://github.com/uuverifiers/princess/issues/8
• https://github.com/uuverifiers/princess/issues/11
• https://github.com/uuverifiers/princess/issues/12
• https://github.com/uuverifiers/princess/issues/13
• https://github.com/uuverifiers/princess/issues/14
• https://github.com/uuverifiers/princess/issues/15
• https://github.com/uuverifiers/princess/issues/16

Ostrich (Strings)

• https://github.com/uuverifiers/princess/issues/9
• https://github.com/uuverifiers/ostrich/issues/87
• https://github.com/uuverifiers/ostrich/issues/88
• https://github.com/uuverifiers/ostrich/issues/89

I've added (partial) workarounds for the two Princess issues, but some work may still be needed. For Ostrich the biggest limitation is that the solver can only handle constraints where (at least) one of the sides is a singleton (= constant) string. Something like "a str.<= b" where both a and b are variables is already impossible. This is a known issue and they're planning a redesign for the solver that will allow it to handle such constraints. In the mean time we might want to add some additional error messages to make sure that the user knows why their program is failing.

[daniel-raffler]

Looks like this was not easy. Good job!

Thanks!

Also, is it possible to use Ostrich without Princess in theory?

No, unforunately not. Ostrich does include a script to run it directly from the command line, however, internally this will still just call Princess.

From our perspective it's probably best to see Ostrich as the String Theory module of Princess.

[daniel-raffler]

Princess/Ostrich has released new versions of their binaries that include the latest bug fixes for this branch.

@kfriedberger Could you handle uploading the files to our repository? We'll need version 2024-11-08 for Princess (maven) and 1.4.1 for Ostrich (maven). I believe some of the dependencies will also have to be updated and uploaded to our mirror.

[daniel-raffler]

@baierd Could you have another look at this branch to see if there are any remaining issues?

[kfriedberger]

Hi @daniel-raffler . I uploaded Princess 2024-11-08 and Ostrich 1.4.1 to the Sosy-Lab Ivy repository.

PS: You can also do the Ivy publication on your own. The requirement is a Sosy-Lab SVN account with write-access to the SVN repository at https://svn.sosy-lab.org/software/ivy/ . The command lines are documented in Libraries.txt. Please note that that repository must be used in "append-only" style, i.e. you must never ever (*) modify or remove an existing library or XML file.

(*) except in very rare and really critical cases :smile:

[daniel-raffler]

Hi @daniel-raffler . I uploaded Princess 2024-11-08 and Ostrich 1.4.1 to the Sosy-Lab Ivy repository.

Great work! Thanks for your help.

PS: You can also do the Ivy publication on your own. The requirement is a Sosy-Lab SVN account with write-access to the SVN repository at https://svn.sosy-lab.org/software/ivy/ . The command lines are documented in Libraries.txt. Please note that that repository must be used in "append-only" style, i.e. you must never ever (*) modify or remove an existing library or XML file.

(*) except in very rare and really critical cases 😄

Thanks for the tip! I'll have to look into this and see if I actually have write-access to the SVN repository.