Equivalence splitting

[Broes De Cat]

Heeft het voordelen om bij het splitsen van equivalenties tseitins in te voeren? Want het zijn duidelijk gedeelde formules, die nu helemaal apart behandeld en dubbel geground worden!

[Bart Bogaerts]

In principe gebeurt dit ook niet. RemoveEquivalences wordt volgens mij enkel gebruikt in de BDDs; volgens mij om een of andere normaalvorm te bekomen.

In principe blijven equivalenties behouden tot in de EquivGrounder, en die groudt elke formule slechts 1 keer

[Broes De Cat]

Ik zal het toevoegen aan de docs, dan is dit inderdaad fixed :)

[Broes De Cat]

Removing milestone: Second Release (automated comment)