Shared tseitin cost AND push quant effect of BDD rewriting

[Broes De Cat]

In the following file, doing shared tseitin transformation explodes the theory and grounding time. Also, putting the theory through a bdd should push quantifications downwards to where it is relevant, but this does not happen? Also check this when the variable ordering is less straightforwardly following the usage.

[Bart Bogaerts]

The BDD generated by this problem is simply too large. And every subBDD occurs too many times in this bdd. Maybe we should rework both the transformation so that they don't do formula -> BDD -> formula, because this results in very inefficient formulas, with many occurences of the same subformula. (for example in a BDD with n kernels, the last kernel might appear 2^n times).

I postpone this issue to later and I'll hide the sharedtseitintransformation-option from the users and comment it in the manual.

[Bart Bogaerts]

see #184 (my last comment)

→ 2c6927f4182a

[Bart Bogaerts]

disabled shared tseitins transformation. See #184

→ 62bfb654d9e7

[Broes De Cat]

Removing milestone: Later (automated comment)