Pushquantifiers can degrade performance significantly, investigate this!

[Broes De Cat]

!x y: P(x) & Q(y) => R(x,y)

of dus

!x y: ~P(x) | ~Q(y) | R(x,y)

dus mooi clausaal, wordt na push

!x: ~P(x) | (!y: ~Q(y) | R(x,y) )

Waarvoor Tseitins geintroduceerd moeten worden tijdens grounden.

[Bart Bogaerts]

Ideetjes:

Misschien moeten we PQ default enkel doen indien er geen context-switch geintroduceerd wordt. (als de totale diepte (alternating conj-disj depth) niet verhoogt, lijkt het een goed idee)

Of... indien de variabelen werkelijk gesplitst worden (als die x niet meer zou voorkomen in de tweede formule (in R dus) zou het ook goed zijn) Dan krijgen we

!x: ~P(x) | T

T <=> !y: ~Q(y) | R(y)

Wat beter is dan het oorpronkeiljke...

[Bart Bogaerts]

Improved PushQuantifications to not introduce extra Tseitins.

Fixes #518

→ <<cset 496bd10efd4e>>

[Bart Bogaerts]

Improved PushQuantifications to not introduce extra Tseitins.

Fixes #518

→ <<cset eecec46fe75f>>