search

elliottt / easy-smt

Easy SMT solver interaction
Apache License 2.0
24 stars 4 forks source link

Implement `check-sat-assuming` #21

Closed rachitnigam closed 1 year ago

rachitnigam commented 1 year ago

Implements check-sat-assuming and reimplements check-sat as a special case of that. The former is useful because often times it lets you get away with not having to use push and pop (and in fact needed to implement #20).

elliottt commented 1 year ago

This is a great addition, thank you! Would you mind converting check back to using check-sat? From what I can tell in the standard there should be no difference, but I don't want to break any existing workflows when introducing this function.

rachitnigam commented 1 year ago

Done! There is a bunch of duplication in the code now unfortunately. Another option I can implement is special casing the check_assuming implementation to use check-sat when props is empty.

rachitnigam commented 1 year ago

@elliottt quick ping to see if the changes look mergable and if we can release a new version of the crate?

elliottt commented 1 year ago

https://crates.io/crates/easy-smt/0.2.0