search

elliottt / easy-smt

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

Ability to write solver interactions to a (replayable) file #3

Closed avanhatt closed 1 year ago

avanhatt commented 1 year ago

Would it be possible to also have a mode that echos all solver interactions to a file that can be replayed by directly feeding to a solver? We have some cases where for debugging/performance investigations (and for sending SMT-LIB files to other folks), it's convenient to interact with just a single file.

Basically, I'm thinking of what was adding in the logging commit (https://github.com/elliottt/easy-smt/commit/963ee2d1b815b7246f4c9c17edbdea36226292f6) but without the logging metadata/arrows. We could strip this information ourselves but it seems like this might be nice as a more general optional feature.

Thanks, we're excited to use this crate!

To clarify: we don't particularly need what is returned from the solver for this use case, just want is sent to the solver's standard in.

fitzgen commented 1 year ago

Yeah this is definitely possible.

Are you imagining providing a file to write to when constructing the easy_smt::Context?

fitzgen commented 1 year ago

@elliottt we may want to switch to a builder for constructing contexts given the number of knobs this seems to be growing.

avanhatt commented 1 year ago

No real preference between providing a file vs a path/filename for a new file to be created. And yes, I was thinking on a per-easy_smt::Context level.