Support for floating-point arithmetic added#6
Support for floating-point arithmetic added#6dannem1337 wants to merge 34 commits intouuverifiers:masterfrom
Conversation
…ionals as an ITerm
…k, tests should be added to both
Presentation
Presentation
.attach_pid35637
Outdated
There was a problem hiding this comment.
There seem to be some empty files added by mistake.
There was a problem hiding this comment.
Please call make on the ACSL parser and commit the new jar file as well (that's not built as part of the build process).
| def isNeginf(t: ITerm): IFormula = longDoubleADT.hasCtor(t, 3) | ||
| } | ||
|
|
||
| object LongDoubles { |
There was a problem hiding this comment.
I think we should avoid making CCReader longer than it already is :-) The new classes/objects you add can be in a new file.
| import CCReader._ | ||
| import ccreader._ | ||
| import tricera.params.TriCeraParameters | ||
| import tricera.concurrency.CCReader |
There was a problem hiding this comment.
The changes in this file seem unnecessary.
|
@dannem1337 Thank you for creating this PR! I added some quick comments , would be nice if you could address them! It would also be helpful to provide a more detailed PR description. |
|
Hello, |
3 participants
This PR adds basic support for Float, Double and Long Double using the theory of rationals.
What has been added:
What is missing: