Set option support #608
Set option support #608
Conversation
Halbaroth
force-pushed
the
set-option-support
branch
2 times, most recently
from
b97b16d to
5ca3313
Compare
…reproducible-resource-limit
|
It is ready :) |
src/lib/util/options.ml
Outdated
| let usc_output = ref Stdout | ||
|
|
||
| let contents = function | ||
| | Stdout | Stderr | Channel _ | Invalid -> "" |
There was a problem hiding this comment.
This is not a very good idea and can only cause confusion if that function ever ends up called on a non-buffer output. At the very least this should raise an exception, but a better API design would be:
- Replace
Buffer of Buffer.t * Format.formatterwithFormatter of Format.formatter - Remove
create_bufferand replace it withlet of_formatter fmt = Formatter fmt - Remove
contentsentirely - Users of
create_buffer(i.e. the js_worker) are responsible for callingformatter_of_bufferandBuffer.contentsdirectly (and maybe there should be app_print_flushsomewhere?)
There was a problem hiding this comment.
I only flush the formatter. According to the documentation:
formatter_of_buffer b returns a new formatter writing to buffer b. At the end of pretty-printing, the formatter must be flushed using Format.pp_print_flush or Format.pp_print_newline, to print all the pending material into the buffer.
it should be fine :)
There was a problem hiding this comment.
The documentation you quoted states that the formatter must be flushed but I didn't see where this actually happens in the code?
There was a problem hiding this comment.
It should happen in the finalizer close_all but I forgot to add it in the js_worker. I will do it right now. Using set-option calls systematically the function Output.close on the old output channel.
There was a problem hiding this comment.
Calling close_all on at_exit in the JS worker is good, but not sufficient to ensure we get the proper content of the buffer. The corresponding formatter must be flushed with pp_print_flush before calling Buffer.contents.
There was a problem hiding this comment.
ooh I thought Buffer.contents calls the flush procedure!
This PR aims to make AE fit better the SMT-LIB standards by adding the support for
set-option.:regular-output-channeland:diagnostic-output-channel:produce-models:verbosity:reproducible-resource-limit:produce-unsat-coresI don't plan to support other standard options in this PR. Maybe we could add
print-successlater.I had to refactor the way AE manages its output channels in order to be able to change the channel during the execution of smt2 scripts.