Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Finally it is here !
This PR adds a printer for smtlib2.6 to
dolmen
. The goal of the printer is to take arbitrary typed expressions, and print them in a way that respects the smtlib syntax.The fact that it is designed to take arbitrary expressions explain part of why it is complex: great care must be taken to make sure that identifiers respect the syntax convention (i.e. which characters are allowed), are not shadowed, etc... Additionally, in typical dolmen fashion, the printers are functorized so that they can be more easily re-used by other projects who'd wish to print their own typed terms in smtlib format.
For quick tests:
will parse and type the contents of
input_file.smt2
and then print them inoutput_file.smt2
. Alternatively, one can also doto have the output printed on the standard output.
Note: this is still a work in progress (not all builtins are yet printed, and some features related to avoiding shadowing are not yet implemented), and slightly experimental (no large scale testing has been done yet).