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.

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

Replace multi_cartesian_product with a correct version #73

Closed
tchajed opened this issue Jun 13, 2023 · 1 comment · Fixed by #107
Closed

Replace multi_cartesian_product with a correct version #73

tchajed opened this issue Jun 13, 2023 · 1 comment · Fixed by #107

Comments

@tchajed
Copy link
Collaborator

tchajed commented Jun 13, 2023

We currently use itertools::multi_cartesian_product in many places. Unfortunately it doesn't handle empty iterators correctly (it produces no results when it should produce a single empty result); see rust-itertools/itertools#337. In several places we handle this ourselves but it would be better to just use a correct version everywhere.

We can implement the correct version by wrapping itertools::multi_cartesian_product.
@Alex-Fischman
Copy link
Collaborator

Locations where we need to replace it (from grep -rn "multi_cartesian_product" --include "*.rs"):

bounded/src/sat.rs:39:                    .multi_cartesian_product()
bounded/src/sat.rs:410:                .multi_cartesian_product()
bounded/src/bdd.rs:38:                    .multi_cartesian_product()
bounded/src/bdd.rs:394:                .multi_cartesian_product()
bounded/src/set.rs:205:                        .multi_cartesian_product()
bounded/src/set.rs:1141:                .multi_cartesian_product()
bounded/src/set.rs:1215:            // so we actually just want multi_cartesian_product, great
bounded/src/set.rs:1216:            // we have to convert to and from Vec for multi_cartesian_product
bounded/src/set.rs:1221:                .multi_cartesian_product()
fly/src/syntax.rs:378:                    .multi_cartesian_product()
fly/src/syntax.rs:399:                            .multi_cartesian_product()
fly/src/semantics.rs:66:        // NOTE: multi_cartesian_product has a bug and doesn't produce the empty
fly/src/semantics.rs:75:                .multi_cartesian_product()
fly/src/semantics.rs:159:                .multi_cartesian_product()
fly/src/semantics.rs:288:                    .multi_cartesian_product()
inference/src/weaken.rs:40:        .multi_cartesian_product()
inference/src/quant.rs:152:            .multi_cartesian_product()
inference/src/quant.rs:221:                    .multi_cartesian_product()
inference/src/basics.rs:194:                .multi_cartesian_product()
inference/src/lemma.rs:159:            .multi_cartesian_product()

@wilcoxjay wilcoxjay mentioned this issue Jul 11, 2023
Merged
tchajed pushed a commit that referenced this issue Jul 11, 2023
@wilcoxjay
Multi cartesian product fix (#107)
ebb6bf5 
This PR implements a corrected wrapper around
`itertools::multi_cartesian_product`.

I added a CI lint that forbids the string `multi_cartesian_product` (as
a standalone word, not a substring, as decided by `grep -w`) from the
code base. Use the wrapper `multi_cartesian_product_fixed` instead.

I ported all existing call sites to use the fixed version. I considered
each call site manually and convinced myself that either the iterator
was never empty or that the old code did not correctly handle that case
already. I also removed some obvious workarounds that handled the empty
iterator case separately to avoid the bug.

Fixes #73

---------

Signed-off-by: James R. Wilcox <wilcoxjay@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Multi cartesian product fix flyvy-verifier/flyvy
2 participants
@tchajed @Alex-Fischman