Array/fun/uf nodes and support

[Skarrabor]

Hello,

is it possible to, somehow, get the nodes of an array and fun/uf that are used as args?

If not, is it possible to maybe add the support to do that, or are there no nodes used internally? (simplified immediately for example?)

Also, is there a possibility to add the ability to parse single nodes via parsing them?  (prefferably in smt2 format)

I am trying to add Boolector to the JavaSMT framework ( https://github.com/sosy-lab/java-smt ), 

and especially the ability to work with the nodes in arrays and fun/uf's would be extremely helpfull.

Your work is greatly appreciated and thank you for any help or support you can provide,

Daniel

[Mathias Preiner]

Hi Daniel,

We do have nodes internally (DAG). What functionality do you exactly
need? Is it traversing the DAG, i.e., getting the children of a node and
so on?

There is currently no functionality to create nodes via parsing
SMT-LIB2, but this shouldn't be too hard to add.

Cheers,
Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/674871fd-7618-44af-8431-d8ac975928f6%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/674871fd-7618-44af-8431-d8ac975928f6%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Karlheinz Friedberger]

Hi Mathias,

I am a collegue of Daniel from LMU Munich.

You are right, we need some possibility to traverse the DAG of nodes,
for example, to replace child-nodes (symbols/variables) by other ones.
There is already a method "boolector_get_fun_arity" that returns the number of child-nodes.
We would like to have a method "boolector_get_child(index)",
which works for simple functions like "and/or/add/subtract/exists/forall/..." and also for UFs.

We allow internal simplification during node construction and
would like to have a immutable DAG as soon as the node is constructed.
From the API, it seems as if "boolector_simplify" and "boolector_sat"
might change the formula "in-place". Is this correct? Does the id remain immutable?

The parsing of simple assertions into nodes is also a basic requirement from our side.
Could the parsing be based on the existing context, and use already defined symbols from the context?
It would be good, if a String-query like "(assert (= someSymbol anotherSymbol))"
would work if "someSymbol" and "anotherSymbol" have already been produced with "boolector_var".
Otherwise we could also cache all defined symbols on our side and prepend to the given query.
It would be very helpful, if defining new symbols and re-defining old symbols (with equal sort) in a parser-query would be possible.

I have a few more questions, just to be sure about Boolectors API and maybe to improve API usage:

- It seems as if Boolector does not cache symbols and returns a new node on every call to "boolector_var".
With the combination of parsing and calling "boolector_var", there seem to be many ways to define symbols.
How can we assure that equal-named equal-sorted symbols are identical?
Can we forbit the construction of equal-named different-sorted symbols and throw an exception?
Could you add an internal cache into Boolector to keep this consistent?

- Does constructing two DAGs via the same API-calls result in the same node?
Can we compare two nodes for structural equivalence (without calling for expensive SAT)?

- When using a cloned instance of Boolector, can nodes/ids be constructed later and inserted into the matching?
Background: we want to have several prover stacks with push/pop/assert/checksat
and want to use the same nodes (or at least easily translatable nodes) across all of them.
Nodes are dynamically constructed during our analysis.
Or is there another way to decouple node construction and prover stacks?
(It is no problem, if Boolector does not yet support such use-cases.)

Best,
Karlheinz


Am 04.09.19 um 20:45 schrieb Mathias Preiner:

--
Karlheinz Friedberger
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Room F009
Phone: 089/2180-9182

[Mathias Preiner]

Hi Karlheinz,

Answers are inlined below.

On 9/5/19 12:50 AM, Karlheinz Friedberger wrote:
> Hi Mathias,
>
> I am a collegue of Daniel from LMU Munich.
>
> You are right, we need some possibility to traverse the DAG of nodes,
> for example, to replace child-nodes (symbols/variables) by other ones.
> There is already a method "boolector_get_fun_arity" that returns the number of child-nodes.
> We would like to have a method "boolector_get_child(index)",
> which works for simple functions like "and/or/add/subtract/exists/forall/..." and also for UFs.
>

So to make the traversal useful, you would at least need the API functions:

- boolector_get_num_children
Return number of children for a given node.

- boolector_get_children
Return array of children for a given node.

