Hi Aina,
Thanks for your informative response.
For our application, there arise a few more questions about Boolector, see below.
>> We would like to have a correct SMTLIB2 formatted String for a
>> boolean formula that - starts with the declarations all used symbols
>> (in the formula) as "(declare-fun SYMBOL SORT)" and - ends with a
>> String for the formula itself, surrounded by the String "(assert
>> FORMULA)" to be valid SMTLIB2. How is this doable?
> For that you have to assert the formula to the solver and use
> boolector_dump_smt2.
Is there a way to do this that is independent of the solver's state?
In our application, we separate the formula construction from formula solving.
Thus, we do not know (and can not know) the solver's state when dumping a single formula.
>> We are using Boolector in version 3.2.1 via the C-API and try to use
>> "boolector_dump_smt2_node
>> <
https://boolector.github.io/docs/cboolector_index.html#c.boolector_dump_smt2_node>"
>>
>> that should print an SMTLIB2 formatted String for a node. We noticed
>> that the output only provides a String representation of the given
>> node, but misses all declarations of symbols, except when the node
>> itself is already a symbol, then we only get the declaration without
>> any futher representation of the node itself. Is this intended
>> behaviour?
> Yes.
Lets assume we want to use the method "boolector_dump_smt2_node".
Then we would need to recursively traverse the formula ourselves,
extract all used symbols, dump the symbols directly, then dump the formula itself. Correct?
We can modify the dump to be valid SMTLIB2 afterwards, as long as the rest works.
Is there a way (via the C-API) to traverse the formula,
i.e., how can we extract the children-nodes of a formula?
>> There is a second method boolector_dump_smt2
>> <
https://boolector.github.io/docs/cboolector_index.html#c.boolector_dump_smt2>"
>> in the API that misses some detailed description about what exactly
>> is dumped. Does is dump every node that is available on the system?
>> Or does is only dump the nodes asserted on the current solver stack?
>> Does the String contain declarations of symbols or not?
> This only dumps the current state of the formula, i.e., what is
> currently asserted to the solver. Expressions that were created but do
> not occur in any assertions are not printed.
>
> Also, beware that this prints the *current* state of the input formula,
> and not an incremental representation in the case of incremental
> solving. We do not fully support dumping in incremental mode.
Would it be possible to clone the Btor-instance,
to assert the match of the given node in the (empty) cloned solver instance,
and then dump the clone with the method "boolector_dump_smt2"?
Would this work and provide the wanted output?
How would we clear an already filled solver-stack (incremental solving)
in the cloned instance that was copied over from the original context?
In our case, we would not use the cloned instance for solving, but only for dumping.
[[ Thinking about it, this way seems to be too much overhead. ]]
On the other hand:
Could you (or some other Boolector developer) provide a method for our use-case?
It might be much easier from *inside* Boolector
to traverse a single formula, dump all used symbols and the formula in correct SMTLIB2.
Note:
The documentation at "
https://boolector.github.io/docs/cboolector_index.html#c.boolector_clone"
only gives information about Lingeling, MiniSAT and PicoSAT, but misses Cadical and CryptoMiniSAT.
>> Additionally, we would like to avoid redundant dumping of common
>> sub-formulae via the "let"-construct of SMTLIB2. Would this be
>> supported by Boolector? As we currently even struggle to dump valid
>> SMTLIB2, this point is future work for now.
> By default, Boolector uses let expressions where possible. Did you
> encounter an instance where this is not the case?
No. We did not yet dump larger formulae so far.
This was just a question about "what happens when...".
If Boolector supports this by default, everything is fine.
Best,
Karlheinz