Skip to content

Add support for IntToFloat and FloatToInt casts#190

Open
ThomasMayerl wants to merge 7 commits into
Aurel300:rewrite-2023from
ThomasMayerl:float_to_int
Open

Add support for IntToFloat and FloatToInt casts#190
ThomasMayerl wants to merge 7 commits into
Aurel300:rewrite-2023from
ThomasMayerl:float_to_int

Conversation

@ThomasMayerl

@ThomasMayerl ThomasMayerl commented Jul 17, 2026

Copy link
Copy Markdown

This PR implements support for IntToFloat and FloatToInt casts by going via the SMT Real domain.

Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/float.rs Outdated
@ThomasMayerl
ThomasMayerl requested a review from Aurel300 July 17, 2026 14:58
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread vir/src/make.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-tests/tests/verify/pass/casts/int_to_float.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/builtin/cast.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/real.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/float.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/real.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/real.rs Outdated
Aurel300
Aurel300 reviewed Jul 17, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/int_real_cast.rs

@Aurel300 Aurel300 Jul 17, 2026

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I imagine this is going to clash with #188.

@ThomasMayerl ThomasMayerl Jul 20, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, because Reals are just Perms. This encoder merely adds functions to be used with them.

JonasAlaif
JonasAlaif reviewed Jul 20, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/real.rs Outdated
JonasAlaif
JonasAlaif reviewed Jul 20, 2026
View reviewed changes
Comment thread vir/src/gendata.rs
JonasAlaif
JonasAlaif reviewed Jul 20, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/real.rs Outdated
JonasAlaif
JonasAlaif reviewed Jul 20, 2026
View reviewed changes
Comment thread prusti-encoder/src/encoders/ty/interpretation/real.rs Outdated
@JonasAlaif

JonasAlaif commented Jul 20, 2026

Copy link
Copy Markdown
Collaborator

I should have put all the comments in a single review, sorry

JonasAlaif
JonasAlaif reviewed Jul 21, 2026
View reviewed changes
Comment thread prusti-tests/tests/verify/fail/casts/int_to_float.rs Outdated
Comment thread vir/src/make.rs Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Aurel300 Aurel300 Aurel300 left review comments
@JonasAlaif JonasAlaif JonasAlaif left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ThomasMayerl @JonasAlaif @Aurel300