Is it possiable to impl AndAbstract? about biodivine-lib-bdd

[daemontus]

My understanding is that Cudd_bddAndAbstract should be equivalent to bdd_a.and(&bdd_b).project(&[v1, v2, ... vk]). Is this correct?

(I haven't used bddAndAbstract before and CUDD documentation is a bit sparse, so please let me know if I understand the function correctly)

Anyway, I don't believe we have a more direct method right now to compute this, and this is definitely not optimal in terms of performance (the project method needs more optimisation, it is rather naive at this point).

But it would certainly be nice to have a native implementation for this. I'll see what we can do...

[gipsyh]

My understanding is that Cudd_bddAndAbstract should be equivalent to bdd_a.and(&bdd_b).project(&[v1, v2, ... vk]). Is this correct?

Logic is equivalent, but the efficiency is different. In some areas, (for example, model checking), a & b is very huge, but the finally result is not to much. AndAbstract allows for projecting certain variables while performing logical AND operation.

Anyway, I don't believe we have a more direct method right now to compute this, and this is definitely not optimal in terms of performance (the project method needs more optimisation, it is rather naive at this point).

But it would certainly be nice to have a native implementation for this. I'll see what we can do...

Ok, thanks!

[daemontus]

I see, the efficiency is a good point... I looked at the algorithm for bddAndAbstract. It seems that we indeed don't have it in the library yet, but it should (hopefully) be reasonably easy to implement :)

I'll try to have a look at it later this week.

[gipsyh]

Thanks!

[daemontus]

With version 0.5.0 it is now possible to implement AndAbstract as follows:

Bdd::binary_op_with_exists(arg_1, arg_2, &[v1, v2, ...], biodivine_lib_bdd::op_function::and)

• The new algorithm indeed performs a single "BDD operation" in this case.
• You can substitute op_function::and for any other valid function to implement other logical operators.
• There is a variant with for_all instead of exists for the second type of abstraction.

For now, I haven't added an equivalent method to AndAbstract explicitly, because then I should probably also add methods for other operations and the matrix of combinations blows up quite quickly (and/or/implies/iff/xor times exists/for_all). But maybe in the future...

There are multiple correctness tests, so I am fairly confident the algorithm is ok. However, I haven't tested the performance on any practical problem yet. So if you see any weird performance with this algorithm, please let me know.