search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

Interactive mode with SMT2 code #343

Closed AndreaCallia closed 7 years ago

AndreaCallia commented 7 years ago

Dear dReal developers,

is there an interactive mode for dReal? I have seen there is an --in option, but it only starts the solving after the EOF character is received. It would be nice to have it interactive, in order to be able to use the dReal solver in a pipe where new "queries" are sent to the solver depending on the previous results.

I have noticed that this is already possible using the C-API, but in order to send the "queries" in SMT2 format it would be nice to activate this (for example it can be done in z3 still using the -in option, together with option -smt2).

Many thanks for all your work and support...

PS I have built dReal in a Ubuntu 14.04 64bit machine with clang-3.8.

soonho-tri commented 7 years ago

Hi @AndreaCallia , sorry but it's not supported yet. We've focused on the core part of the solving and dReal is far from smt2lib-complete.

AndreaCallia commented 7 years ago

Many thanks @soonho-tri for your kind reply... If it is possible, I would like to contribute to this if you tell me which source code files are involved. I think it would not be too difficult for me to change that part of the code, and I can send you the changes if you like.

In summary, I would just need to find a solver object and an open input stream connected to stdin, and instead of waiting for end-of-file I should parse and execute the command every time I find an end-of-line, is this right?

If you think it is not too complex, I would be happy to see the involved lines of code and to make some changes, I would only need to know which files I should inspect.

Again thanks for your work and your support...

scungao commented 7 years ago

Hi @AndreaCallia We'd love to work with you on this. How about sending us an email (sicun.gao and soonho.kong both at gmail) and we could have a skype call to talk about more details.

AndreaCallia commented 7 years ago

Dear @scungao and @soonho-tri ,

sorry for my belated reply (some very urgent deadlines), I would be happy to give my contribute on this and I am happy to have a call via Skype, I am going to send you my contacts via email...

soonho-tri commented 7 years ago

Sounds good to me. I'm closing this one.