More theories for Princess

[serras]

Princess supports more theories than the ones currently announced in java-smt. The goal of this PR is to support them:

• [X] String theory via naïve theory
• [ ] String theory via Ostrich, an extension to Princess
• [x] Rational theory

For the second goal a release of Ostrich must be added to the Sosy Lab Ivy repository. Until them, most of the tests return Inconclusive (and thus fail).

[serras]

@kfriedberger maybe you can help with adding the additional dependency to the repo? It would also be great if Princess could be updated to the 2021-11-15 version. Thanks! 🙇

[kfriedberger]

@serras thanks for your interest in JavaSMT, again :-) I will take a look at the Ostrich library and the update of Princess... within the next days.

[kfriedberger]

@pruemmer Hi Philipp, could you provide the latest version of Ostrich in the Maven repository? I could only find v1.0 from 2018 and there seems to be a newer release v1.0.1 from 2020.

[pruemmer]

Sure, I can create another release here. You can get the latest nightly build from our local Maven repository as well, but there should be a proper release on Maven central of course.

[serras]

Hi again! do you happen to have an estimate about when Ostrich will be available as a dependency for java-smt? No pressure, I'm just trying to plan ahead when I can put the additional work required for this PR.

[pruemmer]

I now published a version of OSTRICH through Maven, an example of how to use OSTRICH as a library is here: http://www.philipp.ruemmer.org/princess/ostrich-example.zip

[kfriedberger]

@pruemmer Why are you not using Scala 2.13 for Ostrich? There is a missing publication for Scala 2.13? We are currently using Princess with Scala 2.13. If there is a deeper reason, we can also go back to Scala 2.12. The only reason for us to use Scala 2.13 was a nicer Scala/Java-integration.

[pruemmer]

Good point, I can update our Scala 2.13 branch. We don't want to lose compatibility with Scala 2.11, which is still producing the fastest bytecode by some margin; in our experience, 2.11 > 2.13 > 2.12. Due to some changes in the collections framework we need to maintain separate branches for 2.11/2.12 and 2.13.

[kfriedberger]

@pruemmer From our side, the change back from Scala 2.13 to Scala 2.12 was already applied in b7bbc3c, so this is not urgent and we do not depend on it.

[pruemmer]

In case you want to switch back, I also just published a Scala 2.13 build of Ostrich 1.1 on Maven.

[serras]

@pruemmer could you help me in figuring out why some of the tests are failing? I got from this file that not all functions on strings are supported, so I've already disabled those from the tests. But still I get a lot of:

Internal exception: java.util.NoSuchElementException: None.get
... <stacktrace pointing to the test>
Caused by: java.util.NoSuchElementException: None.get
at scala.None$.get(Option.scala:529)
at scala.None$.get(Option.scala:527)
at ostrich.StrDatabase.term2ListGet(StrDatabase.scala:84)
at ostrich.OstrichStringFunctionTranslator.$anonfun$apply$4(OstrichStringFunctionTranslator.scala:87)
at ostrich.OstrichSolver.$anonfun$findStringModel$1(OstrichSolver.scala:164) 

[pruemmer]

That exception indicates an occurrence of str.replace in which the second argument is symbolic, and not a concrete string. For which test case or input does this occur?

Note that the list of functions in OstrichStringTheory.scala is not exhaustive, there are more operators that are supported, but they are already simplified away at an earlier point.

[kfriedberger]

@pruemmer Is there a way to convert a term from Real theory to Int theory in Princess? Most solvers provide a method like to_int or floor that is also specified in the SMTLIB standard. I could not find such a method in the API of Princess, except Rationals.ring2int, which seems related, but does not work.

[pruemmer]

|Rationals.ring2int| is the right function, it represents the floor operation. However, since we currently don't have a decision procedure for the combined theory of ints and rationals, you might well see non-termination in quite many cases that mix ints and reals/rationals (if that is what you mean by "does not work" ;-)).

[kfriedberger]

@pruemmer Thanks for the quick answer. Does this mean that also arithmetic operations between Ints and Reals/Rationals are not fully supported, such as addition, subtraction, or comparisons with two operands from different theories?

[pruemmer]

The encoding of such operations combining ints and rationals should be correct, you should not see any wrong answers, but you might see cases of non-termination due to incompleteness of the current calculus.