Question about dumping SMTLIB2 via the C-API

[Karlheinz Friedberger]

Hello Boolector developers,

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?

We are using Boolector in version 3.2.1 via the C-API and try to use "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?

There is a second method 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?

Maybe I overlooked some option or other method. Then please correct me. :-)

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.

Thanks for any response. Best,

Karlheinz

[Aina Niemetz]

Hi Karlheinz,

> 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.

> 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.

> There is a second method boolector_dump_smt2

> <https://https://boolector.github.io/docs/cboolector_index.html#c.boolector_dump_smt2.github.io/docs/cboolector_index.html#c.boolector_dump_smt2_node>"

> 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.

> 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?

HTH,
Aina

[Karlheinz Friedberger]

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

[Aina Niemetz]

Hi Karlheinz,

>>> 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.

As I said in my previous email, with boolector_dump_smt2 Boolector only
dumps what has been asserted to the solver. It will dump a full smt2
file, including all definitions and declarations.

What I referred to as the "solver's state" is the current set of
assertions. In the incremental case, this means it will dump these while
disregarding scopes (i.e., push and pop) or assumptions (assumed with
boolector_assume). It will *not* print push and pop, but assertions that
were asserted in scopes opened with push. It will not dump assumptions
assumed with boolector_assume.

> 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?

No, Boolector takes care of that for you for asserted formulas and
symbols that occur in them (see above).

> 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. ]]

If you dump a node, the node is traversed and dumped. However, without
declaring any symbols, yes. If you assert it to a cloned instance, you
would get the full smt2 dump for that, yes.

> 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.

I'm not sure I fully understand your setup and what exactly you need.
Why do you want to use Boolector to dump nodes that are not asserted?

> 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.

Thanks, will update.

Aina