Princess: No StringFormulaManager

[mkuijn-cb]

The constructor for PrincessFormulaManager passes null for parameter strManager upwards to AbstractFormulaManager. My understanding is that Princess does support strings and regex if combined with the OSTRICH library. Is there a reason why support for this is infeasible or is it just a matter of simply not being implemented yet.

[kfriedberger]

There even exists an older PR for that topic: #257 . That PR was blocked by some issues with Princess. Someone might want to look at the current state of Princess and update the PR to a current state.

[baierd]

@daniel-raffler could you take a look at this?

[daniel-raffler]

I've resurrected the branch from the PR (257-more-theories-for-princess) and updated it to the latest version of JavaSMT. It's now also running the latest version of Ostrich, which fixes one of the issues that was reported by @kfriedberger (this is the bug report).

However, there are unfortunately a number of issues left as can be seen from the results of the test suite here. Support for String theory seems to be missing some key operations that are needed for our tests. I'll open some new tickets for Ostrich later today and will then link them in this thread. Rationals also have some issues left and @kfriedberger has has already opened two tickets for Princess here and here when he last worked on this PR.

All in all Rationals look better than String Theory, but at this point neither seems to be quite ready for inclusion yet. We'll have to wait and see if the remaining issues can be fixed before merging this.

[daniel-raffler]

I've opened tickets for Ostrich now

• Ostrich crashes during model extraction when there are "cyclical definitions" uuverifiers/ostrich#87
• Proving formulas with no singleton Strings uuverifiers/ostrich#88
• str.<= is not reflexiv uuverifiers/ostrich#89