Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More theories for Princess #257

Draft
wants to merge 34 commits into
base: master
Choose a base branch
from
Draft

More theories for Princess #257

wants to merge 34 commits into from

Conversation

serras
Copy link
Contributor

@serras serras commented Dec 6, 2021

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

  • String theory via naïve theory
  • String theory via Ostrich, an extension to Princess
  • 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 serras marked this pull request as draft December 6, 2021 10:39
@serras
Copy link
Contributor Author

serras commented Dec 6, 2021

@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
Copy link
Member

@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
Copy link
Member

@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.

kfriedberger added a commit that referenced this pull request Dec 7, 2021
The update was requested for #257.
@pruemmer
Copy link
Contributor

pruemmer commented Dec 9, 2021 via email

@serras
Copy link
Contributor Author

serras commented Dec 15, 2021

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
Copy link
Contributor

pruemmer commented Dec 15, 2021 via email

Please apply 'ant format-diff' before commiting,
or the extended version 'ant format-source'.
@kfriedberger
Copy link
Member

kfriedberger commented Dec 15, 2021

@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.

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.
@pruemmer
Copy link
Contributor

pruemmer commented Dec 16, 2021 via email

@kfriedberger
Copy link
Member

@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
Copy link
Contributor

pruemmer commented Dec 20, 2021 via email

@serras
Copy link
Contributor Author

serras commented Dec 20, 2021

@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
Copy link
Contributor

pruemmer commented Dec 20, 2021 via email

@kfriedberger
Copy link
Member

@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
Copy link
Contributor

pruemmer commented Dec 27, 2021 via email

@kfriedberger
Copy link
Member

@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
Copy link
Contributor

pruemmer commented Dec 29, 2021 via email

kfriedberger added a commit that referenced this pull request Jul 4, 2022
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

3 participants