More theories for Princess #257
Conversation
|
@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 |
|
@serras thanks for your interest in JavaSMT, again :-) |
|
@pruemmer Hi Philipp, |
The update was requested for #257.
|
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.
|
|
Hi again! do you happen to have an estimate about when Ostrich will be available as a dependency for |
|
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
|
Please apply 'ant format-diff' before commiting, or the extended version 'ant format-source'.
|
@pruemmer Why are you not using Scala 2.13 for Ostrich? There is a missing publication for Scala 2.13? |
Scala is not upwards and not downwards compatible. The upcoming Ostrich library is only available for Scala 2.12, so we downgrade Scala for Princess.
This is an initial step and the usage is still unclear. This is not tested.
|
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.
|
|
In case you want to switch back, I also just published a Scala 2.13
build of Ostrich 1.1 on Maven.
|
|
@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: |
|
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.
|
|
@pruemmer Is there a way to convert a term from Real theory to Int theory in Princess? Most solvers provide a method like |
|
|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" ;-)).
|
|
@pruemmer Thanks for the quick answer. |
|
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.
|
We do not yet add support for building queries (see #257 for that), but only add a minimal capacity for getting the type from parsed formulas containing rational symbols.
… theory and arrays. Princess intenally converts all real-arrays to int-arrays and thus there is some casting and quantification in SMT.
Princess needs non-rational UF arguments to be explicitly casted to rational.
Princess supports more theories than the ones currently announced in
java-smt. The goal of this PR is to support them: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).