Implements the optimisation applicable to gates for which all kids are independent and have a unique parent,
ie applicable only to parts of the nnf formula that are genuine trees from the root and down to input literals.
This optim consists in forcing the maximum number of undefined kids for each possible output value of the gates
For And(kids):
- assert (o = 0) => nofKid(?) >= g.nofKids-1
- assert (o = ?) => nofKids(?) >= g.nofKids
For Or(kids):
- assert (o = 1) => nofKid(?) >= g.nofKids-1
- assert (o = ?) => nofKids(?) >= g.nofKids
Implements the optimisation applicable to gates for which all kids are independent and have a unique parent, ie applicable only to parts of the nnf formula that are genuine trees from the root and down to input literals.
This optim consists in forcing the maximum number of undefined kids for each possible output value of the gates
For And(kids): - assert (o = 0) => nofKid(?) >= g.nofKids-1 - assert (o = ?) => nofKids(?) >= g.nofKids
For Or(kids): - assert (o = 1) => nofKid(?) >= g.nofKids-1 - assert (o = ?) => nofKids(?) >= g.nofKids
For Ite: - assert (o = 0) => optFalse,
with: - define optFalse := And(optFalseFalse, optFalseTrue, optFalseUndef)
with: - define optFalseFalse := (s = 0) => (t = ? and f = 0) - define optFalseTrue := (s = 1) => (t = 0 and f = ?) - define optFalseUndef := (s = ?) => (t = ? and f = ?)
And - assert (o = 1) => optTrue
with: - define optTrue := And( optTrueFalse, optTrueTrue, optTrueUndef )
with: - define optTrueFalse := (s = 0) => (t = ? and f = 1) - define optTrueTrue := (s = 1) => (t = 1 and f = ?) - define optTrueUndef := (s = ?) => (t = 1 and f = 1)
And - assert (o = ?) => optUndef
with: - define optUndef := (t = ? and f = ?)