From 7ebad31cc2f64b6260ef2410ae280c018c23337f Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 27 Mar 2026 15:58:57 +0100 Subject: [PATCH 01/43] feat(solver): introduce `Evaluable` trait to construct values from a solution. --- examples/scheduling/src/search/greedy.rs | 3 +- examples/smt/tests/smt.rs | 3 +- .../preprocessing/action_rolling.rs | 2 +- planning/timelines/src/assignment.rs | 81 ------------------- planning/timelines/src/lib.rs | 8 +- solver/src/core/state/domains.rs | 38 +-------- solver/src/core/state/solution.rs | 40 ++++++++- solver/src/core/views.rs | 62 +++++++++++++- solver/src/model/extensions/domains_ext.rs | 3 +- .../model/extensions/partial_assignment.rs | 2 +- solver/src/model/lang/alternative.rs | 2 +- solver/src/model/lang/boolean.rs | 2 +- solver/src/model/lang/hreif.rs | 3 +- solver/src/model/lang/int.rs | 3 +- solver/src/model/lang/max.rs | 2 +- solver/src/reasoners/cp/no_overlap.rs | 3 +- .../src/reasoners/cp/no_overlap/neg_iatom.rs | 5 +- 17 files changed, 120 insertions(+), 142 deletions(-) delete mode 100644 planning/timelines/src/assignment.rs diff --git a/examples/scheduling/src/search/greedy.rs b/examples/scheduling/src/search/greedy.rs index d3ba73e74..6a3556c6a 100644 --- a/examples/scheduling/src/search/greedy.rs +++ b/examples/scheduling/src/search/greedy.rs @@ -4,7 +4,8 @@ use crate::Var; use crate::problem::Encoding; use crate::search::Model; use aries::backtrack::{Backtrack, DecLvl, DecisionLevelTracker}; -use aries::core::state::{OptDomain, Term}; +use aries::core::state::OptDomain; +use aries::core::views::Term; use aries::core::{IntCst, Lit, VarRef}; use aries::model::extensions::DomainsExt; use aries::solver::search::{Decision, SearchControl}; diff --git a/examples/smt/tests/smt.rs b/examples/smt/tests/smt.rs index c8a7b88fa..f86efe296 100644 --- a/examples/smt/tests/smt.rs +++ b/examples/smt/tests/smt.rs @@ -1,5 +1,6 @@ use aries::backtrack::Backtrack; -use aries::core::state::{OptDomain, Term}; +use aries::core::state::OptDomain; +use aries::core::views::Term; use aries::core::Lit; use aries::model::extensions::DomainsExt; use aries::model::lang::alternative::Alternative; diff --git a/planning/planning/src/chronicles/preprocessing/action_rolling.rs b/planning/planning/src/chronicles/preprocessing/action_rolling.rs index cb9be0443..796d7e8a3 100644 --- a/planning/planning/src/chronicles/preprocessing/action_rolling.rs +++ b/planning/planning/src/chronicles/preprocessing/action_rolling.rs @@ -5,7 +5,7 @@ use crate::chronicles::{ Chronicle, ChronicleLabel, ChronicleTemplate, Condition, Container, Effect, EffectOp, Problem, StateVar, Sub, Substitute, Substitution, Time, VarType, TIME_SCALE, }; -use aries::core::state::Term; +use aries::core::views::Term; use aries::core::{IntCst, Lit, VarRef, INT_CST_MAX}; use aries::model::extensions::partial_assignment::{PartialAssignment, PartialAssignmentBuilder}; use aries::model::lang::linear::LinearSum; diff --git a/planning/timelines/src/assignment.rs b/planning/timelines/src/assignment.rs deleted file mode 100644 index 77b4ad96d..000000000 --- a/planning/timelines/src/assignment.rs +++ /dev/null @@ -1,81 +0,0 @@ -use aries::{core::state::Term, prelude::*}; - -/// Trait representing the capability to be evaluated (to a givn type) when provided a total assignment. -/// -/// TODO: move to `aries` crate and make superseed the provided methods for all atoms. -pub trait Evaluable { - type Value; - - fn evaluate(&self, value_of_var: impl Fn(VarRef) -> Option) -> Option; -} - -impl Evaluable for VarRef { - type Value = IntCst; - - fn evaluate(&self, value_of_var: impl Fn(VarRef) -> Option) -> Option { - value_of_var(*self) - } -} -impl Evaluable for SignedVar { - type Value = IntCst; - - fn evaluate(&self, value_of_var: impl Fn(VarRef) -> Option) -> Option { - value_of_var(self.variable()).map(|val| val * self.sign()) - } -} -impl Evaluable for Lit { - type Value = bool; - - fn evaluate(&self, value_of_var: impl Fn(VarRef) -> Option) -> Option { - self.svar().evaluate(value_of_var).map(|val| val <= self.ub_value()) - } -} - -impl Evaluable for IVar { - type Value = IntCst; - - fn evaluate(&self, value_of_var: impl Fn(VarRef) -> Option) -> Option { - value_of_var(self.variable()) - } -} -impl Evaluable for IAtom { - type Value = IntCst; - - fn evaluate(&self, value_of_var: impl Fn(VarRef) -> Option) -> Option { - self.var.evaluate(value_of_var).map(|val| val + self.shift) - } -} - -/// Represents a total assignment, i.e., constructing this type is only valid if all variables are bound or absent in the model -/// -/// TODO: this type should be removed -pub struct Assignment { - sol: Solution, -} - -impl Assignment { - pub fn new(doms: &Domains) -> Self { - Self { - sol: doms.extract_solution(), - } - } - pub fn shared(sol: Solution) -> Self { - Self { sol } - } - - fn value_of_var(&self, var: VarRef) -> Option { - let doms = &self.sol; - match doms.present(var) { - Some(true) => Some(doms.lb(var)), - Some(false) => None, - None => panic!("The assignment is not total"), - } - } - - pub fn eval(&self, expr: E) -> Option - where - E: Evaluable, - { - expr.evaluate(|v| self.value_of_var(v)) - } -} diff --git a/planning/timelines/src/lib.rs b/planning/timelines/src/lib.rs index 25ed29e11..f972a0e04 100644 --- a/planning/timelines/src/lib.rs +++ b/planning/timelines/src/lib.rs @@ -1,4 +1,3 @@ -pub mod assignment; pub mod boxes; pub mod constraints; mod effects; @@ -22,7 +21,6 @@ use idmap::DirectIdMap; use itertools::Itertools; pub type Model = aries::model::Model; -use crate::assignment::Assignment; pub use crate::effects::*; use crate::explain::ExplainableSolver; use crate::symbols::ObjectEncoding; @@ -153,10 +151,10 @@ impl Sched { encoding } - pub fn solve(&self) -> Option { + pub fn solve(&self) -> Option { let encoding = self.encode(); let mut solver = Solver::new(encoding); - solver.solve(SearchLimit::None).unwrap().map(Assignment::shared) + solver.solve(SearchLimit::None).unwrap() } pub fn explainable_solver( @@ -166,7 +164,7 @@ impl Sched { ExplainableSolver::new(self, project) } - pub fn print(&self, sol: &Assignment) { + pub fn print(&self, sol: &Solution) { let sorted_tasks = self .tasks .iter() diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 9ba20758d..e4234a984 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -7,9 +7,8 @@ use crate::core::state::int_domains::IntDomains; use crate::core::state::{ Cause, DomainsSnapshot, Explainer, Explanation, ExplanationQueue, InvalidUpdate, OptDomain, RangeDomain, Solution, }; -use crate::core::views::{Boundable, VarView}; +use crate::core::views::{Boundable, Term, VarView}; use crate::core::*; -use crate::model::lang::{Atom, IAtom}; use crate::prelude::*; use itertools::Itertools; use std::fmt::{Debug, Formatter}; @@ -866,37 +865,6 @@ impl Debug for Conflict { } } -/// A term that can be converted into a variable. -/// Notably implemented for `VarRef`, `Lit`, `IVar`, `SVar`, `BVar` -pub trait Term { - fn variable(self) -> VarRef; -} -impl Term for Lit { - fn variable(self) -> VarRef { - self.variable() - } -} -impl Term for SignedVar { - fn variable(self) -> VarRef { - self.variable() - } -} -impl> Term for T { - fn variable(self) -> VarRef { - self.into() - } -} -impl Term for IAtom { - fn variable(self) -> VarRef { - self.var.variable() - } -} -impl Term for Atom { - fn variable(self) -> VarRef { - self.variable() - } -} - impl crate::core::views::Dom for Domains { fn upper_bound(&self, svar: SignedVar) -> IntCst { Domains::upper_bound(self, svar) @@ -1316,9 +1284,9 @@ mod tests { model.save_state(); assert!(model.assume(x.leq(3)).unwrap()); - assert_eq!(model.bounds(x.variable()), (0, 3)); + assert_eq!(model.bounds(x), (0, 3)); propagate(&mut model).unwrap(); - assert_eq!(model.bounds(y.variable()), (6, 10)); + assert_eq!(model.bounds(y), (6, 10)); model.save_state(); let err = model.assume(y.leq(4)).unwrap_err(); diff --git a/solver/src/core/state/solution.rs b/solver/src/core/state/solution.rs index 2d79be2bc..8c105469e 100644 --- a/solver/src/core/state/solution.rs +++ b/solver/src/core/state/solution.rs @@ -2,7 +2,10 @@ use std::sync::Arc; use crate::{ collections::ref_store::RefVec, - core::{state::ValueCause, views::Dom}, + core::{ + state::ValueCause, + views::{Dom, Optional, VarView}, + }, prelude::*, }; @@ -25,6 +28,11 @@ impl Solution { } } + /// Returns the value that the expression has in the solution, or None if the value is absent. + pub fn eval(&self, expr: T) -> Option { + expr.evaluate(self) + } + /// Returns the number of variables declared. pub fn num_variables(&self) -> usize { debug_assert!(self.data.values.len().is_multiple_of(2)); @@ -60,3 +68,33 @@ impl Dom for Solution { self.data.presences[var] } } + +/// Denotes expressions that can be evaluated in a solution. +pub trait Evaluable { + /// Type of the value of this expression. + /// + /// For instance it would be [`IntCst`] for [`VarRef`] and `bool` for [`Lit`]. + type Value; + + /// Determines the value that the expression has in a solution. + /// + /// Returns `None` the value is absent and the value wrapped in `Some(...)` otherwise. + fn evaluate(&self, solution: &Solution) -> Option; +} + +impl Evaluable for T +where + T: VarView + Optional, +{ + type Value = ::Value; + + fn evaluate(&self, solution: &Solution) -> Option { + if self.present(solution) { + // in a solution it is guaranteed that the domain of any present variable is a singleton, + // so we only take the lower bound + Some(solution.lb(self)) + } else { + None + } + } +} diff --git a/solver/src/core/views.rs b/solver/src/core/views.rs index 2098dcf88..30ffa7107 100644 --- a/solver/src/core/views.rs +++ b/solver/src/core/views.rs @@ -1,4 +1,4 @@ -use crate::core::{IntCst, Lit, SignedVar, VarRef}; +use crate::{model::lang::Atom, prelude::*}; pub trait Dom { fn upper_bound(&self, svar: SignedVar) -> IntCst; @@ -42,6 +42,18 @@ pub trait VarView { fn lower_bound(&self, dom: impl Dom) -> Self::Value; } +impl VarView for &T { + type Value = ::Value; + + fn upper_bound(&self, dom: impl Dom) -> Self::Value { + VarView::upper_bound(*self, dom) + } + + fn lower_bound(&self, dom: impl Dom) -> Self::Value { + VarView::lower_bound(*self, dom) + } +} + impl VarView for SignedVar { type Value = IntCst; @@ -93,3 +105,51 @@ impl Boundable for SignedVar { Lit::geq(*self, lb) } } + +/// Determine whether an expression is already determined to be present in the given domain.. +/// +/// If an expression is always defined (its presence literal is [`Lit::TRUE`]), it should return `true` regardless of the domain. +pub trait Optional { + fn present(&self, domains: impl Dom) -> bool; +} + +impl Optional for T { + fn present(&self, domains: impl Dom) -> bool { + domains.present(self.variable()) == Some(true) + } +} + +/// An expression that is a view of exactly one variable (which may be the [`VarRef::ZERO`] variable). +/// +/// Notably implemented for `VarRef`, `Lit`, `IVar`, `SVar`, `BVar` +pub trait Term { + /// Extracts the underlying variable in the expression. + /// + /// Note that the resulting in [`VarRef`] cannot in general be considered as equivalent to the expression. + fn variable(self) -> VarRef; +} +impl Term for Lit { + fn variable(self) -> VarRef { + self.variable() + } +} +impl Term for SignedVar { + fn variable(self) -> VarRef { + self.variable() + } +} +impl> Term for T { + fn variable(self) -> VarRef { + self.into() + } +} +impl Term for IAtom { + fn variable(self) -> VarRef { + self.var.variable() + } +} +impl Term for Atom { + fn variable(self) -> VarRef { + self.variable() + } +} diff --git a/solver/src/model/extensions/domains_ext.rs b/solver/src/model/extensions/domains_ext.rs index c8607cecd..e73c4d1b2 100644 --- a/solver/src/model/extensions/domains_ext.rs +++ b/solver/src/model/extensions/domains_ext.rs @@ -1,11 +1,10 @@ use crate::core::state::{FixedDomain, IntDomain, OptDomain, RangeDomain}; -use crate::core::views::{Dom, VarView}; +use crate::core::views::{Dom, Term, VarView}; use crate::core::*; use crate::model::lang::linear::LinearSum; use crate::model::lang::{Atom, Cst, IAtom, Rational, SAtom}; use crate::model::symbols::SymId; use crate::model::symbols::TypedSym; -use state::Term; /// Extension methods for an object containing a partial or total assignment to a problem. pub trait DomainsExt: Dom + Sized { diff --git a/solver/src/model/extensions/partial_assignment.rs b/solver/src/model/extensions/partial_assignment.rs index cea9b6cf8..0b1c19c9e 100644 --- a/solver/src/model/extensions/partial_assignment.rs +++ b/solver/src/model/extensions/partial_assignment.rs @@ -1,4 +1,4 @@ -use crate::core::state::Term; +use crate::core::views::Term; use crate::core::{IntCst, Lit, SignedVar, VarRef}; use crate::model::lang::{Atom, Cst, FAtom, IAtom, Rational, SAtom}; use crate::model::symbols::{SymId, TypedSym}; diff --git a/solver/src/model/lang/alternative.rs b/solver/src/model/lang/alternative.rs index 00350829b..40fa4b7e8 100644 --- a/solver/src/model/lang/alternative.rs +++ b/solver/src/model/lang/alternative.rs @@ -1,4 +1,4 @@ -use crate::core::state::Term; +use crate::core::views::Term; use crate::core::{IntCst, VarRef}; use crate::model::lang::{Atom, ConversionError, IAtom}; use crate::reif::ReifExpr; diff --git a/solver/src/model/lang/boolean.rs b/solver/src/model/lang/boolean.rs index 1d1770123..443fc1537 100644 --- a/solver/src/model/lang/boolean.rs +++ b/solver/src/model/lang/boolean.rs @@ -1,4 +1,4 @@ -use crate::core::state::Term; +use crate::core::views::Term; use crate::core::*; use crate::model::lang::IVar; diff --git a/solver/src/model/lang/hreif.rs b/solver/src/model/lang/hreif.rs index 28ed3aadc..2fad9ffff 100644 --- a/solver/src/model/lang/hreif.rs +++ b/solver/src/model/lang/hreif.rs @@ -1,7 +1,7 @@ use smallvec::SmallVec; use crate::{ - core::{IntCst, Lit, VarRef, state::Term}, + core::{IntCst, Lit, VarRef, views::Term}, model::{ Label, Model, lang::expr::{And, Leq, Or, or}, @@ -252,7 +252,6 @@ mod test { }; use super::*; - use crate::core::state::Term; /// All different with potentially optional variables struct AllDifferent(Vec); diff --git a/solver/src/model/lang/int.rs b/solver/src/model/lang/int.rs index 2d4db6b2b..3e6c41c70 100644 --- a/solver/src/model/lang/int.rs +++ b/solver/src/model/lang/int.rs @@ -1,5 +1,4 @@ -use crate::core::state::Term; -use crate::core::views::{Boundable, VarView}; +use crate::core::views::{Boundable, Term, VarView}; use crate::core::*; use crate::model::lang::ConversionError; use crate::model::lang::linear::LinearTerm; diff --git a/solver/src/model/lang/max.rs b/solver/src/model/lang/max.rs index a296ab4e9..20b8bfbf6 100644 --- a/solver/src/model/lang/max.rs +++ b/solver/src/model/lang/max.rs @@ -1,4 +1,4 @@ -use crate::core::state::Term; +use crate::core::views::Term; use crate::core::{IntCst, SignedVar}; use crate::model::lang::IAtom; use crate::reif::ReifExpr; diff --git a/solver/src/reasoners/cp/no_overlap.rs b/solver/src/reasoners/cp/no_overlap.rs index 60c967a46..43fec015a 100644 --- a/solver/src/reasoners/cp/no_overlap.rs +++ b/solver/src/reasoners/cp/no_overlap.rs @@ -4,10 +4,9 @@ use hashbrown::HashSet; use itertools::Itertools; use crate::core::state::{DomainsSnapshot, Explanation, InvalidUpdate}; -use crate::core::views::{Boundable, Dom, VarView}; +use crate::core::views::{Boundable, Dom, Term, VarView}; use crate::prelude::*; -use crate::core::state::Term; use crate::reasoners::cp::no_overlap::neg_iatom::PMIAtom; use crate::reasoners::cp::propagator::justified::*; use crate::reasoners::cp::{DynPropagator, UserPropagator}; diff --git a/solver/src/reasoners/cp/no_overlap/neg_iatom.rs b/solver/src/reasoners/cp/no_overlap/neg_iatom.rs index 23ad2fb41..8627d528d 100644 --- a/solver/src/reasoners/cp/no_overlap/neg_iatom.rs +++ b/solver/src/reasoners/cp/no_overlap/neg_iatom.rs @@ -1,8 +1,5 @@ use crate::{ - core::{ - state::Term, - views::{Boundable, VarView}, - }, + core::views::{Boundable, Term, VarView}, prelude::*, }; From ef647ee3f6a35e8cd1607b220416de095b116293 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 27 Mar 2026 16:15:00 +0100 Subject: [PATCH 02/43] chore(planning): have `Operation` be generic on its parameter type. --- planning/engine/src/optimize_plan.rs | 6 +++--- planning/engine/src/plans.rs | 3 +++ planning/engine/src/plans/lifted_plan.rs | 23 +++++++---------------- planning/engine/src/plans/operation.rs | 19 +++++++++++++++++++ planning/engine/src/repair.rs | 6 +++--- planning/engine/src/validate.rs | 2 +- planning/timelines/src/explain.rs | 6 +++--- 7 files changed, 39 insertions(+), 26 deletions(-) create mode 100644 planning/engine/src/plans/operation.rs diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index 44052d97b..345976c41 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -37,7 +37,7 @@ pub fn optimize_plan(model: &Model, plan: &LiftedPlan, options: &Options) -> Res let _encoding_time = start.elapsed().as_millis(); - if solver.check_satisfiability() { + if let Some(_solution) = solver.check_satisfiability() { println!("Plan is valid."); return Ok(()); } else { @@ -100,12 +100,12 @@ pub fn encode_plan_optimization_problem( for (param, arg) in a.parameters.iter().zip(op.arguments.iter()) { let arg = match arg { // ground parameter, get the corresponding object constant - lifted_plan::OperationArg::Ground(object) => sched + lifted_plan::ObjectOrVariable::Ground(object) => sched .objects .object_atom(object.name().canonical_str()) .ok_or_else(|| object.name().invalid("unknown object"))?, // variable parameter, retrieve the variable we created for it - lifted_plan::OperationArg::Variable { name } => plan_variables[name], + lifted_plan::ObjectOrVariable::Variable { name } => plan_variables[name], }; // incorpare the potential values taken by this operation param into the one of the action diff --git a/planning/engine/src/plans.rs b/planning/engine/src/plans.rs index 29b09e634..1a1f615f6 100644 --- a/planning/engine/src/plans.rs +++ b/planning/engine/src/plans.rs @@ -1 +1,4 @@ pub mod lifted_plan; +mod operation; + +pub use operation::*; diff --git a/planning/engine/src/plans/lifted_plan.rs b/planning/engine/src/plans/lifted_plan.rs index 73d1c84f9..79cc317ae 100644 --- a/planning/engine/src/plans/lifted_plan.rs +++ b/planning/engine/src/plans/lifted_plan.rs @@ -1,28 +1,19 @@ use std::collections::BTreeMap; -use planx::{ActionRef, Model, Res, Sym, errors::Span}; +use planx::{Model, Res, Sym}; use timelines::IntCst; +use crate::plans::Operation; + #[derive(Debug, Clone)] pub struct LiftedPlan { /// A set of operations: actions instances with arguments, start times and durations - pub operations: Vec, + pub operations: Vec>, /// All variables apprearing in the lifted plan, together with an inferred type (most specific one from all their appearances.) pub variables: BTreeMap, } - -#[derive(Debug, Clone)] -pub struct Operation { - pub start: IntCst, - pub duration: IntCst, - pub action_ref: ActionRef, - pub arguments: Vec, - #[allow(unused)] - pub span: Option, -} - #[derive(Debug, Clone)] -pub enum OperationArg { +pub enum ObjectOrVariable { Ground(planx::Object), Variable { name: Sym }, } @@ -65,7 +56,7 @@ pub fn parse_lifted_plan(plan: &planx::pddl::Plan, model: &Model) -> Res Res { + pub start: Instant, + pub duration: Duration, + pub action_ref: ActionRef, + pub arguments: Vec, + #[allow(unused)] + pub span: Option, +} diff --git a/planning/engine/src/repair.rs b/planning/engine/src/repair.rs index 143c14bc7..4adc6d99e 100644 --- a/planning/engine/src/repair.rs +++ b/planning/engine/src/repair.rs @@ -65,7 +65,7 @@ pub fn domain_repair(model: &Model, plan: &LiftedPlan, options: &RepairOptions) let mut solver = encode_dom_repair(model, plan)?; let encoding_time = start.elapsed().as_millis(); - if solver.check_satisfiability() { + if solver.check_satisfiability().is_some() { println!("Plan is valid."); return Ok(RepairReport { status: RepairStatus::ValidPlan, @@ -187,12 +187,12 @@ fn encode_dom_repair(model: &Model, plan: &LiftedPlan) -> Res sched + lifted_plan::ObjectOrVariable::Ground(object) => sched .objects .object_atom(object.name().canonical_str()) .ok_or_else(|| object.name().invalid("unknown object"))?, // variable parameter, retrieve the variable we created for it - lifted_plan::OperationArg::Variable { name } => plan_variables[name], + lifted_plan::ObjectOrVariable::Variable { name } => plan_variables[name], }; // incorpare the potential values taken by this operation param into the one of the action diff --git a/planning/engine/src/validate.rs b/planning/engine/src/validate.rs index ec46b3258..b031a6ace 100644 --- a/planning/engine/src/validate.rs +++ b/planning/engine/src/validate.rs @@ -15,5 +15,5 @@ pub fn validate(model: &Model, plan: &LiftedPlan, _options: &Options) -> Res ExplainableSolver { } } - /// Returns true if the model is satisfiable with all assumptions - pub fn check_satisfiability(&mut self) -> bool { + /// Check if the model is satifiable with all assumptions, and returns a solution if it is. + pub fn check_satisfiability(&mut self) -> Option { let assumptions = self.enablers.keys().copied().collect_vec(); let res = self .solver .solve_with_assumptions(&assumptions, aries::solver::SearchLimit::None) .unwrap() - .is_ok(); + .ok(); self.solver.print_stats(); self.solver.reset(); // TODO: this should not be needed res From 60d3c4c8b4ea579e7dc4a99954d8a4998414c2a5 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 27 Mar 2026 18:16:50 +0100 Subject: [PATCH 03/43] chore(planning): provind an Encoding structure to allow reconstructing plans --- Cargo.lock | 1 + planning/engine/src/encode.rs | 1 + planning/engine/src/encode/encoding.rs | 114 +++++++++++++++++++++++ planning/engine/src/optimize_plan.rs | 32 +++++-- planning/engine/src/plans/lifted_plan.rs | 5 +- planning/engine/src/plans/operation.rs | 28 +++++- planning/engine/src/validate.rs | 2 +- planning/timelines/Cargo.toml | 1 + planning/timelines/src/lib.rs | 1 + planning/timelines/src/rational.rs | 7 ++ planning/timelines/src/symbols.rs | 26 +++++- solver/src/core/cst.rs | 9 ++ solver/src/model/lang/fixed.rs | 21 ++++- 13 files changed, 234 insertions(+), 14 deletions(-) create mode 100644 planning/engine/src/encode/encoding.rs create mode 100644 planning/timelines/src/rational.rs diff --git a/Cargo.lock b/Cargo.lock index 64f19e813..5cc15171a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -183,6 +183,7 @@ dependencies = [ "env_param", "idmap", "itertools", + "num-rational", "smallvec", "tracing", ] diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 40482eaeb..9d4e7269f 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -1,6 +1,7 @@ //! A number of utility functions for converting from `planx` to `aries-timelines` pub mod constraints; +pub mod encoding; pub mod required_values; use aries::{ diff --git a/planning/engine/src/encode/encoding.rs b/planning/engine/src/encode/encoding.rs new file mode 100644 index 000000000..c3b4361da --- /dev/null +++ b/planning/engine/src/encode/encoding.rs @@ -0,0 +1,114 @@ +use std::fmt::Display; + +use aries::{core::state::Evaluable, prelude::*}; +use itertools::Itertools; +use planx::ActionRef; +use timelines::{Sym, Time, symbols::ObjectDecoder}; + +use crate::plans::Operation; + +/// Representation of the encoding that allows reconstructing a solution plan from a valid assignment. +#[derive(Default)] +pub struct Encoding { + pub actions: Vec, +} + +impl Encoding { + pub fn new() -> Self { + Encoding { actions: vec![] } + } + + pub fn add_action(&mut self, instance: ActionInstance) { + self.actions.push(instance); + } + + /// Extracts the plan corresponding to this solution. + pub fn plan<'a>(&'a self, solution: &'a Solution) -> Plan<'a> { + Plan { + encoding: self, + solution, + } + } +} + +/// A plan that can be formatted in the PDDL format. +pub struct Plan<'a> { + encoding: &'a Encoding, + solution: &'a Solution, +} + +impl<'a> Display for Plan<'a> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!( + f, + "{}", + self.encoding + .actions + .iter() + .filter_map(|a| a.evaluate(self.solution)) + .sorted_by_key(|a| a.start) + .format("\n") + ) + } +} + +/// An action instance in the encoding, containing all variables necessary +/// to determine whether it appears in the solution and its timings and parameters. +pub struct ActionInstance { + pub action_ref: ActionRef, + pub prez: Lit, + pub start: Time, + pub end: Time, + pub arguments: Vec, +} + +impl Evaluable for ActionInstance { + type Value = Operation; + + fn evaluate(&self, solution: &Solution) -> Option { + if !solution.entails(self.prez) { + return None; + } + // the presence variable is true, so we can mindlessly evaluate all the sub-expression + // that are guaranteed to be present. + let start = solution.eval(self.start).unwrap(); + let duration = solution.eval(self.end).unwrap() - start; + Some(Operation { + start, + duration, + action_ref: self.action_ref.clone(), + arguments: self + .arguments + .iter() + .map(|arg_var| arg_var.evaluate(solution).unwrap()) + .collect(), + span: None, + }) + } +} + +/// A variable whose domain is a subset of the objects in the problem. +#[derive(Clone)] +pub struct ObjectVar { + var: IAtom, + decoder: ObjectDecoder, +} + +impl ObjectVar { + pub fn new(var: impl Into, decoder: &ObjectDecoder) -> Self { + Self { + var: var.into(), + decoder: decoder.clone(), + } + } +} + +impl Evaluable for ObjectVar { + type Value = Sym; + + fn evaluate(&self, solution: &Solution) -> Option { + self.var + .evaluate(solution) + .map(|val| self.decoder.decode(val).unwrap().clone()) + } +} diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index 345976c41..524fdbd92 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -2,7 +2,11 @@ use std::{collections::BTreeMap, time::Instant}; use aries::prelude::*; use aries_plan_engine::{ - encode::{required_values::RequiredValues, *}, + encode::{ + encoding::{ActionInstance, Encoding, ObjectVar}, + required_values::RequiredValues, + *, + }, plans::lifted_plan::{self, LiftedPlan}, }; use derive_more::derive::Display; @@ -33,12 +37,13 @@ pub enum Objective { pub fn optimize_plan(model: &Model, plan: &LiftedPlan, options: &Options) -> Res<()> { let start = Instant::now(); - let mut solver = encode_plan_optimization_problem(model, plan, options)?; + let (mut solver, encoding) = encode_plan_optimization_problem(model, plan, options)?; let _encoding_time = start.elapsed().as_millis(); - if let Some(_solution) = solver.check_satisfiability() { - println!("Plan is valid."); + if let Some(solution) = solver.check_satisfiability() { + println!("\n> Problem is satifiable: (non-optimized plan)"); + println!("{}\n", encoding.plan(&solution)); return Ok(()); } else { println!("Invalid plan"); @@ -50,9 +55,12 @@ pub fn encode_plan_optimization_problem( model: &Model, lifted_plan: &LiftedPlan, _options: &Options, // TODO: use those -) -> Res> { +) -> Res<(ExplainableSolver, Encoding)> { + let mut encoding = Encoding::new(); + // build encoding of all objects: associates each object to a int value and each type to a range of values let objs = types(model); + let object_decoder = objs.decoder(); let mut sched = timelines::Sched::new(1, objs); let global_scope = Scope::global(&sched); @@ -125,6 +133,18 @@ pub fn encode_plan_optimization_problem( presence: Lit::TRUE, // TODO: action is necessarily present!! args, }; + // add the action to the encoding so we can retrieve it later + encoding.add_action(ActionInstance { + action_ref: a.name.clone(), + prez: bindings.presence, + start: bindings.start, + end: bindings.end, + arguments: bindings + .args + .values() + .map(|var| ObjectVar::new(*var, &object_decoder)) + .collect(), + }); // for each condition, create a constraint stating it should hold. The constraint is tagged so we can later deactivate it for c in a.conditions.iter() { @@ -200,5 +220,5 @@ pub fn encode_plan_optimization_problem( let constraint_to_repair = |_cid: ConstraintID| None; - Ok(sched.explainable_solver(constraint_to_repair)) + Ok((sched.explainable_solver(constraint_to_repair), encoding)) } diff --git a/planning/engine/src/plans/lifted_plan.rs b/planning/engine/src/plans/lifted_plan.rs index 79cc317ae..d710c1ee1 100644 --- a/planning/engine/src/plans/lifted_plan.rs +++ b/planning/engine/src/plans/lifted_plan.rs @@ -1,5 +1,6 @@ use std::collections::BTreeMap; +use aries::core::QCst; use planx::{Model, Res, Sym}; use timelines::IntCst; @@ -80,8 +81,8 @@ pub fn parse_lifted_plan(plan: &planx::pddl::Plan, model: &Model) -> Res { pub start: Instant, @@ -17,3 +25,17 @@ pub struct Operation { #[allow(unused)] pub span: Option, } + +impl Display for Operation { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "{:>4}: ({}{}{}) [{}]", + self.start, + self.action_ref, + if self.arguments.is_empty() { "" } else { " " }, + self.arguments.iter().format(" "), + self.duration + ) + } +} diff --git a/planning/engine/src/validate.rs b/planning/engine/src/validate.rs index b031a6ace..70c520a5d 100644 --- a/planning/engine/src/validate.rs +++ b/planning/engine/src/validate.rs @@ -13,7 +13,7 @@ pub fn validate(model: &Model, plan: &LiftedPlan, _options: &Options) -> Res IntCst { self.objects.len() as IntCst } + + /// Builds a decoder that allows retrieving the object from its ID. + /// + /// Note: the decoder is heavy to compute but cheap to clone. Best if constructed only once. + pub fn decoder(&self) -> ObjectDecoder { + let id_to_object: BTreeMap = self.objects.iter().map(|(obj, id)| (*id, obj.clone())).collect(); + ObjectDecoder { + decoder: Arc::new(id_to_object), + } + } +} + +/// Mapping from object ID to object names. +/// +/// Note: This datastructure is cheaply clonable. +#[derive(Clone)] +pub struct ObjectDecoder { + decoder: Arc>, +} + +impl ObjectDecoder { + pub fn decode(&self, id: IntCst) -> Option<&Sym> { + self.decoder.get(&id) + } } diff --git a/solver/src/core/cst.rs b/solver/src/core/cst.rs index 33f4c7394..d25c0a2b9 100644 --- a/solver/src/core/cst.rs +++ b/solver/src/core/cst.rs @@ -11,6 +11,9 @@ mod types { /// Name of the `IntCst` underlying type pub const INT_TYPE_NAME: &str = "i32"; + + /// Type representing a rational constant. + pub type QCst = num_rational::Rational32; } #[cfg(all(feature = "i64", not(feature = "i128")))] @@ -23,6 +26,9 @@ mod types { /// Name of the `IntCst` underlying type pub const INT_TYPE_NAME: &str = "i64"; + + /// Type representing a rational constant. + pub type QCst = num_rational::Rational64; } #[cfg(feature = "i128")] @@ -35,6 +41,9 @@ mod types { /// Name of the `IntCst` underlying type pub const INT_TYPE_NAME: &str = "i128"; + + /// Type representing a rational constant. + pub type QCst = num_rational::BigRational; } /// Convert IntCst to LongCst diff --git a/solver/src/model/lang/fixed.rs b/solver/src/model/lang/fixed.rs index e3b5b959f..a8b97e862 100644 --- a/solver/src/model/lang/fixed.rs +++ b/solver/src/model/lang/fixed.rs @@ -1,4 +1,5 @@ -use crate::core::{IntCst, VarRef}; +use crate::core::views::{Dom, Term, VarView}; +use crate::core::{IntCst, QCst, VarRef}; use crate::model::lang::{ConversionError, IAtom, IVar}; use num_rational::Ratio; use std::cmp::Ordering; @@ -59,6 +60,24 @@ pub struct FAtom { pub num: IAtom, pub denom: IntCst, } +impl VarView for FAtom { + type Value = QCst; + + fn upper_bound(&self, dom: impl Dom) -> Self::Value { + debug_assert!(self.denom > 0); + QCst::new(self.num.upper_bound(dom), self.denom) + } + + fn lower_bound(&self, dom: impl Dom) -> Self::Value { + debug_assert!(self.denom > 0); + QCst::new(self.num.lower_bound(dom), self.denom) + } +} +impl Term for FAtom { + fn variable(self) -> VarRef { + self.num.variable() + } +} //Implement Debug for FAtom // `?` represents a variable From 0c7cb6534e36dff9f90a6fdcbfbc98397bb0ae56 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 11:30:26 +0200 Subject: [PATCH 04/43] chore(solver): consistently set `QCst` to `Ratio` --- planning/timelines/src/rational.rs | 2 +- solver/src/core/cst.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/planning/timelines/src/rational.rs b/planning/timelines/src/rational.rs index 371c79f39..efb7103bf 100644 --- a/planning/timelines/src/rational.rs +++ b/planning/timelines/src/rational.rs @@ -1,7 +1,7 @@ use aries::model::lang::FAtom; /// A rational constant -pub type QCst = num_rational::Rational32; +pub type QCst = aries::core::QCst; /// A rational atom pub type QAtom = FAtom; diff --git a/solver/src/core/cst.rs b/solver/src/core/cst.rs index d25c0a2b9..3df1d7062 100644 --- a/solver/src/core/cst.rs +++ b/solver/src/core/cst.rs @@ -43,7 +43,7 @@ mod types { pub const INT_TYPE_NAME: &str = "i128"; /// Type representing a rational constant. - pub type QCst = num_rational::BigRational; + pub type QCst = num_rational::Ratio; } /// Convert IntCst to LongCst From e5ed14a120f1ff3f31ab71326c1d49c1b634b7d1 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 17:09:13 +0200 Subject: [PATCH 05/43] fix(timelines): make sure we respect optionality of the constraint --- planning/timelines/src/explain.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/planning/timelines/src/explain.rs b/planning/timelines/src/explain.rs index f0c448188..6d10853e2 100644 --- a/planning/timelines/src/explain.rs +++ b/planning/timelines/src/explain.rs @@ -32,12 +32,12 @@ impl ExplainableSolver { let l = if let Some(l) = trigger.get(&tag) { *l } else { - let l = encoding.new_literal(Lit::TRUE); + let l = encoding.new_literal(Lit::TRUE); // could we use the conjunctive scope directly? assumptions_map.insert(l, tag.clone()); trigger.insert(tag, l); l }; - c.enforce_if(l, sched, &mut encoding); + c.opt_enforce_if(l, sched, &mut encoding); } else { c.enforce(sched, &mut encoding); } From b6d13bcb9b774c6a4b9b5a5eca2fa37030a3a0d0 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 17:38:11 +0200 Subject: [PATCH 06/43] chore(solver): Generalize optimization API to support assumptions. --- solver/src/solver/solver_impl.rs | 127 ++++++++++++++++++------------- 1 file changed, 73 insertions(+), 54 deletions(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 22009ed54..d626f3c79 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -2,7 +2,7 @@ use crate::backtrack::{Backtrack, DecLvl}; use crate::collections::set::IterableRefSet; use crate::core::literals::{Disjunction, Lits}; use crate::core::state::*; -use crate::core::views::Dom; +use crate::core::views::{Boundable, Dom, Term, VarView}; use crate::core::*; use crate::model::extensions::{DisjunctionExt, DomainsExt, Shaped}; use crate::model::lang::IAtom; @@ -764,35 +764,8 @@ impl Solver { assumptions: &[Lit], limit: SearchLimit, ) -> Result, Exit> { - // make sure brancher has knowledge of all variables. - self.brancher.import_vars(&self.model); - - assert_eq!(self.decision_level, DecLvl::ROOT); - - match self.propagate_and_backtrack_to_consistent() { - Ok(()) => (), - Err(conflict) => { - // conflict at root, return empty unsat core - debug_assert!(conflict.is_empty()); - return Ok(Err(Explanation::new())); - } - }; - for &lit in assumptions { - if let Err(unsat_core) = self.assume_and_propagate(lit) { - return Ok(Err(unsat_core)); - } - } - match self.search(limit)? { - SearchResult::AtSolution => Ok(Ok(self.model.state.extract_solution())), - SearchResult::ExternalSolution(s) => Ok(Ok(s)), - SearchResult::Unsat(conflict) => { - let unsat_core = self - .model - .state - .extract_unsat_core_after_conflict(conflict, &mut self.reasoners); - Ok(Err(unsat_core)) - } - } + // delegate to optimization with a constant objective + self.minimize_with_assumptions(VarRef::ZERO, assumptions, limit, |_sol| {}) } /// Returns an iterable datastructure for computing all MUS and MCS. @@ -957,14 +930,54 @@ impl Solver { ) -> Result, Exit> { assert_eq!(self.decision_level, DecLvl::ROOT); assert_eq!(self.last_assumption_level, DecLvl::ROOT); - // best solution found so far - let mut best = None; - if self.post_constraints().is_err() || self.propagate().is_err() { - // trivially UNSAT - return Ok(None); + let opt_var = if minimize { + SignedVar::plus(objective.var.variable()) + } else { + SignedVar::minus(objective.var.variable()) + }; + if let Ok(sol) = + self.minimize_with_assumptions(opt_var, &[], limit, |sol| on_new_solution(sol.lb(objective), sol))? + { + Ok(Some((sol.lb(objective), sol))) + } else { + Ok(None) } + } + /// Solves the minimization problem under the given assumptions. + /// In case of unsatisfiability, returns an unsat core (composed of these assumptions). + /// + /// A callback can be given that will be invoked on each new solution with an improved cost, as soon as it is discovered. + /// + /// Invariant: the solver must be at the root decision level (meaning that there must be no prior assumptions/decisions on the stack) + pub fn minimize_with_assumptions + VarView>( + &mut self, + objective: ObjVar, + assumptions: &[Lit], + limit: SearchLimit, + mut on_new_solution: impl FnMut(&Solution), + ) -> Result, Exit> { + // make sure brancher has knowledge of all variables. + self.brancher.import_vars(&self.model); + + assert_eq!(self.decision_level, DecLvl::ROOT); + + match self.propagate_and_backtrack_to_consistent() { + Ok(()) => (), + Err(conflict) => { + // conflict at root, return empty unsat core + debug_assert!(conflict.is_empty()); + return Ok(Err(Explanation::new())); + } + }; + for &lit in assumptions { + if let Err(unsat_core) = self.assume_and_propagate(lit) { + return Ok(Err(unsat_core)); + } + } + // best solution found so far + let mut best = None; loop { let sol = match self.search(limit)? { SearchResult::AtSolution => { @@ -972,29 +985,37 @@ impl Solver { // notify other solvers that we have found a new solution let sol = self.model.state.extract_solution(); self.sync.notify_solution_found(sol.clone()); - let objective_value = sol.lb(objective); + let objective_value = sol.lb(&objective); if STATS_AT_SOLUTION.get() { println!("********* New sol: {objective_value} *********"); self.print_stats(); } - on_new_solution(objective_value, &sol); + on_new_solution(&sol); sol } SearchResult::ExternalSolution(sol) => sol, // a solution was handed to us by another solver - SearchResult::Unsat(_conflict) => return Ok(best), // exhausted search space under the current wuality assumptions + SearchResult::Unsat(conflict) => { + // exhausted search space under the current quality assumptions + // 1) if we have a solution return it + // 2) otherwise, the problem is unsatisfiable and we return the corresponding UNSAT core + return match best { + Some((_obj, best)) => Ok(Ok(best)), + None => { + let unsat_core = self + .model + .state + .extract_unsat_core_after_conflict(conflict, &mut self.reasoners); + Ok(Err(unsat_core)) + } + }; + } }; // determine whether the solution found is an improvement on the previous one (might not be the case if sent by another solver) - let objective_value = sol.lb(objective); + let objective_value = sol.lb(&objective); let is_improvement = match best { None => true, - Some((previous_best, _)) => { - if minimize { - objective_value < previous_best - } else { - objective_value > previous_best - } - } + Some((previous_best, _)) => objective_value < previous_best, }; if is_improvement { @@ -1007,16 +1028,14 @@ impl Solver { // save the best solution best = Some((objective_value, sol)); - // force future solutions to improve on this one - let improvement_literal = if minimize { - objective.lt_lit(objective_value) - } else { - objective.gt_lit(objective_value) - }; + // literal that forces future solutions to improve on this one + let improvement_literal = objective.leq(objective_value - 1); + + // undo any decision and post a new assumption that the objective is improved self.reset_search(); match self.assume_and_propagate(improvement_literal) { Ok(_) => {} - Err(_unsat_core) => return Ok(best), // no way to improve this bound + Err(_unsat_core) => return Ok(Ok(best.unwrap().1)), // no way to improve this bound } } } @@ -1068,7 +1087,7 @@ impl Solver { } /// Posts an assumptions on a new decision level, run all propagators and returns an `UnsatCore` - /// if the assumptions turns out to be incompatibly with previous ones. + /// if the assumptions turns out to be incompatible with previous ones. /// /// If the assumption is accepted returns an `Ok(x)` result where is true if the assumption was not already entailed /// (i.e. something changed in the domains). From 5962691894ca257598c4eec264bb14f8c3deeb26 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 17:38:55 +0200 Subject: [PATCH 07/43] chore(solver): implement `Evaluable` for `LinearSum` --- solver/src/model/lang/linear.rs | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs index 7e91d70ed..2a7207af7 100644 --- a/solver/src/model/lang/linear.rs +++ b/solver/src/model/lang/linear.rs @@ -1,6 +1,7 @@ use num_integer::lcm; -use crate::core::{IntCst, Lit, VarRef}; +use crate::core::state::Evaluable; +use crate::core::{IntCst, Lit, QCst, VarRef}; use crate::model::lang::{IAtom, IVar, ValidityScope}; use crate::reif::ReifExpr; use std::collections::BTreeMap; @@ -406,10 +407,34 @@ use crate::transitive_conversion; use super::{Atom, ConversionError, FAtom}; transitive_conversion!(LinearSum, LinearTerm, IVar); +impl Evaluable for LinearSum { + type Value = QCst; + + fn evaluate(&self, solution: &crate::prelude::Solution) -> Option { + let mut sum = QCst::new(self.constant, self.denom); + for term in &self.terms { + // add the contribution of each term, BUT + // we shortcircuit and return None if the term is absent + sum += term.evaluate(solution)?; + } + Some(sum) + } +} + +impl Evaluable for LinearTerm { + type Value = QCst; + + fn evaluate(&self, solution: &crate::prelude::Solution) -> Option { + let var_value = self.var.evaluate(solution)?; + Some(QCst::new(self.factor, self.denom) * QCst::from_integer(var_value)) + } +} + /* ========================================================================== */ /* LinearLeq */ /* ========================================================================== */ +#[derive(Clone)] pub struct LinearLeq { sum: LinearSum, ub: IntCst, From d65eb028eee1e940fa2917580850800157b5279f Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 17:39:58 +0200 Subject: [PATCH 08/43] chore(solver): Implement `BoolExpr` for `LinearLeq` --- solver/src/model/lang/hreif.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/solver/src/model/lang/hreif.rs b/solver/src/model/lang/hreif.rs index 2fad9ffff..f3d2c9385 100644 --- a/solver/src/model/lang/hreif.rs +++ b/solver/src/model/lang/hreif.rs @@ -4,7 +4,10 @@ use crate::{ core::{IntCst, Lit, VarRef, views::Term}, model::{ Label, Model, - lang::expr::{And, Leq, Or, or}, + lang::{ + expr::{And, Leq, Or, or}, + linear::LinearLeq, + }, }, prelude::DomainsExt, reif::ReifExpr, @@ -175,6 +178,7 @@ crate::impl_reif!(Lit); crate::impl_reif!(Or); crate::impl_reif!(And); crate::impl_reif!(Leq); +crate::impl_reif!(LinearLeq); #[macro_export] macro_rules! impl_reif { From ca1a38ad080868fb2802f1beb1b03f0f7d0bd63c Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 18:05:23 +0200 Subject: [PATCH 09/43] chore(planx): add span information to goals --- planning/planx/src/goals.rs | 13 ++++++++++++- planning/planx/src/pddl/convert.rs | 10 ++++++---- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/planning/planx/src/goals.rs b/planning/planx/src/goals.rs index 8f8e9c2f5..798a09205 100644 --- a/planning/planx/src/goals.rs +++ b/planning/planx/src/goals.rs @@ -2,12 +2,16 @@ use std::fmt::Display; use itertools::Itertools; -use crate::{Condition, Env, ExprId, Param, RealValue, Sym, TimeInterval, Timestamp}; +use crate::{ + Condition, Env, ExprId, Param, RealValue, Sym, TimeInterval, Timestamp, + errors::{Span, Spanned}, +}; #[derive(Debug, Clone)] pub struct Goal { pub universal_quantification: Vec, pub goal_expression: SimpleGoal, + pub span: Option, } impl<'a> Display for Env<'a, &Goal> { @@ -24,6 +28,12 @@ impl<'a> Display for Env<'a, &Goal> { } } +impl<'a> Spanned for Env<'a, &Goal> { + fn span(&self) -> Option<&Span> { + self.elem.span.as_ref() + } +} + /// Represents a goal statement (in PDDL goal or constraints). /// /// - Regular PDDL goals (expressions that msut hold in the final state) are encoded as @@ -66,6 +76,7 @@ impl SimpleGoal { Goal { universal_quantification: vars, goal_expression: self, + span: None, } } } diff --git a/planning/planx/src/pddl/convert.rs b/planning/planx/src/pddl/convert.rs index e7d0aea7c..187f67a9a 100644 --- a/planning/planx/src/pddl/convert.rs +++ b/planning/planx/src/pddl/convert.rs @@ -618,16 +618,18 @@ pub fn parse_goal( env: &mut Environment, bindings: &Rc, ) -> Result { - if let Some([vars, sexpr]) = sexpr.as_application("forall") + let mut g = if let Some([vars, sexpr]) = sexpr.as_application("forall") && !at_horizon { // (forall (?x - loc ?y - obj) ) let vars = parse_var_list(vars, env)?; let bindings = Rc::new(Bindings::stacked(&vars, bindings)); - parse_unquantified_goal(sexpr, at_horizon, env, &bindings).map(|g| g.forall(vars)) + parse_unquantified_goal(sexpr, at_horizon, env, &bindings).map(|g| g.forall(vars))? } else { - parse_unquantified_goal(sexpr, at_horizon, env, bindings).map(|g| g.forall(vec![])) - } + parse_unquantified_goal(sexpr, at_horizon, env, bindings).map(|g| g.forall(vec![]))? + }; + g.span = sexpr.span().cloned(); + Ok(g) } /// Parses a goal (at_horizon=true) of constraint (at_horizon=false), without a forall From cd43f6450e45b6cbea17d0df878ba7c1ccbf128b Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 18:17:31 +0200 Subject: [PATCH 10/43] feat(timelines): add optimization interface to explanable solver. --- planning/timelines/src/explain.rs | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/planning/timelines/src/explain.rs b/planning/timelines/src/explain.rs index 6d10853e2..4463be669 100644 --- a/planning/timelines/src/explain.rs +++ b/planning/timelines/src/explain.rs @@ -1,5 +1,6 @@ use std::collections::{BTreeMap, BTreeSet}; +use aries::model::lang::FAtom; use aries::prelude::*; use aries::{ backtrack::Backtrack, @@ -57,10 +58,22 @@ impl ExplainableSolver { .solve_with_assumptions(&assumptions, aries::solver::SearchLimit::None) .unwrap() .ok(); - self.solver.print_stats(); + // self.solver.print_stats(); self.solver.reset(); // TODO: this should not be needed res } + /// + /// Check if the model is satifiable with all assumptions, and returns a solution if it is. + pub fn find_optimal(&mut self, obj: FAtom, on_new_solution: impl FnMut(&Solution)) -> Option { + let assumptions = self.enablers.keys().copied().collect_vec(); + let res = self + .solver + .minimize_with_assumptions(obj.num, &assumptions, aries::solver::SearchLimit::None, on_new_solution) + .unwrap(); + // self.solver.print_stats(); + self.solver.reset(); // TODO: this should not be needed + res.ok() + } /// Returns an iterator over all MUS and MCS in the model. pub fn explain_unsat<'x>(&'x mut self) -> impl Iterator> + 'x { @@ -71,6 +84,14 @@ impl ExplainableSolver { .map(move |mm| mm.project(projection)) } + /// Returns an iterator over all MUS (Minimal Unsatifiable Subsets) in the model. + pub fn muses(&mut self) -> impl Iterator> + '_ { + self.explain_unsat().filter_map(|mus_mcs| match mus_mcs { + MusMcs::Mus(mus) => Some(mus), + MusMcs::Mcs(_) => None, + }) + } + /// Returns the smallest MCS over all assumptions pub fn find_smallest_mcs(&mut self) -> Option> { let assumptions = self.enablers.keys().copied().collect_vec(); From e06703adeb85c25b35109c96ae99573ac06e8270 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 18:19:51 +0200 Subject: [PATCH 11/43] feat(ape): optimization of plan-length + explanations of unsat --- planning/engine/src/encode.rs | 1 + planning/engine/src/encode/encoding.rs | 23 +++-- planning/engine/src/encode/tags.rs | 55 ++++++++++++ planning/engine/src/main.rs | 7 +- planning/engine/src/optimize_plan.rs | 109 ++++++++++++++++++----- planning/engine/src/plans/lifted_plan.rs | 19 +++- planning/engine/src/plans/operation.rs | 11 ++- 7 files changed, 194 insertions(+), 31 deletions(-) create mode 100644 planning/engine/src/encode/tags.rs diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 9d4e7269f..795b5453e 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -3,6 +3,7 @@ pub mod constraints; pub mod encoding; pub mod required_values; +pub mod tags; use aries::{ core::literals::ConjunctionBuilder, diff --git a/planning/engine/src/encode/encoding.rs b/planning/engine/src/encode/encoding.rs index c3b4361da..8c4bb231d 100644 --- a/planning/engine/src/encode/encoding.rs +++ b/planning/engine/src/encode/encoding.rs @@ -1,27 +1,40 @@ -use std::fmt::Display; +use std::{collections::BTreeMap, fmt::Display}; -use aries::{core::state::Evaluable, prelude::*}; +use aries::{core::state::Evaluable, model::lang::FAtom, prelude::*}; use itertools::Itertools; use planx::ActionRef; -use timelines::{Sym, Time, symbols::ObjectDecoder}; +use timelines::{ConstraintID, Sym, Time, symbols::ObjectDecoder}; -use crate::plans::Operation; +use crate::{encode::tags::Tag, plans::Operation}; /// Representation of the encoding that allows reconstructing a solution plan from a valid assignment. #[derive(Default)] pub struct Encoding { + /// All actions instances that may appear in the plan. pub actions: Vec, + /// Variable encoding the objective value (minimization) + pub objective: Option, + /// for each relaxable constraint, stores a constraint tag so that we can later decide if it should be relaxed. + pub constraints_tags: BTreeMap, } impl Encoding { pub fn new() -> Self { - Encoding { actions: vec![] } + Encoding { + actions: vec![], + objective: None, + constraints_tags: Default::default(), + } } pub fn add_action(&mut self, instance: ActionInstance) { self.actions.push(instance); } + pub fn set_objective(&mut self, objective: impl Into) { + self.objective = Some(objective.into()) + } + /// Extracts the plan corresponding to this solution. pub fn plan<'a>(&'a self, solution: &'a Solution) -> Plan<'a> { Plan { diff --git a/planning/engine/src/encode/tags.rs b/planning/engine/src/encode/tags.rs new file mode 100644 index 000000000..906008225 --- /dev/null +++ b/planning/engine/src/encode/tags.rs @@ -0,0 +1,55 @@ +use std::collections::BTreeSet; + +use planx::{ActionRef, Message, Model, errors::Spanned}; + +use crate::plans::lifted_plan::LiftedPlan; + +/// Tag for a cosntraint imposed in the scheduling model +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] +pub enum Tag { + /// Constraint enforcing the i-th goal + EnforceGoal(usize), + /// Constraint enforcing the given condition of the i-th operator (action in the plan) + Support { operator_id: usize, cond: ActionCondition }, +} + +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)] +pub struct ActionCondition { + /// Name of the action in which the condition appears + pub action: ActionRef, + /// Index of the condition in the action. + pub condition_id: usize, +} + +/// Extends a base bessage to display all culprits in it. +pub fn format_culprit_set(mut msg: Message, culprits: &BTreeSet, model: &Model, plan: &LiftedPlan) -> Message { + for culprit in culprits { + match culprit { + Tag::EnforceGoal(g) => { + let g = &model.goals[*g]; + let g = model.env.node(g); + let annot = g.error("Unsatisfied goal"); + msg = msg.snippet(annot); + } + Tag::Support { operator_id, cond } => { + let operator = &plan.operations[*operator_id]; + let annot = operator.error(format!("non applicable (operator #{operator_id})")); + msg = msg.snippet(annot); + // for all previous operators in the plan, display them if they have span (indicating they were read from a file) + for prev in &plan.operations[..*operator_id] { + if let Some(prev_span) = prev.span.as_ref() { + msg = msg.show(prev_span) + } + } + let action = model.actions.get_action(&cond.action).unwrap(); + let cond_expr = action.conditions[cond.condition_id].cond; + let annot = model + .env + .node(cond_expr) + .info(format!("unsatisfiable condition for operator {operator_id}")); + msg = msg.snippet(annot).show(cond.action.span.as_ref().unwrap()); + } + } + } + msg +} diff --git a/planning/engine/src/main.rs b/planning/engine/src/main.rs index c4ebde1b3..fe6015b15 100644 --- a/planning/engine/src/main.rs +++ b/planning/engine/src/main.rs @@ -189,7 +189,7 @@ fn validate_plan(command: &Validate) -> Res<()> { let model = pddl::build_model(&dom, &pb)?; let plan = lifted_plan::parse_lifted_plan(&plan, &model)?; println!("{model}"); - println!("{plan:?}"); + println!("\n===== Plan ====\n\n{plan}\n"); let valid = validate::validate(&model, &plan, &command.options)?; if valid { @@ -213,10 +213,9 @@ fn optimize_plan(command: &OptimizePlan) -> Res<()> { let model = pddl::build_model(&dom, &pb)?; let plan = lifted_plan::parse_lifted_plan(&plan, &model)?; println!("{model}"); - println!("{plan:?}"); + println!("\n===== Plan ====\n\n{plan}\n"); - optimize_plan::optimize_plan(&model, &plan, &command.options)?; - todo!() + optimize_plan::optimize_plan(&model, &plan, &command.options) } fn repair(command: &DomRepair) -> Res<()> { diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index 524fdbd92..dc0571100 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -1,10 +1,15 @@ use std::{collections::BTreeMap, time::Instant}; -use aries::prelude::*; +use aries::{ + core::state::Evaluable, + model::lang::{FAtom, hreif::Store, linear::LinearSum}, + prelude::*, +}; use aries_plan_engine::{ encode::{ encoding::{ActionInstance, Encoding, ObjectVar}, required_values::RequiredValues, + tags::{ActionCondition, Tag, format_culprit_set}, *, }, plans::lifted_plan::{self, LiftedPlan}, @@ -12,9 +17,9 @@ use aries_plan_engine::{ use derive_more::derive::Display; use itertools::Itertools; use planx::{ActionRef, Model, Param, Res, Sym, errors::*}; -use timelines::{ConstraintID, SymAtom, Time, boxes::Segment, explain::ExplainableSolver}; +use timelines::{ConstraintID, Sched, SymAtom, Time, boxes::Segment, explain::ExplainableSolver}; -pub type RelaxableConstraint = (); +pub type RelaxableConstraint = Tag; #[derive(clap::Args, Debug, Clone)] pub struct Options { @@ -25,12 +30,12 @@ pub struct Options { pub objective: Objective, } -#[derive(clap::ValueEnum, Debug, Clone, Copy, Display)] +#[derive(clap::ValueEnum, Debug, Clone, Copy, Display, PartialEq, PartialOrd, Eq, Ord)] pub enum Relaxation { ActionPresence, } -#[derive(clap::ValueEnum, Debug, Clone, Copy, Display)] +#[derive(clap::ValueEnum, Debug, Clone, Copy, Display, PartialEq, Eq, PartialOrd, Ord)] pub enum Objective { PlanLength, } @@ -41,20 +46,30 @@ pub fn optimize_plan(model: &Model, plan: &LiftedPlan, options: &Options) -> Res let _encoding_time = start.elapsed().as_millis(); - if let Some(solution) = solver.check_satisfiability() { - println!("\n> Problem is satifiable: (non-optimized plan)"); - println!("{}\n", encoding.plan(&solution)); - return Ok(()); + let objective = encoding.objective.unwrap(); //TODO: error message + + let print = |sol: &Solution| { + println!("==== Plan (objective: {}) =====", objective.evaluate(sol).unwrap()); + println!("{}\n", encoding.plan(sol)); + }; + + if let Some(solution) = solver.find_optimal(objective, &print) { + println!("\n> Found optimal solution:"); + print(&solution); } else { - println!("Invalid plan"); + println!("No solution !!!!"); + for mus in solver.muses() { + let msg = format_culprit_set(Message::error("Invalid in all relaxation"), &mus, model, plan); + println!("\n{msg}\n"); + } } - todo!() + Ok(()) } pub fn encode_plan_optimization_problem( model: &Model, lifted_plan: &LiftedPlan, - _options: &Options, // TODO: use those + options: &Options, ) -> Res<(ExplainableSolver, Encoding)> { let mut encoding = Encoding::new(); @@ -96,7 +111,7 @@ pub fn encode_plan_optimization_problem( // initial processing of all operations // we create its scope (binding of timepoints, params, ...) and process its conditions // Effects are defered to a later point - for op in lifted_plan.operations.iter() { + for (op_id, op) in lifted_plan.operations.iter().enumerate() { // corresponding action in the model let a = model .actions @@ -126,11 +141,16 @@ pub fn encode_plan_optimization_problem( // add argument to the bindings args.insert(¶m.name, arg); } + let presence = if options.relaxation.contains(&Relaxation::ActionPresence) { + sched.model.new_literal(Lit::TRUE) + } else { + Lit::TRUE + }; let bindings = Scope { start: Time::from(op.start), // start time is the index of the action in the plan end: Time::from(op.start + op.duration), - presence: Lit::TRUE, // TODO: action is necessarily present!! + presence, args, }; // add the action to the encoding so we can retrieve it later @@ -147,12 +167,22 @@ pub fn encode_plan_optimization_problem( }); // for each condition, create a constraint stating it should hold. The constraint is tagged so we can later deactivate it - for c in a.conditions.iter() { + for (cond_id, c) in a.conditions.iter().enumerate() { if let Some(tp) = c.interval.as_timestamp() { let constraint = condition_to_constraint(tp, c.cond, model, &mut sched, &bindings, Some(&mut required_values))?; - sched.add_constraint(constraint); + let cid = sched.add_constraint(constraint); + encoding.constraints_tags.insert( + cid, + Tag::Support { + operator_id: op_id, + cond: ActionCondition { + action: a.name.clone(), + condition_id: cond_id, + }, + }, + ); } } @@ -160,7 +190,7 @@ pub fn encode_plan_optimization_problem( operations_scopes.push((a, bindings)); } // for each goal, add a constraint stating it must hold (the constriant is tagged but not relaxed for domain repair) - for x in model.goals.iter() { + for (gid, x) in model.goals.iter().enumerate() { assert!(x.universal_quantification.is_empty()); match x.goal_expression { planx::SimpleGoal::HoldsDuring(time_interval, expr_id) => { @@ -174,7 +204,8 @@ pub fn encode_plan_optimization_problem( Some(&mut required_values), )?; - sched.add_constraint(constraint); + let cid = sched.add_constraint(constraint); + encoding.constraints_tags.insert(cid, Tag::EnforceGoal(gid)); } else { todo!("durative goal") } @@ -207,7 +238,6 @@ pub fn encode_plan_optimization_problem( for x in a.effects.iter() { let eff = convert_effect(x, true, model, &mut sched, bindings)?; // replace the effect presence by its enabler - assert_eq!(eff.prez, Lit::TRUE); action_effects.push(eff); } @@ -218,7 +248,46 @@ pub fn encode_plan_optimization_problem( } } - let constraint_to_repair = |_cid: ConstraintID| None; + let objective: FAtom = match options.objective { + Objective::PlanLength => { + let mut sum = LinearSum::zero(); + for (_a, scope) in &operations_scopes { + let action_prez = scope.presence; + sum += bool2int(action_prez, &sched.model) + } + reify_sum(sum, &mut sched) + } + }; + encoding.set_objective(objective); + + let tags = encoding.constraints_tags.clone(); + let constraint_to_repair = |cid: ConstraintID| tags.get(&cid).cloned(); Ok((sched.explainable_solver(constraint_to_repair), encoding)) } + +fn bool2int(b: Lit, model: &dyn Store) -> LinearSum { + let is_zero_one = model.bounds(b.variable()) == (0, 1); + if model.entails(b) { + 1.into() + } else if model.entails(!b) { + 0.into() + } else if is_zero_one && b == b.variable().geq(1) { + IVar::new(b.variable()).into() + } else if is_zero_one && b == b.variable().leq(0) { + LinearSum::constant_int(1) - IVar::new(b.variable()) // TODO: careful, the constant part is optional as well + } else { + todo!() // cannot immediately reuse the variable, create a new one and bind it + } +} + +fn reify_sum(sum: LinearSum, model: &mut Sched) -> FAtom { + let reified: FAtom = model + .model + .new_fvar(INT_CST_MIN, INT_CST_MAX, sum.denom(), "Sum reif") + .into(); + model.add_constraint(sum.clone().leq(reified)); + model.add_constraint(sum.geq(reified)); + + reified +} diff --git a/planning/engine/src/plans/lifted_plan.rs b/planning/engine/src/plans/lifted_plan.rs index d710c1ee1..96a31a4a4 100644 --- a/planning/engine/src/plans/lifted_plan.rs +++ b/planning/engine/src/plans/lifted_plan.rs @@ -1,6 +1,7 @@ -use std::collections::BTreeMap; +use std::{collections::BTreeMap, fmt::Display}; use aries::core::QCst; +use itertools::Itertools; use planx::{Model, Res, Sym}; use timelines::IntCst; @@ -13,12 +14,28 @@ pub struct LiftedPlan { /// All variables apprearing in the lifted plan, together with an inferred type (most specific one from all their appearances.) pub variables: BTreeMap, } + +impl Display for LiftedPlan { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{}", self.operations.iter().format("\n")) + } +} + #[derive(Debug, Clone)] pub enum ObjectOrVariable { Ground(planx::Object), Variable { name: Sym }, } +impl Display for ObjectOrVariable { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + ObjectOrVariable::Ground(object) => write!(f, "{object}"), + ObjectOrVariable::Variable { name } => write!(f, "{name}"), + } + } +} + /// Parse a lifted plan into our own representation. /// /// Note: we take as input a `planx::pddl::Plan` that is essentially a set of SExpr. diff --git a/planning/engine/src/plans/operation.rs b/planning/engine/src/plans/operation.rs index 0c1c60f75..bb0571dde 100644 --- a/planning/engine/src/plans/operation.rs +++ b/planning/engine/src/plans/operation.rs @@ -1,7 +1,10 @@ use std::fmt::Display; use itertools::Itertools; -use planx::{ActionRef, errors::Span}; +use planx::{ + ActionRef, + errors::{Span, Spanned}, +}; use timelines::rational::QCst; /// Absolute time, associated to an operation start/end @@ -39,3 +42,9 @@ impl Display for Operation { ) } } + +impl Spanned for Operation { + fn span(&self) -> Option<&Span> { + self.span.as_ref() + } +} From 342ed1aa801bdb93cbe3a439273b179eec5a8750 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 30 Mar 2026 18:20:31 +0200 Subject: [PATCH 12/43] feat(ape): provide explanations of plan invalidity --- planning/engine/src/validate.rs | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/planning/engine/src/validate.rs b/planning/engine/src/validate.rs index 70c520a5d..2effd45e9 100644 --- a/planning/engine/src/validate.rs +++ b/planning/engine/src/validate.rs @@ -1,5 +1,6 @@ -use aries_plan_engine::plans::lifted_plan::LiftedPlan; -use planx::{Model, Res}; +use aries::core::state::Evaluable; +use aries_plan_engine::{encode::tags::format_culprit_set, plans::lifted_plan::LiftedPlan}; +use planx::{Message, Model, Res}; use crate::optimize_plan::{self, encode_plan_optimization_problem}; @@ -13,7 +14,22 @@ pub fn validate(model: &Model, plan: &LiftedPlan, _options: &Options) -> Res Plan is valid"); + if let Some(objective) = encoding.objective { + println!("> objective: {}", objective.evaluate(&solution).unwrap()); + } + + Ok(true) + } else { + println!("Plan is INVALID!!!!"); + for mus in solver.muses() { + let msg = format_culprit_set(Message::error("INVALID PLAN"), &mus, model, plan); + println!("\n{msg}\n"); + } + println!("Plan is INVALID!!!!"); + Ok(false) + } } From a89a3915ed139c8df0fcd46cac92cb030d0ffb50 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 15:51:43 +0200 Subject: [PATCH 13/43] feat(ape): Allow relaxing timings in plan optimization. This commit also introduces support for the action-mutex constraints of PDDL in `timelines`. --- planning/engine/src/encode.rs | 10 +- planning/engine/src/optimize_plan.rs | 26 ++++- planning/engine/src/repair.rs | 22 ++++- planning/timelines/src/constraints.rs | 134 ++++++++++++++++++++------ planning/timelines/src/effects.rs | 7 +- planning/timelines/src/lib.rs | 8 -- planning/timelines/src/tasks.rs | 4 +- 7 files changed, 159 insertions(+), 52 deletions(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 795b5453e..51776e0be 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -16,7 +16,9 @@ use aries::{ }; use itertools::Itertools; use planx::{ExprId, Model, Res, Sym, TimeRef, Timestamp, errors::Spanned}; -use timelines::{Effect, EffectOp, Sched, StateVar, SymAtom, Time, constraints::HasValueAt, symbols::ObjectEncoding}; +use timelines::{ + Effect, EffectOp, Sched, StateVar, SymAtom, TaskId, Time, constraints::HasValueAt, symbols::ObjectEncoding, +}; use crate::encode::{constraints::ConditionConstraint, required_values::RequiredValues}; @@ -46,6 +48,7 @@ pub struct Scope<'a> { pub end: Time, pub presence: Lit, pub args: im::OrdMap<&'a Sym, SymAtom>, + pub source: Option, } impl<'a> Scope<'a> { pub fn global(sched: &Sched) -> Scope<'a> { @@ -54,6 +57,7 @@ impl<'a> Scope<'a> { end: sched.horizon, presence: Lit::TRUE, args: im::OrdMap::new(), + source: None, } } } @@ -87,6 +91,7 @@ pub fn condition_to_constraint( value: Lit::TRUE.into(), timepoint: reify_timing(tp, model, sched, bindings)?, prez: bindings.presence, + source: bindings.source, }; ConditionConstraint::HasValue(c) } @@ -164,6 +169,7 @@ pub fn convert_effect( state_var: sv, operation: op, prez: bindings.presence, + source: bindings.source, }; Ok(eff) } @@ -192,6 +198,8 @@ pub fn add_closed_world_negative_effects(reqs: &RequiredValues, model: &Model, s state_var: sv, operation: EffectOp::Assign(false), prez: Lit::TRUE, + // no action source as it is part of the problem definition + source: None, }; sched.add_effect(eff); } diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index dc0571100..e1b866911 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -17,7 +17,7 @@ use aries_plan_engine::{ use derive_more::derive::Display; use itertools::Itertools; use planx::{ActionRef, Model, Param, Res, Sym, errors::*}; -use timelines::{ConstraintID, Sched, SymAtom, Time, boxes::Segment, explain::ExplainableSolver}; +use timelines::{ConstraintID, Sched, SymAtom, Task, Time, boxes::Segment, explain::ExplainableSolver, rational::QCst}; pub type RelaxableConstraint = Tag; @@ -33,6 +33,7 @@ pub struct Options { #[derive(clap::ValueEnum, Debug, Clone, Copy, Display, PartialEq, PartialOrd, Eq, Ord)] pub enum Relaxation { ActionPresence, + StartTime, } #[derive(clap::ValueEnum, Debug, Clone, Copy, Display, PartialEq, Eq, PartialOrd, Ord)] @@ -146,12 +147,29 @@ pub fn encode_plan_optimization_problem( } else { Lit::TRUE }; - + let start = if options.relaxation.contains(&Relaxation::StartTime) { + sched.new_opt_timepoint(presence) + } else { + Time::from(op.start) + }; + assert_eq!(op.duration, QCst::ZERO, "we use the start as end"); + let end = start; + + // record a task in `Sched` which + // - gives a task id (use by the condition enforcement constraints to enforce mutex conditions) + // - make the scheduler aware of the tasks when computing the makespan. + let task_id = sched.add_task(Task { + name: format!("op{op_id}"), + start, + end, + presence, + }); let bindings = Scope { - start: Time::from(op.start), // start time is the index of the action in the plan - end: Time::from(op.start + op.duration), + start, + end, presence, args, + source: Some(task_id), }; // add the action to the encoding so we can retrieve it later encoding.add_action(ActionInstance { diff --git a/planning/engine/src/repair.rs b/planning/engine/src/repair.rs index 4adc6d99e..184b8b685 100644 --- a/planning/engine/src/repair.rs +++ b/planning/engine/src/repair.rs @@ -19,7 +19,7 @@ use aries_plan_engine::{ use derive_more::derive::Display; use itertools::Itertools; use planx::{ActionRef, FluentId, Message, Model, Param, Res, Sym, errors::Spanned}; -use timelines::{ConstraintID, EffectOp, Sched, SymAtom, Time, boxes::Segment, explain::ExplainableSolver}; +use timelines::{ConstraintID, EffectOp, Sched, SymAtom, Task, Time, boxes::Segment, explain::ExplainableSolver}; use crate::{ ctags::{ActionCondition, ActionEffect, CTag, PotentialEffect, Repair}, @@ -205,12 +205,25 @@ fn encode_dom_repair(model: &Model, plan: &LiftedPlan) -> Res); impl NoOverlap { @@ -51,30 +47,6 @@ impl BoolExpr for Mutex { pub(crate) struct EffectCoherence; -impl EffectCoherence { - /// Adds the constraint that if `l` is true, then the two effects should be non-overlapping. - fn enforce_non_overlapping_if(l: Lit, e: &Effect, e2: &Effect, ctx: &Sched, store: &mut dyn Store) { - debug_assert_eq!(e.state_var.fluent, e2.state_var.fluent); - let mut disjuncts = DisjunctionBuilder::new(); - for (x1, x2) in e.state_var.args.iter().zip_eq(e2.state_var.args.iter()) { - for opt in neq(*x1, *x2).as_elementary_disjuncts(store) { - disjuncts.push(opt.implicant(ctx, store)); - if disjuncts.tautological() { - return; - } - } - } - // put last as we are more likely to be able to short circuit on the parameters - disjuncts.push(f_leq(e.mutex_end, e2.transition_start).implicant(ctx, store)); - disjuncts.push(f_leq(e2.mutex_end, e.transition_start).implicant(ctx, store)); - disjuncts.push(!e.prez); - disjuncts.push(!e2.prez); - if !disjuncts.tautological() { - or(disjuncts).opt_enforce_if(l, ctx, store); - } - } -} - impl BoolExpr for EffectCoherence { fn enforce_if(&self, l: Lit, ctx: &Sched, store: &mut dyn Store) { for e in ctx.effects.iter() { @@ -88,7 +60,23 @@ impl BoolExpr for EffectCoherence { // - broad phase: computing a bounding box of the space potentially affected by the effect and gather all overlapping boxes // - for any pair of effects with overlapping bounding boxes, add coherence constraints for (eff_id1, eff_id2) in ctx.effects.potentially_interacting_effects() { - Self::enforce_non_overlapping_if(l, &ctx.effects[eff_id1], &ctx.effects[eff_id2], ctx, store); + // ensure that the interval `(transition_start, mutex_end]` do not overlap + let eff1 = &ctx.effects[eff_id1]; + let eff2 = &ctx.effects[eff_id2]; + let itv1 = IntervalOnStateVariable { + state_var: &eff1.state_var, + start: eff1.transition_start + FAtom::EPSILON, + end: eff1.mutex_end, + presence: eff1.prez, + }; + let itv2 = IntervalOnStateVariable { + state_var: &eff2.state_var, + start: eff2.transition_start + FAtom::EPSILON, + end: eff2.mutex_end, + presence: eff2.prez, + }; + let exclu = Exclusive { a: &itv1, b: &itv2 }; + exclu.opt_enforce_if(l, ctx, store); } } @@ -104,6 +92,11 @@ pub struct HasValueAt { pub timepoint: Time, /// Presence of the condition. Must imply the presence of all variables appearing in it. pub prez: Lit, + /// Specifies if this condition originates from a particular task. + /// This is used to enforce the PDDL-mutex constraint that specifies + /// that an aciton must not rely on a value that is immediately delete by *another* action. + /// (mutex conditions). + pub source: Option, } impl HasValueAt { @@ -133,6 +126,7 @@ impl BoolExpr for HasValueAt { let value_box = self.value_box(|v| ctx.model.int_bounds(v)); + // ensures that at least one effect supports the conditions for eff_id in ctx .effects .potentially_supporting_effects(&self.state_var.fluent, value_box.as_ref()) @@ -162,9 +156,87 @@ impl BoolExpr for HasValueAt { } } or(options).opt_enforce_if(l, ctx, store); + + // PDDL mutex: a condition of an action cannot rely on a fact that is about to be modified by another action + // given the interval `[cond.start, cond.end]`, we ensure it does not meet the interval `[eff.transition_start, eff.transition_end)` + // for any effect `eff` with a different source + let itv_cond = IntervalOnStateVariable { + state_var: &self.state_var, + start: self.timepoint, + end: self.timepoint, + presence: self.prez, + }; + for eff in ctx.effects.iter() { + // TODO: here we iterate on all effects AND do a string comparison which + // may be very slow. Use bounding boxes to do a broad-phase filter + if eff.source != self.source && eff.state_var.fluent == self.state_var.fluent { + let itv_eff = IntervalOnStateVariable { + state_var: &eff.state_var, + start: eff.transition_start, + end: eff.transition_end - FAtom::EPSILON, + presence: eff.prez, + }; + dbg!(eff, self); + let exclu = Exclusive { + a: &itv_cond, + b: &itv_eff, + }; + exclu.opt_enforce_if(l, ctx, store); + } + } } fn conj_scope(&self, _ctx: &Sched, _store: &dyn Store) -> hreif::Lits { lits![self.prez] } } + +/// A closed interval `[start, end]` associated to a state variable +struct IntervalOnStateVariable<'a> { + state_var: &'a StateVar, + start: Time, + end: Time, + presence: Lit, +} + +/// Enforces that if both intervals are present and on the same state variable, +/// then their should be an epsilon separation between them: +/// +/// `!prez1 | !prez2 | sv1 != sv2 | end1 < start2 | end2 < start1` +/// +/// Note: it assumed that the two state variable share the same fluent (which is only checked in debug mode to avoid costly stirng comparisons) +struct Exclusive<'a> { + a: &'a IntervalOnStateVariable<'a>, + b: &'a IntervalOnStateVariable<'a>, +} +impl<'a> BoolExpr for Exclusive<'a> { + fn enforce_if(&self, l: Lit, ctx: &Sched, store: &mut dyn Store) { + let a = &self.a; + let b = &self.b; + debug_assert_eq!( + a.state_var.fluent, b.state_var.fluent, + "To expensive to check here, must be filtered earlier" + ); + let mut disjuncts = DisjunctionBuilder::new(); + for (x1, x2) in a.state_var.args.iter().zip_eq(b.state_var.args.iter()) { + for opt in neq(*x1, *x2).as_elementary_disjuncts(store) { + disjuncts.push(opt.implicant(ctx, store)); + if disjuncts.tautological() { + return; + } + } + } + // put last as we are more likely to be able to short circuit on the parameters + disjuncts.push(f_lt(a.end, b.start).implicant(ctx, store)); + disjuncts.push(f_lt(b.end, a.start).implicant(ctx, store)); + disjuncts.push(!a.presence); + disjuncts.push(!b.presence); + if !disjuncts.tautological() { + or(disjuncts).opt_enforce_if(l, ctx, store); + } + } + + fn conj_scope(&self, _ctx: &Sched, _store: &dyn Store) -> hreif::Lits { + lits![] + } +} diff --git a/planning/timelines/src/effects.rs b/planning/timelines/src/effects.rs index a579dfbf0..d34325f9b 100644 --- a/planning/timelines/src/effects.rs +++ b/planning/timelines/src/effects.rs @@ -9,7 +9,7 @@ use std::{ }; use crate::{ - StateVar, Time, + StateVar, TaskId, Time, boxes::{BoxRef, BoxUniverse, Segment}, }; @@ -33,6 +33,11 @@ pub struct Effect { pub operation: EffectOp, /// Presence literal indicating whether the effect is present pub prez: Lit, + /// Specifies if this effect originates from a particular task. + /// This is used to enforce the PDDL-mutex constraint that specifies + /// that an aciton must not rely on a value that is immediately delete by *another* action. + /// (mutex conditions). + pub source: Option, } #[derive(Clone, Eq, PartialEq)] pub enum EffectOp { diff --git a/planning/timelines/src/lib.rs b/planning/timelines/src/lib.rs index 2c4d9db40..b8c8e99d5 100644 --- a/planning/timelines/src/lib.rs +++ b/planning/timelines/src/lib.rs @@ -10,7 +10,6 @@ use aries::model::extensions::DomainsExt; use constraints::*; use core::fmt::Debug; use core::hash::{Hash, Hasher}; -use std::collections::HashMap; use aries::core::INT_CST_MAX; pub use aries::core::IntCst; @@ -92,7 +91,6 @@ pub struct Sched { pub makespan: Time, pub tasks: Tasks, pub effects: Effects, - tags: HashMap>, constraints: Vec, } @@ -111,16 +109,10 @@ impl Sched { makespan, tasks: Default::default(), effects: Default::default(), - tags: Default::default(), constraints: vec![Box::new(EffectCoherence)], // TODO: add default constraints (consitency, makespan), ... } } - pub fn tag(&mut self, atom: impl Into, tag: Tag) { - let atom = atom.into(); - self.tags.entry(atom).or_default().push(tag); - } - pub fn add_task(&mut self, task: Task) -> TaskId { self.tasks.insert(task) } diff --git a/planning/timelines/src/tasks.rs b/planning/timelines/src/tasks.rs index 32e7684cd..49c638d05 100644 --- a/planning/timelines/src/tasks.rs +++ b/planning/timelines/src/tasks.rs @@ -20,14 +20,12 @@ pub struct Task { pub start: Time, /// Time reference at which the task must end pub end: Time, - /// Arguments of the task - pub args: Vec, /// Presence of the task, true iff it appears in the solution pub presence: Lit, } impl Debug for Task { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "[{:?},{:?}] {:?}{:?}", self.start, self.end, self.name, self.args)?; + write!(f, "[{:?},{:?}] {:?}", self.start, self.end, self.name)?; Ok(()) } } From b487d71baf3d4014c57493e6ca4b7d7621cebc5d Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 16:19:18 +0200 Subject: [PATCH 14/43] optim(timelines): add broad-phase filtering for finding overlapping transitions. --- planning/timelines/src/constraints.rs | 10 +++-- planning/timelines/src/effects.rs | 56 ++++++++++++++++++++++++++- 2 files changed, 60 insertions(+), 6 deletions(-) diff --git a/planning/timelines/src/constraints.rs b/planning/timelines/src/constraints.rs index 748bcda86..c06d23f85 100644 --- a/planning/timelines/src/constraints.rs +++ b/planning/timelines/src/constraints.rs @@ -166,10 +166,12 @@ impl BoolExpr for HasValueAt { end: self.timepoint, presence: self.prez, }; - for eff in ctx.effects.iter() { - // TODO: here we iterate on all effects AND do a string comparison which - // may be very slow. Use bounding boxes to do a broad-phase filter - if eff.source != self.source && eff.state_var.fluent == self.state_var.fluent { + for eff_id in ctx + .effects + .potentially_overlapping_transitions(&self.state_var.fluent, value_box.as_ref()) + { + let eff = &ctx.effects[eff_id]; + if eff.source != self.source { let itv_eff = IntervalOnStateVariable { state_var: &eff.state_var, start: eff.transition_start, diff --git a/planning/timelines/src/effects.rs b/planning/timelines/src/effects.rs index d34325f9b..d768b086e 100644 --- a/planning/timelines/src/effects.rs +++ b/planning/timelines/src/effects.rs @@ -111,6 +111,19 @@ pub struct Effects { /// /// If the boxes of two effects to not overlap, they can be safely determined to never overlap (and thus do not require coherence enforcement constraints). achieved_bounding_boxes: BoxUniverse, + /// Associates every effect to a `Box` in a universe. + /// This box denotes a the set of values that the effect may support. + /// The intuition if that + /// + /// Boxes are partitioned based on their state variables (one world per state variable). + /// The box of each effect captures the space-time region it affects with dimesions: + /// + /// - time: `[lb(transition_start), ub(transition_end))` + /// - for each parameter p: + /// - `[lb(p), ub(p)]` + /// + /// If the boxes of two effects to not overlap, they can be safely determined to never overlap (and thus do not require coherence enforcement constraints). + transition_bounding_boxes: BoxUniverse, } type Segments = SmallVec<[Segment; 16]>; @@ -121,6 +134,7 @@ impl Effects { effects: Default::default(), affected_bb: BoxUniverse::new(), achieved_bounding_boxes: BoxUniverse::new(), + transition_bounding_boxes: BoxUniverse::new(), } } @@ -161,15 +175,36 @@ impl Effects { self.achieved_bounding_boxes .add_box(&eff.state_var.fluent, &buff, eff_id); + // compute and store the achievable bounding boxes + buff.clear(); + buff.push(Segment::new( + dom(eff.transition_start.num).0, + dom(eff.transition_end.num).1 - 1, + )); // TODO: careful with denom + for arg in &eff.state_var.args { + let (lb, ub) = dom(*arg); + buff.push(Segment::new(lb, ub)); + } + self.transition_bounding_boxes + .add_box(&eff.state_var.fluent, &buff, eff_id); + self.effects.push(eff); eff_id } - pub fn potentially_interacting_effects(&self) -> impl Iterator + '_ { + /// Returns a list of effects that may overlap on the state variable and overall activity period `[transition_start, mutex_end]` + pub(crate) fn potentially_interacting_effects(&self) -> impl Iterator + '_ { self.affected_bb.overlapping_boxes().map(|(e1, e2)| (*e1, *e2)) } - pub fn potentially_supporting_effects<'a>( + /// Returns a list of potentially supporting effect for a condition, representing as a bounding box with + /// the given fluents and the following segments: + /// + /// - time: `[lb(condition_start), ub(condition_end)]` + /// - for each parameter p: + /// - `[lb(p), ub(p)]` + /// - value: `[lb(value), ub(value)]` + pub(crate) fn potentially_supporting_effects<'a>( &'a self, fluent: &'a String, value_box: BoxRef<'a>, @@ -180,6 +215,23 @@ impl Effects { .find_overlapping_with(fluent, value_box) .copied() } + + /// Returns a list of effects whose transition period `[transition_start, transition_end)` may overlap a condition with the + /// the given fluents and a given value_box (same bounding box as [`Self::potentially_supporting_effects`]). + /// + /// Note that the last segment of the box (representing the value) is ignored in the lookup. + pub(crate) fn potentially_overlapping_transitions<'a>( + &'a self, + fluent: &'a String, + value_box: BoxRef<'a>, + ) -> impl Iterator + 'a { + // the same box but without the value + let box_without_value = value_box.drop_tail(1); + + self.transition_bounding_boxes + .find_overlapping_with(fluent, box_without_value) + .copied() + } } impl Default for Effects { From 352049011b5146563326abf44b785a0b117e0289 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 16:24:54 +0200 Subject: [PATCH 15/43] chore(timelines): use generic `Dom` trait instead of ad-hoc closure. --- planning/timelines/src/constraints.rs | 1 - planning/timelines/src/effects.rs | 24 ++++++++++++------------ planning/timelines/src/lib.rs | 2 +- 3 files changed, 13 insertions(+), 14 deletions(-) diff --git a/planning/timelines/src/constraints.rs b/planning/timelines/src/constraints.rs index c06d23f85..ed4640603 100644 --- a/planning/timelines/src/constraints.rs +++ b/planning/timelines/src/constraints.rs @@ -178,7 +178,6 @@ impl BoolExpr for HasValueAt { end: eff.transition_end - FAtom::EPSILON, presence: eff.prez, }; - dbg!(eff, self); let exclu = Exclusive { a: &itv_cond, b: &itv_eff, diff --git a/planning/timelines/src/effects.rs b/planning/timelines/src/effects.rs index d768b086e..3fe0ced83 100644 --- a/planning/timelines/src/effects.rs +++ b/planning/timelines/src/effects.rs @@ -1,7 +1,4 @@ -use aries::{ - core::{IntCst, Lit}, - model::lang::IAtom, -}; +use aries::{core::views::Dom, prelude::*}; use smallvec::SmallVec; use std::{ fmt::{Debug, Formatter}, @@ -146,25 +143,28 @@ impl Effects { &self.effects[eff_id] } - pub fn add_effect(&mut self, eff: Effect, dom: impl Fn(IAtom) -> (IntCst, IntCst)) -> EffectId { + pub fn add_effect(&mut self, eff: Effect, dom: impl Dom) -> EffectId { // ID of the effect will be the index of the next free slot let eff_id = self.effects.len(); let mut buff = Segments::new(); // compute and store affected bounding_box - buff.push(Segment::new(dom(eff.transition_start.num).0, dom(eff.mutex_end.num).1)); // TODO: careful with denom + buff.push(Segment::new( + dom.lb(eff.transition_start.num), + dom.ub(eff.mutex_end.num), + )); // TODO: careful with denom for arg in &eff.state_var.args { - let (lb, ub) = dom(*arg); + let (lb, ub) = dom.bounds(*arg); buff.push(Segment::new(lb, ub)); } self.affected_bb.add_box(&eff.state_var.fluent, &buff, eff_id); // compute and store the achievable bounding boxes buff.clear(); - buff.push(Segment::new(dom(eff.transition_end.num).0, dom(eff.mutex_end.num).1)); // TODO: careful with denom + buff.push(Segment::new(dom.lb(eff.transition_end.num), dom.ub(eff.mutex_end.num))); // TODO: careful with denom for arg in &eff.state_var.args { - let (lb, ub) = dom(*arg); + let (lb, ub) = dom.bounds(*arg); buff.push(Segment::new(lb, ub)); } let value_segment = match &eff.operation { @@ -178,11 +178,11 @@ impl Effects { // compute and store the achievable bounding boxes buff.clear(); buff.push(Segment::new( - dom(eff.transition_start.num).0, - dom(eff.transition_end.num).1 - 1, + dom.lb(eff.transition_start.num), + dom.ub(eff.transition_end.num) - 1, )); // TODO: careful with denom for arg in &eff.state_var.args { - let (lb, ub) = dom(*arg); + let (lb, ub) = dom.bounds(*arg); buff.push(Segment::new(lb, ub)); } self.transition_bounding_boxes diff --git a/planning/timelines/src/lib.rs b/planning/timelines/src/lib.rs index b8c8e99d5..d85a059ce 100644 --- a/planning/timelines/src/lib.rs +++ b/planning/timelines/src/lib.rs @@ -118,7 +118,7 @@ impl Sched { } pub fn add_effect(&mut self, eff: Effect) -> EffectId { - self.effects.add_effect(eff, |var| self.model.int_bounds(var)) + self.effects.add_effect(eff, &self.model) } pub fn new_timepoint(&mut self) -> Time { From 9b6f64aba6a659297c64ec3bc2c058817e4c41e3 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 17:21:54 +0200 Subject: [PATCH 16/43] chore(solver): simplify and generalize `EqMax` constraint decomposition. --- solver/src/model/lang/linear.rs | 18 +++++++++++++++++- solver/src/solver/solver_impl.rs | 29 ++++------------------------- 2 files changed, 21 insertions(+), 26 deletions(-) diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs index 2a7207af7..5b74b02c9 100644 --- a/solver/src/model/lang/linear.rs +++ b/solver/src/model/lang/linear.rs @@ -1,7 +1,7 @@ use num_integer::lcm; use crate::core::state::Evaluable; -use crate::core::{IntCst, Lit, QCst, VarRef}; +use crate::core::{IntCst, Lit, QCst, SignedVar, VarRef}; use crate::model::lang::{IAtom, IVar, ValidityScope}; use crate::reif::ReifExpr; use std::collections::BTreeMap; @@ -323,6 +323,22 @@ impl From for LinearSum { } } +impl From for LinearTerm { + fn from(value: SignedVar) -> Self { + LinearTerm { + factor: if value.is_plus() { 1 } else { -1 }, + var: IVar::new(value.variable()), + denom: 1, + } + } +} + +impl From for LinearSum { + fn from(value: SignedVar) -> Self { + LinearSum::from(LinearTerm::from(value)) + } +} + impl TryFrom for LinearSum { type Error = ConversionError; diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index d626f3c79..3b51a71fa 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -6,6 +6,7 @@ use crate::core::views::{Boundable, Dom, Term, VarView}; use crate::core::*; use crate::model::extensions::{DisjunctionExt, DomainsExt, Shaped}; use crate::model::lang::IAtom; +use crate::model::lang::linear::LinearSum; use crate::model::{Constraint, Label, Model, ModelShape}; use crate::reasoners::cp::max::{AtLeastOneGeq, MaxElem}; use crate::reasoners::{Contradiction, ReasonerId, Reasoners}; @@ -460,32 +461,10 @@ impl Solver { for item in &a.rhs { let item_scope = self.model.state.presence(item.var); debug_assert!(self.model.state.implies(item_scope, scope)); - // a.lhs >= item.var + item.cst - // a.lhs - item.var >= item.cst - // item.var - a.lhs <= -item.cst let alt_value = self.model.get_tautology_of_scope(item_scope); - if item.var.is_plus() { - assert!(a.lhs.is_plus()); - self.post_constraint(&Constraint::HalfReified( - ReifExpr::MaxDiff(DifferenceExpression::new( - item.var.variable(), - a.lhs.variable(), - -item.cst, - )), - alt_value, - ))?; - } else { - assert!(a.lhs.is_minus()); - // item.var - a.lhs <= -item.cst - let x = item.var.variable(); - let y = a.lhs.variable(); - // (-x) - (-y) <= -item.cst - // y - x <= -item.cst - self.post_constraint(&Constraint::HalfReified( - ReifExpr::MaxDiff(DifferenceExpression::new(y, x, -item.cst)), - alt_value, - ))?; - } + // a.lhs >= item.var + item.cst + let constraint = LinearSum::from(a.lhs).geq(LinearSum::from(item.var) + item.cst); + self.post_constraint(&Constraint::HalfReified(constraint.into(), alt_value))?; } let prez = |v: SignedVar| self.model.state.presence(v); From 3071915ab4b23cc2cfea0431eea52bb762d40e67 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 17:23:07 +0200 Subject: [PATCH 17/43] feat(ape): add makespan objective to plan optimization --- planning/engine/src/optimize_plan.rs | 2 ++ planning/timelines/src/constraints.rs | 25 +++++++++++++++++++++++++ planning/timelines/src/lib.rs | 2 +- solver/src/model/lang/hreif.rs | 3 +++ solver/src/model/lang/max.rs | 2 ++ 5 files changed, 33 insertions(+), 1 deletion(-) diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index e1b866911..51d82c1a1 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -39,6 +39,7 @@ pub enum Relaxation { #[derive(clap::ValueEnum, Debug, Clone, Copy, Display, PartialEq, Eq, PartialOrd, Ord)] pub enum Objective { PlanLength, + Makespan, } pub fn optimize_plan(model: &Model, plan: &LiftedPlan, options: &Options) -> Res<()> { @@ -275,6 +276,7 @@ pub fn encode_plan_optimization_problem( } reify_sum(sum, &mut sched) } + Objective::Makespan => sched.makespan, }; encoding.set_objective(objective); diff --git a/planning/timelines/src/constraints.rs b/planning/timelines/src/constraints.rs index ed4640603..9d38ca78f 100644 --- a/planning/timelines/src/constraints.rs +++ b/planning/timelines/src/constraints.rs @@ -4,11 +4,36 @@ use aries::{ model::lang::{ expr::{and, eq, f_geq, f_leq, f_lt, neq, or}, hreif::{BoolExpr, Store, exclu_choice}, + max::EqMax, }, }; use crate::{boxes::Segment, effects::EffectOp, *}; +/// Constraint that enforces the [`Sched::makespan`] variable to be equal to the +/// maximum end time of tasks, or zero in the absence of tasks. +pub(crate) struct MakespanIsMaxTaskEnd; +impl BoolExpr for MakespanIsMaxTaskEnd { + fn enforce_if(&self, l: Lit, ctx: &Sched, store: &mut dyn Store) { + assert_eq!(ctx.makespan.denom, ctx.time_scale); + let mut ends = ctx + .tasks + .iter() + .map(|t| { + assert_eq!(t.end.denom, ctx.time_scale); + t.end.num + }) + .collect_vec(); + ends.push(IAtom::ZERO); // default value when no task is present + EqMax::new(ctx.makespan.num, ends).enforce_if(l, ctx, store); + } + + fn conj_scope(&self, _ctx: &Sched, _store: &dyn Store) -> hreif::Lits { + // constraints is always valid (scope of makespan variable) + lits![] + } +} + pub struct NoOverlap(Vec); impl NoOverlap { pub fn new(tasks: Vec) -> Self { diff --git a/planning/timelines/src/lib.rs b/planning/timelines/src/lib.rs index d85a059ce..fd654283a 100644 --- a/planning/timelines/src/lib.rs +++ b/planning/timelines/src/lib.rs @@ -109,7 +109,7 @@ impl Sched { makespan, tasks: Default::default(), effects: Default::default(), - constraints: vec![Box::new(EffectCoherence)], // TODO: add default constraints (consitency, makespan), ... + constraints: vec![Box::new(MakespanIsMaxTaskEnd), Box::new(EffectCoherence)], } } diff --git a/solver/src/model/lang/hreif.rs b/solver/src/model/lang/hreif.rs index f3d2c9385..81ed3c938 100644 --- a/solver/src/model/lang/hreif.rs +++ b/solver/src/model/lang/hreif.rs @@ -7,6 +7,7 @@ use crate::{ lang::{ expr::{And, Leq, Or, or}, linear::LinearLeq, + max::{EqMax, EqMin}, }, }, prelude::DomainsExt, @@ -179,6 +180,8 @@ crate::impl_reif!(Or); crate::impl_reif!(And); crate::impl_reif!(Leq); crate::impl_reif!(LinearLeq); +crate::impl_reif!(EqMax); +crate::impl_reif!(EqMin); #[macro_export] macro_rules! impl_reif { diff --git a/solver/src/model/lang/max.rs b/solver/src/model/lang/max.rs index 20b8bfbf6..516520268 100644 --- a/solver/src/model/lang/max.rs +++ b/solver/src/model/lang/max.rs @@ -6,6 +6,7 @@ use itertools::Itertools; use std::fmt::{Debug, Formatter}; /// Constraint equivalent to `lhs = max { e | e \in rhs }` +#[derive(Clone)] pub struct EqMax { lhs: IAtom, rhs: Vec, @@ -21,6 +22,7 @@ impl EqMax { } /// Constraint equivalent to `lhs = min { e | e \in rhs }` +#[derive(Clone)] pub struct EqMin { lhs: IAtom, rhs: Vec, From ebc12b071e23a5e9f9e727559416f20d3ee9dc52 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 17:50:07 +0200 Subject: [PATCH 18/43] doc(ape): add documentation for plan optimization --- planning/engine/README.md | 134 ++++++++++++++++++ planning/engine/examples/gripper/domain.pddl | 17 +++ planning/engine/examples/gripper/plan | 13 ++ planning/engine/examples/gripper/problem.pddl | 10 ++ 4 files changed, 174 insertions(+) create mode 100644 planning/engine/examples/gripper/domain.pddl create mode 100644 planning/engine/examples/gripper/plan create mode 100644 planning/engine/examples/gripper/problem.pddl diff --git a/planning/engine/README.md b/planning/engine/README.md index 3097203e6..e5f193cf4 100644 --- a/planning/engine/README.md +++ b/planning/engine/README.md @@ -63,3 +63,137 @@ my-planner --domain `ape find-domain ${PROBLEM_FILE}` --problem ${PROBLEM_FILE} It is notably used in the [`zed-pddl`](https://github.com/arbimo/zed-pddl) extension for Zed. Note that at this point, the discovery is purely based on the filenames, with no attempt to validate that the domain name matches the one declared in the problem. + + + +## Plan Optimization + +The `optimize-plan` command allow specify objectives: + + - `makespan`: minimizes the end time of the last action + - `plan-length`: minimizes the number of actions + +It also allow to specify the allowed relaxations (what is allowed to change in the plan): + + - `action-presence`: allow removing actions + - `start-time`: allow changing the start time of actions + +### Example plan + +The file [examples/gripper/plan](examples/gripper/plan) contains the following plan: + +``` +(pick ball1 rooma left) +(pick ball2 rooma right) +(move rooma roomb) +(move roomb rooma) +(move rooma roomb) +(drop ball1 roomb left) +(drop ball2 roomb right) +(move roomb rooma) +(pick ball3 rooma left) +(pick ball4 rooma right) +(move rooma roomb) +(drop ball3 roomb left) +(drop ball4 roomb right) +``` + +### No relaxation -> same plan + +Running the `optimize-plan` command with no relaxation will always give the same plan and will succeed if the plan is valid: + +``` +> ape optimize-plan examples/gripper/plan -o plan-length +... +==== Plan (objective: 13) ===== + 0: (pick left ball1 rooma) [0] + 1: (pick right ball2 rooma) [0] + 2: (move rooma roomb) [0] + 3: (move roomb rooma) [0] + 4: (move rooma roomb) [0] + 5: (drop left ball1 roomb) [0] + 6: (drop right ball2 roomb) [0] + 7: (move roomb rooma) [0] + 8: (pick left ball3 rooma) [0] + 9: (pick right ball4 rooma) [0] + 10: (move rooma roomb) [0] + 11: (drop left ball3 roomb) [0] + 12: (drop right ball4 roomb) [0] +``` + +Notice that here, the plan is unchanged. In case of a sequential plan, the start time of each action corresponds to its position in the original plan. + + +### Action presence relaxation + +Relaxing action presence (and optimize plan length) will yield a new plan with the third and fourth actions removed: + +``` +> ape optimize-plan examples/gripper/plan -o plan-length -r action-presence +... +==== Plan (objective: 11) ===== + 0: (pick left ball1 rooma) [0] + 1: (pick right ball2 rooma) [0] + 4: (move rooma roomb) [0] + 5: (drop left ball1 roomb) [0] + 6: (drop right ball2 roomb) [0] + 7: (move roomb rooma) [0] + 8: (pick left ball3 rooma) [0] + 9: (pick right ball4 rooma) [0] + 10: (move rooma roomb) [0] + 11: (drop left ball3 roomb) [0] + 12: (drop right ball4 roomb) [0] +``` + +Note that the timing of actions does not change, and two unoccopied time-stamps remain (2 and 3) + + +### Action timing relaxation + +Relaxing action start times (and optimizing makespan) will give a plan where actions are freely allowed to move around and packed so has to minimize the total time: + + +``` +> ape optimize-plan examples/gripper/plan -o makespan -r start-time +... +==== Plan (objective: 8) ===== + 0: (pick right ball2 rooma) [0] + 0: (pick left ball3 rooma) [0] + 1: (move rooma roomb) [0] + 2: (drop right ball2 roomb) [0] + 2: (drop left ball3 roomb) [0] + 3: (move roomb rooma) [0] + 4: (pick left ball1 rooma) [0] + 4: (pick right ball4 rooma) [0] + 5: (move rooma roomb) [0] + 6: (drop left ball1 roomb) [0] + 6: (drop right ball4 roomb) [0] + 7: (move roomb rooma) [0] + 8: (move rooma roomb) [0] +``` + +Here the pick actions are performed in parallel when possible. +Note that this goes beyond a partial order extraction: the two useless move actions have been repositioned at the end of the plan (i.e. changing some causal links in the plan). +However, those actions were not removed: without the `action-presence` relaxation, the solver is not allowed to remove them. + + +### Combining relaxations + +Relaxation can of course be combined, e.g., to allow both removing actions and moving them around: + +``` +> ape optimize-plan examples/gripper/plan -o makespan -r start-time -r action-presence +... +==== Plan (objective: 6) ===== + 0: (pick right ball2 rooma) [0] + 0: (pick left ball3 rooma) [0] + 1: (move rooma roomb) [0] + 2: (drop right ball2 roomb) [0] + 2: (drop left ball3 roomb) [0] + 3: (move roomb rooma) [0] + 4: (pick left ball1 rooma) [0] + 4: (pick right ball4 rooma) [0] + 5: (move rooma roomb) [0] + 6: (drop left ball1 roomb) [0] + 6: (drop right ball4 roomb) [0] +``` diff --git a/planning/engine/examples/gripper/domain.pddl b/planning/engine/examples/gripper/domain.pddl new file mode 100644 index 000000000..c62c8605b --- /dev/null +++ b/planning/engine/examples/gripper/domain.pddl @@ -0,0 +1,17 @@ +(define (domain gripper_x_1-domain) + (:requirements :strips :typing) + (:types room ball gripper) + (:predicates (at_robby ?r - room) (at_ ?b - ball ?r - room) (free ?g - gripper) (carry ?o - ball ?g - gripper)) + (:action move + :parameters ( ?from - room ?to - room) + :precondition (and (at_robby ?from)) + :effect (and (at_robby ?to) (not (at_robby ?from)))) + (:action pick + :parameters ( ?obj - ball ?room - room ?gripper - gripper) + :precondition (and (at_ ?obj ?room) (at_robby ?room) (free ?gripper)) + :effect (and (carry ?obj ?gripper) (not (at_ ?obj ?room)) (not (free ?gripper)))) + (:action drop + :parameters ( ?obj - ball ?room - room ?gripper - gripper) + :precondition (and (carry ?obj ?gripper) (at_robby ?room)) + :effect (and (at_ ?obj ?room) (free ?gripper) (not (carry ?obj ?gripper)))) +) diff --git a/planning/engine/examples/gripper/plan b/planning/engine/examples/gripper/plan new file mode 100644 index 000000000..2d037dcb1 --- /dev/null +++ b/planning/engine/examples/gripper/plan @@ -0,0 +1,13 @@ +(pick ball1 rooma left) +(pick ball2 rooma right) +(move rooma roomb) +(move roomb rooma) +(move rooma roomb) +(drop ball1 roomb left) +(drop ball2 roomb right) +(move roomb rooma) +(pick ball3 rooma left) +(pick ball4 rooma right) +(move rooma roomb) +(drop ball3 roomb left) +(drop ball4 roomb right) diff --git a/planning/engine/examples/gripper/problem.pddl b/planning/engine/examples/gripper/problem.pddl new file mode 100644 index 000000000..19f85e5eb --- /dev/null +++ b/planning/engine/examples/gripper/problem.pddl @@ -0,0 +1,10 @@ +(define (problem gripper_x_1-problem) + (:domain gripper_x_1-domain) + (:objects + rooma roomb - room + ball4 ball3 ball2 ball1 - ball + left right - gripper + ) + (:init (at_robby rooma) (free left) (free right) (at_ ball4 rooma) (at_ ball3 rooma) (at_ ball2 rooma) (at_ ball1 rooma)) + (:goal (and (at_ ball4 roomb) (at_ ball3 roomb) (at_ ball2 roomb) (at_ ball1 roomb))) +) From 8574aa4023a2e4b10b186ecd9373c52e9b986097 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 23:28:48 +0200 Subject: [PATCH 19/43] chore(ape): make validation output less verbose by default --- planning/engine/src/main.rs | 17 +++++++++++++---- planning/engine/src/validate.rs | 4 ++-- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/planning/engine/src/main.rs b/planning/engine/src/main.rs index fe6015b15..983f08f10 100644 --- a/planning/engine/src/main.rs +++ b/planning/engine/src/main.rs @@ -78,6 +78,9 @@ pub struct Validate { /// Expanded to provide command line options to get the plan, problem and domain #[command(flatten)] plan_pb: PlanAndProblem, + /// If set, will print verbose output + #[arg(short, long)] + verbose: bool, /// If set, the plan is expected to be invalid, /// The process will exit with error code 1 if the plan is valid. #[arg(short, long)] @@ -188,17 +191,19 @@ fn validate_plan(command: &Validate) -> Res<()> { // processed model (from planx) let model = pddl::build_model(&dom, &pb)?; let plan = lifted_plan::parse_lifted_plan(&plan, &model)?; - println!("{model}"); - println!("\n===== Plan ====\n\n{plan}\n"); + if command.verbose { + println!("\n===== Model ====\n\n{model}\n"); + println!("\n===== Plan ====\n\n{plan}\n"); + } let valid = validate::validate(&model, &plan, &command.options)?; if valid { - println!("Plan is valid!"); + println!("VALID"); if command.invalid { std::process::exit(1); } } else { - println!("INVALID plan!"); + println!("INVALID"); if !command.invalid { std::process::exit(1); } @@ -282,6 +287,10 @@ impl PlanAndProblem { &pddl::find_domain_of(pb)? }; + println!("> Domain: {}", dom.display()); + println!("> Problem: {}", pb.display()); + println!("> Plan: {}", plan.display()); + // raw PDDL model let dom = pddl::parse_pddl_domain(Input::from_file(dom)?)?; let pb = pddl::parse_pddl_problem(Input::from_file(pb)?)?; diff --git a/planning/engine/src/validate.rs b/planning/engine/src/validate.rs index 2effd45e9..21c3dbbda 100644 --- a/planning/engine/src/validate.rs +++ b/planning/engine/src/validate.rs @@ -17,9 +17,9 @@ pub fn validate(model: &Model, plan: &LiftedPlan, _options: &Options) -> Res Plan is valid"); + println!("> Plan is valid"); if let Some(objective) = encoding.objective { - println!("> objective: {}", objective.evaluate(&solution).unwrap()); + println!("> Objective: {}", objective.evaluate(&solution).unwrap()); } Ok(true) From 08941e7aeeae5787b7df81fa1eda219b0bb793b3 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 31 Mar 2026 23:35:19 +0200 Subject: [PATCH 20/43] chore(ape): improve error messages on unsupported syntax --- planning/engine/src/encode.rs | 16 ++++++++++------ planning/planx/src/errors.rs | 17 +++++++++++++++++ 2 files changed, 27 insertions(+), 6 deletions(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 51776e0be..061488b37 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -15,7 +15,7 @@ use aries::{ reif::ReifExpr, }; use itertools::Itertools; -use planx::{ExprId, Model, Res, Sym, TimeRef, Timestamp, errors::Spanned}; +use planx::{ExprId, Message, Model, Res, Sym, TimeRef, Timestamp, errors::Spanned}; use timelines::{ Effect, EffectOp, Sched, StateVar, SymAtom, TaskId, Time, constraints::HasValueAt, symbols::ObjectEncoding, }; @@ -115,7 +115,7 @@ pub fn condition_to_constraint( let e2 = reify_sym(exprs[1], model, sched, bindings)?; ConditionConstraint::Eq(e1, e2) } - e => todo!("{e:?}"), + _ => return Err(expr.todo("not supported")), }; // update the required values if requested by caller @@ -294,7 +294,11 @@ pub fn convert_to_pddl_set_semantics(effs: Vec, sched: &mut Sched) -> Ve pub fn reify_timing(t: Timestamp, model: &Model, sched: &mut Sched, binding: &Scope) -> Res { let tp = reify_timeref(t.reference, model, sched, binding)?; - if *t.delay.numer() == 0 { Ok(tp) } else { todo!() } + if *t.delay.numer() == 0 { + Ok(tp) + } else { + Message::todo("unsupported non-zero delay").failed() + } } pub fn reify_timeref(t: TimeRef, _model: &Model, sched: &Sched, binding: &Scope) -> Res { match t { @@ -302,7 +306,7 @@ pub fn reify_timeref(t: TimeRef, _model: &Model, sched: &Sched, binding: &Scope) TimeRef::Horizon => Ok(sched.horizon), TimeRef::ActionStart => Ok(binding.start), TimeRef::ActionEnd => Ok(binding.end), - _ => todo!("{t:?}"), + _ => Message::todo(format!("unsupported timeref {t:?}")).failed(), } } @@ -321,7 +325,7 @@ pub fn reify_sym(e: ExprId, model: &Model, sched: &mut Sched, binding: &Scope) - .get(param.name().canonical_str()) .copied() .ok_or_else(|| param.name().invalid("unknown parameter")), - _ => todo!(), + _ => e.todo("not supported").failed(), } } @@ -329,6 +333,6 @@ pub fn reify_bool(e: ExprId, model: &Model, _sched: &mut Sched) -> Res { let e = model.env.node(e); match e.expr() { planx::Expr::Bool(b) => Ok(*b), - _ => todo!(), + _ => e.todo("not supported").failed(), } } diff --git a/planning/planx/src/errors.rs b/planning/planx/src/errors.rs index 8cdd7e006..4d8cffad6 100644 --- a/planning/planx/src/errors.rs +++ b/planning/planx/src/errors.rs @@ -1,6 +1,7 @@ use std::{ fmt::{Debug, Display}, ops::Range, + panic::Location, }; pub type Res = Result; @@ -103,6 +104,14 @@ pub trait Spanned: Display { } } + /// Creates a debug error message that will also provide the source code location appended to the message. + #[track_caller] + fn todo(&self, msg: impl ToString) -> Message { + let caller = Location::caller(); + let msg = format!("{} ({}:{})", msg.to_string(), caller.file(), caller.line()); + self.invalid(msg) + } + fn error(&self, message: impl ToString) -> Annot { self.annotate(Level::ERROR, message) } @@ -167,6 +176,14 @@ impl Message { pub fn error(title: impl ToString) -> Self { Self::new(Level::ERROR, title) } + + /// Builds an error message with the file:line of the call site + #[cold] + #[track_caller] + pub fn todo(title: impl ToString) -> Self { + let caller = Location::caller(); + Self::error(format!("{} ({}:{}", title.to_string(), caller.file(), caller.line())) + } #[cold] pub fn warning(title: impl ToString) -> Self { Self::new(Level::WARNING, title) From 1241802840524b5a53f82ae38feb81f8de3fb1ba Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 1 Apr 2026 15:18:10 +0200 Subject: [PATCH 21/43] chore(timelines): All state variables use integers to represent their values internally. --- planning/engine/src/encode.rs | 44 ++++++++++++------- planning/engine/src/encode/required_values.rs | 3 +- planning/engine/src/optimize_plan.rs | 25 ++++++++--- planning/engine/src/repair.rs | 7 +-- planning/timelines/src/constraints.rs | 23 ++++------ planning/timelines/src/effects.rs | 9 ++-- planning/timelines/src/lib.rs | 1 - solver/src/model/lang/int.rs | 6 +++ 8 files changed, 72 insertions(+), 46 deletions(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 061488b37..583a01b0f 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -88,7 +88,7 @@ pub fn condition_to_constraint( }; let c = HasValueAt { state_var, - value: Lit::TRUE.into(), + value: IAtom::TRUE, timepoint: reify_timing(tp, model, sched, bindings)?, prez: bindings.presence, source: bindings.source, @@ -100,11 +100,14 @@ pub fn condition_to_constraint( let c = condition_to_constraint(tp, exprs[0], model, sched, bindings, None)?; match c { ConditionConstraint::HasValue(mut c) => { - let Ok(x) = Lit::try_from(c.value) else { - panic!(); - }; - c.value = x.not().into(); - ConditionConstraint::HasValue(c) + if let Ok(x) = IntCst::try_from(c.value) + && (x == 0 || x == 1) + { + c.value = (1 - x).into(); // negation : 0 -> 1 and 1 -> 0 + ConditionConstraint::HasValue(c) + } else { + return expr.todo("unsupported").failed(); + } } ConditionConstraint::Eq(a, b) => ConditionConstraint::Neq(a, b), ConditionConstraint::Neq(a, b) => ConditionConstraint::Eq(a, b), @@ -124,7 +127,7 @@ pub fn condition_to_constraint( ConditionConstraint::HasValue(c) => { // record that someone required such a value let fluent_id = model.env.fluents.get_by_name(&c.state_var.fluent).unwrap(); - reqs.add(fluent_id, c.value_box(|v| sched.model.int_bounds(v)).as_ref()); + reqs.add(fluent_id, c.value_box(&sched.model).as_ref()); } // not on a fluent and thus no need to update the required_values ConditionConstraint::Eq(_, _) => {} @@ -157,7 +160,7 @@ pub fn convert_effect( }; let op = match x.operation { planx::EffectOp::Assign(e) => { - let val = reify_bool(e, model, sched)?; + let val = reify_value(e, model, sched)?; EffectOp::Assign(val) } _ => todo!(), @@ -196,7 +199,7 @@ pub fn add_closed_world_negative_effects(reqs: &RequiredValues, model: &Model, s transition_end: t, mutex_end, state_var: sv, - operation: EffectOp::Assign(false), + operation: EffectOp::FALSE_ASSIGNMENT, prez: Lit::TRUE, // no action source as it is part of the problem definition source: None, @@ -223,12 +226,13 @@ pub fn convert_to_pddl_set_semantics(effs: Vec, sched: &mut Sched) -> Ve let possible_overriden_by = |oid: usize, o: &Effect| -> bool { let cancellable = match (&e.operation, &o.operation) { // the delete can be overriden by the add (add-after-delete semantics) - (EffectOp::Assign(false), EffectOp::Assign(true)) => true, + (&EffectOp::FALSE_ASSIGNMENT, &EffectOp::TRUE_ASSIGNMENT) => true, // the two effects are of the same kind, the currend (eid) can be overriden by one appearing earlier in the effect list - (EffectOp::Assign(true), EffectOp::Assign(true)) => eid > oid, - (EffectOp::Assign(false), EffectOp::Assign(false)) => eid > oid, + (&EffectOp::TRUE_ASSIGNMENT, &EffectOp::TRUE_ASSIGNMENT) => eid > oid, + (&EffectOp::FALSE_ASSIGNMENT, &EffectOp::FALSE_ASSIGNMENT) => eid > oid, // an add cannot be overriden by a delete - (EffectOp::Assign(true), EffectOp::Assign(false)) => false, + (&EffectOp::TRUE_ASSIGNMENT, &EffectOp::FALSE_ASSIGNMENT) => false, + (_, _) => todo!("Not a boolean state variable or non-constant assignment"), // TODO: make it truly unreachable }; cancellable @@ -329,10 +333,20 @@ pub fn reify_sym(e: ExprId, model: &Model, sched: &mut Sched, binding: &Scope) - } } -pub fn reify_bool(e: ExprId, model: &Model, _sched: &mut Sched) -> Res { +pub fn reify_value(e: ExprId, model: &Model, _sched: &mut Sched) -> Res { let e = model.env.node(e); + use planx::Expr::*; match e.expr() { - planx::Expr::Bool(b) => Ok(*b), + Bool(true) => Ok(1), + Bool(false) => Ok(0), + Real(r) if r.denom() == &1 => { + if let Ok(i) = IntCst::try_from(*r.numer()) { + Ok(i) + } else { + e.todo(format!("Cannot be converted to an {}", aries::core::INT_TYPE_NAME)) + .failed() + } + } _ => e.todo("not supported").failed(), } } diff --git a/planning/engine/src/encode/required_values.rs b/planning/engine/src/encode/required_values.rs index e12a3cc28..b9c95fa13 100644 --- a/planning/engine/src/encode/required_values.rs +++ b/planning/engine/src/encode/required_values.rs @@ -44,8 +44,7 @@ impl RequiredValues { .is_some_and(|b| b.as_ref().overlaps(vbox)) } - pub fn may_require_value(&self, fluent: FluentId, value: bool) -> bool { - let value = if value { 1 } else { 0 }; + pub fn may_require_value(&self, fluent: FluentId, value: IntCst) -> bool { self.values_by_fluent .get(&fluent) .is_some_and(|b| b.as_ref().last().unwrap().points().contains(&value)) diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index 51d82c1a1..1ee7f59a8 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -250,18 +250,33 @@ pub fn encode_plan_optimization_problem( // vec to accumulate all effects of the action. // these will then be post-processed to match the set-based semantics of PDDL (add-after-delete, ...) - let mut action_effects = Vec::with_capacity(64); + let mut action_effects = Vec::with_capacity(16); + // store the effects on predicates independently at first because they will need post-processing + let mut predicate_action_effects = Vec::with_capacity(16); // add an effect to the scheduling problem for each effect in the action template // the presence of the effect is controlled by the global enabler of the effect in the template for x in a.effects.iter() { let eff = convert_effect(x, true, model, &mut sched, bindings)?; - // replace the effect presence by its enabler - action_effects.push(eff); + // store the effect either in hte global pool or in the predicate specific one + let is_predicate = model + .env + .fluents + .get(x.effect_expression.state_variable.fluent) + .return_type + == planx::Type::Bool; + if is_predicate { + predicate_action_effects.push(eff); + } else { + action_effects.push(eff); + } } - // post process the effect to align them with PDDL semantics - let action_effects = convert_to_pddl_set_semantics(action_effects, &mut sched); + // post process the effects on predicates to align them with PDDL semantics + let predicate_action_effects = convert_to_pddl_set_semantics(predicate_action_effects, &mut sched); + + // merge the post-processed effects on predicate in the global effect set + action_effects.extend(predicate_action_effects); for eff in action_effects { sched.add_effect(eff); } diff --git a/planning/engine/src/repair.rs b/planning/engine/src/repair.rs index 184b8b685..b5bea3757 100644 --- a/planning/engine/src/repair.rs +++ b/planning/engine/src/repair.rs @@ -322,9 +322,9 @@ fn encode_dom_repair(model: &Model, plan: &LiftedPlan) -> Res { // hacky way to determine if the effect is positive (will only work for classical planning) - let imposed_value = reify_bool(*expr_id, model, &mut sched)?; - let possibly_detrimental = - required_values.may_require_value(eff.effect_expression.state_variable.fluent, !imposed_value); + let imposed_value = reify_value(*expr_id, model, &mut sched)?; + let possibly_detrimental = required_values + .may_require_value(eff.effect_expression.state_variable.fluent, 1 - imposed_value); if possibly_detrimental { // effect may delete a precondition, it must be relaxable and we tie its presence to a new literal sched.model.new_literal(Lit::TRUE) @@ -452,6 +452,7 @@ fn create_potential_effect( fluent: model.env.fluents.get(fid).name().to_string(), args, }; + let value = if value { 1 } else { 0 }; let op = EffectOp::Assign(value); let eff = timelines::Effect { transition_start: t, diff --git a/planning/timelines/src/constraints.rs b/planning/timelines/src/constraints.rs index 9d38ca78f..6e4a3aa17 100644 --- a/planning/timelines/src/constraints.rs +++ b/planning/timelines/src/constraints.rs @@ -1,5 +1,6 @@ +use aries::prelude::*; use aries::{ - core::literals::DisjunctionBuilder, + core::{literals::DisjunctionBuilder, views::Dom}, lits, model::lang::{ expr::{and, eq, f_geq, f_leq, f_lt, neq, or}, @@ -113,7 +114,7 @@ impl BoolExpr for EffectCoherence { #[derive(Debug)] pub struct HasValueAt { pub state_var: StateVar, - pub value: Atom, + pub value: IAtom, pub timepoint: Time, /// Presence of the condition. Must imply the presence of all variables appearing in it. pub prez: Lit, @@ -126,21 +127,13 @@ pub struct HasValueAt { impl HasValueAt { /// Returns a box capturing when and what may be the value required by this condition. - pub fn value_box(&self, dom: impl Fn(IAtom) -> (IntCst, IntCst)) -> crate::boxes::BBox { + pub fn value_box(&self, dom: impl Dom) -> crate::boxes::BBox { let mut buff = Vec::with_capacity(self.state_var.args.len() + 2); - let (earliest, latest) = dom(self.timepoint.num); // TODO: careful with denom - buff.push(Segment::new(earliest, latest)); + buff.push(Segment::from(dom.bounds(self.timepoint.num))); // TODO: careful with denom for arg in &self.state_var.args { - let (lb, ub) = dom(*arg); - buff.push(Segment::new(lb, ub)); + buff.push(Segment::from(dom.bounds(*arg))); } - let value_segment = match self.value { - Atom::Bool(lit) if lit.tautological() => Segment::new(1, 1), - Atom::Bool(lit) if lit.absurd() => Segment::new(0, 0), - Atom::Bool(_) => Segment::new(0, 1), - _ => todo!(), - }; - buff.push(value_segment); + buff.push(Segment::from(dom.bounds(self.value))); crate::boxes::BBox::new(buff) } } @@ -149,7 +142,7 @@ impl BoolExpr for HasValueAt { fn enforce_if(&self, l: Lit, ctx: &Sched, store: &mut dyn Store) { let mut options = Vec::with_capacity(4); - let value_box = self.value_box(|v| ctx.model.int_bounds(v)); + let value_box = self.value_box(&ctx.model); // ensures that at least one effect supports the conditions for eff_id in ctx diff --git a/planning/timelines/src/effects.rs b/planning/timelines/src/effects.rs index 3fe0ced83..316a246c2 100644 --- a/planning/timelines/src/effects.rs +++ b/planning/timelines/src/effects.rs @@ -38,11 +38,11 @@ pub struct Effect { } #[derive(Clone, Eq, PartialEq)] pub enum EffectOp { - Assign(bool), + Assign(IntCst), } impl EffectOp { - // pub const TRUE_ASSIGNMENT: EffectOp = EffectOp::Assign(Atom::TRUE); - // pub const FALSE_ASSIGNMENT: EffectOp = EffectOp::Assign(Atom::FALSE); + pub const TRUE_ASSIGNMENT: EffectOp = EffectOp::Assign(1); + pub const FALSE_ASSIGNMENT: EffectOp = EffectOp::Assign(0); } impl Debug for EffectOp { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { @@ -168,8 +168,7 @@ impl Effects { buff.push(Segment::new(lb, ub)); } let value_segment = match &eff.operation { - EffectOp::Assign(true) => Segment::new(1, 1), - EffectOp::Assign(false) => Segment::new(0, 0), + EffectOp::Assign(v) => Segment::new(*v, *v), }; buff.push(value_segment); self.achieved_bounding_boxes diff --git a/planning/timelines/src/lib.rs b/planning/timelines/src/lib.rs index fd654283a..ce0f3d929 100644 --- a/planning/timelines/src/lib.rs +++ b/planning/timelines/src/lib.rs @@ -6,7 +6,6 @@ pub mod rational; pub mod symbols; pub mod tasks; -use aries::model::extensions::DomainsExt; use constraints::*; use core::fmt::Debug; use core::hash::{Hash, Hasher}; diff --git a/solver/src/model/lang/int.rs b/solver/src/model/lang/int.rs index 3e6c41c70..ea8b3376c 100644 --- a/solver/src/model/lang/int.rs +++ b/solver/src/model/lang/int.rs @@ -114,6 +114,12 @@ impl IAtom { var: IVar::ZERO, shift: 0, }; + pub const ONE: IAtom = IAtom { + var: IVar::ZERO, + shift: 1, + }; + pub const TRUE: IAtom = Self::ONE; + pub const FALSE: IAtom = Self::ZERO; pub fn new(var: IVar, shift: IntCst) -> IAtom { IAtom { var, shift } } From 23b1977ff3ec163c1f489663a3ce75ec4cea45ae Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 1 Apr 2026 15:50:21 +0200 Subject: [PATCH 22/43] chore(timelines): make sure we only use closed world assumption for predicates. --- planning/engine/src/encode.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 583a01b0f..b61c7e660 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -182,11 +182,14 @@ pub fn add_closed_world_negative_effects(reqs: &RequiredValues, model: &Model, s // time at which to place the negative effects. This is -1 so that it can be overrided by an initial effect (at 0). let t = Time::from(-1); - // all state variables that may require a `false` value + // all state variables that may require a `0` value, which encodes `false` for predicates // we will only place a negative effect for those state variables. let req_state_vars = reqs.state_variables(|v| v == 0); for sv in req_state_vars { + if model.env.fluents.get(sv.fluent).return_type != planx::Type::Bool { + continue; // this is not a boolean fluent and thus not eligible for the closed world assumption + } let args: Vec = sv.params.0.into_iter().map(SymAtom::from).collect_vec(); let sv = timelines::StateVar { fluent: model.env.fluents.get(sv.fluent).name().to_string(), From 9cd2a4ffd09e87d15e5f2a8048d23decc1a753f1 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 1 Apr 2026 15:52:16 +0200 Subject: [PATCH 23/43] chore(ape): provide better error messages for effects. --- planning/engine/src/encode.rs | 11 ++++++----- planning/planx/src/effects.rs | 16 ++++++++++++++++ planning/planx/src/pddl/convert.rs | 9 ++++----- 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index b61c7e660..1475feb40 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -138,15 +138,16 @@ pub fn condition_to_constraint( } pub fn convert_effect( - x: &planx::Effect, + effect: &planx::Effect, transition_time: bool, model: &Model, sched: &mut Sched, bindings: &Scope, ) -> Res { - assert!(x.universal_quantification.is_empty()); - let x = &x.effect_expression; - assert!(x.condition.is_none()); + if !effect.universal_quantification.is_empty() || effect.effect_expression.condition.is_some() { + return model.env.node(effect).todo("Unsupported").failed(); + } + let x = &effect.effect_expression; let t = reify_timing(x.timing, model, sched, bindings)?; let args: Vec = x .state_variable @@ -163,7 +164,7 @@ pub fn convert_effect( let val = reify_value(e, model, sched)?; EffectOp::Assign(val) } - _ => todo!(), + _ => return model.env.node(effect).todo("Unsupported").failed(), }; let eff = timelines::Effect { transition_start: t, diff --git a/planning/planx/src/effects.rs b/planning/planx/src/effects.rs index 3116681fb..8b2af8194 100644 --- a/planning/planx/src/effects.rs +++ b/planning/planx/src/effects.rs @@ -97,6 +97,7 @@ impl SimpleEffect { Effect { universal_quantification: vars, effect_expression: self, + span: None, } } @@ -104,6 +105,7 @@ impl SimpleEffect { Effect { universal_quantification: Vec::new(), effect_expression: self, + span: None, } } } @@ -130,6 +132,7 @@ pub struct Effect { /// Universally quantified variables in the effect expression pub universal_quantification: Vec, pub effect_expression: SimpleEffect, + pub span: Option, } impl Effect { @@ -145,8 +148,15 @@ impl Effect { Self { universal_quantification: self.universal_quantification, effect_expression: self.effect_expression.with_condition(cond), + span: self.span, } } + + /// Set the span of the effect to be the same as `s` + pub fn with_span(mut self, s: impl Spanned) -> Self { + self.span = s.span().cloned(); + self + } } impl<'a> Display for Env<'a, &Effect> { @@ -162,3 +172,9 @@ impl<'a> Display for Env<'a, &Effect> { Ok(()) } } + +impl<'a> Spanned for Env<'a, &Effect> { + fn span(&self) -> Option<&Span> { + self.elem.span.as_ref() + } +} diff --git a/planning/planx/src/pddl/convert.rs b/planning/planx/src/pddl/convert.rs index 187f67a9a..5f71de9c2 100644 --- a/planning/planx/src/pddl/convert.rs +++ b/planning/planx/src/pddl/convert.rs @@ -394,14 +394,14 @@ fn into_effects( // stack bindings so that downstream expression know the declared variables let bindings = Rc::new(Bindings::stacked(&vars, bindings)); let effs = into_effects(default_timestamp, quantified_expr, env, &bindings)?; - all_effs.extend(effs.into_iter().map(|e| e.with_quantification(&vars))) + all_effs.extend(effs.into_iter().map(|e| e.with_quantification(&vars).with_span(expr))) } else if let Some([tp, expr]) = expr.as_application("at") && let Ok(time) = parse_timestamp(tp) { // (at end (not (loc r1 l1))) or (at 12.3 (loc r1 l2)) // in the condition we check that we indeed have a valid timepoint because it is common to have also an `at` fluent let effs = into_effects(Some(time), expr, env, bindings)?; - all_effs.extend(effs); + all_effs.extend(effs.into_iter().map(|e| e.with_span(expr))); } else if let Some([cond, expr]) = expr.as_application("when") { let cond = parse(cond, env, bindings)?; let effs = into_effects(default_timestamp, expr, env, bindings)?; @@ -409,17 +409,16 @@ fn into_effects( if let Some(other_cond) = eff.effect_expression.condition { return Err(env.node(other_cond).invalid("expected second condition")); } - all_effs.push(eff.with_condition(cond)); + all_effs.push(eff.with_condition(cond).with_span(expr)); } } else { let Some(time) = default_timestamp else { return Err(expr.invalid("expected temporal qualifier, e.g., (at end ...)")); }; let eff = into_effect(time, expr, env, bindings)?; - all_effs.push(eff.not_quantified()); + all_effs.push(eff.not_quantified().with_span(expr)); } } - Ok(all_effs) } From bd544461c54282a0b37c644f78d9770a817e16c0 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Thu, 2 Apr 2026 15:07:14 +0200 Subject: [PATCH 24/43] wip(ape): initial support for simple numeric planning --- planning/engine/src/encode.rs | 8 +- planning/engine/src/optimize_plan.rs | 17 +- planning/timelines/src/boxes.rs | 13 +- planning/timelines/src/constraints.rs | 207 ++++++++++++++++++--- planning/timelines/src/effects.rs | 140 +++++++++----- solver/src/core/views.rs | 4 +- solver/src/model/extensions/domains_ext.rs | 4 +- solver/src/model/lang/expr.rs | 41 +++- solver/src/model/lang/hreif.rs | 73 ++++---- 9 files changed, 365 insertions(+), 142 deletions(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 1475feb40..0a911074a 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -160,11 +160,9 @@ pub fn convert_effect( args, }; let op = match x.operation { - planx::EffectOp::Assign(e) => { - let val = reify_value(e, model, sched)?; - EffectOp::Assign(val) - } - _ => return model.env.node(effect).todo("Unsupported").failed(), + planx::EffectOp::Assign(v) => EffectOp::Assign(reify_value(v, model, sched)?), + planx::EffectOp::Increase(v) => EffectOp::Step(reify_value(v, model, sched)?), + planx::EffectOp::Decrease(v) => EffectOp::Step(-reify_value(v, model, sched)?), }; let eff = timelines::Effect { transition_start: t, diff --git a/planning/engine/src/optimize_plan.rs b/planning/engine/src/optimize_plan.rs index 1ee7f59a8..87fc593ab 100644 --- a/planning/engine/src/optimize_plan.rs +++ b/planning/engine/src/optimize_plan.rs @@ -287,7 +287,7 @@ pub fn encode_plan_optimization_problem( let mut sum = LinearSum::zero(); for (_a, scope) in &operations_scopes { let action_prez = scope.presence; - sum += bool2int(action_prez, &sched.model) + sum += timelines::constraints::bool2int(action_prez, &sched.model) } reify_sum(sum, &mut sched) } @@ -301,21 +301,6 @@ pub fn encode_plan_optimization_problem( Ok((sched.explainable_solver(constraint_to_repair), encoding)) } -fn bool2int(b: Lit, model: &dyn Store) -> LinearSum { - let is_zero_one = model.bounds(b.variable()) == (0, 1); - if model.entails(b) { - 1.into() - } else if model.entails(!b) { - 0.into() - } else if is_zero_one && b == b.variable().geq(1) { - IVar::new(b.variable()).into() - } else if is_zero_one && b == b.variable().leq(0) { - LinearSum::constant_int(1) - IVar::new(b.variable()) // TODO: careful, the constant part is optional as well - } else { - todo!() // cannot immediately reuse the variable, create a new one and bind it - } -} - fn reify_sum(sum: LinearSum, model: &mut Sched) -> FAtom { let reified: FAtom = model .model diff --git a/planning/timelines/src/boxes.rs b/planning/timelines/src/boxes.rs index 6855f5aad..512ea1cdc 100644 --- a/planning/timelines/src/boxes.rs +++ b/planning/timelines/src/boxes.rs @@ -21,6 +21,7 @@ impl Segment { Segment { first, last } } + /// A segment that spans all possible values pub fn all() -> Self { Self { first: IntCst::MIN, @@ -28,10 +29,12 @@ impl Segment { } } + /// A segment that contains conly a specific value pub fn point(val: IntCst) -> Self { Self { first: val, last: val } } + /// A segment with no values. pub fn empty() -> Self { Self { first: IntCst::MAX, @@ -61,7 +64,7 @@ impl From<(IntCst, IntCst)> for Segment { } } -type Segments = SmallVec<[Segment; 5]>; +pub(crate) type Segments = SmallVec<[Segment; 5]>; #[derive(Clone, Debug)] pub struct BBox { @@ -84,6 +87,10 @@ impl BBox { pub fn as_ref<'a>(&'a self) -> BoxRef<'a> { BoxRef::new(&self.dimensions) } + + pub fn segments(&self) -> &[Segment] { + &self.dimensions + } } /// An axis-aligned box, defined by its projection on all dimensions. #[derive(Copy, Clone)] @@ -218,6 +225,10 @@ impl BoxUniverse { .into_iter() .flat_map(move |w| w.find_overlapping_with(bx)) } + + pub fn has_world(&self, world: &World) -> bool { + self.worlds.contains_key(world) + } } impl Default for BoxUniverse { diff --git a/planning/timelines/src/constraints.rs b/planning/timelines/src/constraints.rs index 6e4a3aa17..e01283294 100644 --- a/planning/timelines/src/constraints.rs +++ b/planning/timelines/src/constraints.rs @@ -1,3 +1,6 @@ +use aries::core::literals::{ConjunctionBuilder, Disjunction}; +use aries::model::lang::expr::And; +use aries::model::lang::linear::LinearSum; use aries::prelude::*; use aries::{ core::{literals::DisjunctionBuilder, views::Dom}, @@ -82,13 +85,21 @@ impl BoolExpr for EffectCoherence { f_leq(e.transition_end, e.mutex_end).opt_enforce_if(l, ctx, store); } - // two phases coherence enforcement: + // two phases coherence enforcement (between assignments only): // - broad phase: computing a bounding box of the space potentially affected by the effect and gather all overlapping boxes // - for any pair of effects with overlapping bounding boxes, add coherence constraints for (eff_id1, eff_id2) in ctx.effects.potentially_interacting_effects() { // ensure that the interval `(transition_start, mutex_end]` do not overlap let eff1 = &ctx.effects[eff_id1]; let eff2 = &ctx.effects[eff_id2]; + + // this phase only concerns assignments + let EffectOp::Assign(_) = eff1.operation else { + continue; + }; + let EffectOp::Assign(_) = eff2.operation else { + continue; + }; let itv1 = IntervalOnStateVariable { state_var: &eff1.state_var, start: eff1.transition_start + FAtom::EPSILON, @@ -104,6 +115,46 @@ impl BoolExpr for EffectCoherence { let exclu = Exclusive { a: &itv1, b: &itv2 }; exclu.opt_enforce_if(l, ctx, store); } + + // for any step, ensures that: + // 1) it appears in an assignments exclusivity interval + // 2) its mutex_end matches this assignments' mutex end + // Condition 2) is necessary to make sure that any time at which the step contributes to the state variable value is included in its interval + for step in ctx.effects.iter() { + let EffectOp::Step(_) = step.operation else { + continue; + }; + let compatible_assignemnts = ctx + .effects + .potentially_overlapping_effects(&step.state_var.fluent, step.affected_box(&store).as_ref()) + .filter_map(|eid| { + let eff = &ctx.effects[eid]; + match eff.operation { + EffectOp::Assign(_) => Some(eff), + EffectOp::Step(_) => None, + } + }) + .collect_vec(); + + let mut support_options = DisjunctionBuilder::new(); + + for ass in compatible_assignemnts { + let mut conjuncts = ConjunctionBuilder::new(); + conjuncts.push(ass.prez); + conjuncts.push(f_leq(ass.transition_end, step.transition_start).implicant(ctx, store)); + // note: this forces the `step` interval to exactly match the end of the assignment + conjuncts.push(f_leq(ass.mutex_end, step.mutex_end).implicant(ctx, store)); + conjuncts.push(f_geq(ass.mutex_end, step.mutex_end).implicant(ctx, store)); + for (arg1, arg2) in ass.state_var.args.iter().zip_eq(step.state_var.args.iter()) { + conjuncts.push(eq(*arg1, *arg2).implicant(ctx, store)) + } + let supports = and(conjuncts.build().into_lits().into_boxed_slice()).implicant(ctx, store); + support_options.push(supports); + } + // if the step it present, then at least one of the assignment must "support it" + support_options.push(!step.prez); + support_options.build().enforce_if(l, ctx, store); + } } fn conj_scope(&self, _ctx: &Sched, _store: &dyn Store) -> hreif::Lits { @@ -138,42 +189,103 @@ impl HasValueAt { } } +#[derive(Debug)] +struct StepContributor { + contributes: Lit, + contribution: IntCst, +} +#[derive(Debug)] +struct AssignEstablisher { + establishes: Lit, + base: IntCst, +} + impl BoolExpr for HasValueAt { fn enforce_if(&self, l: Lit, ctx: &Sched, store: &mut dyn Store) { - let mut options = Vec::with_capacity(4); - let value_box = self.value_box(&ctx.model); - // ensures that at least one effect supports the conditions - for eff_id in ctx + // gathers all effect that may contribute to the value + let relevant_effects = ctx .effects .potentially_supporting_effects(&self.state_var.fluent, value_box.as_ref()) - { - let eff = &ctx.effects[eff_id]; - let EffectOp::Assign(value) = eff.operation; + .map(|eff_id| &ctx.effects[eff_id]) + .collect_vec(); + + let mut step_contributors = Vec::new(); + for &eff in &relevant_effects { + debug_assert_eq!(self.state_var.fluent, eff.state_var.fluent); + let EffectOp::Step(step) = eff.operation else { + continue; + }; + if step == 0 { + continue; + } + + let mut conjuncts = ConjunctionBuilder::new(); + conjuncts.push(eff.prez); + conjuncts.push(f_geq(self.timepoint, eff.effective_start()).reified(ctx, store)); + conjuncts.push(f_leq(self.timepoint, eff.mutex_end).reified(ctx, store)); + for (arg1, arg2) in self.state_var.args.iter().zip_eq(eff.state_var.args.iter()) { + conjuncts.push(eq(*arg1, *arg2).reified(ctx, store)) + } + if !conjuncts.absurd() { + let conjuncts: And = and(conjuncts.build().into_lits().into_boxed_slice()); // TODO: make And = Conjunction + let contributes = conjuncts.reified(ctx, store); // presence should be the same as self.presence? + step_contributors.push(StepContributor { + contributes, + contribution: step, + }); + } + } + + // compute assign establisehrs. Those are exclusive (by effect coherence) so half reification is sufficient + let mut establishers = Vec::with_capacity(16); + for &eff in &relevant_effects { + debug_assert_eq!(self.state_var.fluent, eff.state_var.fluent); + let EffectOp::Assign(assignment) = eff.operation else { + continue; + }; if self.state_var.fluent != eff.state_var.fluent { continue; } - assert_eq!(self.state_var.args.len(), eff.state_var.args.len()); - let mut conjuncts = vec![ - eff.prez, - f_geq(self.timepoint, eff.effective_start()).implicant(ctx, store), - f_leq(self.timepoint, eff.mutex_end).implicant(ctx, store), - ]; - conjuncts.extend( - self.state_var - .args - .iter() - .zip(eff.state_var.args.iter()) - .map(|(x, y)| eq(*x, *y).implicant(ctx, store)), - ); - conjuncts.push(eq(self.value, Atom::from(value)).implicant(ctx, store)); - - if conjuncts.iter().all(|c| *c != Lit::FALSE) { - options.push(and(conjuncts.as_slice()).implicant(ctx, store)); + let mut conjuncts = ConjunctionBuilder::new(); + conjuncts.push(eff.prez); + conjuncts.push(f_geq(self.timepoint, eff.effective_start()).implicant(ctx, store)); + conjuncts.push(f_leq(self.timepoint, eff.mutex_end).implicant(ctx, store)); + for (arg1, arg2) in self.state_var.args.iter().zip_eq(eff.state_var.args.iter()) { + conjuncts.push(eq(*arg1, *arg2).implicant(ctx, store)) + } + if !conjuncts.absurd() { + let conjuncts: And = and(conjuncts.build().into_lits().into_boxed_slice()); // TODO: make And = Conjunction + let establishes = conjuncts.implicant(ctx, store); // presence should be the same as self.presence? + establishers.push(AssignEstablisher { + establishes, + base: assignment, + }); + } + } + + if step_contributors.is_empty() { + bind_alternative(l, self.value, self.prez, &establishers, store); + } else { + // note: if there are not steps, we can use self.value as the base_variable (which is equivalent to the previous encoding?) + + // Create a `base_variable` that will take the value of the selected establisher + // has a base_variable = alternative { e in assign_establishers } + let base_lb = establishers.iter().map(|e| e.base).min().unwrap_or(0); + let base_ub = establishers.iter().map(|e| e.base).max().unwrap_or(0); + let base_var: IAtom = store.new_optional_var(base_lb, base_ub, self.prez).into(); + bind_alternative(l, base_var, self.prez, &establishers, store); + + // and self.value = base_variable + Sum { step contirbutions } + let lhs = LinearSum::from(self.value); + let mut rhs = LinearSum::from(base_var); + for step in step_contributors { + rhs += bool2int(step.contributes, store) * step.contribution; } + lhs.clone().leq(rhs.clone()).enforce(ctx, store); + lhs.geq(rhs).enforce(ctx, store); } - or(options).opt_enforce_if(l, ctx, store); // PDDL mutex: a condition of an action cannot rely on a fact that is about to be modified by another action // given the interval `[cond.start, cond.end]`, we ensure it does not meet the interval `[eff.transition_start, eff.transition_end)` @@ -188,6 +300,7 @@ impl BoolExpr for HasValueAt { .effects .potentially_overlapping_transitions(&self.state_var.fluent, value_box.as_ref()) { + // TODO: mutex when considering steps? let eff = &ctx.effects[eff_id]; if eff.source != self.source { let itv_eff = IntervalOnStateVariable { @@ -210,7 +323,31 @@ impl BoolExpr for HasValueAt { } } +/// Enforce that, if presence is true, then, +/// - exactly one of the alternatives is holds (call it a) +/// - for this alternative a , `value = a.base` +fn bind_alternative(l: Lit, value: IAtom, presence: Lit, alternatives: &[AssignEstablisher], store: &mut dyn Store) { + // println!("\n\n ===== bind alts ===== \n\n"); + // dbg!(value, presence, alternatives); + let ctx = &(); // constraints used here are independent of any context, so we just use the unit type + + // at least one esatablisher must hold + Disjunction::from_iter(alternatives.iter().map(|a| a.establishes)).enforce_if(l, ctx, store); + + for (ai, a) in alternatives.iter().enumerate() { + // it is exclusive of all other establishers + // note that is expected to be a redundant constraint (already indirectly enforced by effect coherence) + for b in &alternatives[ai + 1..] { + or([!presence, !a.establishes, !b.establishes]).enforce_if(l, ctx, store); + } + + // if `a` is the establishers the the variable must have its value + or([!presence, !a.establishes, eq(a.base, value).implicant(ctx, store)]).enforce_if(l, ctx, store); + } +} + /// A closed interval `[start, end]` associated to a state variable +#[derive(Debug)] struct IntervalOnStateVariable<'a> { state_var: &'a StateVar, start: Time, @@ -259,3 +396,21 @@ impl<'a> BoolExpr for Exclusive<'a> { lits![] } } + +/// Transforms a boolean into an integer expression +/// NOte: the implementation is currently incomplete +#[doc(hidden)] +pub fn bool2int(b: Lit, model: &dyn Store) -> LinearSum { + let is_zero_one = model.bounds(b.variable()) == (0, 1); + if model.entails(b) { + 1.into() + } else if model.entails(!b) { + 0.into() + } else if is_zero_one && b == b.variable().geq(1) { + IVar::new(b.variable()).into() + } else if is_zero_one && b == b.variable().leq(0) { + LinearSum::constant_int(1) - IVar::new(b.variable()) // TODO: careful, the constant part is optional as well + } else { + todo!() // cannot immediately reuse the variable, create a new one and bind it + } +} diff --git a/planning/timelines/src/effects.rs b/planning/timelines/src/effects.rs index 316a246c2..26e7ec531 100644 --- a/planning/timelines/src/effects.rs +++ b/planning/timelines/src/effects.rs @@ -1,5 +1,4 @@ use aries::{core::views::Dom, prelude::*}; -use smallvec::SmallVec; use std::{ fmt::{Debug, Formatter}, ops::Index, @@ -7,7 +6,7 @@ use std::{ use crate::{ StateVar, TaskId, Time, - boxes::{BoxRef, BoxUniverse, Segment}, + boxes::{BBox, BoxRef, BoxUniverse, Segment}, }; /// Represents an effect on a state variable. @@ -38,7 +37,10 @@ pub struct Effect { } #[derive(Clone, Eq, PartialEq)] pub enum EffectOp { + /// Sets the state variable to an absolute value Assign(IntCst), + /// Increase the state variable by a given value (positive or negative) + Step(IntCst), } impl EffectOp { pub const TRUE_ASSIGNMENT: EffectOp = EffectOp::Assign(1); @@ -50,6 +52,8 @@ impl Debug for EffectOp { EffectOp::Assign(val) => { write!(f, ":= {val:?}") } + EffectOp::Step(v) if v >= &0 => write!(f, "+= {v:?}"), + EffectOp::Step(v) => write!(f, "-= {:?}", -v), } } } @@ -74,6 +78,58 @@ impl Effect { pub fn variable(&self) -> &StateVar { &self.state_var } + + /// Bounding box capturing the space affected by this effect + /// + /// - `[lb(trans-start), ub(mutex_end)]` + /// - `[lb(a), ub(a)]` for a in args + pub(crate) fn affected_box(&self, dom: impl Dom) -> crate::boxes::BBox { + let mut buff = crate::boxes::Segments::new(); + buff.push(Segment::new( + dom.lb(self.transition_start.num), + dom.ub(self.mutex_end.num), + )); // TODO: carfeul with denom + buff.extend(self.args_segments(&dom)); + BBox::new(buff) + } + /// Returns a box capturing when and what may be the value the effect may help achieve + /// + /// - `[lb(trans-start), ub(mutex_end)]` + /// - `[lb(a), ub(a)]` for a in args + /// - `[v, v]` where v is the value in the assignment or step operation + pub(crate) fn value_box(&self, dom: impl Dom) -> crate::boxes::BBox { + let mut buff = crate::boxes::Segments::new(); + let start = dom.lb(self.transition_end.num); // TODO: carerful with denom + let end = dom.ub(self.mutex_end.num); // TODO: carerful with denom + buff.push(Segment::new(start, end)); + buff.extend(self.args_segments(&dom)); + let value_segment = match self.operation { + EffectOp::Assign(v) | EffectOp::Step(v) => Segment::point(v), + }; + buff.push(value_segment); + crate::boxes::BBox::new(buff) + } + + /// Returns a box capturing when the effect induces a transition + /// + /// - `[lb(trans-start), ub(trans-end)[` (note that the transition is excluded from the segment) + /// - `[lb(a), ub(a)]` for a in args + pub(crate) fn transition_box(&self, dom: &impl Dom) -> crate::boxes::BBox { + let mut buff = crate::boxes::Segments::new(); + buff.push(Segment::new( + dom.lb(self.transition_start.num), + dom.ub(self.transition_end.num) - 1, + )); // TODO: carfeul with denom + buff.extend(self.args_segments(&dom)); + BBox::new(buff) + } + + fn args_segments(&self, dom: impl Dom) -> impl Iterator { + self.state_var + .args + .iter() + .map(move |arg| Segment::from(dom.bounds(arg))) + } } pub type EffectId = usize; @@ -107,7 +163,8 @@ pub struct Effects { /// - value: `[lb(value), ub(value)]` /// /// If the boxes of two effects to not overlap, they can be safely determined to never overlap (and thus do not require coherence enforcement constraints). - achieved_bounding_boxes: BoxUniverse, + assignment_bounding_boxes: BoxUniverse, + steps_bounding_boxes: BoxUniverse, /// Associates every effect to a `Box` in a universe. /// This box denotes a the set of values that the effect may support. /// The intuition if that @@ -123,14 +180,13 @@ pub struct Effects { transition_bounding_boxes: BoxUniverse, } -type Segments = SmallVec<[Segment; 16]>; - impl Effects { pub fn new() -> Self { Self { effects: Default::default(), affected_bb: BoxUniverse::new(), - achieved_bounding_boxes: BoxUniverse::new(), + assignment_bounding_boxes: BoxUniverse::new(), + steps_bounding_boxes: BoxUniverse::new(), transition_bounding_boxes: BoxUniverse::new(), } } @@ -147,45 +203,22 @@ impl Effects { // ID of the effect will be the index of the next free slot let eff_id = self.effects.len(); - let mut buff = Segments::new(); + let fluent = &eff.state_var.fluent; // compute and store affected bounding_box - buff.push(Segment::new( - dom.lb(eff.transition_start.num), - dom.ub(eff.mutex_end.num), - )); // TODO: careful with denom - for arg in &eff.state_var.args { - let (lb, ub) = dom.bounds(*arg); - buff.push(Segment::new(lb, ub)); - } - self.affected_bb.add_box(&eff.state_var.fluent, &buff, eff_id); + let bbox = eff.affected_box(&dom); + self.affected_bb.add_box(fluent, bbox.segments(), eff_id); // compute and store the achievable bounding boxes - buff.clear(); - buff.push(Segment::new(dom.lb(eff.transition_end.num), dom.ub(eff.mutex_end.num))); // TODO: careful with denom - for arg in &eff.state_var.args { - let (lb, ub) = dom.bounds(*arg); - buff.push(Segment::new(lb, ub)); + let bbox = eff.value_box(&dom); + match eff.operation { + EffectOp::Assign(_) => self.assignment_bounding_boxes.add_box(fluent, bbox.segments(), eff_id), + EffectOp::Step(_) => self.steps_bounding_boxes.add_box(fluent, bbox.segments(), eff_id), } - let value_segment = match &eff.operation { - EffectOp::Assign(v) => Segment::new(*v, *v), - }; - buff.push(value_segment); - self.achieved_bounding_boxes - .add_box(&eff.state_var.fluent, &buff, eff_id); // compute and store the achievable bounding boxes - buff.clear(); - buff.push(Segment::new( - dom.lb(eff.transition_start.num), - dom.ub(eff.transition_end.num) - 1, - )); // TODO: careful with denom - for arg in &eff.state_var.args { - let (lb, ub) = dom.bounds(*arg); - buff.push(Segment::new(lb, ub)); - } - self.transition_bounding_boxes - .add_box(&eff.state_var.fluent, &buff, eff_id); + let bbox = eff.transition_box(&dom); + self.transition_bounding_boxes.add_box(fluent, bbox.segments(), eff_id); self.effects.push(eff); eff_id @@ -196,7 +229,16 @@ impl Effects { self.affected_bb.overlapping_boxes().map(|(e1, e2)| (*e1, *e2)) } - /// Returns a list of potentially supporting effect for a condition, representing as a bounding box with + /// Returns a list of effects that may overlap the given box (time + arguments) + pub(crate) fn potentially_overlapping_effects<'a>( + &'a self, + fluent: &'a String, + affected_box: BoxRef<'a>, + ) -> impl Iterator + 'a { + self.affected_bb.find_overlapping_with(fluent, affected_box).copied() + } + + /// Returns a list of potentially supporting effect (assign or step) for a condition, represented as a bounding box with /// the given fluents and the following segments: /// /// - time: `[lb(condition_start), ub(condition_end)]` @@ -208,11 +250,21 @@ impl Effects { fluent: &'a String, value_box: BoxRef<'a>, ) -> impl Iterator + 'a { - // compute the value bounding box - - self.achieved_bounding_boxes - .find_overlapping_with(fluent, value_box) - .copied() + if self.steps_bounding_boxes.has_world(fluent) { + // there exists step effects for this fluent + // This means we cannot immediately rely on the value because the values achievable for an assignment should consider the contribution of any step + // + // For now, we workaround this by ignoring the value and juste looking for boxes that overlap the box on time and arguments. + // A potential improvement would be to consider the min/max for all steps and then look for the assignment that achieve the value expaned by this min/max + // Note that that the step effects must be included in the return as well + let affected_box = value_box.drop_tail(1); + self.affected_bb.find_overlapping_with(fluent, affected_box).copied() + } else { + // no steps, we simply return + self.assignment_bounding_boxes + .find_overlapping_with(fluent, value_box) + .copied() + } } /// Returns a list of effects whose transition period `[transition_start, transition_end)` may overlap a condition with the diff --git a/solver/src/core/views.rs b/solver/src/core/views.rs index 30ffa7107..2602d2e08 100644 --- a/solver/src/core/views.rs +++ b/solver/src/core/views.rs @@ -10,7 +10,7 @@ pub trait Dom { } } -impl Dom for &X +impl Dom for &X where X: Dom, { @@ -22,7 +22,7 @@ where Dom::presence(*self, var) } } -impl Dom for &mut X +impl Dom for &mut X where X: Dom, { diff --git a/solver/src/model/extensions/domains_ext.rs b/solver/src/model/extensions/domains_ext.rs index e73c4d1b2..30c63f03a 100644 --- a/solver/src/model/extensions/domains_ext.rs +++ b/solver/src/model/extensions/domains_ext.rs @@ -7,7 +7,7 @@ use crate::model::symbols::SymId; use crate::model::symbols::TypedSym; /// Extension methods for an object containing a partial or total assignment to a problem. -pub trait DomainsExt: Dom + Sized { +pub trait DomainsExt: Dom { fn entails(&self, literal: Lit) -> bool { Dom::upper_bound(self, literal.svar()) <= literal.ub_value() } @@ -111,7 +111,7 @@ pub trait DomainsExt: Dom + Sized { } } -impl DomainsExt for D where D: Dom + Sized {} +impl DomainsExt for D where D: Dom {} #[cfg(test)] mod test { diff --git a/solver/src/model/lang/expr.rs b/solver/src/model/lang/expr.rs index 0559f91e2..c2140bb91 100644 --- a/solver/src/model/lang/expr.rs +++ b/solver/src/model/lang/expr.rs @@ -1,9 +1,9 @@ use crate::core::literals::{Disjunction, Lits}; -use crate::core::*; use crate::model::lang::alternative::Alternative; use crate::model::lang::hreif::{BoolExpr, Store}; use crate::model::lang::{Atom, FAtom, IAtom, SAtom}; use crate::model::{Label, Model}; +use crate::prelude::*; use crate::reif::{DifferenceExpression, ReifExpr, Reifiable}; use env_param::EnvParam; use itertools::Itertools; @@ -107,6 +107,13 @@ impl Not for And { Disjunction::from_vec(lits.to_vec()) } } +impl Not for &And { + type Output = Or; + + fn not(self) -> Self::Output { + Disjunction::from_iter(self.0.iter().map(|&l| !l)) + } +} impl From for ReifExpr { fn from(value: And) -> Self { @@ -127,6 +134,13 @@ impl Not for Leq { gt(self.0, self.1) } } +impl Not for &Leq { + type Output = Leq; + + fn not(self) -> Self::Output { + !*self + } +} impl From for ReifExpr { fn from(value: Leq) -> Self { @@ -160,6 +174,21 @@ impl From for ReifExpr { #[derive(Copy, Clone, Debug)] pub struct Eq(Atom, Atom); +impl Not for Eq { + type Output = Neq; + + fn not(self) -> Self::Output { + Neq(self.0, self.1) + } +} +impl Not for &Eq { + type Output = Neq; + + fn not(self) -> Self::Output { + !*self + } +} + impl Reifiable for Eq { fn decompose(self, model: &mut Model) -> ReifExpr { let a = self.0; @@ -287,10 +316,7 @@ impl BoolExpr for Eq { } fn conj_scope(&self, _ctx: &Ctx, store: &dyn Store) -> super::hreif::Lits { - smallvec::smallvec![ - store.presence_of_var(self.0.variable()), - store.presence_of_var(self.1.variable()) - ] + smallvec::smallvec![store.presence_literal(self.0), store.presence_literal(self.1)] } } @@ -383,9 +409,6 @@ impl BoolExpr for Neq { store.get_implicant(or(disjuncts).into()) } fn conj_scope(&self, _ctx: &Ctx, store: &dyn Store) -> super::hreif::Lits { - smallvec::smallvec![ - store.presence_of_var(self.0.variable()), - store.presence_of_var(self.1.variable()) - ] + smallvec::smallvec![store.presence_literal(self.0), store.presence_literal(self.1)] } } diff --git a/solver/src/model/lang/hreif.rs b/solver/src/model/lang/hreif.rs index 81ed3c938..819181503 100644 --- a/solver/src/model/lang/hreif.rs +++ b/solver/src/model/lang/hreif.rs @@ -1,7 +1,7 @@ use smallvec::SmallVec; use crate::{ - core::{IntCst, Lit, VarRef, views::Term}, + core::{IntCst, Lit, VarRef, views::Dom}, model::{ Label, Model, lang::{ @@ -10,35 +10,35 @@ use crate::{ max::{EqMax, EqMin}, }, }, - prelude::DomainsExt, + prelude::*, reif::ReifExpr, }; -pub trait Store { +pub trait Store: Dom { fn new_literal(&mut self, presence: Lit) -> Lit; fn new_optional_var(&mut self, lb: IntCst, ub: IntCst, presence: Lit) -> VarRef; fn get_implicant(&mut self, e: ReifExpr) -> Lit; fn add_implies(&mut self, l: Lit, e: ReifExpr); - fn bounds(&self, var: VarRef) -> (IntCst, IntCst); - fn entails(&self, l: Lit) -> bool; + // fn bounds(&self, var: VarRef) -> (IntCst, IntCst); + // fn entails(&self, l: Lit) -> bool; - /// Returns the literal indicating whether the variable is present. - /// - /// See [`presence`] for a more general version. - fn presence_of_var(&self, var: VarRef) -> Lit; + // /// Returns the literal indicating whether the variable is present. + // /// + // /// See [`presence`] for a more general version. + // fn presence_of_var(&self, var: VarRef) -> Lit; fn conjunctive_scope(&mut self, lits: &[Lit]) -> Lit; fn tautology_of_scope(&mut self, scope: Lit) -> Lit; - /// Returns the literal indicate the whether the term is present. - /// - /// Note: this method is not dyn-compatible. - /// [`presence_of_var`] may be used as a more verbose fall-back. - fn presence(&self, var: impl Term) -> Lit - where - Self: Sized, - { - self.presence_of_var(var.variable()) - } + // /// Returns the literal indicate the whether the term is present. + // /// + // /// Note: this method is not dyn-compatible. + // /// [`presence_of_var`] may be used as a more verbose fall-back. + // fn presence(&self, var: impl Term) -> Lit + // where + // Self: Sized, + // { + // self.presence_of_var(var.variable()) + // } } pub trait ModelWrapper { @@ -58,7 +58,7 @@ impl ModelWrapper for Model { } } -impl Store for T +impl Store for T where T: ModelWrapper, { @@ -76,16 +76,7 @@ where //println!("[{:?}] {l:?} -> {e:?}", self.presence(l)); // TODO: remove self.get_model_mut().enforce_if(l, e); } - fn bounds(&self, var: VarRef) -> (IntCst, IntCst) { - self.get_model().state.bounds(var) - } - fn entails(&self, l: Lit) -> bool { - self.get_model().state.entails(l) - } - fn presence_of_var(&self, var: VarRef) -> Lit { - self.get_model().state.presence_literal(var) - } fn conjunctive_scope(&mut self, presence_variables: &[Lit]) -> Lit { self.get_model_mut().get_conjunctive_scope(presence_variables) } @@ -110,7 +101,7 @@ pub trait BoolExpr { } fn opt_enforce_if(&self, l: Lit, ctx: &Ctx, store: &mut dyn Store) { let scope = self.scope(ctx, store); - let implicant = if scope == store.presence_of_var(l.variable()) { + let implicant = if scope == store.presence(l.variable()) { l // TODO: here we should instead test that scope => prez(l) } else if store.entails(l) { store.tautology_of_scope(scope) @@ -127,6 +118,17 @@ pub trait BoolExpr { self.enforce_if(implicant, ctx, store); implicant } + fn reified<'a, NotSelf>(&'a self, ctx: &Ctx, store: &mut dyn Store) -> Lit + where + Self: Sized, + &'a Self: std::ops::Not, + NotSelf: BoolExpr, + { + let implicant = self.implicant(ctx, store); + let negated = !self; + negated.enforce_if(!implicant, ctx, store); + implicant + } fn enforce(&self, ctx: &Ctx, store: &mut dyn Store) { self.opt_enforce_if(Lit::TRUE, ctx, store); } @@ -160,7 +162,7 @@ impl BoolExpr for ReifExpr { } fn conj_scope(&self, _ctx: &Ctx, store: &dyn Store) -> Lits { - let vs = self.scope(|v| store.presence_of_var(v)); + let vs = self.scope(|v| store.presence_literal(v)); // TODO: give flattening context let conj_scope = vs.to_conjunction(|_| Option::<[Lit; 0]>::None, |l| l == Lit::TRUE); SmallVec::from_iter(conj_scope.literals()) @@ -227,7 +229,7 @@ impl> BoolExpr for ExclusiveChoice { fn enforce_if(&self, l: Lit, ctx: &Ctx, store: &mut dyn Store) { if store.entails(l) { // a tautolgy, create a single variable representing both options - let choice_var = store.new_literal(store.presence_of_var(l.variable())); + let choice_var = store.new_literal(store.presence_literal(l)); self.alt1.opt_enforce_if(choice_var, ctx, store); self.alt2.opt_enforce_if(!choice_var, ctx, store); } else { @@ -248,6 +250,7 @@ impl> BoolExpr for ExclusiveChoice { #[cfg(test)] mod test { use crate::{ + core::views::Term, model::{ extensions::DomainsExt, lang::{ @@ -266,10 +269,6 @@ mod test { /// True if the the two atoms are different, and undefined if at least one is absent struct Different(IAtom, IAtom); - fn prez(v: impl Term, store: &dyn Store) -> Lit { - store.presence_of_var(v.variable()) - } - impl BoolExpr for AllDifferent { fn enforce_if(&self, l: Lit, ctx: &Ctx, store: &mut dyn Store) { for (i, t1) in self.0.iter().copied().enumerate() { @@ -290,7 +289,7 @@ mod test { } fn conj_scope(&self, _ctx: &Ctx, store: &dyn Store) -> Lits { - lits![prez(self.0, store), prez(self.1, store)] + lits![store.presence_literal(self.0), store.presence_literal(self.1)] } } From 547bb8e296150191d51c4f06273ac119545703c0 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Thu, 2 Apr 2026 22:14:43 +0200 Subject: [PATCH 25/43] chore(timelines): Add primitive effect printing for debugging --- planning/timelines/src/lib.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/planning/timelines/src/lib.rs b/planning/timelines/src/lib.rs index ce0f3d929..3e9395094 100644 --- a/planning/timelines/src/lib.rs +++ b/planning/timelines/src/lib.rs @@ -6,6 +6,7 @@ pub mod rational; pub mod symbols; pub mod tasks; +use aries::core::state::Evaluable; use constraints::*; use core::fmt::Debug; use core::hash::{Hash, Hasher}; @@ -157,6 +158,7 @@ impl Sched { } pub fn print(&self, sol: &Solution) { + println!("==== tasks ===="); let sorted_tasks = self .tasks .iter() @@ -165,5 +167,19 @@ impl Sched { for t in sorted_tasks { println!("{}: {}", t.name, sol.eval(t.start.num).unwrap()) } + println!("==== Effects ===="); + for e in self.effects.iter().sorted_by_key(|e| &e.state_var.fluent) { + if !sol.entails(e.prez) { + continue; + } + println!( + "{}: [{},{}] {:?} ...[{}]", + e.state_var.fluent, + e.transition_start.evaluate(sol).unwrap(), + e.transition_end.evaluate(sol).unwrap(), + e.operation, + e.mutex_end.evaluate(sol).unwrap(), + ); + } } } From 977b08c9a0bfd0594c247f4cf816cba2ca72fe3e Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Thu, 2 Apr 2026 22:15:57 +0200 Subject: [PATCH 26/43] chore(ape): add general expression reification --- planning/engine/src/encode.rs | 79 ++++++++++++++++++++-------- planning/engine/src/optimize_plan.rs | 24 +++++++-- planning/engine/src/repair.rs | 2 +- planning/engine/src/validate.rs | 8 +-- 4 files changed, 83 insertions(+), 30 deletions(-) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 0a911074a..91c2a3871 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -160,9 +160,9 @@ pub fn convert_effect( args, }; let op = match x.operation { - planx::EffectOp::Assign(v) => EffectOp::Assign(reify_value(v, model, sched)?), - planx::EffectOp::Increase(v) => EffectOp::Step(reify_value(v, model, sched)?), - planx::EffectOp::Decrease(v) => EffectOp::Step(-reify_value(v, model, sched)?), + planx::EffectOp::Assign(v) => EffectOp::Assign(reify_constant(v, model, sched, bindings)?), + planx::EffectOp::Increase(v) => EffectOp::Step(reify_constant(v, model, sched, bindings)?), + planx::EffectOp::Decrease(v) => EffectOp::Step(-reify_constant(v, model, sched, bindings)?), }; let eff = timelines::Effect { transition_start: t, @@ -317,8 +317,35 @@ pub fn reify_timeref(t: TimeRef, _model: &Model, sched: &Sched, binding: &Scope) } pub fn reify_sym(e: ExprId, model: &Model, sched: &mut Sched, binding: &Scope) -> Res { + reify_expression(e, None, model, sched, binding) +} + +pub fn reify_constant(e: ExprId, model: &Model, sched: &mut Sched, scope: &Scope) -> Res { + let reif = reify_expression(e, None, model, sched, scope)?; + let cst = IntCst::try_from(reif).map_err(|_| model.env.node(e).todo("non constant term unsupported"))?; + Ok(cst) +} + +pub fn reify_expression( + e: ExprId, + time: Option