The 'produce-model' option seems to do nothing (except occasionally produce segfaults), and the smt2 parser refuses to parse (get-assignement) and (get-value ...) etc.
The '-model' command line option is almost useful, but the destination file cannot be set. This is especially problematic when forking dReal as a subprocess and communicating via stdin, because then I have no control at all over where the model file is written. Finally, this file format is clearly intended for human consumption rather than machine parsing.
In short, I'd like to be able to call dReal as a subprocess and reliably get out model information when the prover returns "sat".
Bonus: it would be nice if dReal would behave interactively when fed commands on stdin. Currently, waits for (exit) and EOF before doing anything, which is kind of a bummer.
The 'produce-model' option seems to do nothing (except occasionally produce segfaults), and the smt2 parser refuses to parse (get-assignement) and (get-value ...) etc.
The '-model' command line option is almost useful, but the destination file cannot be set. This is especially problematic when forking dReal as a subprocess and communicating via stdin, because then I have no control at all over where the model file is written. Finally, this file format is clearly intended for human consumption rather than machine parsing.
In short, I'd like to be able to call dReal as a subprocess and reliably get out model information when the prover returns "sat".
Bonus: it would be nice if dReal would behave interactively when fed commands on stdin. Currently, waits for (exit) and EOF before doing anything, which is kind of a bummer.