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

A std::io::Read-based parser. Also, ran cargo format. #3

Merged
merged 4 commits into from
Oct 31, 2019

Conversation

alex-ozdemir
Copy link
Contributor

The reason for this is that it allows parsing to begin without reading the whole file into memory.

At some point it might be nice to add a "clause stream" output as well---then you could incrementally read clauses and assimilate them directly into the SAT solver data structures.

I chose to panic on IO error during the read, because I don't think that users would want to catch them, and panicking is much simpler.

Also, I ran cargo format. Sorry about the large diff, but my editor handles tabs poorly.

This change is straightforward because the DIMACS format is ASCII-only.
Panics on IO errors

Why?

Because the alternatives are:
   * `collect` the first IO error -- requiring us to pull the whole
   string into memory
   * catch those IO errors deep in the lexer, and bubble them up as a
   special kind of `ParseError`.

Since we'll generally be reading form files, read errors won't typically
happen, so I figure its better to just panic, since a use wouldn't want
to recover any ways.
@coveralls
Copy link

Coverage Status

Coverage increased (+1.07%) to 91.111% when pulling bfb6df8 on alex-ozdemir:master into fc12ab4 on Robbepop:master.

1 similar comment
@coveralls
Copy link

Coverage Status

Coverage increased (+1.07%) to 91.111% when pulling bfb6df8 on alex-ozdemir:master into fc12ab4 on Robbepop:master.

Copy link
Owner

@Robbepop Robbepop left a comment

Choose a reason for hiding this comment

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

LGTM

@Robbepop
Copy link
Owner

The reason for this is that it allows parsing to begin without reading the whole file into memory.

At some point it might be nice to add a "clause stream" output as well---then you could incrementally read clauses and assimilate them directly into the SAT solver data structures.

I chose to panic on IO error during the read, because I don't think that users would want to catch them, and panicking is much simpler.

Also, I ran cargo format. Sorry about the large diff, but my editor handles tabs poorly.

Didn't know that the dimacs crate was in use.
Haven't touched it in ages but might do so now.
Your improvements are nice, thank you for them. :)

@alex-ozdemir
Copy link
Contributor Author

Didn't know that the dimacs crate was in use.

I'm not using it yet, but I plan to write a set of teaching SAT solvers on top of it.

@Robbepop
Copy link
Owner

Didn't know that the dimacs crate was in use.

I'm not using it yet, but I plan to write a set of teaching SAT solvers on top of it.

Good to know then we might want to improve it and also provide a streaming interface for clauses using the https://crates.io/crates/ipasir crate.

@Robbepop
Copy link
Owner

Thanks for the PR. I merge this now.

@Robbepop Robbepop merged commit 90915a2 into Robbepop:master Oct 31, 2019
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.

None yet

3 participants