search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

C interface "get-value" #50

Closed sy6sy2 closed 4 years ago

sy6sy2 commented 5 years ago

Hi,

It would be fantastic if you can implement the (get-value (my_var)) SMTLIB command with a C API function?

Thank you!

mpreiner commented 5 years ago

What exactly would you want to get as a result for boolector_get_value? There is also boolector_bv_assignment and boolector_array_assignment to return the assigments as strings.

mpreiner commented 4 years ago

@SylvainCecchetto can you provide more information on this issue?

sy6sy2 commented 4 years ago

Sorry I completely forgot my open issues :-/

I do not use the C interface anymore in my project. Instead, I use the fork, execv, pipe and dup2 friends to play in parallel with Boolector, CVC4 and Z3 (then I wait for the result, finally the faster solver print the result then I can kill the other "slow" ones). I send my formulas in the SMTLIB language to my forked child solvers process through stdin then I wait for the result on stdout. I use https://github.com/DaanDeMeyer/reproc to launch the SMT solvers processes.

I I recall correctly, I was not been able to find the C function to perform the SMTLIB (get-value) command.

Feel free to close this issue if needed.