- And probably some function to get the indices of indexed operators (in
Boolector's case this is the slice operator)

But only traversing does not make much sense, so you would also need a
way to identify the kind of the current node, where you would need
somthing like:

- boolector_get_node_kind
Returns the kind of a given node.

For that we would additionally need to extract all node kinds via the
API, which will be quite a change in the API.

> We allow internal simplification during node construction and
> would like to have a immutable DAG as soon as the node is constructed.
> From the API, it seems as if "boolector_simplify" and "boolector_sat"
> might change the formula "in-place". Is this correct? Does the id remain immutable?
>

Yes you are right, nodes can get simplified, but the ids remain
immutable and are not recycled. It could just be that an id is
"outdated".

> The parsing of simple assertions into nodes is also a basic requirement from our side.
> Could the parsing be based on the existing context, and use already defined symbols from the context?
> It would be good, if a String-query like "(assert (= someSymbol anotherSymbol))"
> would work if "someSymbol" and "anotherSymbol" have already been produced with "boolector_var".
> Otherwise we could also cache all defined symbols on our side and prepend to the given query.
> It would be very helpful, if defining new symbols and re-defining old symbols (with equal sort) in a parser-query would be possible.
>

Wouldn't it be better to directly create your assertions via the API
instead of creating a SMT-LIB string? Mixing SMT-LIB parsing with nodes
created via the API can get tricky since the parser needs to know the
state of all symbols that were also created via the API. Currently, the
parser has its own symbol table.

> I have a few more questions, just to be sure about Boolectors API and maybe to improve API usage:
>
> - It seems as if Boolector does not cache symbols and returns a new node on every call to "boolector_var".
> With the combination of parsing and calling "boolector_var", there seem to be many ways to define symbols.
> How can we assure that equal-named equal-sorted symbols are identical?
> Can we forbit the construction of equal-named different-sorted symbols and throw an exception?
> Could you add an internal cache into Boolector to keep this consistent?
>

The symbol you specify via boolector_var will be checked for uniqueness.

> - Does constructing two DAGs via the same API-calls result in the same node?
> Can we compare two nodes for structural equivalence (without calling for expensive SAT)?
>

Boolector uses structural hashing for nodes, so if you create the DAGs
with the same structure and inputs, you will get the same node.

> - When using a cloned instance of Boolector, can nodes/ids be constructed later and inserted into the matching?
> Background: we want to have several prover stacks with push/pop/assert/checksat
> and want to use the same nodes (or at least easily translatable nodes) across all of them.
> Nodes are dynamically constructed during our analysis.
> Or is there another way to decouple node construction and prover stacks?
> (It is no problem, if Boolector does not yet support such use-cases.)
>

It's probably best to use boolector_push/boolector_pop since with
cloning you may do more work since the information from a check-sat call
is not exchanged between clones.


I'm not sure if you are aware of this work:

https://github.com/makaimann/smt-switch

A PhD student in our lab started a generic C++ API for SMT-LIB, which
provides abstract classes that can be implemented by differen SMT
solvers. It currently supports CVC4 and Boolector, but the goal is to
add more SMT solvers.

Cheers,
Mathias

[Karlheinz Friedberger]

Hi Mathias.

thank you for your response. My answers are also inlined below.

>> You are right, we need some possibility to traverse the DAG of nodes,
>> for example, to replace child-nodes (symbols/variables) by other ones.
>> There is already a method "boolector_get_fun_arity" that returns the number of child-nodes.
>> We would like to have a method "boolector_get_child(index)",
>> which works for simple functions like "and/or/add/subtract/exists/forall/..." and also for UFs.
>>
> So to make the traversal useful, you would at least need the API functions:
>
> - boolector_get_num_children
> Return number of children for a given node.

Does the method "boolector_get_fun_arity" not already provide that kind of information?

> - boolector_get_children
> Return array of children for a given node.

Yes, either "get_all_children" (returning an array) or simply "get_child_at_index"
(returning a single node, called for every index from 0 to arity) would be possible.

> - And probably some function to get the indices of indexed operators (in
> Boolector's case this is the slice operator)

For indexed operators, the indices could also be provided as children of the operator.
For example, an integer value would be a constant bitvector with 32 bit.
The number of children needs to consider/include such additional children.

> But only traversing does not make much sense, so you would also need a
> way to identify the kind of the current node, where you would need
> somthing like:
>
> - boolector_get_node_kind
> Returns the kind of a given node.

There are already several methods like "boolector_is_const/_is_fun/_is_array".
Would it be sufficient to simply use those methods?
Are there more kind of nodes that are not yet covered by these methods?

> For that we would additionally need to extract all node kinds via the
> API, which will be quite a change in the API.

That might be a one-time-cost per type of node. :-)

>> We allow internal simplification during node construction and
>> would like to have a immutable DAG as soon as the node is constructed.
>> From the API, it seems as if "boolector_simplify" and "boolector_sat"
>> might change the formula "in-place". Is this correct? Does the id remain immutable?
>>
>
> Yes you are right, nodes can get simplified, but the ids remain
> immutable and are not recycled. It could just be that an id is
> "outdated".

Maybe I should clarify my question:
Does a simplified node have the same id than before simplification?
If not, what is the use of the id?

>> The parsing of simple assertions into nodes is also a basic requirement from our side.
>> Could the parsing be based on the existing context, and use already defined symbols from the context?
>> It would be good, if a String-query like "(assert (= someSymbol anotherSymbol))"
>> would work if "someSymbol" and "anotherSymbol" have already been produced with "boolector_var".
>> Otherwise we could also cache all defined symbols on our side and prepend to the given query.
>> It would be very helpful, if defining new symbols and re-defining old symbols (with equal sort) in a parser-query would be possible.
>>
>
> Wouldn't it be better to directly create your assertions via the API
> instead of creating a SMT-LIB string? Mixing SMT-LIB parsing with nodes
> created via the API can get tricky since the parser needs to know the
> state of all symbols that were also created via the API. Currently, the
> parser has its own symbol table.
>
>> I have a few more questions, just to be sure about Boolectors API and maybe to improve API usage:
>>
>> - It seems as if Boolector does not cache symbols and returns a new node on every call to "boolector_var".
>> With the combination of parsing and calling "boolector_var", there seem to be many ways to define symbols.
>> How can we assure that equal-named equal-sorted symbols are identical?
>> Can we forbit the construction of equal-named different-sorted symbols and throw an exception?
>> Could you add an internal cache into Boolector to keep this consistent?
>>
>
> The symbol you specify via boolector_var will be checked for uniqueness.

I have not yet tried that, so I am simply asking:
Calling "boolector_var" twice with the same arguments will return the same node?

In our software, we have two ways of constructing formulae/nodes:
(1) Directly via SMTlib-input and (2) via API-calls.
Both approaches can be used interleaved.
In the end, all formulae from both approaches are used together.
It should be possible to combine them.
Therefore the variables/symbols need to be shared somehow.

>> - Does constructing two DAGs via the same API-calls result in the same node?
>> Can we compare two nodes for structural equivalence (without calling for expensive SAT)?
>>
>
> Boolector uses structural hashing for nodes, so if you create the DAGs
> with the same structure and inputs, you will get the same node.

That is good news.
... except that one node could already be simplified if used in a sat-query. Correct?

>> - When using a cloned instance of Boolector, can nodes/ids be constructed later and inserted into the matching?
>> Background: we want to have several prover stacks with push/pop/assert/checksat
>> and want to use the same nodes (or at least easily translatable nodes) across all of them.
>> Nodes are dynamically constructed during our analysis.
>> Or is there another way to decouple node construction and prover stacks?
>> (It is no problem, if Boolector does not yet support such use-cases.)
>>
>
> It's probably best to use boolector_push/boolector_pop since with
> cloning you may do more work since the information from a check-sat call
> is not exchanged between clones.

Lets assume the following pseudocode:

btor_1 = new btor();
var_X = btor_var(btor_1, BOOL, "x");
btor_2 = btor_clone(btor_1);
var_Y = btor_var(btor_1, BOOL, "y");
var_Z = btor_var(btor_2, BOOL, "z");

- Can "var_X" be used with "btor_2"? I assume YES, because the node was created before cloning.
- Can "var_Y" be used with "btor_2"? I assume NO, because "btor_match_node" must be called first.
- Can "var_Z" be used with "btor_1"? I assume NO, because "btor_match_node" must be called first.
We do not need to exchange information about check-sat calls.
If my assumption are correct, then that is ok for us.

> I'm not sure if you are aware of this work:
>
> https://github.com/makaimann/smt-switch
>
> A PhD student in our lab started a generic C++ API for SMT-LIB, which
> provides abstract classes that can be implemented by differen SMT
> solvers. It currently supports CVC4 and Boolector, but the goal is to
> add more SMT solvers.

Thanks for the hint on the new software :-)
We are working on a very similar kind of software: https://github.com/sosy-lab/java-smt
We aim towards good usability and therefore we have some special requirements towards the native solvers.
For example, we support formula transformations (as visitors from a user's point of view).


Best,
Karlheinz

[Mathias Preiner]

Hi Karlheinz,

On 9/5/19 1:34 PM, Karlheinz Friedberger wrote:
> Hi Mathias.
>
> thank you for your response. My answers are also inlined below.
>
>>> You are right, we need some possibility to traverse the DAG of nodes,
>>> for example, to replace child-nodes (symbols/variables) by other ones.
>>> There is already a method "boolector_get_fun_arity" that returns the number of child-nodes.
>>> We would like to have a method "boolector_get_child(index)",
>>> which works for simple functions like "and/or/add/subtract/exists/forall/..." and also for UFs.
>>>
>> So to make the traversal useful, you would at least need the API functions:
>>
>> - boolector_get_num_children
>> Return number of children for a given node.
>
> Does the method "boolector_get_fun_arity" not already provide that kind of information?
>

No this only provides the arity for functions created via
boolector_fun/boolector_uf and has nothing to do with the number of
children of a constructed node.

>
>> - boolector_get_children
>> Return array of children for a given node.
>
> Yes, either "get_all_children" (returning an array) or simply "get_child_at_index"
> (returning a single node, called for every index from 0 to arity) would be possible.
>
>
>> - And probably some function to get the indices of indexed operators (in
>> Boolector's case this is the slice operator)
>
> For indexed operators, the indices could also be provided as children of the operator.
> For example, an integer value would be a constant bitvector with 32 bit.
> The number of children needs to consider/include such additional children.
>
>
>> But only traversing does not make much sense, so you would also need a
>> way to identify the kind of the current node, where you would need
>> somthing like:
>>
>> - boolector_get_node_kind
>> Returns the kind of a given node.
>
> There are already several methods like "boolector_is_const/_is_fun/_is_array".
> Would it be sufficient to simply use those methods?
> Are there more kind of nodes that are not yet covered by these methods?
>

Yes, there are many more kinds. Also some internal ones that probably
shouldn't be exposed to the user.

>
>> For that we would additionally need to extract all node kinds via the
>> API, which will be quite a change in the API.
>
> That might be a one-time-cost per type of node. :-)
>

It's more than that. If the Boolector API would provide kinds, one also
wants to construct nodes with these kinds, e.g.,
instead of boolector_add(btor, a, b) you can construct a node via a
function like boolector_mk_term2 (btor, BV_ADD, a, b).

This would change the API quite a bit.

>>> We allow internal simplification during node construction and
>>> would like to have a immutable DAG as soon as the node is constructed.
>>> From the API, it seems as if "boolector_simplify" and "boolector_sat"
>>> might change the formula "in-place". Is this correct? Does the id remain immutable?
>>>
>>
>> Yes you are right, nodes can get simplified, but the ids remain
>> immutable and are not recycled. It could just be that an id is
>> "outdated".
>
> Maybe I should clarify my question:
> Does a simplified node have the same id than before simplification?
> If not, what is the use of the id?
>

The nodes you hold will have the same id, but if you use a simplified
node to create new nodes it will use the simplified version of it.

For example, if node n1 gets simplified to n2 and you create an adder n1
+ n3 it will actually create the adder n2 + n3.

boolector_var/boolector_array/boolector_uf will always return a fresh
variable. It is disallowed via the API to create a fresh var/array/uf
with an already existing symbol. However, the API provides the function
boolector_match_node_by_symbol, where you can retrieve nodes with a
specific symbol.

1) Correct.
2+3) Yes, in both cases no, but boolector_match_node(...) would not
change anything since it only matches the node (by id) in the other
Boolector instance if it exists.

