14 views

Skip to first unread message

Apr 7, 2020, 5:50:38 AM4/7/20

to Boolector

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

Apr 9, 2020, 12:17:20 AM4/9/20

to bool...@googlegroups.com, Karlheinz Friedberger

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

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

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

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

boolector_dump_smt2.

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

Yes.
>

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?

This only dumps the current state of the formula, i.e., what is
> 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?

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.

encounter an instance where this is not the case?

HTH,

Aina

Apr 9, 2020, 3:14:08 AM4/9/20

to Aina Niemetz, bool...@googlegroups.com

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

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

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.

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.

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

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

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?

This was just a question about "what happens when...".

If Boolector supports this by default, everything is fine.

Best,

Karlheinz

Apr 9, 2020, 2:14:53 PM4/9/20

to Karlheinz Friedberger, bool...@googlegroups.com

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

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

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?

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

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.

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.

Aina

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu