-
Notifications
You must be signed in to change notification settings - Fork 4
Implement SMTLib2 parser #5
Copy link
Copy link
Open
Labels
A-parserTask operating on the stevia_parser crate in isolation.Task operating on the stevia_parser crate in isolation.B-enhancementAn enhancement or new feature.An enhancement or new feature.D-mediumA task that is considered to be moderately hard to implement.A task that is considered to be moderately hard to implement.
Description
Metadata
Metadata
Assignees
Labels
A-parserTask operating on the stevia_parser crate in isolation.Task operating on the stevia_parser crate in isolation.B-enhancementAn enhancement or new feature.An enhancement or new feature.D-mediumA task that is considered to be moderately hard to implement.A task that is considered to be moderately hard to implement.
Stevia requires support for SMTLib2 parsing to make it work with SMTLib2 inputs.
Implementation Status
Past Discussion & Design
For this the rsmt2 crate provides parsing support, however, its current implementation isn't flexible enough to allow for decoupled integration of other SMT solver than the currently implemented ones (Z3 and CVC4). This issue is described in detail here.Adrien Champion reported that this was a wrong assumption about rsmt2.For the parsing of SMTLib2 there are effectively two approaches.
The eager approach would simply parse an SMTLib2 input, process it and directly returns the entire parsed construct represented as an apropriate data structure to feed into stevia. This approach is simple, however, has the downside to be very inflexible and may require more memory to store a temporary data structure and maybe even has negative performance implications.
A more flexible and thus superior approach is to define an interface to let an underlying SMT solver know about newly parsed entities. In this situation a proper interface has yet to be found but the advantage is that this should be more optimal for memory consumption and runtime performance.