For example, you can get the btor_2 version of var_X as follows:

var_X2 = boolector_match_node (btor_2, var_X);

And the btor_1 version of var_X2 as follows:

var_X1 = boolector_match_node (btor_1, var_X2);

where now var_X1 and var_X are the same.

Node matching can be useful if you want to continue with a cloned
instances, but only have nodes from the original instance.


Cheers,
Mathias

[Skarrabor]

Hi Mathias,

i dont want to interrupt the discussion above, therefore i will be swift.

For my work the methods you proposed, namely:

- boolector_get_num_children

  Return number of children for a given node.

- boolector_get_children

  Return array of children for a given node.

- boolector_get_node_kind

  Returns the kind of a given node.

- And probably some function to get the indices of indexed operators

would be enough to ensure the base functionality of JavaSMT and i would be more then happy. 

Another thing that might be usefull would be the de brujin index of the quantifier variables. 

But thats not as important.

Your help here, and with questions in other threads are highly appreciated, thanks!

Best,

Daniel

[baier.d...@googlemail.com]

Hi,

are there any new developments in this regard?

Best,

Daniel

[Mathias Preiner]

Hi Daniel,

Boolector is in maintenance mode and won't be extended for new features.
We are currently working on a source release of our new solver Bitwuzla
(and successor of Boolector), which already has the API functionality
you need. Migrating from Boolector to Bitwuzla should be very simple and
straightforward. Unfortunately, we don't have an ETA yet for the source
release, we'll keep you posted.

Cheers,
Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/boolector/1aca1ee3-1dd5-47b6-b29d-e82bdc434441n%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/1aca1ee3-1dd5-47b6-b29d-e82bdc434441n%40googlegroups.com?utm_medium=email&utm_source=footer>.