Make the dreal usable at the end-of-a-pipe

[LeventErkok]

Hi there.. Most tools built on top of solvers use a text-pipe to communicate with the solver. It appears that dReal is waiting for the input file to close before it responds back. And this makes it harder to integrate with upstream tools.

For example, consider the following input:

(set-logic QF_NRA)
(declare-fun x1 () Real)
(assert (<= 3.0 x1))
(check-sat)
(exit)

If I send this input to dReal and but keep the pipe open, it never responds:

$ tail -qf a.smt2 /dev/null | dReal --in --smt2
... waits forever ...

Instead, it should respond to the (check-sat) command, and wait forever. Compare this to how, for instance, z3 behaves on the same input:

$ tail -qf a.smt2 /dev/null | z3 -in -smt2
sat
... waits forever ...

You can try other solvers as well, yices-smt2, mathsat etc., they all behave this way.

It'd be great to have this mode of interaction implemented for integration with other tools.

[soonho-tri]

Thanks for the suggestion. We have been aware of this issue. I'll check if I can easily change the implementation to support this behavior.

[soonho-tri]

Fixed by f4acd0f698c53560dabecce3fc30d1935cb84e0a. Please use --in option.