From 3c9476699957f26e1d21589cbc2819d242190a7b Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 10 Oct 2023 11:03:15 +0200 Subject: [PATCH 01/71] [up] Support new finer grained problem types --- planning/unified/deps/unified-planning | 2 +- planning/unified/plugin/up_aries/solver.py | 26 +++++++++++++++++----- 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index d0df86de..fd361915 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit d0df86de2ee570cfd52c1a1e35d394cd4ba8bd53 +Subproject commit fd361915af4dd469a68d8ae04b74c4eaf70257cc diff --git a/planning/unified/plugin/up_aries/solver.py b/planning/unified/plugin/up_aries/solver.py index 165c0827..a27bc108 100644 --- a/planning/unified/plugin/up_aries/solver.py +++ b/planning/unified/plugin/up_aries/solver.py @@ -53,7 +53,7 @@ "SIMPLE_NUMERIC_PLANNING", # "GENERAL_NUMERIC_PLANNING", # TIME - # "CONTINUOUS_TIME", + "CONTINUOUS_TIME", "DISCRETE_TIME", "INTERMEDIATE_CONDITIONS_AND_EFFECTS", "EXTERNAL_CONDITIONS_AND_EFFECTS", @@ -61,12 +61,14 @@ "TIMED_EFFECT", # backward compat "TIMED_GOALS", "DURATION_INEQUALITIES", - # "SELF_OVERLAPPING" + "SELF_OVERLAPPING" # EXPRESSION_DURATION "STATIC_FLUENTS_IN_DURATIONS", "STATIC_FLUENTS_IN_DURATION", # backward compat "FLUENTS_IN_DURATIONS", "FLUENTS_IN_DURATION", # backward compat + "INT_TYPE_DURATIONS", + # "REAL_TYPE_DURATIONS", # NUMBERS # "CONTINUOUS_NUMBERS", "DISCRETE_NUMBERS", @@ -95,6 +97,8 @@ # FLUENTS_TYPE "NUMERIC_FLUENTS", "OBJECT_FLUENTS", + "INT_FLUENTS", + # "REAL_FLUENTS", # PARAMETERS # "BOOL_FLUENT_PARAMETERS", # "BOUNDED_INT_FLUENT_PARAMETERS", @@ -109,9 +113,13 @@ "PLAN_LENGTH", # "OVERSUBSCRIPTION", # "TEMPORAL_OVERSUBSCRIPTION", + "INT_NUMBERS_IN_OVERSUBSCRIPTION", + "REAL_NUMBERS_IN_OVERSUBSCRIPTION", # ACTIONS_COST_KIND - # "STATIC_FLUENTS_IN_ACTIONS_COST", - # "FLUENTS_IN_ACTIONS_COST", + "STATIC_FLUENTS_IN_ACTIONS_COST", + "FLUENTS_IN_ACTIONS_COST", + "INT_NUMBERS_IN_ACTIONS_COST", + # "REAL_NUMBERS_IN_ACTIONS_COST", # SIMULATED_ENTITIES # "SIMULATED_EFFECTS", # CONSTRAINTS_KIND @@ -146,12 +154,14 @@ "TIMED_EFFECT", # backward compat "TIMED_GOALS", "DURATION_INEQUALITIES", - # "SELF_OVERLAPPING" + "SELF_OVERLAPPING" # EXPRESSION_DURATION "STATIC_FLUENTS_IN_DURATIONS", "STATIC_FLUENTS_IN_DURATION", # backward compat "FLUENTS_IN_DURATIONS", "FLUENTS_IN_DURATION", # backward compat + "INT_TYPE_DURATIONS", + "REAL_TYPE_DURATIONS", # NUMBERS "CONTINUOUS_NUMBERS", "DISCRETE_NUMBERS", @@ -180,6 +190,8 @@ # FLUENTS_TYPE "NUMERIC_FLUENTS", "OBJECT_FLUENTS", + "INT_FLUENTS", + "REAL_FLUENTS", # PARAMETERS # "BOOL_FLUENT_PARAMETERS", # "BOUNDED_INT_FLUENT_PARAMETERS", @@ -194,9 +206,13 @@ "PLAN_LENGTH", "OVERSUBSCRIPTION", "TEMPORAL_OVERSUBSCRIPTION", + "INT_NUMBERS_IN_OVERSUBSCRIPTION", + "REAL_NUMBERS_IN_OVERSUBSCRIPTION", # ACTIONS_COST_KIND "STATIC_FLUENTS_IN_ACTIONS_COST", "FLUENTS_IN_ACTIONS_COST", + "INT_NUMBERS_IN_ACTIONS_COST", + "REAL_NUMBERS_IN_ACTIONS_COST", # SIMULATED_ENTITIES # "SIMULATED_EFFECTS", # CONSTRAINTS_KIND From 8561f4a2ec32df8781c74d59ce93e8bc8ace944e Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 10 Oct 2023 16:07:43 +0200 Subject: [PATCH 02/71] [up] Update protobuf definition --- planning/grpc/api/src/unified_planning.proto | 9 +++++++ planning/grpc/api/src/unified_planning.rs | 27 ++++++++++++++++++++ 2 files changed, 36 insertions(+) diff --git a/planning/grpc/api/src/unified_planning.proto b/planning/grpc/api/src/unified_planning.proto index 1e1869d6..6af410df 100644 --- a/planning/grpc/api/src/unified_planning.proto +++ b/planning/grpc/api/src/unified_planning.proto @@ -598,6 +598,8 @@ enum Feature { // EXPRESSION_DURATION STATIC_FLUENTS_IN_DURATIONS = 27; FLUENTS_IN_DURATIONS = 28; + REAL_TYPE_DURATIONS = 62; + INT_TYPE_DURATIONS = 63; // NUMBERS CONTINUOUS_NUMBERS = 7; DISCRETE_NUMBERS = 8; @@ -625,6 +627,8 @@ enum Feature { // FLUENTS_TYPE NUMERIC_FLUENTS = 19; OBJECT_FLUENTS = 20; + INT_FLUENTS = 60; + REAL_FLUENTS = 61; // PARAMETERS BOOL_FLUENT_PARAMETERS = 50; BOUNDED_INT_FLUENT_PARAMETERS = 51; @@ -642,6 +646,11 @@ enum Feature { // ACTION_COST_KIND STATIC_FLUENTS_IN_ACTIONS_COST = 45; FLUENTS_IN_ACTIONS_COST = 46; + REAL_NUMBERS_IN_ACTIONS_COST = 64; + INT_NUMBERS_IN_ACTIONS_COST = 65; + // OVERSUBSCRIPTION_KIND + REAL_NUMBERS_IN_OVERSUBSCRIPTION = 66; + INT_NUMBERS_IN_OVERSUBSCRIPTION = 67; // SIMULATED_ENTITIES SIMULATED_EFFECTS = 25; // CONSTRAINTS_KIND diff --git a/planning/grpc/api/src/unified_planning.rs b/planning/grpc/api/src/unified_planning.rs index 5cf13bdd..8432a506 100644 --- a/planning/grpc/api/src/unified_planning.rs +++ b/planning/grpc/api/src/unified_planning.rs @@ -1193,6 +1193,8 @@ pub enum Feature { /// EXPRESSION_DURATION StaticFluentsInDurations = 27, FluentsInDurations = 28, + RealTypeDurations = 62, + IntTypeDurations = 63, /// NUMBERS ContinuousNumbers = 7, DiscreteNumbers = 8, @@ -1220,6 +1222,8 @@ pub enum Feature { /// FLUENTS_TYPE NumericFluents = 19, ObjectFluents = 20, + IntFluents = 60, + RealFluents = 61, /// PARAMETERS BoolFluentParameters = 50, BoundedIntFluentParameters = 51, @@ -1237,6 +1241,11 @@ pub enum Feature { /// ACTION_COST_KIND StaticFluentsInActionsCost = 45, FluentsInActionsCost = 46, + RealNumbersInActionsCost = 64, + IntNumbersInActionsCost = 65, + /// OVERSUBSCRIPTION_KIND + RealNumbersInOversubscription = 66, + IntNumbersInOversubscription = 67, /// SIMULATED_ENTITIES SimulatedEffects = 25, /// CONSTRAINTS_KIND @@ -1274,6 +1283,8 @@ impl Feature { Feature::SelfOverlapping => "SELF_OVERLAPPING", Feature::StaticFluentsInDurations => "STATIC_FLUENTS_IN_DURATIONS", Feature::FluentsInDurations => "FLUENTS_IN_DURATIONS", + Feature::RealTypeDurations => "REAL_TYPE_DURATIONS", + Feature::IntTypeDurations => "INT_TYPE_DURATIONS", Feature::ContinuousNumbers => "CONTINUOUS_NUMBERS", Feature::DiscreteNumbers => "DISCRETE_NUMBERS", Feature::BoundedTypes => "BOUNDED_TYPES", @@ -1302,6 +1313,8 @@ impl Feature { Feature::HierarchicalTyping => "HIERARCHICAL_TYPING", Feature::NumericFluents => "NUMERIC_FLUENTS", Feature::ObjectFluents => "OBJECT_FLUENTS", + Feature::IntFluents => "INT_FLUENTS", + Feature::RealFluents => "REAL_FLUENTS", Feature::BoolFluentParameters => "BOOL_FLUENT_PARAMETERS", Feature::BoundedIntFluentParameters => "BOUNDED_INT_FLUENT_PARAMETERS", Feature::BoolActionParameters => "BOOL_ACTION_PARAMETERS", @@ -1316,6 +1329,10 @@ impl Feature { Feature::TemporalOversubscription => "TEMPORAL_OVERSUBSCRIPTION", Feature::StaticFluentsInActionsCost => "STATIC_FLUENTS_IN_ACTIONS_COST", Feature::FluentsInActionsCost => "FLUENTS_IN_ACTIONS_COST", + Feature::RealNumbersInActionsCost => "REAL_NUMBERS_IN_ACTIONS_COST", + Feature::IntNumbersInActionsCost => "INT_NUMBERS_IN_ACTIONS_COST", + Feature::RealNumbersInOversubscription => "REAL_NUMBERS_IN_OVERSUBSCRIPTION", + Feature::IntNumbersInOversubscription => "INT_NUMBERS_IN_OVERSUBSCRIPTION", Feature::SimulatedEffects => "SIMULATED_EFFECTS", Feature::TrajectoryConstraints => "TRAJECTORY_CONSTRAINTS", Feature::StateInvariants => "STATE_INVARIANTS", @@ -1347,6 +1364,8 @@ impl Feature { "SELF_OVERLAPPING" => Some(Self::SelfOverlapping), "STATIC_FLUENTS_IN_DURATIONS" => Some(Self::StaticFluentsInDurations), "FLUENTS_IN_DURATIONS" => Some(Self::FluentsInDurations), + "REAL_TYPE_DURATIONS" => Some(Self::RealTypeDurations), + "INT_TYPE_DURATIONS" => Some(Self::IntTypeDurations), "CONTINUOUS_NUMBERS" => Some(Self::ContinuousNumbers), "DISCRETE_NUMBERS" => Some(Self::DiscreteNumbers), "BOUNDED_TYPES" => Some(Self::BoundedTypes), @@ -1375,6 +1394,8 @@ impl Feature { "HIERARCHICAL_TYPING" => Some(Self::HierarchicalTyping), "NUMERIC_FLUENTS" => Some(Self::NumericFluents), "OBJECT_FLUENTS" => Some(Self::ObjectFluents), + "INT_FLUENTS" => Some(Self::IntFluents), + "REAL_FLUENTS" => Some(Self::RealFluents), "BOOL_FLUENT_PARAMETERS" => Some(Self::BoolFluentParameters), "BOUNDED_INT_FLUENT_PARAMETERS" => Some(Self::BoundedIntFluentParameters), "BOOL_ACTION_PARAMETERS" => Some(Self::BoolActionParameters), @@ -1389,6 +1410,12 @@ impl Feature { "TEMPORAL_OVERSUBSCRIPTION" => Some(Self::TemporalOversubscription), "STATIC_FLUENTS_IN_ACTIONS_COST" => Some(Self::StaticFluentsInActionsCost), "FLUENTS_IN_ACTIONS_COST" => Some(Self::FluentsInActionsCost), + "REAL_NUMBERS_IN_ACTIONS_COST" => Some(Self::RealNumbersInActionsCost), + "INT_NUMBERS_IN_ACTIONS_COST" => Some(Self::IntNumbersInActionsCost), + "REAL_NUMBERS_IN_OVERSUBSCRIPTION" => { + Some(Self::RealNumbersInOversubscription) + } + "INT_NUMBERS_IN_OVERSUBSCRIPTION" => Some(Self::IntNumbersInOversubscription), "SIMULATED_EFFECTS" => Some(Self::SimulatedEffects), "TRAJECTORY_CONSTRAINTS" => Some(Self::TrajectoryConstraints), "STATE_INVARIANTS" => Some(Self::StateInvariants), From 8d72c7b423a6ddd15de9d31e00eaf6dc4f324b16 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 10 Oct 2023 16:12:21 +0200 Subject: [PATCH 03/71] fix(up): Minor fixes to supported problem declarations --- planning/unified/plugin/up_aries/solver.py | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/planning/unified/plugin/up_aries/solver.py b/planning/unified/plugin/up_aries/solver.py index a27bc108..e2a57308 100644 --- a/planning/unified/plugin/up_aries/solver.py +++ b/planning/unified/plugin/up_aries/solver.py @@ -61,7 +61,7 @@ "TIMED_EFFECT", # backward compat "TIMED_GOALS", "DURATION_INEQUALITIES", - "SELF_OVERLAPPING" + "SELF_OVERLAPPING", # EXPRESSION_DURATION "STATIC_FLUENTS_IN_DURATIONS", "STATIC_FLUENTS_IN_DURATION", # backward compat @@ -107,14 +107,14 @@ "UNBOUNDED_INT_ACTION_PARAMETERS", # "REAL_ACTION_PARAMETERS", # QUALITY_METRICS - # "ACTIONS_COST", + "ACTIONS_COST", # "FINAL_VALUE", "MAKESPAN", "PLAN_LENGTH", # "OVERSUBSCRIPTION", # "TEMPORAL_OVERSUBSCRIPTION", "INT_NUMBERS_IN_OVERSUBSCRIPTION", - "REAL_NUMBERS_IN_OVERSUBSCRIPTION", + # "REAL_NUMBERS_IN_OVERSUBSCRIPTION", # ACTIONS_COST_KIND "STATIC_FLUENTS_IN_ACTIONS_COST", "FLUENTS_IN_ACTIONS_COST", @@ -132,7 +132,8 @@ "TASK_ORDER_TOTAL", "TASK_ORDER_PARTIAL", # "TASK_ORDER_TEMPORAL", - } + }, + version=2 ) _ARIES_VAL_SUPPORTED_KIND = up.model.ProblemKind( @@ -154,7 +155,7 @@ "TIMED_EFFECT", # backward compat "TIMED_GOALS", "DURATION_INEQUALITIES", - "SELF_OVERLAPPING" + "SELF_OVERLAPPING", # EXPRESSION_DURATION "STATIC_FLUENTS_IN_DURATIONS", "STATIC_FLUENTS_IN_DURATION", # backward compat @@ -225,7 +226,8 @@ "TASK_ORDER_TOTAL", "TASK_ORDER_PARTIAL", "TASK_ORDER_TEMPORAL", - } + }, + version=2 ) From 2cfee67cf48ce55461b8b8660efe10d5c32b8f03 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 25 Oct 2023 09:37:24 +0200 Subject: [PATCH 04/71] fix(up): Remove declared support for pre-1.0 features --- planning/unified/deps/unified-planning | 2 +- planning/unified/plugin/up_aries/solver.py | 8 -------- 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index fd361915..145ce9b9 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit fd361915af4dd469a68d8ae04b74c4eaf70257cc +Subproject commit 145ce9b90ee176a4e30260568741581c35ad9a75 diff --git a/planning/unified/plugin/up_aries/solver.py b/planning/unified/plugin/up_aries/solver.py index e2a57308..c4b4e17e 100644 --- a/planning/unified/plugin/up_aries/solver.py +++ b/planning/unified/plugin/up_aries/solver.py @@ -58,15 +58,12 @@ "INTERMEDIATE_CONDITIONS_AND_EFFECTS", "EXTERNAL_CONDITIONS_AND_EFFECTS", "TIMED_EFFECTS", - "TIMED_EFFECT", # backward compat "TIMED_GOALS", "DURATION_INEQUALITIES", "SELF_OVERLAPPING", # EXPRESSION_DURATION "STATIC_FLUENTS_IN_DURATIONS", - "STATIC_FLUENTS_IN_DURATION", # backward compat "FLUENTS_IN_DURATIONS", - "FLUENTS_IN_DURATION", # backward compat "INT_TYPE_DURATIONS", # "REAL_TYPE_DURATIONS", # NUMBERS @@ -77,7 +74,6 @@ "NEGATIVE_CONDITIONS", "DISJUNCTIVE_CONDITIONS", "EQUALITIES", - "EQUALITY", # backward compat # "EXISTENTIAL_CONDITIONS", # "UNIVERSAL_CONDITIONS", # EFFECTS_KIND @@ -152,15 +148,12 @@ "INTERMEDIATE_CONDITIONS_AND_EFFECTS", "EXTERNAL_CONDITIONS_AND_EFFECTS", "TIMED_EFFECTS", - "TIMED_EFFECT", # backward compat "TIMED_GOALS", "DURATION_INEQUALITIES", "SELF_OVERLAPPING", # EXPRESSION_DURATION "STATIC_FLUENTS_IN_DURATIONS", - "STATIC_FLUENTS_IN_DURATION", # backward compat "FLUENTS_IN_DURATIONS", - "FLUENTS_IN_DURATION", # backward compat "INT_TYPE_DURATIONS", "REAL_TYPE_DURATIONS", # NUMBERS @@ -171,7 +164,6 @@ "NEGATIVE_CONDITIONS", "DISJUNCTIVE_CONDITIONS", "EQUALITIES", - "EQUALITY", # backward compat "EXISTENTIAL_CONDITIONS", "UNIVERSAL_CONDITIONS", # EFFECTS_KIND From d9373ead413f9547dff4b6f3e32bb732e51598eb Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 25 Oct 2023 10:01:59 +0200 Subject: [PATCH 05/71] deps: Update UP upstream version --- planning/unified/deps/unified-planning | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index 145ce9b9..1b401403 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit 145ce9b90ee176a4e30260568741581c35ad9a75 +Subproject commit 1b401403d829edf5b8743177376842b5cc5363f4 From 7d74b96eebc248a1daad0213a5a559b40949837e Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 25 Oct 2023 10:28:22 +0200 Subject: [PATCH 06/71] deps(up): Use UP master branch --- planning/unified/deps/unified-planning | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index 1b401403..4b068216 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit 1b401403d829edf5b8743177376842b5cc5363f4 +Subproject commit 4b0682168f8ac198df54c25a5e84cd214426b166 From 3d6249dbb656f0cc1bfa89e22fa9e37932e029d1 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 25 Oct 2023 10:52:21 +0200 Subject: [PATCH 07/71] fix(up): add ignore domain to allow CI to proceed --- ci/up_integration.py | 2 ++ planning/unified/deps/unified-planning | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/ci/up_integration.py b/ci/up_integration.py index 9c6c2799..c3dcbb76 100755 --- a/ci/up_integration.py +++ b/ci/up_integration.py @@ -8,6 +8,7 @@ # declare aries val get_environment().factory.add_engine("aries-val", "up_aries", "AriesVal") +IGNORED_SOLVE_DOMAINS = ["up:basic_numeric"] mode = sys.argv[1] @@ -15,6 +16,7 @@ errors = report.report_validation('aries-val') elif mode.lower() == 'solve': errors = report.report_oneshot("aries") + errors = list(filter(lambda solver_pb: solver_pb[1] not in IGNORED_SOLVE_DOMAINS, errors)) else: raise ValueError(f"Unknown mode: {mode}") diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index 4b068216..1b401403 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit 4b0682168f8ac198df54c25a5e84cd214426b166 +Subproject commit 1b401403d829edf5b8743177376842b5cc5363f4 From 1c7061262429053ed15523f917bd853f6b74c072 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 25 Oct 2023 12:36:30 +0200 Subject: [PATCH 08/71] ci: Switch to new UP testing facilities --- .github/workflows/aries.yml | 9 +++++++-- .gitmodules | 3 --- ci/up_integration.py | 24 ----------------------- planning/unified/deps/planning-test-cases | 1 - planning/unified/deps/unified-planning | 2 +- 5 files changed, 8 insertions(+), 31 deletions(-) delete mode 100755 ci/up_integration.py delete mode 160000 planning/unified/deps/planning-test-cases diff --git a/.github/workflows/aries.yml b/.github/workflows/aries.yml index 5b59a34a..ff50a9cc 100644 --- a/.github/workflows/aries.yml +++ b/.github/workflows/aries.yml @@ -126,9 +126,14 @@ jobs: - name: Install python dependencies run: python3 -m pip install -r planning/unified/requirements.txt - name: Validator tests - run: source planning/unified/dev.env && python3 ci/up_integration.py val + run: | + source planning/unified/dev.env + python3 planning/unified/deps/unified-planning/up_test_cases/report.py aries-val - name: Solver tests - run: source planning/unified/dev.env && python3 ci/up_integration.py solve + run: | + source planning/unified/dev.env + python3 planning/unified/deps/unified-planning/up_test_cases/report.py aries + tests: # Meta-job that only requires all test-jobs to pass needs: [lints, unit-tests, integration-tests, unified-planning-api, unified-planning-integration] diff --git a/.gitmodules b/.gitmodules index 181d2cbf..bdb6f130 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,3 @@ -[submodule "planning/unified/deps/planning-test-cases"] - path = planning/unified/deps/planning-test-cases - url = https://github.com/aiplan4eu/planning-test-cases.git [submodule "planning/unified/deps/unified-planning"] path = planning/unified/deps/unified-planning url = https://github.com/aiplan4eu/unified-planning.git diff --git a/ci/up_integration.py b/ci/up_integration.py deleted file mode 100755 index c3dcbb76..00000000 --- a/ci/up_integration.py +++ /dev/null @@ -1,24 +0,0 @@ -#!/usr/bin/python3 - -# Script that run the UP integration tests. - -import report # from planning-test-case, should probably change once the upstream repository stabilizes -from unified_planning.shortcuts import * - -# declare aries val -get_environment().factory.add_engine("aries-val", "up_aries", "AriesVal") - -IGNORED_SOLVE_DOMAINS = ["up:basic_numeric"] - -mode = sys.argv[1] - -if mode.lower() == "val": - errors = report.report_validation('aries-val') -elif mode.lower() == 'solve': - errors = report.report_oneshot("aries") - errors = list(filter(lambda solver_pb: solver_pb[1] not in IGNORED_SOLVE_DOMAINS, errors)) -else: - raise ValueError(f"Unknown mode: {mode}") - - -assert len(errors) == 0 diff --git a/planning/unified/deps/planning-test-cases b/planning/unified/deps/planning-test-cases deleted file mode 160000 index b76281e0..00000000 --- a/planning/unified/deps/planning-test-cases +++ /dev/null @@ -1 +0,0 @@ -Subproject commit b76281e0133c2ac9290ba564cf61018129ae0642 diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index 1b401403..8d728713 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit 1b401403d829edf5b8743177376842b5cc5363f4 +Subproject commit 8d72871352ebd7a4f18c3837bd41a91713c4cc7e From aefd59c239db92aa4a87ed936244d7132b8c6804 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 25 Oct 2023 15:43:25 +0200 Subject: [PATCH 09/71] deps(up): Update upstream UP version --- planning/unified/deps/unified-planning | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/planning/unified/deps/unified-planning b/planning/unified/deps/unified-planning index 8d728713..282488f3 160000 --- a/planning/unified/deps/unified-planning +++ b/planning/unified/deps/unified-planning @@ -1 +1 @@ -Subproject commit 8d72871352ebd7a4f18c3837bd41a91713c4cc7e +Subproject commit 282488f335c8d081ebf05c3d510a83ae71b199d2 From d592df92763378169d4bf5b13762c93c9b61bcbd Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 4 Sep 2023 15:52:43 +0200 Subject: [PATCH 10/71] fix(encode|resource): set assignment literal `la` to condition value --- planning/planners/src/encode.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 67405d25..efea6aa1 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -1083,7 +1083,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result for &(li, ci) in lis.get(idx).unwrap() { sum += LinearSum::with_lit(ci, li); } - sum -= LinearSum::from(cond_val); + sum -= LinearSum::with_lit(cond_val, la); solver.enforce(sum.clone().leq(0), [prez_cond]); solver.enforce(sum.geq(0), [prez_cond]); } From 40e79d05cc0b0c6c97a982a4d39a9ed792a269d9 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 5 Sep 2023 09:58:47 +0200 Subject: [PATCH 11/71] feat(grpc): export activity parameters for scheduling --- planning/grpc/server/src/serialize.rs | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/planning/grpc/server/src/serialize.rs b/planning/grpc/server/src/serialize.rs index abd1b495..41e4338c 100644 --- a/planning/grpc/server/src/serialize.rs +++ b/planning/grpc/server/src/serialize.rs @@ -127,7 +127,7 @@ pub fn serialize_plan( }; // If this is a scheduling problem, interpret all actions as activities - // TODO: currently, parameters/variables are not supported. + // TODO: currently, variables are not supported. let schedule = if _problem_request.scheduling_extension.is_some() { let mut schedule = Schedule { activities: vec![], @@ -144,6 +144,27 @@ pub fn serialize_plan( format!("{name}.end"), a.end_time.expect("No end time in scheduling solution").into(), ); + if !a.parameters.is_empty() { + // Search for the corresponding activity definition + let mut act: Option = None; + for _a in _problem_request + .scheduling_extension + .as_ref() + .unwrap() + .activities + .iter() + { + if _a.name == name { + act = Some(_a.clone()); + break; + } + } + let act = act.expect(format!("Cannot find the activity {} definition", name).as_str()); + // Assign the solution value to each action parameter + for (v, p) in a.parameters.iter().zip(act.parameters) { + schedule.variable_assignments.insert(p.name, v.clone()); + } + } schedule.activities.push(name); } Some(schedule) From c8a48b4d728af6afcc23beb86fb2cfd2df8bf0cf Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 11 Sep 2023 16:40:21 +0200 Subject: [PATCH 12/71] refactor(encode|resource): redesign the encoding --- planning/planners/src/encode.rs | 254 +++++++++++++++++++++----------- 1 file changed, 164 insertions(+), 90 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index efea6aa1..3ad81a63 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -930,6 +930,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result let _span = span.enter(); let mut num_resource_constraints = 0; + // Get the effects and the conditions on numeric state variables. + // Filter those who are not present. let assignments: Vec<_> = effs .iter() .filter(|(_, prez, eff)| { @@ -952,7 +954,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .map(|&(_, prez, cond)| (prez, cond.clone())) .collect(); - // Force the new assigned value to be in the state variable domain + // Force the new assigned values to be in the state variable domain. for &&(_, prez, eff) in &assignments { let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { unreachable!() }; let EffectOp::Assign(val) = eff.operation else { unreachable!() }; @@ -962,19 +964,24 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result num_resource_constraints += 1; } - // Convert the increase effects into conditions in order to check that - // the new value is in the state variable domain + // Convert the increase effects into conditions in order to check that the new value is in the state variable domain. for &&(eff_id, prez, eff) in &increases { - assert_eq!(eff.transition_start + FAtom::EPSILON, eff.persistence_start); - assert!(eff.min_persistence_end.is_empty()); + assert!( + eff.transition_start + FAtom::EPSILON == eff.persistence_start && eff.min_persistence_end.is_empty(), + "Only instantaneous effects are supported" + ); + // Get the bounds of the state variable. let (lb, ub) = if let Type::Int { lb, ub } = eff.state_var.fluent.return_type() { (lb, ub) } else { (INT_CST_MIN, INT_CST_MAX) }; + // Create a new variable with those bounds. let var = solver .model .new_ivar(lb, ub, Container::Instance(eff_id.instance_id) / VarType::Reification); + // Check that the state variable value is equals to that new variable. + // It will force the state variable value to be in the bounds of the new variable. conditions.push(( prez, Condition { @@ -986,108 +993,175 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result )); } - // Convert the conditions into linear constraints - let spp = |solver: &mut Solver, cond: &Condition, eff: &&Effect, prez_eff: &Lit| { - // Checks that the effect is present and has the same parameters as the condition. - let mut same_params_and_prez = vec![*prez_eff]; - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - same_params_and_prez.push(solver.reify(eq(a, b))); - } - same_params_and_prez - }; + /* + * For each condition `R == z`, a set of linear sum constraints of the form + * `la_j*ca_j + li_jk*ci_jk + ... + li_jm*ci_jm - la_j*z == 0` are created. + * + * The `la_j` literal is true if and only if the associated assignment effect `e_j` is the last one for the condition. + * A disjunctive clause will force to have at least one `la_j`. + * The `ca_j` value is the value of the assignment effect `e_j`. + * The `li_j*` literals are true if and only if: + * - `la_j` is true + * - the associated increase effect `e_*` is between `e_j` and the condition + * The `ci_j*` values are the value of the increase effects `e_*`. + * The `z` variable is the value of the condition. + * + * With all these literals, only one constraint will be taken into account: that associated with the last assignment. + */ for (prez_cond, cond) in conditions { - // Only the instantaneous conditions are supported for the moment - assert_eq!(cond.start, cond.end); + assert_eq!(cond.start, cond.end, "Only the instantaneous conditions are supported"); - // Filter effects to keep the ones which are unifiable with the condition. - let unifiable_assignments: Vec<_> = assignments + // Whether the effect is likely to support the condition. + let eff_compatible_with_cond = |solver: &Solver, prez_eff: Lit, eff: &Effect| { + !solver.model.state.exclusive(prez_eff, prez_cond) + && unifiable_sv(&solver.model, &cond.state_var, &eff.state_var) + }; + + let compatible_assignments = assignments .iter() - .filter(|(_, _, ass)| unifiable_sv(&solver.model, &cond.state_var, &ass.state_var)) - .collect(); - let unifiable_increases: Vec<_> = increases + .filter(|(_, prez, eff)| eff_compatible_with_cond(&solver, *prez, eff)) + .collect::>(); + let compatible_increases = increases .iter() - .filter(|(_, _, ass)| unifiable_sv(&solver.model, &cond.state_var, &ass.state_var)) - .collect(); - - // Get the assignment literals and the associated value. - // A literal is true if: - // - the associated chronicle is present - // - the parameters of the resource match the ones of the condition - // - the assignment is the latest one before the condition - let las: Vec<(Lit, IAtom)> = unifiable_assignments + .filter(|(_, prez, eff)| eff_compatible_with_cond(&solver, *prez, eff)) + .collect::>(); + + /* + * Vector to store the `la_j` literals, `ca_j` values and the persistence timepoint of the effect `e_j`. + * + * `la_j` is true if and only if the associated assignment effect `e_j`: + * - is present + * - is before the condition + * - has the same state variable as the condition + * - for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` + */ + let la_ca_ta = compatible_assignments .iter() - .map(|(ass_1_id, prez_ass_1, ass_1)| { - let is_before_cond_1 = solver.reify(f_leq(ass_1.persistence_start, cond.start)); - let mut same_params_and_prez_1 = spp(&mut solver, &cond, ass_1, prez_ass_1); - let mut is_last_assign: Vec = vec![]; - for (ass_2_id, prez_ass_2, ass_2) in &unifiable_assignments { - if ass_2_id == ass_1_id { + .map(|(eff_id, prez_eff, eff)| { + let mut la_conjunction: Vec = Vec::with_capacity(32); + // is present + la_conjunction.push(*prez_eff); + // is before the condition + la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + // has the same state variable as the condition + debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + la_conjunction.push(solver.reify(eq(a, b))); + } + // for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` + // This implies constraint is expressed as a disjunction. + for (other_eff_id, prez_other_eff, other_eff) in compatible_assignments.iter() { + // same effect: continue + if eff_id == other_eff_id { continue; } - let is_before_cond_2 = solver.reify(f_leq(ass_2.persistence_start, cond.start)); - let is_before_ass_1 = solver.reify(f_lt(ass_2.persistence_start, ass_1.persistence_start)); - let mut same_params_and_prez_2 = spp(&mut solver, &cond, ass_2, prez_ass_2); - same_params_and_prez_2.push(is_before_cond_2); - let same_params_and_prez_2 = solver.reify(and(same_params_and_prez_2)); - is_last_assign.push(solver.reify(implies(same_params_and_prez_2, is_before_ass_1))); + let mut disjunction: Vec = Vec::with_capacity(12); + // is not present + disjunction.push(!*prez_other_eff); + // is after the condition + disjunction.push(solver.reify(f_lt(cond.end, other_eff.persistence_start))); + // has a state variable different from the condition + debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + disjunction.push(solver.reify(neq(a, b))); + } + // is before the effect `e_j` + disjunction.push(solver.reify(f_lt(eff_ends[other_eff_id], eff.persistence_start))); + + let disjunction_lit = solver.reify(or(disjunction.clone())); + la_conjunction.push(disjunction_lit); } - is_last_assign.append(&mut same_params_and_prez_1); - is_last_assign.push(is_before_cond_1); - // Get the value of the assignment - let EffectOp::Assign(val) = ass_1.operation else { unreachable!() }; - let val: IAtom = val.try_into().expect("Not integer assignment to an int state variable"); - (solver.reify(and(is_last_assign)), val) + + // Create the `la_j` literal. + let la_lit = solver.reify(and(la_conjunction.clone())); + debug_assert!(solver + .model + .state + .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); + + // Get the `ca_j` variable. + let EffectOp::Assign(eff_val) = eff.operation else { unreachable!() }; + let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); + + // Get the persistence timepoint of the effect `e_j`. + let ta = eff.persistence_start; + return (la_lit, ca, ta); }) - .collect(); - // Force to have one assignment literal, i.e. one latest assignment. - solver.enforce(or(las.iter().map(|&(l, _)| l).collect::>()), [prez_cond]); - - // Get the increase literals and the associated value. - // A literal is true if: - // - the associated assignment literal is true, so we are considering the latest assignment - // - the increase is after this assignment - // - the associated chronicle is present - // - the parameters of the resource match the ones of the condition - // - the increase is before the condition - let lis: Vec> = unifiable_assignments + .collect::>(); + + // Force to have at least one assignment. + let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| la.clone()).collect::>(); + solver.enforce(or(la_disjuncts), [prez_cond]); + + /* + * Matrix to store the `li_j*` literals and `ci_j*` values. + * + * `li_j*` is true if and only if the associated increase effect `e_*`: + * - is present + * - is before the condition + * - is after the assignment effect `e_j` + * - has the same state variable as the condition + * - `la_j` is true + */ + let m_li_ci = la_ca_ta .iter() - .enumerate() - .map(|(idx, (_, _, ass))| { - let Some(&(la_ass,_)) = las.get(idx) else { unreachable!() }; - unifiable_increases + .map(|(la, _, ta)| { + compatible_increases .iter() - .map(|(_, prez_inc, inc)| { - let mut disjuncts = spp(&mut solver, &cond, inc, prez_inc); - disjuncts.push(la_ass); - disjuncts.push(solver.reify(f_lt(ass.persistence_start, inc.persistence_start))); - disjuncts.push(solver.reify(f_lt(inc.persistence_start, cond.start))); - // Get the value of the increase - let EffectOp::Increase(val) = inc.operation else { unreachable!() }; - (solver.reify(and(disjuncts)), val.into()) + .map(|(_, prez_eff, eff)| { + let mut li_conjunction: Vec = Vec::with_capacity(12); + // `la_j` is true + li_conjunction.push(la.clone()); + // is present + li_conjunction.push(*prez_eff); + // is before the condition + li_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + // is after the assignment effect `e_j` + li_conjunction.push(solver.reify(f_lt(*ta, eff.persistence_start))); + // has the same state variable as the condition + debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + li_conjunction.push(solver.reify(eq(a, b))); + } + // Create the `li_j*` literal. + let li_lit = solver.reify(and(li_conjunction)); + debug_assert!(solver + .model + .state + .implies(prez_cond, solver.model.presence_literal(li_lit.variable()))); + + // Get the `ci_j*` value. + let EffectOp::Increase(eff_val) = eff.operation else { unreachable!() }; + let ci: IAtom = eff_val.into(); + return (li_lit, ci); }) - .collect() + .collect::>() }) - .collect(); - - // Create the linear constraints. - // For a condition `[t]R=z`, there are of the form - // `l^a_q*c^a_q + l^i_{q1}*c^i_1 + ... + l^i_{qm}*c^i_m - z = 0` - let cond_val: IAtom = cond - .value - .try_into() - .expect("Not integer comparison for an int state variable"); - for (idx, &(la, ca)) in las.iter().enumerate() { - let mut sum = LinearSum::with_lit(ca, la); - for &(li, ci) in lis.get(idx).unwrap() { + .collect::>(); + + // Create the linear sum constraints. + for (&(la, ca, _), li_ci) in la_ca_ta.iter().zip(m_li_ci) { + // Create the sum. + let mut sum = LinearSum::zero(); + sum += LinearSum::with_lit(ca, la); + for &(li, ci) in li_ci.iter() { sum += LinearSum::with_lit(ci, li); } + let cond_val = + IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); sum -= LinearSum::with_lit(cond_val, la); - solver.enforce(sum.clone().leq(0), [prez_cond]); - solver.enforce(sum.geq(0), [prez_cond]); + // Force the sum to be equals to 0. + solver.enforce(sum.clone().geq(0), [prez_cond]); + solver.enforce(sum.leq(0), [prez_cond]); + num_resource_constraints += 1; } - num_resource_constraints += 1; + println!(); } tracing::debug!(%num_resource_constraints); From 7778348e97597760cb9ccb4b53e89c23ad15884f Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 11 Sep 2023 17:05:41 +0200 Subject: [PATCH 13/71] fix: cargo clippy warning && upf ci failure --- planning/grpc/server/src/serialize.rs | 2 +- planning/planners/src/encode.rs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/planning/grpc/server/src/serialize.rs b/planning/grpc/server/src/serialize.rs index 41e4338c..9d88a4f1 100644 --- a/planning/grpc/server/src/serialize.rs +++ b/planning/grpc/server/src/serialize.rs @@ -159,7 +159,7 @@ pub fn serialize_plan( break; } } - let act = act.expect(format!("Cannot find the activity {} definition", name).as_str()); + let act = act.unwrap_or_else(|| panic!("Cannot find the activity {} definition", name)); // Assign the solution value to each action parameter for (v, p) in a.parameters.iter().zip(act.parameters) { schedule.variable_assignments.insert(p.name, v.clone()); diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 3ad81a63..bad5e27b 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -1089,12 +1089,12 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // Get the persistence timepoint of the effect `e_j`. let ta = eff.persistence_start; - return (la_lit, ca, ta); + (la_lit, ca, ta) }) .collect::>(); // Force to have at least one assignment. - let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| la.clone()).collect::>(); + let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| *la).collect::>(); solver.enforce(or(la_disjuncts), [prez_cond]); /* @@ -1115,7 +1115,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .map(|(_, prez_eff, eff)| { let mut li_conjunction: Vec = Vec::with_capacity(12); // `la_j` is true - li_conjunction.push(la.clone()); + li_conjunction.push(*la); // is present li_conjunction.push(*prez_eff); // is before the condition @@ -1139,7 +1139,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // Get the `ci_j*` value. let EffectOp::Increase(eff_val) = eff.operation else { unreachable!() }; let ci: IAtom = eff_val.into(); - return (li_lit, ci); + (li_lit, ci) }) .collect::>() }) From 6602a9558429bb2cfa670b302c93dbfcaa471608 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 12 Sep 2023 09:18:00 +0200 Subject: [PATCH 14/71] refactor(encode|resource): `la` creation in function --- planning/planners/src/encode.rs | 144 +++++++++++++++++--------------- 1 file changed, 78 insertions(+), 66 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index bad5e27b..88362a9b 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -1026,72 +1026,9 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .filter(|(_, prez, eff)| eff_compatible_with_cond(&solver, *prez, eff)) .collect::>(); - /* - * Vector to store the `la_j` literals, `ca_j` values and the persistence timepoint of the effect `e_j`. - * - * `la_j` is true if and only if the associated assignment effect `e_j`: - * - is present - * - is before the condition - * - has the same state variable as the condition - * - for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` - */ - let la_ca_ta = compatible_assignments - .iter() - .map(|(eff_id, prez_eff, eff)| { - let mut la_conjunction: Vec = Vec::with_capacity(32); - // is present - la_conjunction.push(*prez_eff); - // is before the condition - la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - la_conjunction.push(solver.reify(eq(a, b))); - } - // for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` - // This implies constraint is expressed as a disjunction. - for (other_eff_id, prez_other_eff, other_eff) in compatible_assignments.iter() { - // same effect: continue - if eff_id == other_eff_id { - continue; - } - let mut disjunction: Vec = Vec::with_capacity(12); - // is not present - disjunction.push(!*prez_other_eff); - // is after the condition - disjunction.push(solver.reify(f_lt(cond.end, other_eff.persistence_start))); - // has a state variable different from the condition - debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - disjunction.push(solver.reify(neq(a, b))); - } - // is before the effect `e_j` - disjunction.push(solver.reify(f_lt(eff_ends[other_eff_id], eff.persistence_start))); - - let disjunction_lit = solver.reify(or(disjunction.clone())); - la_conjunction.push(disjunction_lit); - } - - // Create the `la_j` literal. - let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver - .model - .state - .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); - - // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { unreachable!() }; - let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - - // Get the persistence timepoint of the effect `e_j`. - let ta = eff.persistence_start; - (la_lit, ca, ta) - }) - .collect::>(); + // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. + let la_ca_ta = + create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, &eff_ends, &mut solver); // Force to have at least one assignment. let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| *la).collect::>(); @@ -1177,3 +1114,78 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result encoding, }) } + +/** +Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. + +`la_j` is true if and only if the associated assignment effect `e_j`: + - is present + - is before the condition + - has the same state variable as the condition + - for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` +**/ +fn create_la_vector_without_timepoints( + assignments: Vec<&&(EffID, Lit, &Effect)>, + cond: &Condition, + prez_cond: Lit, + eff_ends: &HashMap, + solver: &mut Solver, +) -> Vec<(Lit, IAtom, FAtom)> { + assignments + .iter() + .map(|(eff_id, prez_eff, eff)| { + let mut la_conjunction: Vec = Vec::with_capacity(32); + // is present + la_conjunction.push(*prez_eff); + // is before the condition + la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + // has the same state variable as the condition + debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + la_conjunction.push(solver.reify(eq(a, b))); + } + // for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` + // This implies constraint is expressed as a disjunction. + for (other_eff_id, prez_other_eff, other_eff) in assignments.iter() { + // same effect: continue + if eff_id == other_eff_id { + continue; + } + let mut disjunction: Vec = Vec::with_capacity(12); + // is not present + disjunction.push(!*prez_other_eff); + // is after the condition + disjunction.push(solver.reify(f_lt(cond.end, other_eff.persistence_start))); + // has a state variable different from the condition + debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + disjunction.push(solver.reify(neq(a, b))); + } + // is before the effect `e_j` + disjunction.push(solver.reify(f_lt(eff_ends[other_eff_id], eff.persistence_start))); + + let disjunction_lit = solver.reify(or(disjunction.clone())); + la_conjunction.push(disjunction_lit); + } + + // Create the `la_j` literal. + let la_lit = solver.reify(and(la_conjunction.clone())); + debug_assert!(solver + .model + .state + .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); + + // Get the `ca_j` variable. + let EffectOp::Assign(eff_val) = eff.operation else { unreachable!() }; + let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); + + // Get the persistence timepoint of the effect `e_j`. + let ta = eff.persistence_start; + (la_lit, ca, ta) + }) + .collect::>() +} From 8833c1296a3f76c1ecd75b09c655cb3ac3b13991 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 12 Sep 2023 09:37:30 +0200 Subject: [PATCH 15/71] refactor(encode): rename eff persistence ends map --- planning/planners/src/encode.rs | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 88362a9b..027aebfb 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -520,7 +520,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result let effs: Vec<_> = effects(pb).collect(); let conds: Vec<_> = conditions(pb).collect(); - let eff_ends: HashMap = effs + let eff_persis_ends: HashMap = effs .iter() .map(|(eff_id, prez, _)| { let var = solver.model.new_optional_fvar( @@ -718,7 +718,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // for each effect, make sure the three time points are ordered for &(eff_id, prez_eff, eff) in &effs { - let persistence_end = eff_ends[&eff_id]; + let persistence_end = eff_persis_ends[&eff_id]; solver.enforce(f_leq(eff.persistence_start, persistence_end), [prez_eff]); solver.enforce(f_leq(eff.transition_start, eff.persistence_start), [prez_eff]); for &min_persistence_end in &eff.min_persistence_end { @@ -776,8 +776,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result clause.push(solver.reify(neq(a, b))); } } - clause.push(solver.reify(f_leq(eff_ends[&j], e1.transition_start))); - clause.push(solver.reify(f_leq(eff_ends[&i], e2.transition_start))); + clause.push(solver.reify(f_leq(eff_persis_ends[&j], e1.transition_start))); + clause.push(solver.reify(f_leq(eff_persis_ends[&i], e2.transition_start))); // add coherence constraint solver.enforce(or(clause.as_slice()), [p1, p2]); @@ -837,7 +837,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // effect's persistence contains condition supported_by_eff_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); - supported_by_eff_conjunction.push(solver.reify(f_leq(cond.end, eff_ends[&eff_id]))); + supported_by_eff_conjunction.push(solver.reify(f_leq(cond.end, eff_persis_ends[&eff_id]))); supported_by_eff_conjunction.push(prez_eff); let support_lit = solver.reify(and(supported_by_eff_conjunction)); @@ -1027,8 +1027,13 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .collect::>(); // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. - let la_ca_ta = - create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, &eff_ends, &mut solver); + let la_ca_ta = create_la_vector_without_timepoints( + compatible_assignments, + &cond, + prez_cond, + &eff_persis_ends, + &mut solver, + ); // Force to have at least one assignment. let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| *la).collect::>(); From 656584ed50947d755e8c400bdfee647a5b98df13 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 12 Sep 2023 09:57:30 +0200 Subject: [PATCH 16/71] feat(encode|resource): new `la` encoding using assign end timepoint --- planning/planners/src/encode.rs | 125 +++++++++++++++++--- planning/planners/src/solver.rs | 2 +- planning/planning/src/chronicles/mod.rs | 1 + planning/planning/src/chronicles/printer.rs | 1 + 4 files changed, 113 insertions(+), 16 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 027aebfb..0e3335ba 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -518,6 +518,9 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result let symmetry_breaking_tpe = SYMMETRY_BREAKING.get(); + // is the state variable numeric? + let is_integer = |sv: &StateVar| matches!(sv.fluent.return_type().into(), Kind::Int); + let effs: Vec<_> = effects(pb).collect(); let conds: Vec<_> = conditions(pb).collect(); let eff_persis_ends: HashMap = effs @@ -533,6 +536,26 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result (*eff_id, var) }) .collect(); + let eff_assign_ends: HashMap = effs + .iter() + .filter_map(|(eff_id, prez, eff)| { + if !solver.model.entails(!*prez) + && matches!(eff.operation, EffectOp::Assign(_)) + && is_integer(&eff.state_var) + { + // Those time points are only present for numeric assignment effects + let var = solver.model.new_optional_fvar( + ORIGIN * TIME_SCALE.get(), + HORIZON * TIME_SCALE.get(), + TIME_SCALE.get(), + *prez, + Container::Instance(eff_id.instance_id) / VarType::EffectEnd, + ); + return Some((*eff_id, var)); + } + None + }) + .collect(); tracing::debug!("#chronicles: {}", pb.chronicles.len()); tracing::debug!("#effects: {}", effs.len()); @@ -715,8 +738,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } tracing::debug!("Chronicles removed by eager propagation: {}", num_removed_chronicles); - // for each effect, make sure the three time points are ordered - + // for each effect, make sure the three (or four for numeric assignments) time points are ordered for &(eff_id, prez_eff, eff) in &effs { let persistence_end = eff_persis_ends[&eff_id]; solver.enforce(f_leq(eff.persistence_start, persistence_end), [prez_eff]); @@ -724,6 +746,10 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result for &min_persistence_end in &eff.min_persistence_end { solver.enforce(f_leq(min_persistence_end, persistence_end), [prez_eff]) } + if eff_assign_ends.contains_key(&eff_id) { + let assignment_end = eff_assign_ends[&eff_id]; + solver.enforce(f_leq(persistence_end, assignment_end), [prez_eff]); + } } solver.propagate()?; @@ -732,8 +758,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result let unifiable_sv = |model: &Model, sv1: &StateVar, sv2: &StateVar| { sv1.fluent == sv2.fluent && model.unifiable_seq(&sv1.args, &sv2.args) }; - // is the state variable numeric? - let is_integer = |sv: &StateVar| matches!(sv.fluent.return_type().into(), Kind::Int); { // coherence constraints @@ -776,8 +800,16 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result clause.push(solver.reify(neq(a, b))); } } - clause.push(solver.reify(f_leq(eff_persis_ends[&j], e1.transition_start))); - clause.push(solver.reify(f_leq(eff_persis_ends[&i], e2.transition_start))); + + // For two numeric assignments, force [transition_start, assignment_end] to not overlaps. + // Otherwise, force [transition_start, persistence_end] to not overlaps. + if eff_assign_ends.contains_key(&i) && eff_assign_ends.contains_key(&j) { + clause.push(solver.reify(f_leq(eff_assign_ends[&j], e1.transition_start))); + clause.push(solver.reify(f_leq(eff_assign_ends[&i], e2.transition_start))); + } else { + clause.push(solver.reify(f_leq(eff_persis_ends[&j], e1.transition_start))); + clause.push(solver.reify(f_leq(eff_persis_ends[&i], e2.transition_start))); + } // add coherence constraint solver.enforce(or(clause.as_slice()), [p1, p2]); @@ -1027,13 +1059,24 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .collect::>(); // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. - let la_ca_ta = create_la_vector_without_timepoints( - compatible_assignments, - &cond, - prez_cond, - &eff_persis_ends, - &mut solver, - ); + let use_assign_end_timepoint = EnvParam::::new("ARIES_RESOURCE_LA_USE_ASSIGN_END_TIMEPOINT", "false"); + let la_ca_ta = if use_assign_end_timepoint.get() { + create_la_vector_with_timepoints( + compatible_assignments, + &cond, + prez_cond, + &eff_assign_ends, + &mut solver, + ) + } else { + create_la_vector_without_timepoints( + compatible_assignments, + &cond, + prez_cond, + &eff_persis_ends, + &mut solver, + ) + }; // Force to have at least one assignment. let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| *la).collect::>(); @@ -1120,6 +1163,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result }) } +/* ======================= Resource `la` Vector Creation ====================== */ + /** Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. @@ -1133,7 +1178,7 @@ fn create_la_vector_without_timepoints( assignments: Vec<&&(EffID, Lit, &Effect)>, cond: &Condition, prez_cond: Lit, - eff_ends: &HashMap, + eff_persis_ends: &HashMap, solver: &mut Solver, ) -> Vec<(Lit, IAtom, FAtom)> { assignments @@ -1171,7 +1216,7 @@ fn create_la_vector_without_timepoints( disjunction.push(solver.reify(neq(a, b))); } // is before the effect `e_j` - disjunction.push(solver.reify(f_lt(eff_ends[other_eff_id], eff.persistence_start))); + disjunction.push(solver.reify(f_lt(eff_persis_ends[other_eff_id], eff.persistence_start))); let disjunction_lit = solver.reify(or(disjunction.clone())); la_conjunction.push(disjunction_lit); @@ -1194,3 +1239,53 @@ fn create_la_vector_without_timepoints( }) .collect::>() } + +/** +Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. + +`la_j` is true if and only if the associated assignment effect `e_j`: + - is present + - has the same state variable as the condition + - the condition is between the start persistence and the assignment end (new timepoint) +**/ +fn create_la_vector_with_timepoints( + assignments: Vec<&&(EffID, Lit, &Effect)>, + cond: &Condition, + prez_cond: Lit, + eff_assign_ends: &HashMap, + solver: &mut Solver, +) -> Vec<(Lit, IAtom, FAtom)> { + assignments + .iter() + .map(|(eff_id, prez_eff, eff)| { + let mut la_conjunction: Vec = Vec::with_capacity(32); + // is present + la_conjunction.push(*prez_eff); + // has the same state variable as the condition + debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + la_conjunction.push(solver.reify(eq(a, b))); + } + // the condition is between the start persistence and the assignment end + la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + la_conjunction.push(solver.reify(f_leq(cond.end, eff_assign_ends[eff_id]))); + + // Create the `la_j` literal. + let la_lit = solver.reify(and(la_conjunction.clone())); + debug_assert!(solver + .model + .state + .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); + + // Get the `ca_j` variable. + let EffectOp::Assign(eff_val) = eff.operation else { unreachable!() }; + let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); + + // Get the persistence timepoint of the effect `e_j`. + let ta = eff.persistence_start; + (la_lit, ca, ta) + }) + .collect::>() +} diff --git a/planning/planners/src/solver.rs b/planning/planners/src/solver.rs index 449d725a..ce281127 100644 --- a/planning/planners/src/solver.rs +++ b/planning/planners/src/solver.rs @@ -219,7 +219,7 @@ impl Heuristic for ActivityNonTemporalFirstHeuristic { Some(VarLabel(_, tpe)) => match tpe { VarType::Presence | VarType::Reification | VarType::Parameter(_) => 0, VarType::ChronicleStart | VarType::ChronicleEnd | VarType::TaskStart(_) | VarType::TaskEnd(_) => 1, - VarType::Horizon | VarType::EffectEnd | VarType::Cost => 2, + VarType::Horizon | VarType::EffectEnd | VarType::AssignEnd | VarType::Cost => 2, }, } } diff --git a/planning/planning/src/chronicles/mod.rs b/planning/planning/src/chronicles/mod.rs index f2a2cd47..d31115c8 100644 --- a/planning/planning/src/chronicles/mod.rs +++ b/planning/planning/src/chronicles/mod.rs @@ -253,6 +253,7 @@ pub enum VarType { ChronicleStart, ChronicleEnd, EffectEnd, + AssignEnd, /// Start time of the i-th task TaskStart(u32), /// End time of the i-th task diff --git a/planning/planning/src/chronicles/printer.rs b/planning/planning/src/chronicles/printer.rs index 0ad88200..42755ec1 100644 --- a/planning/planning/src/chronicles/printer.rs +++ b/planning/planning/src/chronicles/printer.rs @@ -200,6 +200,7 @@ impl<'a> Printer<'a> { VarType::ChronicleStart => print!("start"), VarType::ChronicleEnd => print!("end"), VarType::EffectEnd => print!("eff_end_{v:?}"), + VarType::AssignEnd => print!("eff_assign_end_{v:?}"), VarType::TaskStart(i) => print!("ts({i})"), VarType::TaskEnd(i) => print!("te({i})"), VarType::Parameter(name) => print!("{name}"), From 1a8f0bff408eb3d7e7e34ced540bd4a147bf61f4 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Thu, 14 Sep 2023 11:30:52 +0200 Subject: [PATCH 17/71] docs(sched): update with new encoding --- doc/src/resources.md | 109 +++++++++++++++++++++++++++---------------- 1 file changed, 70 insertions(+), 39 deletions(-) diff --git a/doc/src/resources.md b/doc/src/resources.md index 6692cad4..0aaaf95e 100644 --- a/doc/src/resources.md +++ b/doc/src/resources.md @@ -16,6 +16,7 @@ The right-hand side of the operator could be either a constant or a variable. ### 1.2 Effects The value of a resource can be : + - changed with an **assignment**, the new value could be either a constant or a variable - **increased** by a constant value - **decreased** by a constant value, internally it is an increased operation with a negative constant value @@ -24,55 +25,85 @@ The value of a resource can be : ### 2.1. Effects -Every time a resource value is updated, new conditions are created in order to check that the value can be updated and that the new value is contained in the bounded domain of the resource. +Every time a resource value is updated, new constraints or conditions are created in order to check that the value can be updated and that the new value is contained in the bounded domain of the resource. + +#### 2.1.1 Assign effects + +For an assign effect $[t^a] R^a := z$, we will create the following constraints: -For an **assign effect** $[t^a] R^a := z$, we will create the following conditions: -$$\begin{cases} +$$ +\begin{cases} [t^a] z \ge l \\ [t^a] z \le u \\ -\end{cases}$$ +\end{cases} +$$ -For an **increase effect** $[t^i] R^i \mathrel{+}= c$, we will create the following conditions: -$$\begin{cases} -[t^i] R^i \le u - c \\ -[t^i] R^i \ge l - c \\ -[t^i+\varepsilon] R^i \le u \\ -[t^i+\varepsilon] R^i \ge l \\ -\end{cases}$$ +#### 2.1.2 Increase effects -For a **decrease effect** $[t^d] R^d \mathrel{-}= c$, we convert it into the increase effect $[t^d] R^d \mathrel{+}= (-c)$ and then create the associated conditions. +For an increase effect $[t^i] R^i \mathrel{+}= c$, we will create a new variable $v$ with the same domain as the resource and add a new condition $[t^i]R^i = v$. -Next, these conditions are converted into linear constraints as explained in the next section. +This will ensure that the new value of the resource is in the correct domain after the increase. +Next, this condition is converted into linear constraints as explained in the next section. + +#### 2.1.3 Decrease effects + +For a decrease effect $[t^d] R^d \mathrel{-}= c$, we convert it into the increase effect $[t^d] R^d \mathrel{+}= (-c)$ and then create the associated conditions. ### 2.2. Conditions Every time a resource must be tested, a set of associated linear constraints are created. -For an **equality condition** $[t^c] R^c = z$, we will have the **linear constraints** -$$\begin{cases} -l^a_1c^a_1 + l^i_{11}c^i_1 + \dots + l^i_{1m}c^i_m - z = 0 \\ -\dots \\ -l^a_qc^a_q + l^i_{q1}c^i_1 + \dots + l^i_{qm}c^i_m - z = 0 \\ -\end{cases}$$ - -Where $l^a_jc^a_j$ represents an assignment to the resource and $l^i_{jk}c^i_k$ represents an increase, the $l$ variables are booleans used to know if the associated $c$ variable (which is the value of the assignment or the increase) should be used. The idea is to consider only the constraint corresponding to the latest assignment. - -To do so, we define $\textit{SP}$ which test if the parameters of two resources are the same, $\textit{SPP}$ which test the presence and the parameters, $\textit{LA}$ which test if the assignment is the last one for the current condition: -$$\begin{cases} -\textit{SP}(R^1,R^2) &\Leftrightarrow \bigwedge_{b} (p^1_b=p^2_b) \\ -\textit{SPP}(j, b) &\Leftrightarrow \textit{SP}(R^j,R^b) \land \textit{prez}(j) \land \textit{prez}(b) \\ -\textit{LA}(j) &\Leftrightarrow \bigwedge_{b \ne j} (t^a_b \le t^c \land \textit{SPP}(j,b) \implies t^a_b < t^a_j) \\ -\end{cases}$$ - -Using these intermediate variables, we obtain -$$\begin{cases} -\bigvee_{b} l^a_b \\ -l^a_j \Leftrightarrow t^a_j \le t^c \land \textit{LA}(j) \land \textit{SPP}(j,c) \\ -l^i_{jk} \Leftrightarrow l^a_j \land t^a_j < t^i_k \land t^i_k < t^c \land \textit{SPP}(k,c) \\ -\end{cases}$$ - -For **others conditions**, we convert them into equality conditions. For example, the condition $[t^c] R^c \le z$ is converted into -$$\begin{cases} +#### 2.2.1 Equality conditions + +For an equality condition $[t^c] R^c = z$, we will have the **linear constraints** + +$$ +\begin{cases} +l^a_1c^a_1 + l^i_{11}c^i_1 + \dots + l^i_{1n}c^i_n - l^a_1z = 0 \\ +\vdots \\ +l^a_kc^a_k + l^i_{k1}c^i_1 + \dots + l^i_{kn}c^i_n - l^a_kz = 0 \\ +\end{cases} +$$ + +Where $l^a_jc^a_j$ represents an assignment to the resource and $l^i_{jm}c^i_m$ represents an increase, the $l$ variables are boolean literals used to know if the associated $c$ variable (which is the value of the effect) should be used. +The idea is to consider only the constraint corresponding to the latest assignment. + +To do so, we define $\textit{SP}$ which test if the parameters of two resources are the same by: + +$$\textit{SP}(x,y) \Leftrightarrow \bigwedge_{b} (p^x_b=p^y_b)$$ + +We also define $\textit{LA}$ which test if the assignment effect is the last one before the condition. +**There are two ways to define it**. +The **first** one is to check that the effect is before the condition and for other compatible assignment effects, check that they are not between the considering effect and the condition: + +$$\textit{LA}(j) \Leftrightarrow t^a_j \le t_c \land \bigwedge_{b \ne j} (\neg \textit{prez}_b \lor \neg\textit{SP}(b,c) \lor t^a_b < t^a_j \lor t^a_b > t^c)$$ + +The **second** way to define $\textit{LA}$ is to add a fourth time point to the numeric assignment effects. +Currently, the effects have three time points: the start of the transition, the start of the persistence, and the end of the persistence. +We add a fourth one, the **end of the assignment**, which holds while the current assignment is the last one. +This time point is forced to be after or equals to the end of the persistence. +This way, we just need to check that the condition is between the start of the persistence $t^a_{j,s}$ and the end of the assignment $t^a_{j,e}$: + +$$\textit{LA}(j) \Leftrightarrow t^a_{j,s} \le t_c \land t_c \le t^a_{j,e}$$ + +At the end, the $l^a_j$ literal is true if the effect is present, is the effect before the condition, and has the same resource as the condition: + +$$l^a_j \Leftrightarrow \textit{prez}_j \land \textit{LA}(j) \land \textit{SP}(j,c)$$ + +Moreover, we enforce to have at least one last assignment effect with the disjunction $\bigvee_{j}l^a_j$. + +The $l^i_{jm}$ literal is true if the increase $m$ is present with the same resource as the condition, if the assignment $j$ is the last one and if the increase $m$ is between the assignment $j$ and the condition: + +$$l^i_{jm} \Leftrightarrow \textit{prez}_m \land \textit{SP}(m,c) \land l^a_j \land t^a_j < t^i_m \land t^i_m \le t_c$$ + +#### 2.2.2 Others conditions + +For others conditions, we convert them into equality conditions. +For example, the condition $[t^c] R^c \le z$ is converted into + +$$ +\begin{cases} [t^c] R^c = z' \\ [t^c] z' \le z -\end{cases}$$ \ No newline at end of file +\end{cases} +$$ From 60067e90021719de724c433535640997050d6863 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 9 Oct 2023 12:46:56 +0200 Subject: [PATCH 18/71] fix(encode|resource): `la` creation without timepoints --- planning/planners/src/encode.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 0e3335ba..b08f7e8e 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -1146,7 +1146,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result solver.enforce(sum.leq(0), [prez_cond]); num_resource_constraints += 1; } - println!(); } tracing::debug!(%num_resource_constraints); @@ -1212,7 +1211,7 @@ fn create_la_vector_without_timepoints( debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); for idx in 0..cond.state_var.args.len() { let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; + let b = other_eff.state_var.args[idx]; disjunction.push(solver.reify(neq(a, b))); } // is before the effect `e_j` From b8f097519c84b8e4ccbbeebf63b3495b8c57e837 Mon Sep 17 00:00:00 2001 From: Yirmandias Date: Fri, 13 Oct 2023 15:47:19 +0200 Subject: [PATCH 19/71] increase and decrease support integer variables --- planning/grpc/server/src/chronicles.rs | 6 +-- planning/planners/src/encode.rs | 44 ++++++++++++++------ planning/planning/src/chronicles/concrete.rs | 20 ++++++--- planning/planning/src/chronicles/printer.rs | 9 +++- planning/planning/src/parsing/mod.rs | 2 +- 5 files changed, 57 insertions(+), 24 deletions(-) diff --git a/planning/grpc/server/src/chronicles.rs b/planning/grpc/server/src/chronicles.rs index 1aee3ecb..354eae15 100644 --- a/planning/grpc/server/src/chronicles.rs +++ b/planning/grpc/server/src/chronicles.rs @@ -536,12 +536,12 @@ impl<'a> ChronicleFactory<'a> { let operation = match kind { EffectKind::Assign => EffectOp::Assign(value), EffectKind::Increase => { - let value = IntCst::try_from(value).context("Increase effect require a constant value.")?; + let value = IAtom::try_from(value).context("Increase effect require an integer value.")?; EffectOp::Increase(value) } EffectKind::Decrease => { - let value = IntCst::try_from(value).context("Decrease effect require a constant value.")?; - EffectOp::Increase(-value) + let value = IAtom::try_from(value).context("Decrease effect require an integer value.")?; + EffectOp::Decrease(value) } }; self.chronicle.effects.push(Effect { diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index b08f7e8e..302f5d54 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -785,7 +785,9 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } // skip if it's two increases - if matches!(e1.operation, EffectOp::Increase(_)) && matches!(e2.operation, EffectOp::Increase(_)) { + if matches!(e1.operation, EffectOp::Increase(_) | EffectOp::Decrease(_)) + && matches!(e2.operation, EffectOp::Increase(_) | EffectOp::Decrease(_)) + { continue; } @@ -847,7 +849,9 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result if !unifiable_sv(&solver.model, &cond.state_var, &eff.state_var) { continue; } - let EffectOp::Assign(effect_value) = eff.operation else { unreachable!() }; + let EffectOp::Assign(effect_value) = eff.operation else { + unreachable!() + }; if !solver.model.unifiable(cond.value, effect_value) { continue; } @@ -976,7 +980,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .iter() .filter(|(_, prez, eff)| { !solver.model.entails(!*prez) - && matches!(eff.operation, EffectOp::Increase(_)) + && matches!(eff.operation, EffectOp::Increase(_) | EffectOp::Decrease(_)) && is_integer(&eff.state_var) }) .collect(); @@ -988,8 +992,12 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // Force the new assigned values to be in the state variable domain. for &&(_, prez, eff) in &assignments { - let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { unreachable!() }; - let EffectOp::Assign(val) = eff.operation else { unreachable!() }; + let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { + unreachable!() + }; + let EffectOp::Assign(val) = eff.operation else { + unreachable!() + }; let val: IAtom = val.try_into().expect("Not integer assignment to an int state variable"); solver.enforce(geq(val, lb), [prez]); solver.enforce(leq(val, ub), [prez]); @@ -1122,9 +1130,13 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .implies(prez_cond, solver.model.presence_literal(li_lit.variable()))); // Get the `ci_j*` value. - let EffectOp::Increase(eff_val) = eff.operation else { unreachable!() }; - let ci: IAtom = eff_val.into(); - (li_lit, ci) + let (ci, sign) = match eff.operation { + EffectOp::Increase(eff_val) => (eff_val, 1), + EffectOp::Decrease(eff_val) => (eff_val, -1), + _ => unreachable!(), + }; + // let ci: IAtom = eff_val.into(); + (li_lit, ci, sign) }) .collect::>() }) @@ -1135,8 +1147,12 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // Create the sum. let mut sum = LinearSum::zero(); sum += LinearSum::with_lit(ca, la); - for &(li, ci) in li_ci.iter() { - sum += LinearSum::with_lit(ci, li); + for &(li, ci, sign) in li_ci.iter() { + match sign { + -1 => sum -= LinearSum::with_lit(ci, li), + 1 => sum += LinearSum::with_lit(ci, li), + _ => unreachable!(), + } } let cond_val = IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); @@ -1229,7 +1245,9 @@ fn create_la_vector_without_timepoints( .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { unreachable!() }; + let EffectOp::Assign(eff_val) = eff.operation else { + unreachable!() + }; let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); // Get the persistence timepoint of the effect `e_j`. @@ -1279,7 +1297,9 @@ fn create_la_vector_with_timepoints( .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { unreachable!() }; + let EffectOp::Assign(eff_val) = eff.operation else { + unreachable!() + }; let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); // Get the persistence timepoint of the effect `e_j`. diff --git a/planning/planning/src/chronicles/concrete.rs b/planning/planning/src/chronicles/concrete.rs index d41bbd17..c49c55b0 100644 --- a/planning/planning/src/chronicles/concrete.rs +++ b/planning/planning/src/chronicles/concrete.rs @@ -293,7 +293,8 @@ pub struct Effect { #[derive(Clone, Copy, Eq, PartialEq)] pub enum EffectOp { Assign(Atom), - Increase(IntCst), + Increase(IAtom), + Decrease(IAtom), } impl EffectOp { pub const TRUE_ASSIGNMENT: EffectOp = EffectOp::Assign(Atom::TRUE); @@ -305,11 +306,11 @@ impl Debug for EffectOp { EffectOp::Assign(val) => { write!(f, ":= {val:?}") } - EffectOp::Increase(val) if *val >= 0 => { - write!(f, "+= {val:?}") - } EffectOp::Increase(val) => { - write!(f, "-= {}", -val) + write!(f, "+= {:?}", val) + } + EffectOp::Decrease(val) => { + write!(f, "-= {:?}", val) } } } @@ -352,9 +353,15 @@ impl Substitute for EffectOp { match self { EffectOp::Assign(val) => EffectOp::Assign(substitution.sub(*val)), EffectOp::Increase(val) => { - let x: IntCst = *val; // guard: this will need substitution when val becomes a variable + let x = substitution.sub(Atom::from(*val)).try_into().unwrap(); + //let x: IntCst = *val; // guard: this will need substitution when val becomes a variable EffectOp::Increase(x) } + EffectOp::Decrease(val) => { + let x = substitution.sub(Atom::from(*val)).try_into().unwrap(); + //let x: IntCst = *val; // guard: this will need substitution when val becomes a variable + EffectOp::Decrease(x) + } } } } @@ -552,6 +559,7 @@ impl Chronicle { match eff.operation { EffectOp::Assign(x) => vars.add_atom(x), EffectOp::Increase(x) => vars.add_atom(x), + EffectOp::Decrease(x) => vars.add_atom(x), } vars.add_sv(&eff.state_var) } diff --git a/planning/planning/src/chronicles/printer.rs b/planning/planning/src/chronicles/printer.rs index 42755ec1..cfdecf51 100644 --- a/planning/planning/src/chronicles/printer.rs +++ b/planning/planning/src/chronicles/printer.rs @@ -142,10 +142,15 @@ impl<'a> Printer<'a> { match op { EffectOp::Assign(value) => { print!(" := "); - self.atom(*value) + self.atom(*value); } EffectOp::Increase(i) => { - print!(" += {i}") + print!(" += "); + self.atom((*i).into()); + } + EffectOp::Decrease(i) => { + print!(" -= "); + self.atom((*i).into()); } } } diff --git a/planning/planning/src/parsing/mod.rs b/planning/planning/src/parsing/mod.rs index 997b7e60..402b51b8 100644 --- a/planning/planning/src/parsing/mod.rs +++ b/planning/planning/src/parsing/mod.rs @@ -250,7 +250,7 @@ fn read_init( if closed_world { // closed world, every predicate that is not given a true value should be given a false value // to do this, we rely on the classical classical planning state - let state_desc = World::new(context.model.get_symbol_table().deref().clone(), &context.fluents)?; + let state_desc = World::new(context.model.get_symbol_table().clone(), &context.fluents)?; let mut s = state_desc.make_new_state(); for init in initial_facts { let pred = read_sv(init, &state_desc)?; From a31c2d49308e344dbb55e88f8ef5a130df672562 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 16 Oct 2023 11:00:11 +0200 Subject: [PATCH 20/71] feat(resource): support linear sum values --- planning/grpc/server/src/chronicles.rs | 4 +- planning/planners/src/encode.rs | 23 +++-------- planning/planning/src/chronicles/concrete.rs | 43 ++++++++++---------- planning/planning/src/chronicles/printer.rs | 8 +--- 4 files changed, 32 insertions(+), 46 deletions(-) diff --git a/planning/grpc/server/src/chronicles.rs b/planning/grpc/server/src/chronicles.rs index 354eae15..a945c57d 100644 --- a/planning/grpc/server/src/chronicles.rs +++ b/planning/grpc/server/src/chronicles.rs @@ -537,11 +537,11 @@ impl<'a> ChronicleFactory<'a> { EffectKind::Assign => EffectOp::Assign(value), EffectKind::Increase => { let value = IAtom::try_from(value).context("Increase effect require an integer value.")?; - EffectOp::Increase(value) + EffectOp::Increase(LinearSum::from(value)) } EffectKind::Decrease => { let value = IAtom::try_from(value).context("Decrease effect require an integer value.")?; - EffectOp::Decrease(value) + EffectOp::Increase(-LinearSum::from(value)) } }; self.chronicle.effects.push(Effect { diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 302f5d54..f409cd54 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -785,9 +785,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } // skip if it's two increases - if matches!(e1.operation, EffectOp::Increase(_) | EffectOp::Decrease(_)) - && matches!(e2.operation, EffectOp::Increase(_) | EffectOp::Decrease(_)) - { + if matches!(e1.operation, EffectOp::Increase(_)) && matches!(e2.operation, EffectOp::Increase(_)) { continue; } @@ -980,7 +978,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .iter() .filter(|(_, prez, eff)| { !solver.model.entails(!*prez) - && matches!(eff.operation, EffectOp::Increase(_) | EffectOp::Decrease(_)) + && matches!(eff.operation, EffectOp::Increase(_)) && is_integer(&eff.state_var) }) .collect(); @@ -1130,13 +1128,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .implies(prez_cond, solver.model.presence_literal(li_lit.variable()))); // Get the `ci_j*` value. - let (ci, sign) = match eff.operation { - EffectOp::Increase(eff_val) => (eff_val, 1), - EffectOp::Decrease(eff_val) => (eff_val, -1), - _ => unreachable!(), - }; - // let ci: IAtom = eff_val.into(); - (li_lit, ci, sign) + let EffectOp::Increase(eff_val) = eff.operation.clone() else { unreachable!() }; + (li_lit, eff_val) }) .collect::>() }) @@ -1147,12 +1140,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // Create the sum. let mut sum = LinearSum::zero(); sum += LinearSum::with_lit(ca, la); - for &(li, ci, sign) in li_ci.iter() { - match sign { - -1 => sum -= LinearSum::with_lit(ci, li), - 1 => sum += LinearSum::with_lit(ci, li), - _ => unreachable!(), - } + for (li, ci) in li_ci.iter() { + sum += LinearSum::with_lit(ci.clone(), *li) } let cond_val = IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); diff --git a/planning/planning/src/chronicles/concrete.rs b/planning/planning/src/chronicles/concrete.rs index c49c55b0..f71e19bd 100644 --- a/planning/planning/src/chronicles/concrete.rs +++ b/planning/planning/src/chronicles/concrete.rs @@ -290,11 +290,10 @@ pub struct Effect { pub operation: EffectOp, } -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Eq, PartialEq)] pub enum EffectOp { Assign(Atom), - Increase(IAtom), - Decrease(IAtom), + Increase(LinearSum), } impl EffectOp { pub const TRUE_ASSIGNMENT: EffectOp = EffectOp::Assign(Atom::TRUE); @@ -307,10 +306,7 @@ impl Debug for EffectOp { write!(f, ":= {val:?}") } EffectOp::Increase(val) => { - write!(f, "+= {:?}", val) - } - EffectOp::Decrease(val) => { - write!(f, "-= {:?}", val) + write!(f, "+= {:?}", val.simplify()) } } } @@ -352,16 +348,7 @@ impl Substitute for EffectOp { fn substitute(&self, substitution: &impl Substitution) -> Self { match self { EffectOp::Assign(val) => EffectOp::Assign(substitution.sub(*val)), - EffectOp::Increase(val) => { - let x = substitution.sub(Atom::from(*val)).try_into().unwrap(); - //let x: IntCst = *val; // guard: this will need substitution when val becomes a variable - EffectOp::Increase(x) - } - EffectOp::Decrease(val) => { - let x = substitution.sub(Atom::from(*val)).try_into().unwrap(); - //let x: IntCst = *val; // guard: this will need substitution when val becomes a variable - EffectOp::Decrease(x) - } + EffectOp::Increase(val) => EffectOp::Increase(substitution.sub_linear_sum(val)), } } } @@ -534,6 +521,21 @@ impl VarSet { self.add_atom(*a) } } + + fn add_linear_term(&mut self, term: &LinearTerm) { + self.add_atom(term.var()); + self.add_atom(term.factor()); + self.add_atom(term.denom()); + self.add_lit(term.lit()); + } + + fn add_linear_sum(&mut self, sum: &LinearSum) { + self.add_atom(sum.constant()); + self.add_atom(sum.denom()); + for term in sum.terms() { + self.add_linear_term(term); + } + } } impl Chronicle { @@ -556,10 +558,9 @@ impl Chronicle { for eff in &self.effects { vars.add_atom(eff.transition_start); vars.add_atom(eff.persistence_start); - match eff.operation { - EffectOp::Assign(x) => vars.add_atom(x), - EffectOp::Increase(x) => vars.add_atom(x), - EffectOp::Decrease(x) => vars.add_atom(x), + match &eff.operation { + EffectOp::Assign(x) => vars.add_atom(*x), + EffectOp::Increase(x) => vars.add_linear_sum(x), } vars.add_sv(&eff.state_var) } diff --git a/planning/planning/src/chronicles/printer.rs b/planning/planning/src/chronicles/printer.rs index cfdecf51..e195ccb1 100644 --- a/planning/planning/src/chronicles/printer.rs +++ b/planning/planning/src/chronicles/printer.rs @@ -144,13 +144,9 @@ impl<'a> Printer<'a> { print!(" := "); self.atom(*value); } - EffectOp::Increase(i) => { + EffectOp::Increase(sum) => { print!(" += "); - self.atom((*i).into()); - } - EffectOp::Decrease(i) => { - print!(" -= "); - self.atom((*i).into()); + self.linear_sum(sum); } } } From cbc1cfcb330328e37b4a88939f366ccaaeba3dde Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 16 Oct 2023 11:12:14 +0200 Subject: [PATCH 21/71] fix: cargo clippy warning --- planning/planning/src/parsing/mod.rs | 1 - solver/src/collections/heap.rs | 6 +++--- solver/src/reasoners/cp/mod.rs | 10 +++++----- solver/src/reasoners/stn/theory.rs | 1 + validator/src/interfaces/unified_planning/factories.rs | 2 +- validator/src/interfaces/unified_planning/mod.rs | 8 ++++---- validator/src/interfaces/unified_planning/utils.rs | 2 +- validator/src/models/action.rs | 4 ++-- validator/src/models/method.rs | 2 +- validator/src/models/time.rs | 2 +- validator/src/procedures.rs | 4 ++-- validator/src/utils.rs | 2 +- 12 files changed, 22 insertions(+), 22 deletions(-) diff --git a/planning/planning/src/parsing/mod.rs b/planning/planning/src/parsing/mod.rs index 402b51b8..f3a60ffe 100644 --- a/planning/planning/src/parsing/mod.rs +++ b/planning/planning/src/parsing/mod.rs @@ -18,7 +18,6 @@ use aries::utils::input::{ErrLoc, Loc, Sym}; use itertools::Itertools; use std::collections::{HashMap, HashSet}; use std::convert::TryFrom; -use std::ops::Deref; use std::str::FromStr; use std::sync::Arc; diff --git a/solver/src/collections/heap.rs b/solver/src/collections/heap.rs index b408d11d..04121f98 100644 --- a/solver/src/collections/heap.rs +++ b/solver/src/collections/heap.rs @@ -398,13 +398,13 @@ mod test { } let check_all_priorities = |heap: &IdxHeap| { - for i in 0..N { + for (i, &priority) in priorities.iter().enumerate().take(N) { assert!( - eq(heap.priority(i), priorities[i]), + eq(heap.priority(i), priority), "Elt: {}, found: {}, expected: {}", i, heap.priority(i), - priorities[i] + priority ); } }; diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 554c8712..bdfc7067 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -572,14 +572,14 @@ mod tests { while dom.last_event().is_some() { dom.undo_last_event(); } - check_bounds_var(v, &dom, -100, 100); - check_bounds(&s, x, &dom, -200, 200); - check_bounds(&s, y, &dom, -100, 100); - check_bounds(&s, c, &dom, 25, 25); + check_bounds_var(v, dom, -100, 100); + check_bounds(&s, x, dom, -200, 200); + check_bounds(&s, y, dom, -100, 100); + check_bounds(&s, c, dom, 25, 25); // Set the new value dom.set_lb(v, val, Cause::Decision); dom.set_ub(v, val, Cause::Decision); - check_bounds_var(v, &dom, val, val); + check_bounds_var(v, dom, val, val); }; // Check bounds diff --git a/solver/src/reasoners/stn/theory.rs b/solver/src/reasoners/stn/theory.rs index 2c8ee684..51f00f36 100644 --- a/solver/src/reasoners/stn/theory.rs +++ b/solver/src/reasoners/stn/theory.rs @@ -1200,6 +1200,7 @@ impl Backtrack for StnTheory { } } +#[allow(clippy::let_unit_value)] #[cfg(test)] mod tests { use crate::model::extensions::AssignmentExt; diff --git a/validator/src/interfaces/unified_planning/factories.rs b/validator/src/interfaces/unified_planning/factories.rs index f4f02ec7..d8e837e4 100644 --- a/validator/src/interfaces/unified_planning/factories.rs +++ b/validator/src/interfaces/unified_planning/factories.rs @@ -250,7 +250,7 @@ pub mod expression { } pub fn fluent_symbol_with_type(s: &str, t: &str) -> Expression { - atom(super::content::symbol(s), t.into(), ExpressionKind::FluentSymbol) + atom(super::content::symbol(s), t, ExpressionKind::FluentSymbol) } pub fn function_symbol(s: &str) -> Expression { diff --git a/validator/src/interfaces/unified_planning/mod.rs b/validator/src/interfaces/unified_planning/mod.rs index b14dd4be..0e3ba303 100644 --- a/validator/src/interfaces/unified_planning/mod.rs +++ b/validator/src/interfaces/unified_planning/mod.rs @@ -815,9 +815,9 @@ mod tests { let mut p = problem::mock_nontemporal(); let pl = plan::mock_nontemporal(); let mut e = Env::::default(); - assert_eq!(e.verbose, false); - assert_eq!(e.discrete_time, false); - assert_eq!(e.schedule_problem, false); + assert!(!e.verbose); + assert!(!e.discrete_time); + assert!(!e.schedule_problem); // Types e.bound_type("locatable".into(), "".into()); @@ -866,7 +866,7 @@ mod tests { // Schedule problem let p = problem::mock_schedule(); let pl = plan::mock_schedule(); - assert_eq!(build_env(&p, &pl, false)?.schedule_problem, true); + assert!(build_env(&p, &pl, false)?.schedule_problem); Ok(()) } diff --git a/validator/src/interfaces/unified_planning/utils.rs b/validator/src/interfaces/unified_planning/utils.rs index ee5d8157..be8e2567 100644 --- a/validator/src/interfaces/unified_planning/utils.rs +++ b/validator/src/interfaces/unified_planning/utils.rs @@ -95,7 +95,7 @@ mod tests { #[test] fn test_content() -> Result<()> { let c = Content::Symbol("o".into()); - let e1 = expression::atom(c.clone(), "t".into(), ExpressionKind::Constant.into()); + let e1 = expression::atom(c.clone(), "t", ExpressionKind::Constant); let mut e2 = e1.clone(); e2.atom.as_mut().unwrap().content = None; let mut e3 = e1.clone(); diff --git a/validator/src/models/action.rs b/validator/src/models/action.rs index 0a156882..e97568f9 100644 --- a/validator/src/models/action.rs +++ b/validator/src/models/action.rs @@ -469,7 +469,7 @@ mod tests { ei2.clone(), ]; - for condition in vec![true, false] { + for &condition in &[true, false] { for e1 in effects.iter() { for e2 in effects.iter() { let conditions = [condition]; @@ -498,7 +498,7 @@ mod tests { let efb = e(&[false], "b", 2); let effects = vec![eta.clone(), etb.clone(), efa.clone(), efb.clone()]; - for condition in vec![true, false] { + for &condition in &[true, false] { for e1 in effects.iter() { for e2 in effects.iter() { let conditions = [condition]; diff --git a/validator/src/models/method.rs b/validator/src/models/method.rs index 85f92481..55693e60 100644 --- a/validator/src/models/method.rs +++ b/validator/src/models/method.rs @@ -209,7 +209,7 @@ mod tests { Method::new(n.into(), n.into(), vec![], vec![], vec![], st) } fn st_m(n: &str, st: HashMap>) -> Subtask { - let tn = n.replace("m", "t"); + let tn = n.replace('m', "t"); Subtask::Task(Task::new(tn.clone(), tn, vec![], Refiner::Method(m(n, st)))) } fn t(i: i32) -> Timepoint { diff --git a/validator/src/models/time.rs b/validator/src/models/time.rs index d7c75fd6..186e0c82 100644 --- a/validator/src/models/time.rs +++ b/validator/src/models/time.rs @@ -331,7 +331,7 @@ mod tests { let expect = expected[i * kinds.len() + j]; assert_eq!( Timepoint::new(kind, delay.into()) - .eval::>(Some(&a.clone().into()), &env), + .eval::>(Some(&a.clone()), &env), Rational::from(expect) ); } diff --git a/validator/src/procedures.rs b/validator/src/procedures.rs index 218ec4ec..25158e82 100644 --- a/validator/src/procedures.rs +++ b/validator/src/procedures.rs @@ -738,7 +738,7 @@ mod tests { MockExpression(true.into()), MockExpression(15.into()), ]; - for f in fails.into_iter() { + for f in fails.iter() { test_err!(end, env, f); } @@ -775,7 +775,7 @@ mod tests { MockExpression(true.into()), MockExpression(15.into()), ]; - for f in fails.into_iter() { + for f in fails.iter() { test_err!(start, env, f); } diff --git a/validator/src/utils.rs b/validator/src/utils.rs index 261b0c04..6f9eeff7 100644 --- a/validator/src/utils.rs +++ b/validator/src/utils.rs @@ -23,7 +23,7 @@ mod tests { #[test] fn test_extract_bounds() { for name in ["integer", "real", "foo", "bar"] { - let empty_res = extract_bounds(format!("{name}").as_str()); + let empty_res = extract_bounds(name.to_string().as_str()); assert!(empty_res.is_ok(), "{}", name); assert!(empty_res.unwrap().is_none(), "{}", name); From 58c953c785552383da8fe9477bf4db55e7edf78a Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 16 Oct 2023 11:50:42 +0200 Subject: [PATCH 22/71] refactor(encode): rename env var for timepoints --- planning/planners/src/encode.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index f409cd54..9ce1d3bc 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -19,6 +19,12 @@ use std::collections::{HashMap, HashSet}; use std::convert::TryFrom; use std::ptr; +/// Parameter that activates the usage of timepoints to encode the increase's literals. +/// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS`. +/// Possible values are `false` and `true` (default). +pub static RESOURCE_CONSTRAINT_TIMEPOINTS: EnvParam = + EnvParam::new("ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS", "true"); + /// Parameter that defines the symmetry breaking strategy to use. /// The value of this parameter is loaded from the environment variable `ARIES_LCP_SYMMETRY_BREAKING`. /// Possible values are `none` and `simple` (default). @@ -1065,8 +1071,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result .collect::>(); // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. - let use_assign_end_timepoint = EnvParam::::new("ARIES_RESOURCE_LA_USE_ASSIGN_END_TIMEPOINT", "false"); - let la_ca_ta = if use_assign_end_timepoint.get() { + let la_ca_ta = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { create_la_vector_with_timepoints( compatible_assignments, &cond, From 0575d7dab1b3e4919f25d7c19c72d271fd6ad971 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 16 Oct 2023 12:26:32 +0200 Subject: [PATCH 23/71] refactor(encode): move resources in separate func --- planning/planners/src/encode.rs | 408 ++++++++++++++++---------------- 1 file changed, 207 insertions(+), 201 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 9ce1d3bc..0bb3f090 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -510,6 +510,16 @@ pub struct EncodedProblem { pub encoding: Encoding, } +/// Returns whether the state variable is numeric. +fn is_integer(sv: &StateVar) -> bool { + matches!(sv.fluent.return_type().into(), Kind::Int) +} + +/// Returns whether two state variables are unifiable. +fn unifiable_sv(model: &Model, sv1: &StateVar, sv2: &StateVar) -> bool { + sv1.fluent == sv2.fluent && model.unifiable_seq(&sv1.args, &sv2.args) +} + /// Encodes a finite problem. /// If a metric is given, it will return along with the model an `IAtom` that should be minimized /// Returns an error if the encoded problem is found to be unsatisfiable. @@ -524,9 +534,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result let symmetry_breaking_tpe = SYMMETRY_BREAKING.get(); - // is the state variable numeric? - let is_integer = |sv: &StateVar| matches!(sv.fluent.return_type().into(), Kind::Int); - let effs: Vec<_> = effects(pb).collect(); let conds: Vec<_> = conditions(pb).collect(); let eff_persis_ends: HashMap = effs @@ -760,11 +767,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result solver.propagate()?; - // are two state variables unifiable? - let unifiable_sv = |model: &Model, sv1: &StateVar, sv2: &StateVar| { - sv1.fluent == sv2.fluent && model.unifiable_seq(&sv1.args, &sv2.args) - }; - { // coherence constraints let span = tracing::span!(tracing::Level::TRACE, "coherence"); @@ -966,214 +968,218 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result { // Resource constraints - let span = tracing::span!(tracing::Level::TRACE, "resources"); - let _span = span.enter(); - let mut num_resource_constraints = 0; + encode_resource_constraints(&mut solver, &effs, &conds, &eff_assign_ends, &eff_persis_ends); + solver.propagate()?; + } + + let metric = metric.map(|metric| add_metric(pb, &mut solver.model, metric)); + + tracing::debug!("Done."); + Ok(EncodedProblem { + model: solver.model, + objective: metric, + encoding, + }) +} - // Get the effects and the conditions on numeric state variables. - // Filter those who are not present. - let assignments: Vec<_> = effs +/* ========================================================================== */ +/* Resource Constraints */ +/* ========================================================================== */ + +fn encode_resource_constraints( + solver: &mut Box>, + effs: &[(EffID, Lit, &Effect)], + conds: &[(CondID, Lit, &Condition)], + eff_assign_ends: &HashMap, + eff_persis_ends: &HashMap, +) { + /* ============================= Variables setup ============================ */ + + let span = tracing::span!(tracing::Level::TRACE, "resources"); + let _span = span.enter(); + let mut num_resource_constraints = 0; + + // Get the effects and the conditions on numeric state variables. + // Filter those who are not present. + let assignments: Vec<_> = effs + .iter() + .filter(|(_, prez, eff)| { + !solver.model.entails(!*prez) && matches!(eff.operation, EffectOp::Assign(_)) && is_integer(&eff.state_var) + }) + .collect(); + let increases: Vec<_> = effs + .iter() + .filter(|(_, prez, eff)| { + !solver.model.entails(!*prez) + && matches!(eff.operation, EffectOp::Increase(_)) + && is_integer(&eff.state_var) + }) + .collect(); + let mut conditions: Vec<_> = conds + .iter() + .filter(|(_, prez, cond)| !solver.model.entails(!*prez) && is_integer(&cond.state_var)) + .map(|&(_, prez, cond)| (prez, cond.clone())) + .collect(); + + /* =============================== Assignments ============================== */ + + // Force the new assigned values to be in the state variable domain. + for &&(_, prez, eff) in &assignments { + let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { + unreachable!() + }; + let EffectOp::Assign(val) = eff.operation else { + unreachable!() + }; + let val: IAtom = val.try_into().expect("Not integer assignment to an int state variable"); + solver.enforce(geq(val, lb), [prez]); + solver.enforce(leq(val, ub), [prez]); + num_resource_constraints += 1; + } + + /* ================================ Increases =============================== */ + + // Convert the increase effects into conditions in order to check that the new value is in the state variable domain. + for &&(eff_id, prez, eff) in &increases { + assert!( + eff.transition_start + FAtom::EPSILON == eff.persistence_start && eff.min_persistence_end.is_empty(), + "Only instantaneous effects are supported" + ); + // Get the bounds of the state variable. + let (lb, ub) = if let Type::Int { lb, ub } = eff.state_var.fluent.return_type() { + (lb, ub) + } else { + (INT_CST_MIN, INT_CST_MAX) + }; + // Create a new variable with those bounds. + let var = solver + .model + .new_ivar(lb, ub, Container::Instance(eff_id.instance_id) / VarType::Reification); + // Check that the state variable value is equals to that new variable. + // It will force the state variable value to be in the bounds of the new variable. + conditions.push(( + prez, + Condition { + start: eff.persistence_start, + end: eff.persistence_start, + state_var: eff.state_var.clone(), + value: var.into(), + }, + )); + } + + /* =============================== Conditions =============================== */ + + /* + * For each condition `R == z`, a set of linear sum constraints of the form + * `la_j*ca_j + li_jk*ci_jk + ... + li_jm*ci_jm - la_j*z == 0` are created. + * + * The `la_j` literal is true if and only if the associated assignment effect `e_j` is the last one for the condition. + * A disjunctive clause will force to have at least one `la_j`. + * The `ca_j` value is the value of the assignment effect `e_j`. + * The `li_j*` literals are true if and only if: + * - `la_j` is true + * - the associated increase effect `e_*` is between `e_j` and the condition + * The `ci_j*` values are the value of the increase effects `e_*`. + * The `z` variable is the value of the condition. + * + * With all these literals, only one constraint will be taken into account: that associated with the last assignment. + */ + for (prez_cond, cond) in conditions { + assert_eq!(cond.start, cond.end, "Only the instantaneous conditions are supported"); + + // Whether the effect is likely to support the condition. + let eff_compatible_with_cond = |solver: &Solver, prez_eff: Lit, eff: &Effect| { + !solver.model.state.exclusive(prez_eff, prez_cond) + && unifiable_sv(&solver.model, &cond.state_var, &eff.state_var) + }; + + let compatible_assignments = assignments .iter() - .filter(|(_, prez, eff)| { - !solver.model.entails(!*prez) - && matches!(eff.operation, EffectOp::Assign(_)) - && is_integer(&eff.state_var) - }) - .collect(); - let increases: Vec<_> = effs + .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) + .collect::>(); + let compatible_increases = increases .iter() - .filter(|(_, prez, eff)| { - !solver.model.entails(!*prez) - && matches!(eff.operation, EffectOp::Increase(_)) - && is_integer(&eff.state_var) - }) - .collect(); - let mut conditions: Vec<_> = conds - .iter() - .filter(|(_, prez, cond)| !solver.model.entails(!*prez) && is_integer(&cond.state_var)) - .map(|&(_, prez, cond)| (prez, cond.clone())) - .collect(); + .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) + .collect::>(); - // Force the new assigned values to be in the state variable domain. - for &&(_, prez, eff) in &assignments { - let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { - unreachable!() - }; - let EffectOp::Assign(val) = eff.operation else { - unreachable!() - }; - let val: IAtom = val.try_into().expect("Not integer assignment to an int state variable"); - solver.enforce(geq(val, lb), [prez]); - solver.enforce(leq(val, ub), [prez]); - num_resource_constraints += 1; - } + // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. + let la_ca_ta = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { + create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_assign_ends, solver) + } else { + create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, eff_persis_ends, solver) + }; - // Convert the increase effects into conditions in order to check that the new value is in the state variable domain. - for &&(eff_id, prez, eff) in &increases { - assert!( - eff.transition_start + FAtom::EPSILON == eff.persistence_start && eff.min_persistence_end.is_empty(), - "Only instantaneous effects are supported" - ); - // Get the bounds of the state variable. - let (lb, ub) = if let Type::Int { lb, ub } = eff.state_var.fluent.return_type() { - (lb, ub) - } else { - (INT_CST_MIN, INT_CST_MAX) - }; - // Create a new variable with those bounds. - let var = solver - .model - .new_ivar(lb, ub, Container::Instance(eff_id.instance_id) / VarType::Reification); - // Check that the state variable value is equals to that new variable. - // It will force the state variable value to be in the bounds of the new variable. - conditions.push(( - prez, - Condition { - start: eff.persistence_start, - end: eff.persistence_start, - state_var: eff.state_var.clone(), - value: var.into(), - }, - )); - } + // Force to have at least one assignment. + let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| *la).collect::>(); + solver.enforce(or(la_disjuncts), [prez_cond]); /* - * For each condition `R == z`, a set of linear sum constraints of the form - * `la_j*ca_j + li_jk*ci_jk + ... + li_jm*ci_jm - la_j*z == 0` are created. + * Matrix to store the `li_j*` literals and `ci_j*` values. * - * The `la_j` literal is true if and only if the associated assignment effect `e_j` is the last one for the condition. - * A disjunctive clause will force to have at least one `la_j`. - * The `ca_j` value is the value of the assignment effect `e_j`. - * The `li_j*` literals are true if and only if: + * `li_j*` is true if and only if the associated increase effect `e_*`: + * - is present + * - is before the condition + * - is after the assignment effect `e_j` + * - has the same state variable as the condition * - `la_j` is true - * - the associated increase effect `e_*` is between `e_j` and the condition - * The `ci_j*` values are the value of the increase effects `e_*`. - * The `z` variable is the value of the condition. - * - * With all these literals, only one constraint will be taken into account: that associated with the last assignment. */ - for (prez_cond, cond) in conditions { - assert_eq!(cond.start, cond.end, "Only the instantaneous conditions are supported"); - - // Whether the effect is likely to support the condition. - let eff_compatible_with_cond = |solver: &Solver, prez_eff: Lit, eff: &Effect| { - !solver.model.state.exclusive(prez_eff, prez_cond) - && unifiable_sv(&solver.model, &cond.state_var, &eff.state_var) - }; - - let compatible_assignments = assignments - .iter() - .filter(|(_, prez, eff)| eff_compatible_with_cond(&solver, *prez, eff)) - .collect::>(); - let compatible_increases = increases - .iter() - .filter(|(_, prez, eff)| eff_compatible_with_cond(&solver, *prez, eff)) - .collect::>(); - - // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. - let la_ca_ta = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { - create_la_vector_with_timepoints( - compatible_assignments, - &cond, - prez_cond, - &eff_assign_ends, - &mut solver, - ) - } else { - create_la_vector_without_timepoints( - compatible_assignments, - &cond, - prez_cond, - &eff_persis_ends, - &mut solver, - ) - }; - - // Force to have at least one assignment. - let la_disjuncts = la_ca_ta.iter().map(|(la, _, _)| *la).collect::>(); - solver.enforce(or(la_disjuncts), [prez_cond]); - - /* - * Matrix to store the `li_j*` literals and `ci_j*` values. - * - * `li_j*` is true if and only if the associated increase effect `e_*`: - * - is present - * - is before the condition - * - is after the assignment effect `e_j` - * - has the same state variable as the condition - * - `la_j` is true - */ - let m_li_ci = la_ca_ta - .iter() - .map(|(la, _, ta)| { - compatible_increases - .iter() - .map(|(_, prez_eff, eff)| { - let mut li_conjunction: Vec = Vec::with_capacity(12); - // `la_j` is true - li_conjunction.push(*la); - // is present - li_conjunction.push(*prez_eff); - // is before the condition - li_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); - // is after the assignment effect `e_j` - li_conjunction.push(solver.reify(f_lt(*ta, eff.persistence_start))); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - li_conjunction.push(solver.reify(eq(a, b))); - } - // Create the `li_j*` literal. - let li_lit = solver.reify(and(li_conjunction)); - debug_assert!(solver - .model - .state - .implies(prez_cond, solver.model.presence_literal(li_lit.variable()))); - - // Get the `ci_j*` value. - let EffectOp::Increase(eff_val) = eff.operation.clone() else { unreachable!() }; - (li_lit, eff_val) - }) - .collect::>() - }) - .collect::>(); - - // Create the linear sum constraints. - for (&(la, ca, _), li_ci) in la_ca_ta.iter().zip(m_li_ci) { - // Create the sum. - let mut sum = LinearSum::zero(); - sum += LinearSum::with_lit(ca, la); - for (li, ci) in li_ci.iter() { - sum += LinearSum::with_lit(ci.clone(), *li) - } - let cond_val = - IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); - sum -= LinearSum::with_lit(cond_val, la); - // Force the sum to be equals to 0. - solver.enforce(sum.clone().geq(0), [prez_cond]); - solver.enforce(sum.leq(0), [prez_cond]); - num_resource_constraints += 1; + let m_li_ci = la_ca_ta + .iter() + .map(|(la, _, ta)| { + compatible_increases + .iter() + .map(|(_, prez_eff, eff)| { + let mut li_conjunction: Vec = Vec::with_capacity(12); + // `la_j` is true + li_conjunction.push(*la); + // is present + li_conjunction.push(*prez_eff); + // is before the condition + li_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + // is after the assignment effect `e_j` + li_conjunction.push(solver.reify(f_lt(*ta, eff.persistence_start))); + // has the same state variable as the condition + debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); + for idx in 0..cond.state_var.args.len() { + let a = cond.state_var.args[idx]; + let b = eff.state_var.args[idx]; + li_conjunction.push(solver.reify(eq(a, b))); + } + // Create the `li_j*` literal. + let li_lit = solver.reify(and(li_conjunction)); + debug_assert!(solver + .model + .state + .implies(prez_cond, solver.model.presence_literal(li_lit.variable()))); + + // Get the `ci_j*` value. + let EffectOp::Increase(eff_val) = eff.operation.clone() else { unreachable!() }; + (li_lit, eff_val) + }) + .collect::>() + }) + .collect::>(); + + // Create the linear sum constraints. + for (&(la, ca, _), li_ci) in la_ca_ta.iter().zip(m_li_ci) { + // Create the sum. + let mut sum = LinearSum::zero(); + sum += LinearSum::with_lit(ca, la); + for (li, ci) in li_ci.iter() { + sum += LinearSum::with_lit(ci.clone(), *li) } + let cond_val = IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); + sum -= LinearSum::with_lit(cond_val, la); + // Force the sum to be equals to 0. + solver.enforce(sum.clone().geq(0), [prez_cond]); + solver.enforce(sum.leq(0), [prez_cond]); + num_resource_constraints += 1; } - tracing::debug!(%num_resource_constraints); - - solver.propagate()?; } - - let metric = metric.map(|metric| add_metric(pb, &mut solver.model, metric)); - - tracing::debug!("Done."); - Ok(EncodedProblem { - model: solver.model, - objective: metric, - encoding, - }) + tracing::debug!(%num_resource_constraints); } -/* ======================= Resource `la` Vector Creation ====================== */ - /** Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. From 5f9e808daae2edbed0e1b180114c9feb5e06b112 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 16 Oct 2023 13:18:32 +0200 Subject: [PATCH 24/71] ci(up): can specify problem prefix --- ci/up_integration.py | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100755 ci/up_integration.py diff --git a/ci/up_integration.py b/ci/up_integration.py new file mode 100755 index 00000000..44aad3f4 --- /dev/null +++ b/ci/up_integration.py @@ -0,0 +1,23 @@ +#!/usr/bin/python3 + +# Script that run the UP integration tests. + +import report # from planning-test-case, should probably change once the upstream repository stabilizes +from unified_planning.shortcuts import * + +# declare aries val +get_environment().factory.add_engine("aries-val", "up_aries", "AriesVal") + + +mode = sys.argv[1] +pb = sys.argv[2] if sys.argv[2:] else "" + +if mode.lower() == "val": + errors = report.report_validation("aries-val", problem_prefix=pb) +elif mode.lower() == "solve": + errors = report.report_oneshot("aries", problem_prefix=pb) +else: + raise ValueError(f"Unknown mode: {mode}") + + +assert len(errors) == 0 From 26135819033b0545614d5aa99b1f884092fb4b3c Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 17 Oct 2023 11:00:31 +0200 Subject: [PATCH 25/71] chore(lin sum): add display impl --- planning/planning/src/chronicles/printer.rs | 24 ++++++- solver/src/lib.rs | 2 +- solver/src/model/lang/linear.rs | 70 +++++++++++++++++++++ solver/src/model/model_impl.rs | 13 +++- solver/src/reasoners/cp/mod.rs | 31 +++++++++ solver/src/reif/mod.rs | 22 +++++++ 6 files changed, 157 insertions(+), 5 deletions(-) diff --git a/planning/planning/src/chronicles/printer.rs b/planning/planning/src/chronicles/printer.rs index e195ccb1..51445fa0 100644 --- a/planning/planning/src/chronicles/printer.rs +++ b/planning/planning/src/chronicles/printer.rs @@ -7,6 +7,7 @@ use aries::model::lang::linear::{LinearSum, LinearTerm}; use aries::model::lang::{Atom, BVar, IAtom, IVar, SAtom}; use aries::model::symbols::SymId; use aries::model::Model; +use itertools::Itertools; pub struct Printer<'a> { model: &'a Model, @@ -105,11 +106,28 @@ impl<'a> Printer<'a> { println!() } + pub fn print_reif_constraints(constraints: &[aries::model::Constraint], model: &Model) { + for c in constraints.iter().unique() { + Self::print_reif_constraint(c, model); + } + } + + pub fn print_reif_constraint(constraint: &aries::model::Constraint, model: &Model) { + let printer = Printer { model }; + printer.reif_constraint(constraint); + } + + fn reif_constraint(&self, constraint: &aries::model::Constraint) { + println!("{constraint}"); + } + fn list(&self, l: &[impl Into + Copy]) { - for e in l { + for (i, e) in l.iter().enumerate() { + if i != 0 { + print!(" "); + } let a: Atom = (*e).into(); self.atom(a); - print!(" "); } } @@ -262,7 +280,7 @@ impl<'a> Printer<'a> { print!("<") } ConstraintType::Leq => { - print!("<") + print!("<=") } ConstraintType::Eq => { print!("=") diff --git a/solver/src/lib.rs b/solver/src/lib.rs index 8b1c266f..8f54b45f 100644 --- a/solver/src/lib.rs +++ b/solver/src/lib.rs @@ -3,6 +3,6 @@ pub mod collections; pub mod core; pub mod model; pub mod reasoners; -pub(crate) mod reif; +pub mod reif; pub mod solver; pub mod utils; diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs index 64d48c28..d764a2f7 100644 --- a/solver/src/model/lang/linear.rs +++ b/solver/src/model/lang/linear.rs @@ -24,6 +24,23 @@ pub struct LinearTerm { denom: IntCst, } +impl std::fmt::Display for LinearTerm { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if self.factor != 1 { + if self.factor < 0 { + write!(f, "({})", self.factor)?; + } else { + write!(f, "{}", self.factor)?; + } + write!(f, "*")?; + } + if self.var != IVar::ONE { + write!(f, "{:?}", self.var)?; + } + write!(f, "[{:?}]", self.lit) + } +} + impl LinearTerm { pub const fn new(factor: IntCst, var: IVar, lit: Lit, denom: IntCst) -> LinearTerm { LinearTerm { @@ -127,6 +144,24 @@ pub struct LinearSum { denom: IntCst, } +impl std::fmt::Display for LinearSum { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + for (i, e) in self.terms.iter().enumerate() { + if i != 0 { + write!(f, " + ")?; + } + write!(f, "{e}")?; + } + if self.constant != 0 { + if !self.terms.is_empty() { + write!(f, " + ")?; + } + write!(f, "{}", self.constant)?; + } + Ok(()) + } +} + impl LinearSum { pub fn zero() -> LinearSum { LinearSum { @@ -364,6 +399,12 @@ pub struct LinearLeq { ub: IntCst, } +impl std::fmt::Display for LinearLeq { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{} <= {}", self.sum, self.ub) + } +} + impl LinearLeq { pub fn new(sum: LinearSum, ub: IntCst) -> LinearLeq { LinearLeq { sum, ub } @@ -402,6 +443,23 @@ pub struct NFLinearSumItem { pub lit: Lit, } +impl std::fmt::Display for NFLinearSumItem { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if self.factor != 1 { + if self.factor < 0 { + write!(f, "({})", self.factor)?; + } else { + write!(f, "{}", self.factor)?; + } + write!(f, "*")?; + } + if self.var != VarRef::ONE { + write!(f, "{:?}", self.var)?; + } + write!(f, "[{:?}]", self.lit) + } +} + impl std::ops::Neg for NFLinearSumItem { type Output = NFLinearSumItem; @@ -424,6 +482,18 @@ pub struct NFLinearLeq { pub upper_bound: IntCst, } +impl std::fmt::Display for NFLinearLeq { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + for (i, e) in self.sum.iter().enumerate() { + if i != 0 { + write!(f, " + ")?; + } + write!(f, "{e}")?; + } + write!(f, " <= {}", self.upper_bound) + } +} + impl NFLinearLeq { pub(crate) fn validity_scope(&self, presence: impl Fn(VarRef) -> Lit) -> ValidityScope { // the expression is valid if all variables are present, except for those that do not evaluate to zero when absent diff --git a/solver/src/model/model_impl.rs b/solver/src/model/model_impl.rs index 67eb82eb..52af300c 100644 --- a/solver/src/model/model_impl.rs +++ b/solver/src/model/model_impl.rs @@ -1,4 +1,5 @@ use std::convert::TryFrom; +use std::fmt::Formatter; use std::sync::Arc; use crate::backtrack::{Backtrack, DecLvl}; @@ -18,12 +19,22 @@ use crate::reif::{ReifExpr, Reifiable}; mod scopes; -#[derive(Clone)] +#[derive(PartialEq, Eq, Hash, Debug, Clone)] pub enum Constraint { /// Constraint enforcing that the left and right terms evaluate to the same value. Reified(ReifExpr, Lit), } +impl std::fmt::Display for Constraint { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match self { + Constraint::Reified(r, l) => { + write!(f, "{l:?} <=> {r}") + } + } + } +} + /// Defines the structure of a model: variables names, types, relations, ... #[derive(Clone)] pub struct ModelShape { diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index bdfc7067..cf9b1c45 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -22,6 +22,23 @@ struct SumElem { lit: Lit, } +impl std::fmt::Display for SumElem { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if self.factor != 1 { + if self.factor < 0 { + write!(f, "({})", self.factor)?; + } else { + write!(f, "{}", self.factor)?; + } + write!(f, "*")?; + } + if self.var != VarRef::ONE { + write!(f, "{:?}", self.var)?; + } + write!(f, "[{:?}]", self.lit) + } +} + impl SumElem { fn is_constant(&self) -> bool { self.var == VarRef::ONE @@ -35,6 +52,20 @@ struct LinearSumLeq { active: Lit, } +impl std::fmt::Display for LinearSumLeq { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let prez = format!("[{:?}]", self.active); + write!(f, "{prez:<8}")?; + for (i, e) in self.elements.iter().enumerate() { + if i != 0 { + write!(f, " + ")?; + } + write!(f, "{e}")?; + } + write!(f, " <= {}", self.ub) + } +} + impl LinearSumLeq { fn get_lower_bound(&self, elem: SumElem, domains: &Domains) -> IntCst { let var_is_present = domains.present(elem.var) == Some(true); diff --git a/solver/src/reif/mod.rs b/solver/src/reif/mod.rs index d74f8f77..b494c5a6 100644 --- a/solver/src/reif/mod.rs +++ b/solver/src/reif/mod.rs @@ -26,6 +26,28 @@ pub enum ReifExpr { Linear(NFLinearLeq), } +impl std::fmt::Display for ReifExpr { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match self { + ReifExpr::Lit(l) => { + write!(f, "{l:?}") + } + ReifExpr::MaxDiff(md) => { + write!(f, "{md:?}") + } + ReifExpr::Or(or) => { + write!(f, "or{or:?}") + } + ReifExpr::And(and) => { + write!(f, "and{and:?}") + } + ReifExpr::Linear(l) => { + write!(f, "{l}") + } + } + } +} + impl ReifExpr { pub fn scope(&self, presence: impl Fn(VarRef) -> Lit) -> ValidityScope { match self { From 2cccca004c03e0e5a26518fcbcaa3e8de8261c91 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 17 Oct 2023 11:09:58 +0200 Subject: [PATCH 26/71] chore(encode|resource): add debug view --- planning/planners/src/encode.rs | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 0bb3f090..59a013e9 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -13,12 +13,18 @@ use aries::model::lang::{expr::*, Kind, Type}; use aries::model::lang::{Atom, FAtom, FVar, IAtom, Variable}; use aries::solver::Solver; use aries_planning::chronicles::constraints::{ConstraintType, Duration}; +use aries_planning::chronicles::printer::Printer; use aries_planning::chronicles::*; use env_param::EnvParam; use std::collections::{HashMap, HashSet}; use std::convert::TryFrom; use std::ptr; +/// Parameter that activates the debug view of the resource constraints. +/// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_DEBUG`. +/// Possible values are `false`(default) and `true`. +pub static RESOURCE_CONSTRAINT_DEBUG: EnvParam = EnvParam::new("ARIES_RESOURCE_CONSTRAINT_DEBUG", "false"); + /// Parameter that activates the usage of timepoints to encode the increase's literals. /// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS`. /// Possible values are `false` and `true` (default). @@ -969,7 +975,26 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result { // Resource constraints encode_resource_constraints(&mut solver, &effs, &conds, &eff_assign_ends, &eff_persis_ends); + + if RESOURCE_CONSTRAINT_DEBUG.get() { + println!("\n=============================== Constraints =============================="); + Printer::print_reif_constraints(&solver.get_shape().constraints, &solver.model); + + println!("\n=========================== Before Propagation ==========================="); + solver.model.print_state(); + + let after = |solver: &Solver| { + println!("\n============================ After Propagation ==========================="); + solver.model.print_state(); + }; + + match solver.propagate() { + Ok(_) => after(&solver), + Err(_) => after(&solver), + }; + } else { solver.propagate()?; + } } let metric = metric.map(|metric| add_metric(pb, &mut solver.model, metric)); From e0a9f82e78f77953c4b0f4956a5da0f1f59ffb8a Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 17 Oct 2023 11:45:45 +0200 Subject: [PATCH 27/71] feat(lin): can map the literals of a sum --- solver/src/model/lang/linear.rs | 44 +++++++++++++++++++++++++++++++-- 1 file changed, 42 insertions(+), 2 deletions(-) diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs index d764a2f7..f6fb3bd6 100644 --- a/solver/src/model/lang/linear.rs +++ b/solver/src/model/lang/linear.rs @@ -172,8 +172,17 @@ impl LinearSum { } pub fn with_lit>(value: T, lit: Lit) -> LinearSum { - let mut sum: LinearSum = value.into(); - sum.terms.iter_mut().for_each(|term| term.lit = lit); + let sum: LinearSum = value.into(); + sum.map_with_lit(|_| lit) + } + + /// Returns a copy of the linear sum where the literals are updated according to the mapping. + pub fn map_with_lit(&self, mut map: F) -> LinearSum + where + F: FnMut(&LinearTerm) -> Lit, + { + let mut sum = self.clone(); + sum.terms.iter_mut().for_each(|t| t.lit = map(t)); sum } @@ -778,6 +787,37 @@ mod tests { } } + #[test] + fn test_sum_map_with_lit() { + let var = IVar::new(VarRef::from_u32(5)); + + let t1 = LinearTerm::rational(1, var, 10, Lit::TRUE); + let t2 = LinearTerm::constant_rational(5, 10, Lit::TRUE); + let sum = LinearSum::of([t1, t2].to_vec()); + for l1 in [var.geq(2), var.leq(6), Lit::FALSE, Lit::TRUE] { + for l2 in [var.geq(2), var.leq(6), Lit::FALSE, Lit::TRUE] { + let new_sum = sum.map_with_lit(|t| { + if *t == t1 { + return l1; + } + l2 + }); + assert_eq!(new_sum.constant, sum.constant); + assert_eq!(new_sum.denom, sum.denom); + for (t, nt) in sum.terms.iter().zip(new_sum.terms) { + assert_eq!(nt.factor, t.factor); + assert_eq!(nt.var, t.var); + assert_eq!(nt.denom, t.denom); + if *t == t1 { + assert_eq!(nt.lit, l1); + } else { + assert_eq!(nt.lit, l2); + } + } + } + } + } + #[test] fn test_sum_constant_int() { for n in [0, 1, 2, 5, 10, 15, 20, 50, 100] { From 67571a704a24dac20e15497004f1ad302b859b00 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 17 Oct 2023 11:46:38 +0200 Subject: [PATCH 28/71] fix(encode|resource): lit => prez(var) --- planning/planners/src/encode.rs | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 59a013e9..f3d94de9 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -993,7 +993,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result Err(_) => after(&solver), }; } else { - solver.propagate()?; + solver.propagate()?; } } @@ -1190,12 +1190,21 @@ fn encode_resource_constraints( for (&(la, ca, _), li_ci) in la_ca_ta.iter().zip(m_li_ci) { // Create the sum. let mut sum = LinearSum::zero(); - sum += LinearSum::with_lit(ca, la); + sum += LinearSum::with_lit( + ca, + solver.reify(and([la, solver.model.presence_literal(ca.var.into())])), + ); for (li, ci) in li_ci.iter() { - sum += LinearSum::with_lit(ci.clone(), *li) + sum += ci + .map_with_lit(|t| solver.reify(and([t.lit(), *li, solver.model.presence_literal(t.var().into())]))); + // sum += LinearSum::with_lit(ci.clone(), *li) } let cond_val = IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); - sum -= LinearSum::with_lit(cond_val, la); + sum -= LinearSum::with_lit( + cond_val, + solver.reify(and([la, solver.model.presence_literal(cond_val.var.into())])), + ); + sum = sum.simplify(); // Force the sum to be equals to 0. solver.enforce(sum.clone().geq(0), [prez_cond]); solver.enforce(sum.leq(0), [prez_cond]); From 31b1e9dbdc61f0a73ff35c980dabe957f3d79a34 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Thu, 19 Oct 2023 14:45:24 +0200 Subject: [PATCH 29/71] fix(encode|resource): force literals to be always defined --- planning/planners/src/encode.rs | 36 +++++++++++++++++++++------------ solver/src/model/model_impl.rs | 2 +- solver/src/reif/mod.rs | 1 + 3 files changed, 25 insertions(+), 14 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index f3d94de9..a52cdf89 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -1148,6 +1148,7 @@ fn encode_resource_constraints( * - is after the assignment effect `e_j` * - has the same state variable as the condition * - `la_j` is true + * - the condition is present */ let m_li_ci = la_ca_ta .iter() @@ -1158,6 +1159,8 @@ fn encode_resource_constraints( let mut li_conjunction: Vec = Vec::with_capacity(12); // `la_j` is true li_conjunction.push(*la); + // the condition is present + li_conjunction.push(prez_cond); // is present li_conjunction.push(*prez_eff); // is before the condition @@ -1173,10 +1176,7 @@ fn encode_resource_constraints( } // Create the `li_j*` literal. let li_lit = solver.reify(and(li_conjunction)); - debug_assert!(solver - .model - .state - .implies(prez_cond, solver.model.presence_literal(li_lit.variable()))); + debug_assert!(solver.model.entails(solver.model.presence_literal(li_lit.variable()))); // Get the `ci_j*` value. let EffectOp::Increase(eff_val) = eff.operation.clone() else { unreachable!() }; @@ -1197,7 +1197,6 @@ fn encode_resource_constraints( for (li, ci) in li_ci.iter() { sum += ci .map_with_lit(|t| solver.reify(and([t.lit(), *li, solver.model.presence_literal(t.var().into())]))); - // sum += LinearSum::with_lit(ci.clone(), *li) } let cond_val = IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); sum -= LinearSum::with_lit( @@ -1205,6 +1204,17 @@ fn encode_resource_constraints( solver.reify(and([la, solver.model.presence_literal(cond_val.var.into())])), ); sum = sum.simplify(); + + // Check that all the literals of the sum are always defined. + // It is wrapped in a `debug_assert!` for performance in release mode. + debug_assert!({ + for term in sum.terms() { + let prez = solver.model.presence_literal(term.lit().variable()); + debug_assert!(solver.model.entails(prez)); + } + true + }); + // Force the sum to be equals to 0. solver.enforce(sum.clone().geq(0), [prez_cond]); solver.enforce(sum.leq(0), [prez_cond]); @@ -1222,6 +1232,7 @@ Vector to store the `la_j` literals, `ca_j` values and the start persistence tim - is before the condition - has the same state variable as the condition - for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` + - the condition is present **/ fn create_la_vector_without_timepoints( assignments: Vec<&&(EffID, Lit, &Effect)>, @@ -1270,13 +1281,12 @@ fn create_la_vector_without_timepoints( let disjunction_lit = solver.reify(or(disjunction.clone())); la_conjunction.push(disjunction_lit); } + // the condition is present + la_conjunction.push(prez_cond); // Create the `la_j` literal. let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver - .model - .state - .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); + debug_assert!(solver.model.entails(solver.model.presence_literal(la_lit.variable()))); // Get the `ca_j` variable. let EffectOp::Assign(eff_val) = eff.operation else { @@ -1298,6 +1308,7 @@ Vector to store the `la_j` literals, `ca_j` values and the start persistence tim - is present - has the same state variable as the condition - the condition is between the start persistence and the assignment end (new timepoint) + - the condition is present **/ fn create_la_vector_with_timepoints( assignments: Vec<&&(EffID, Lit, &Effect)>, @@ -1322,13 +1333,12 @@ fn create_la_vector_with_timepoints( // the condition is between the start persistence and the assignment end la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); la_conjunction.push(solver.reify(f_leq(cond.end, eff_assign_ends[eff_id]))); + // the condition is present + la_conjunction.push(prez_cond); // Create the `la_j` literal. let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver - .model - .state - .implies(prez_cond, solver.model.presence_literal(la_lit.variable()))); + debug_assert!(solver.model.entails(solver.model.presence_literal(la_lit.variable()))); // Get the `ca_j` variable. let EffectOp::Assign(eff_val) = eff.operation else { diff --git a/solver/src/model/model_impl.rs b/solver/src/model/model_impl.rs index 52af300c..42369e46 100644 --- a/solver/src/model/model_impl.rs +++ b/solver/src/model/model_impl.rs @@ -90,7 +90,7 @@ impl ModelShape { let expected_value = Some(assignment.value(*reified).unwrap()); anyhow::ensure!( actual_value == expected_value, - "{:?}: {:?} != {:?} [{:?}]", + "{}: {:?} != {:?} [{:?}]", expr, actual_value, expected_value, diff --git a/solver/src/reif/mod.rs b/solver/src/reif/mod.rs index b494c5a6..ec950bcb 100644 --- a/solver/src/reif/mod.rs +++ b/solver/src/reif/mod.rs @@ -106,6 +106,7 @@ impl ReifExpr { let lin = lin.simplify(); let mut sum = 0; for term in &lin.sum { + debug_assert!(assignment.entails(term.lit) || assignment.entails(!term.lit)); if assignment.entails(term.lit) { assert!(prez(term.var)); sum += value(term.var) * term.factor; From b297093020380e18932969d7183e795c600950ee Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 27 Oct 2023 18:00:30 +0200 Subject: [PATCH 30/71] misc(up): Minor code refactoring --- planning/grpc/server/src/serialize.rs | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/planning/grpc/server/src/serialize.rs b/planning/grpc/server/src/serialize.rs index 9d88a4f1..752b995d 100644 --- a/planning/grpc/server/src/serialize.rs +++ b/planning/grpc/server/src/serialize.rs @@ -146,23 +146,18 @@ pub fn serialize_plan( ); if !a.parameters.is_empty() { // Search for the corresponding activity definition - let mut act: Option = None; - for _a in _problem_request + let act = _problem_request .scheduling_extension .as_ref() - .unwrap() + .expect("Missing scheduling extension") .activities .iter() - { - if _a.name == name { - act = Some(_a.clone()); - break; - } - } - let act = act.unwrap_or_else(|| panic!("Cannot find the activity {} definition", name)); + .find(|a| a.name == name) + .unwrap_or_else(|| panic!("Missing the activity `{}` definition", name)); + // Assign the solution value to each action parameter - for (v, p) in a.parameters.iter().zip(act.parameters) { - schedule.variable_assignments.insert(p.name, v.clone()); + for (v, p) in a.parameters.iter().zip(&act.parameters) { + schedule.variable_assignments.insert(p.name.clone(), v.clone()); } } schedule.activities.push(name); From 07a8d912633c4fb7ac3c90d96bc3d97aa92778f4 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 6 Nov 2023 14:29:35 +0100 Subject: [PATCH 31/71] chore(encode|resource): use 3 timepoints for assign --- planning/planners/src/encode.rs | 56 +++++++++------------------------ 1 file changed, 14 insertions(+), 42 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index a52cdf89..ca8fceb3 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -555,26 +555,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result (*eff_id, var) }) .collect(); - let eff_assign_ends: HashMap = effs - .iter() - .filter_map(|(eff_id, prez, eff)| { - if !solver.model.entails(!*prez) - && matches!(eff.operation, EffectOp::Assign(_)) - && is_integer(&eff.state_var) - { - // Those time points are only present for numeric assignment effects - let var = solver.model.new_optional_fvar( - ORIGIN * TIME_SCALE.get(), - HORIZON * TIME_SCALE.get(), - TIME_SCALE.get(), - *prez, - Container::Instance(eff_id.instance_id) / VarType::EffectEnd, - ); - return Some((*eff_id, var)); - } - None - }) - .collect(); tracing::debug!("#chronicles: {}", pb.chronicles.len()); tracing::debug!("#effects: {}", effs.len()); @@ -757,7 +737,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } tracing::debug!("Chronicles removed by eager propagation: {}", num_removed_chronicles); - // for each effect, make sure the three (or four for numeric assignments) time points are ordered + // for each effect, make sure the time points are ordered for &(eff_id, prez_eff, eff) in &effs { let persistence_end = eff_persis_ends[&eff_id]; solver.enforce(f_leq(eff.persistence_start, persistence_end), [prez_eff]); @@ -765,10 +745,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result for &min_persistence_end in &eff.min_persistence_end { solver.enforce(f_leq(min_persistence_end, persistence_end), [prez_eff]) } - if eff_assign_ends.contains_key(&eff_id) { - let assignment_end = eff_assign_ends[&eff_id]; - solver.enforce(f_leq(persistence_end, assignment_end), [prez_eff]); - } } solver.propagate()?; @@ -798,10 +774,13 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result continue; } - // skip if it's two increases - if matches!(e1.operation, EffectOp::Increase(_)) && matches!(e2.operation, EffectOp::Increase(_)) { + // skip if it is not two assignments + if matches!(e1.operation, EffectOp::Increase(_)) || matches!(e2.operation, EffectOp::Increase(_)) { continue; } + debug_assert!( + matches!(e1.operation, EffectOp::Assign(_)) && matches!(e2.operation, EffectOp::Assign(_)) + ); clause.clear(); debug_assert_eq!(e1.state_var.fluent, e2.state_var.fluent); @@ -815,15 +794,9 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } } - // For two numeric assignments, force [transition_start, assignment_end] to not overlaps. - // Otherwise, force [transition_start, persistence_end] to not overlaps. - if eff_assign_ends.contains_key(&i) && eff_assign_ends.contains_key(&j) { - clause.push(solver.reify(f_leq(eff_assign_ends[&j], e1.transition_start))); - clause.push(solver.reify(f_leq(eff_assign_ends[&i], e2.transition_start))); - } else { - clause.push(solver.reify(f_leq(eff_persis_ends[&j], e1.transition_start))); - clause.push(solver.reify(f_leq(eff_persis_ends[&i], e2.transition_start))); - } + // Force assign effects to not overlaps. + clause.push(solver.reify(f_leq(eff_persis_ends[&j], e1.transition_start))); + clause.push(solver.reify(f_leq(eff_persis_ends[&i], e2.transition_start))); // add coherence constraint solver.enforce(or(clause.as_slice()), [p1, p2]); @@ -974,7 +947,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result { // Resource constraints - encode_resource_constraints(&mut solver, &effs, &conds, &eff_assign_ends, &eff_persis_ends); + encode_resource_constraints(&mut solver, &effs, &conds, &eff_persis_ends); if RESOURCE_CONSTRAINT_DEBUG.get() { println!("\n=============================== Constraints =============================="); @@ -1015,7 +988,6 @@ fn encode_resource_constraints( solver: &mut Box>, effs: &[(EffID, Lit, &Effect)], conds: &[(CondID, Lit, &Condition)], - eff_assign_ends: &HashMap, eff_persis_ends: &HashMap, ) { /* ============================= Variables setup ============================ */ @@ -1130,7 +1102,7 @@ fn encode_resource_constraints( // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. let la_ca_ta = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { - create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_assign_ends, solver) + create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_persis_ends, solver) } else { create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, eff_persis_ends, solver) }; @@ -1314,7 +1286,7 @@ fn create_la_vector_with_timepoints( assignments: Vec<&&(EffID, Lit, &Effect)>, cond: &Condition, prez_cond: Lit, - eff_assign_ends: &HashMap, + eff_persis_ends: &HashMap, solver: &mut Solver, ) -> Vec<(Lit, IAtom, FAtom)> { assignments @@ -1330,9 +1302,9 @@ fn create_la_vector_with_timepoints( let b = eff.state_var.args[idx]; la_conjunction.push(solver.reify(eq(a, b))); } - // the condition is between the start persistence and the assignment end + // the condition is between the start and the end of the effect la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); - la_conjunction.push(solver.reify(f_leq(cond.end, eff_assign_ends[eff_id]))); + la_conjunction.push(solver.reify(f_leq(cond.end, eff_persis_ends[eff_id]))); // the condition is present la_conjunction.push(prez_cond); From e2e0b4d390c4c119bad11140094296d385bc0ac5 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 6 Nov 2023 14:47:33 +0100 Subject: [PATCH 32/71] refactor(effects): rename time points --- planning/grpc/server/src/chronicles.rs | 4 +- planning/planners/src/encode.rs | 104 ++++++++++-------- planning/planning/src/chronicles/concrete.rs | 27 ++--- .../preprocessing/merge_conditions_effects.rs | 4 +- .../preprocessing/state_variables.rs | 4 +- .../preprocessing/unused_effects.rs | 15 +-- planning/planning/src/chronicles/printer.rs | 8 +- planning/planning/src/parsing/mod.rs | 20 ++-- 8 files changed, 96 insertions(+), 90 deletions(-) diff --git a/planning/grpc/server/src/chronicles.rs b/planning/grpc/server/src/chronicles.rs index a945c57d..06fb1253 100644 --- a/planning/grpc/server/src/chronicles.rs +++ b/planning/grpc/server/src/chronicles.rs @@ -546,8 +546,8 @@ impl<'a> ChronicleFactory<'a> { }; self.chronicle.effects.push(Effect { transition_start: span.start, - persistence_start: span.end, - min_persistence_end: Vec::new(), + transition_end: span.end, + min_mutex_end: Vec::new(), state_var: sv, operation, }); diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index ca8fceb3..7c807be0 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -516,6 +516,16 @@ pub struct EncodedProblem { pub encoding: Encoding, } +/// Returns whether the effect is an assignment. +fn is_assignment(eff: &Effect) -> bool { + matches!(eff.operation, EffectOp::Assign(_)) +} + +/// Returns whether the effect is an increase. +fn is_increase(eff: &Effect) -> bool { + matches!(eff.operation, EffectOp::Increase(_)) +} + /// Returns whether the state variable is numeric. fn is_integer(sv: &StateVar) -> bool { matches!(sv.fluent.return_type().into(), Kind::Int) @@ -542,8 +552,11 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result let effs: Vec<_> = effects(pb).collect(); let conds: Vec<_> = conditions(pb).collect(); - let eff_persis_ends: HashMap = effs + + // Represents the final time point where an assignment is exclusive. + let eff_mutex_ends: HashMap = effs .iter() + .filter(|(_, __, eff)| is_assignment(eff)) .map(|(eff_id, prez, _)| { let var = solver.model.new_optional_fvar( ORIGIN * TIME_SCALE.get(), @@ -739,11 +752,14 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // for each effect, make sure the time points are ordered for &(eff_id, prez_eff, eff) in &effs { - let persistence_end = eff_persis_ends[&eff_id]; - solver.enforce(f_leq(eff.persistence_start, persistence_end), [prez_eff]); - solver.enforce(f_leq(eff.transition_start, eff.persistence_start), [prez_eff]); - for &min_persistence_end in &eff.min_persistence_end { - solver.enforce(f_leq(min_persistence_end, persistence_end), [prez_eff]) + solver.enforce(f_leq(eff.transition_start, eff.transition_end), [prez_eff]); + if eff_mutex_ends.contains_key(&eff_id) { + debug_assert!(is_assignment(eff)); + let mutex_end = eff_mutex_ends[&eff_id]; + solver.enforce(f_leq(eff.transition_end, mutex_end), [prez_eff]); + for &min_mutex_end in &eff.min_mutex_end { + solver.enforce(f_leq(min_mutex_end, mutex_end), [prez_eff]) + } } } @@ -775,12 +791,10 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } // skip if it is not two assignments - if matches!(e1.operation, EffectOp::Increase(_)) || matches!(e2.operation, EffectOp::Increase(_)) { + if !(is_assignment(e1) && is_assignment(e2)) { continue; } - debug_assert!( - matches!(e1.operation, EffectOp::Assign(_)) && matches!(e2.operation, EffectOp::Assign(_)) - ); + debug_assert!(is_assignment(e1) && is_assignment(e2)); clause.clear(); debug_assert_eq!(e1.state_var.fluent, e2.state_var.fluent); @@ -795,8 +809,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } // Force assign effects to not overlaps. - clause.push(solver.reify(f_leq(eff_persis_ends[&j], e1.transition_start))); - clause.push(solver.reify(f_leq(eff_persis_ends[&i], e2.transition_start))); + clause.push(solver.reify(f_leq(eff_mutex_ends[&j], e1.transition_start))); + clause.push(solver.reify(f_leq(eff_mutex_ends[&i], e2.transition_start))); // add coherence constraint solver.enforce(or(clause.as_slice()), [p1, p2]); @@ -857,8 +871,8 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result supported_by_eff_conjunction.push(solver.reify(eq(condition_value, effect_value))); // effect's persistence contains condition - supported_by_eff_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); - supported_by_eff_conjunction.push(solver.reify(f_leq(cond.end, eff_persis_ends[&eff_id]))); + supported_by_eff_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); + supported_by_eff_conjunction.push(solver.reify(f_leq(cond.end, eff_mutex_ends[&eff_id]))); supported_by_eff_conjunction.push(prez_eff); let support_lit = solver.reify(and(supported_by_eff_conjunction)); @@ -929,10 +943,10 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result non_overlapping.push(solver.reify(neq(a, b))); } - // or does not overlap the interval `[eff.transition_start, eff.persistence_start[` + // or does not overlap the interval `[eff.transition_start, eff.transition_end[` // note that the interval is left-inclusive to enforce the epsilon separation non_overlapping.push(solver.reify(f_lt(cond.end, eff.transition_start))); - non_overlapping.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + non_overlapping.push(solver.reify(f_leq(eff.transition_end, cond.start))); solver.enforce(or(non_overlapping), [act1.chronicle.presence, act2.chronicle.presence]); num_mutex_constraints += 1; @@ -947,7 +961,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result { // Resource constraints - encode_resource_constraints(&mut solver, &effs, &conds, &eff_persis_ends); + encode_resource_constraints(&mut solver, &effs, &conds, &eff_mutex_ends); if RESOURCE_CONSTRAINT_DEBUG.get() { println!("\n=============================== Constraints =============================="); @@ -988,7 +1002,7 @@ fn encode_resource_constraints( solver: &mut Box>, effs: &[(EffID, Lit, &Effect)], conds: &[(CondID, Lit, &Condition)], - eff_persis_ends: &HashMap, + eff_mutex_ends: &HashMap, ) { /* ============================= Variables setup ============================ */ @@ -1000,17 +1014,11 @@ fn encode_resource_constraints( // Filter those who are not present. let assignments: Vec<_> = effs .iter() - .filter(|(_, prez, eff)| { - !solver.model.entails(!*prez) && matches!(eff.operation, EffectOp::Assign(_)) && is_integer(&eff.state_var) - }) + .filter(|(_, prez, eff)| !solver.model.entails(!*prez) && is_assignment(eff) && is_integer(&eff.state_var)) .collect(); let increases: Vec<_> = effs .iter() - .filter(|(_, prez, eff)| { - !solver.model.entails(!*prez) - && matches!(eff.operation, EffectOp::Increase(_)) - && is_integer(&eff.state_var) - }) + .filter(|(_, prez, eff)| !solver.model.entails(!*prez) && is_increase(eff) && is_integer(&eff.state_var)) .collect(); let mut conditions: Vec<_> = conds .iter() @@ -1039,7 +1047,7 @@ fn encode_resource_constraints( // Convert the increase effects into conditions in order to check that the new value is in the state variable domain. for &&(eff_id, prez, eff) in &increases { assert!( - eff.transition_start + FAtom::EPSILON == eff.persistence_start && eff.min_persistence_end.is_empty(), + eff.transition_start + FAtom::EPSILON == eff.transition_end && eff.min_mutex_end.is_empty(), "Only instantaneous effects are supported" ); // Get the bounds of the state variable. @@ -1057,8 +1065,8 @@ fn encode_resource_constraints( conditions.push(( prez, Condition { - start: eff.persistence_start, - end: eff.persistence_start, + start: eff.transition_end, + end: eff.transition_end, state_var: eff.state_var.clone(), value: var.into(), }, @@ -1100,11 +1108,11 @@ fn encode_resource_constraints( .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) .collect::>(); - // Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. + // Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j`. let la_ca_ta = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { - create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_persis_ends, solver) + create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_mutex_ends, solver) } else { - create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, eff_persis_ends, solver) + create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, eff_mutex_ends, solver) }; // Force to have at least one assignment. @@ -1136,9 +1144,9 @@ fn encode_resource_constraints( // is present li_conjunction.push(*prez_eff); // is before the condition - li_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + li_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); // is after the assignment effect `e_j` - li_conjunction.push(solver.reify(f_lt(*ta, eff.persistence_start))); + li_conjunction.push(solver.reify(f_lt(*ta, eff.transition_end))); // has the same state variable as the condition debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); for idx in 0..cond.state_var.args.len() { @@ -1197,7 +1205,7 @@ fn encode_resource_constraints( } /** -Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. +Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j`. `la_j` is true if and only if the associated assignment effect `e_j`: - is present @@ -1210,7 +1218,7 @@ fn create_la_vector_without_timepoints( assignments: Vec<&&(EffID, Lit, &Effect)>, cond: &Condition, prez_cond: Lit, - eff_persis_ends: &HashMap, + eff_mutex_ends: &HashMap, solver: &mut Solver, ) -> Vec<(Lit, IAtom, FAtom)> { assignments @@ -1220,7 +1228,7 @@ fn create_la_vector_without_timepoints( // is present la_conjunction.push(*prez_eff); // is before the condition - la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); + la_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); // has the same state variable as the condition debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); for idx in 0..cond.state_var.args.len() { @@ -1239,7 +1247,7 @@ fn create_la_vector_without_timepoints( // is not present disjunction.push(!*prez_other_eff); // is after the condition - disjunction.push(solver.reify(f_lt(cond.end, other_eff.persistence_start))); + disjunction.push(solver.reify(f_lt(cond.end, other_eff.transition_end))); // has a state variable different from the condition debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); for idx in 0..cond.state_var.args.len() { @@ -1248,7 +1256,7 @@ fn create_la_vector_without_timepoints( disjunction.push(solver.reify(neq(a, b))); } // is before the effect `e_j` - disjunction.push(solver.reify(f_lt(eff_persis_ends[other_eff_id], eff.persistence_start))); + disjunction.push(solver.reify(f_lt(eff_mutex_ends[other_eff_id], eff.transition_end))); let disjunction_lit = solver.reify(or(disjunction.clone())); la_conjunction.push(disjunction_lit); @@ -1266,27 +1274,27 @@ fn create_la_vector_without_timepoints( }; let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - // Get the persistence timepoint of the effect `e_j`. - let ta = eff.persistence_start; + // Get the end of the transition time point of the effect `e_j`. + let ta = eff.transition_end; (la_lit, ca, ta) }) .collect::>() } /** -Vector to store the `la_j` literals, `ca_j` values and the start persistence timepoint of the effect `e_j`. +Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j`. `la_j` is true if and only if the associated assignment effect `e_j`: - is present - has the same state variable as the condition - - the condition is between the start persistence and the assignment end (new timepoint) + - the condition is between the end of the transition and the mutex end - the condition is present **/ fn create_la_vector_with_timepoints( assignments: Vec<&&(EffID, Lit, &Effect)>, cond: &Condition, prez_cond: Lit, - eff_persis_ends: &HashMap, + eff_mutex_ends: &HashMap, solver: &mut Solver, ) -> Vec<(Lit, IAtom, FAtom)> { assignments @@ -1303,8 +1311,8 @@ fn create_la_vector_with_timepoints( la_conjunction.push(solver.reify(eq(a, b))); } // the condition is between the start and the end of the effect - la_conjunction.push(solver.reify(f_leq(eff.persistence_start, cond.start))); - la_conjunction.push(solver.reify(f_leq(cond.end, eff_persis_ends[eff_id]))); + la_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); + la_conjunction.push(solver.reify(f_leq(cond.end, eff_mutex_ends[eff_id]))); // the condition is present la_conjunction.push(prez_cond); @@ -1318,8 +1326,8 @@ fn create_la_vector_with_timepoints( }; let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - // Get the persistence timepoint of the effect `e_j`. - let ta = eff.persistence_start; + // Get the end of the transition time point of the effect `e_j`. + let ta = eff.transition_end; (la_lit, ca, ta) }) .collect::>() diff --git a/planning/planning/src/chronicles/concrete.rs b/planning/planning/src/chronicles/concrete.rs index f71e19bd..2445cf92 100644 --- a/planning/planning/src/chronicles/concrete.rs +++ b/planning/planning/src/chronicles/concrete.rs @@ -272,21 +272,22 @@ impl Substitute for StateVar { } /// Represents an effect on a state variable. -/// The effect has a first transition phase `]transition_start, persistence_start[` during which the +/// The effect has a first transition phase `]transition_start, transition_end[` during which the /// value of the state variable is unknown. -/// Exactly at time `persistence_start`, the state variable `state_var` takes the given `value`. -/// This value will persist until another effect starts its own transition. +/// Exactly at time `transition_end`, the state variable `state_var` is update with `value` +/// (assignment or increase based on `operation`). +/// For assignment effects, this value will persist until another assignment effect starts its own transition. #[derive(Clone)] pub struct Effect { /// Time at which the transition to the new value will start pub transition_start: Time, - /// Time at which the persistence will start - pub persistence_start: Time, - /// If specified, the effect is required to persist at least until all of these timepoints. - pub min_persistence_end: Vec