Skip to content

Add explicit cast in mixed integer-real term #466

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 9 commits into from
Apr 16, 2025
Merged

Add explicit cast in mixed integer-real term #466

merged 9 commits into from
Apr 16, 2025

Conversation

daniel-raffler
Copy link
Contributor

Hello,
several solvers fail when integer terms and rational terms are used together in RationalFormulaManager. This PR adds explicit casting operations for solvers that don't convert implicitly.

@daniel-raffler daniel-raffler linked an issue Mar 22, 2025 that may be closed by this pull request
Z3 fails when given mixed integer-real arguments for division #461
Closed
@kfriedberger
Copy link
Member

kfriedberger commented Apr 12, 2025 •
edited
Loading

It is not clear why this change is required. Please add useful tests that show your contribution, i.e., tests need to fail upfront and show a violation the official interfaces or documentation, and pass with your changes.

@daniel-raffler
Copy link
Contributor Author

It is not clear why this change is required. Please add useful tests that show your contribution, i.e., tests need to fail upfront and show a violation the official interfaces or documentation, and pass with your changes.

Did you already try running MixedArithmeticsTest with version 53b4026? Some of the assertions might be debatable, but I'm also getting 24 crashes due to type errors, which shouldn't be possible. The JavaSMT API guarantees that something like RationalFormulaManager.add(a,b) will always return a RationalFormula. Yet several of the solvers return Integer terms and crash either while trying to wrap the result, or later when the type of the formula does not match in the next operation.

If you want to avoid explicit casts we could still report this to the solver developers and ask them for help?

@kfriedberger
more tests on Integer and Rational numbers.
7642539
@kfriedberger
Remove irrelevant casting methods that return only a BooleanFormula a…
b87df92 
…nd do not depend on RationalFormula.

And shorten some code that was added for overriding theory-independent default behaviour.
Only Princess seems to need separate handling for Integers and Rationals.
@kfriedberger
Copy link
Member

I'm surprised that the issues in this PR have not been reported earlier, particularly the potentially breaking casts in multiple solver bindings and the invalid formula comparisons (LESS_THAN, LESS_EQUAL, GREATER_THAN, GREATER_EQUAL) in Princess for Real/Rational theory.

The PR looks completely valid from my side.

kfriedberger
kfriedberger approved these changes Apr 16, 2025
View reviewed changes
Copy link
Member

@kfriedberger kfriedberger left a comment

Choose a reason for hiding this comment

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

lgtm.

@kfriedberger kfriedberger merged commit e6a45ac into master Apr 16, 2025
2 of 3 checks passed
@kfriedberger
Copy link
Member

kfriedberger commented Apr 16, 2025 •
edited
Loading

@daniel-raffler Thanks for reporting this issue and providing a solid basis and tests for the fix. Well done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kfriedberger kfriedberger kfriedberger approved these changes

Assignees
No one assigned
Labels
bug CVC5 Princess SMTInterpol Z3
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Z3 fails when given mixed integer-real arguments for division
2 participants
@daniel-raffler @kfriedberger