C interface "get-value"

[sy6sy2]

Hi,

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

Thank you!

[mpreiner]

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]

@SylvainCecchetto can you provide more information on this issue?

[sy6sy2]

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.