From 9e9040cac06165cc284ce76904a50cbb512be039 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 15 Nov 2017 17:26:56 +0100 Subject: [PATCH] =?UTF-8?q?Added=20normalization=20tests=20for=20=E2=80=9C?= =?UTF-8?q?forall=E2=80=9D=20statements.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- lib/pddl/tests/TestNormalization.cpp | 66 +++++++++++++++++++ tests/data/normalization/normalization-3.pddl | 49 ++++++++++++++ 2 files changed, 115 insertions(+) create mode 100644 tests/data/normalization/normalization-3.pddl diff --git a/lib/pddl/tests/TestNormalization.cpp b/lib/pddl/tests/TestNormalization.cpp index f893d30..5df794c 100644 --- a/lib/pddl/tests/TestNormalization.cpp +++ b/lib/pddl/tests/TestNormalization.cpp @@ -158,3 +158,69 @@ TEST_CASE("[normalization] Implications are correctly reduced", "[normalization] CHECK(or2->declaration->name == "test-predicate-1"); } } + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +TEST_CASE("[normalization] Universal quantifiers are correctly reduced", "[normalization]") +{ + pddl::Tokenizer tokenizer; + pddl::Context context(std::move(tokenizer), ignoreWarnings); + + const auto domainFile = fs::path("data") / "normalization" / "normalization-3.pddl"; + context.tokenizer.read(domainFile); + auto description = pddl::parseDescription(context); + const auto normalizedDescription = pddl::normalize(std::move(description)); + + const auto &actions = normalizedDescription.domain->actions; + + SECTION("top-level “forall” statement is replaced with negated “exists” statement over negated argument") + { + const auto &d = actions[0]->precondition.value().get().get>()->argument.get(); + REQUIRE(d->arguments.empty()); + REQUIRE(d->declaration->existentialParameters.size() == 2); + CHECK(d->declaration->existentialParameters[0]->name == "x"); + CHECK(d->declaration->existentialParameters[1]->name == "y"); + const auto &dp = d->declaration->precondition.value().get().get>()->argument.get(); + CHECK(dp->declaration->name == "test-predicate-2"); + REQUIRE(dp->declaration->parameters.size() == 2); + CHECK(dp->declaration->parameters[0]->name == "x"); + CHECK(dp->declaration->parameters[1]->name == "y"); + } + + SECTION("nested “forall” statement is replaced with negated “exists” statement over negated argument") + { + const auto &and1 = actions[1]->precondition.value().get>(); + REQUIRE(and1->arguments.size() == 2); + const auto &d1 = and1->arguments[0].get().get(); + const auto &and2 = d1->declaration->precondition.value().get>(); + REQUIRE(and2->arguments.size() == 2); + const auto &d2 = and2->arguments[0].get>()->argument.get(); + REQUIRE(d2->arguments.empty()); + REQUIRE(d2->declaration->existentialParameters.size() == 2); + CHECK(d2->declaration->existentialParameters[0]->name == "x"); + CHECK(d2->declaration->existentialParameters[1]->name == "y"); + const auto &d2p = d2->declaration->precondition.value().get().get>()->argument.get(); + CHECK(d2p->declaration->name == "test-predicate-2"); + REQUIRE(d2p->declaration->parameters.size() == 2); + CHECK(d2p->declaration->parameters[0]->name == "x"); + CHECK(d2p->declaration->parameters[1]->name == "y"); + } + + SECTION("“forall” statement in goal description is replaced with negated “exists” statement over negated argument") + { + const auto &goal = normalizedDescription.problem.value()->goal.value(); + + const auto &and_ = goal.get>(); + REQUIRE(and_->arguments.size() == 2); + const auto &d = and_->arguments[0].get>()->argument.get(); + REQUIRE(d->arguments.empty()); + REQUIRE(d->declaration->existentialParameters.size() == 2); + CHECK(d->declaration->existentialParameters[0]->name == "x"); + CHECK(d->declaration->existentialParameters[1]->name == "y"); + const auto &dp = d->declaration->precondition.value().get().get>()->argument.get(); + CHECK(dp->declaration->name == "test-predicate-2"); + REQUIRE(dp->declaration->parameters.size() == 2); + CHECK(dp->declaration->parameters[0]->name == "x"); + CHECK(dp->declaration->parameters[1]->name == "y"); + } +} diff --git a/tests/data/normalization/normalization-3.pddl b/tests/data/normalization/normalization-3.pddl new file mode 100644 index 0000000..b929c00 --- /dev/null +++ b/tests/data/normalization/normalization-3.pddl @@ -0,0 +1,49 @@ +; tests that universal quantifiers in preconditions are correctly reduced +(define (domain test-normalization) + (:predicates + (test-predicate-0) + (test-predicate-1 ?x) + (test-predicate-2 ?x ?y)) + + ; top-level “forall” statement + (:action test-action-1 + :parameters + (?x) + :precondition + (forall + (?x ?y) + (test-predicate-2 ?x ?y)) + :effect + (test-predicate-1 ?x)) + + ; nested “forall” statement + (:action test-action-2 + :parameters + (?x) + :precondition + (and + (and + (forall + (?x ?y) + (test-predicate-2 ?x ?y)) + (test-predicate-0)) + (test-predicate-0)) + :effect + (test-predicate-1 ?x)) +) + +(define (problem test-normalization) + (:domain test-normalization) + + (:objects a b c) + + (:init + (test-predicate-0)) + + ; “forall” statement in goal + (:goal + (and + (forall + (?x ?y) + (test-predicate-2 ?x ?y)) + (test-predicate-0))))