These tests ensure that multiple negations are eliminated, negated
quantifiers are replaced appropriately, negations introduced by
reduction are correctly handled, and negated disjunctions and
conjunctions are replaced according to De Morgan’s rules.
These tests ensure that universal quantifiers are correctly reduced to
negated existential quantifiers over the negated argument via derived
predicates in preconditions (nested and not) and goal descriptions.
Previously, the parser read the first statement of the goal as its
precondition, but didn’t check that it was properly terminated with a
closing parenthesis. This allowed arbitrary text to be included within
the goal description without error, which was incorrect.
This commit fixes this issue and adds a corresponding unit test.
While derived predicates stemming from the domain were already
translated, the ones from the problem were missing. This commit fixes
that, although it duplicates the definition of “contains.”
The IDs of derived predicates within problems were accidentally starting
with 1 again, colliding with the IDs of derived predicates in the
domain. With this fix, the IDs are continuously incremented, even after
switching from domain to problem.
Patrick Lühne