Skip to content

Inline inside solver. #3432

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
Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Inline inside solver. #3432

wants to merge 2 commits into from

Conversation

@chriseth
Copy link
Member

@chriseth chriseth commented Nov 6, 2025

No description provided.

chriseth
chriseth commented Nov 6, 2025
View reviewed changes
constraint-solver/src/solver/base.rs
.algebraic_constraints()
.iter()
.filter(|constr| {
constr.expression.is_affine() && constr.referenced_unknown_variables().count() == 2
Copy link
Member Author

@chriseth chriseth Nov 6, 2025

Choose a reason for hiding this comment

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

We should filter out constraints that contain new variables, although internally it could make sense.

@chriseth
Copy link
Member Author

chriseth commented Nov 12, 2025

With this, after the second run of the solver-based optimizer, we get

30720 * rs1_data__0_0 + 7864320 * rs1_data__1_0 - 30720 * mem_ptr_limbs__0_0 + bool_2 = 0

and

mem_ptr_limbs__0_0: [0, 65535] & 0xffff
rs1_data__0_0: [0, 255] & 0xff
rs1_data__1_0: [0, 255] & 0xff

The constraint splitter does not split out bool_0, because it only work with the correct coefficient.

Exhaustive search does not detect the problem either also because the scaling is wrong and range constraints do not work in that case.

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

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@chriseth