search

sarsko / CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
MIT License
614 stars 12 forks source link

Use as a Crate? | Adding a Rust API? #30

Open Eh2406 opened 2 years ago

Eh2406 commented 2 years ago

Thank you! I love any progress in the Rust SAT space. varisat has an api witch I have used extensively for testing libraries I work on. Would you be interested in adding an Rust API interface to CreuSAT?

sarsko commented 2 years ago

Thanks!

I agree that adding an API (and perhaps getting it published on crates.io) would be nice. I'll probably not be able to prioritize it immediately (even though it should not be all that much work), but I'll try to find time to look at how varisat does it, and try to offer something similar in the not too distant future :smile:

Eh2406 commented 2 years ago

Also I read the dissertation in the repo. I was surprised at how long it was and wasn't sure I would finish. I read it completely! As someone with no background in software verification, and only a self taught background in SAT, I found it one of the most accessible introduction to either topic I have read! Thank you!

sarsko commented 2 years ago

Also I read the dissertation in the repo. I was surprised at how long it was and wasn't sure I would finish. I read it completely! As someone with no background in software verification, and only a self taught background in SAT, I found it one of the most accessible introduction to either topic I have read! Thank you!

Very cool! Thanks! I am very happy to hear that! (also, if anything was not clear, then feel free to ask)

sirandreww commented 2 years ago

I actually would love this feature as well, I'm writing a library for the development and prototyping of formal verification algorithms in rust and I'd love to have this SAT solver be in there. How long do you think it might take to do that?

sarsko commented 2 years ago

I actually would love this feature as well, I'm writing a library for the development and prototyping of formal verification algorithms in rust and I'd love to have this SAT solver be in there. How long do you think it might take to do that?

Thanks. I appreciate the interest, and I still think that it would be nice. It would probably not take too long (one would look at how varisat does it, do something similar + do things like proper feedback on parser errors and also add incremental solving), but I have not done anything to achieve it in 4 months, so I will make no promise on when/if it will happen.

moberer commented 4 weeks ago

Would you be accepting pull requests for adding a Rust API?

sarsko commented 4 weeks ago

Yes, would most likely accept pull requests adding an API.