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.

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

Semantic BDD Pointers! #163

Draft
wants to merge 24 commits into
base: main
Choose a base branch
from
Draft

Semantic BDD Pointers! #163

wants to merge 24 commits into from

Conversation

mattxwang
Copy link
Member

@mattxwang mattxwang commented Jul 26, 2023

heavily in draft; need to cherry pick some of these changes

interesting results

$ cargo run --example parallel_semantic -- -t -n 16 -f cnf/s298.cnf           
=== TIMING ===
Compile: 0.01s, Merge: 240.99s (ds: 0.58s, ands: 240.40s)
Single-threaded: 45.18s
Speedup ratio: 0.19x

Blocker: need access to builder for some operations (namely, deref).

Doesn't build rn :(
This doesn't compile; need to pause since some `BddPtr` logic
lives in `VarOrder`, and it probably shouldn't.
mattxwang added a commit that referenced this pull request Jul 27, 2023
…trait, fixes ref/lifetimes

Two problems:

1. `VarOrder`'s `first`, `first_essential`, and `sort` methods rely
   on the input type being a `BddPtr`, which causes problems for
   #163. So, I've instead abstracted the idea of a partial variable order,
   i.e. that structs may or may not have a sortable variable,
   to a trait; `BddPtr` (and soon, `SemanticBddPtr`) implements
   this trait. This caused minimal code impact.
2. `first`, `first_essential`, and `sort` shouldn't consume their
   inputs, so I've changed these to just be refs. Required lifetime
   annotations.

Then, added doctests for these methods!
mattxwang added a commit that referenced this pull request Jul 27, 2023
…164)

Two problems:

1. `VarOrder`'s `first`, `first_essential`, and `sort` methods rely on the input type being a `BddPtr`, which causes problems for #163. So, I've instead abstracted the idea of a partial variable order, i.e. that structs may or may not have a sortable variable, to a trait; `BddPtr` (and soon, `SemanticBddPtr`) implements this trait. This caused minimal code impact.
2. `first`, `first_essential`, and `sort` shouldn't consume their inputs, so I've changed these to just be refs. Required lifetime annotations.

Then, added doctests for these methods!
mattxwang added a commit that referenced this pull request Aug 3, 2023
Note to self: before merging this, we should do a bit
more benchmarking to see how this actually affects perf.

From #163, it seems negligble.
mattxwang added a commit that referenced this pull request Aug 3, 2023
Cherry-picking this change over from #163, to make it easier to review (and to revert this if necessary).
mattxwang added a commit that referenced this pull request Aug 3, 2023
#168)

Cherry-picking this change over from #163, to make it easier to review (and to revert this if necessary).
mattxwang added a commit that referenced this pull request Aug 3, 2023
Cherry-picking this change over from #163, to make it easier to review (and to revert this if necessary).

Note to self: before merging this, we should do a bit more benchmarking to see how this actually affects perf.

From #163, it seems negligble.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant