diff --git a/.github/workflows/aries.yml b/.github/workflows/aries.yml index af9b2595d..b9b151147 100644 --- a/.github/workflows/aries.yml +++ b/.github/workflows/aries.yml @@ -50,6 +50,8 @@ jobs: run: ./ci/sat.py debug - name: Scheduler testing run: ./ci/scheduling.py + - name: APE validator + run: ./ci/ape-val.sh - name: GG solving run: ./ci/gg.py - name: PDDL Solving (PDDL & HDDL) diff --git a/Cargo.lock b/Cargo.lock index 64f19e813..84e08d29c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -173,6 +173,8 @@ dependencies = [ "itertools", "planx", "smallvec", + "tracing", + "tracing-subscriber", ] [[package]] @@ -183,6 +185,7 @@ dependencies = [ "env_param", "idmap", "itertools", + "num-rational", "smallvec", "tracing", ] diff --git a/Cargo.toml b/Cargo.toml index ca5dc58b8..034d42d16 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -60,7 +60,7 @@ tokio = { default-features = false, version = "1.49.0", features = [ "macros", ] } tokio-stream = { default-features = false, version = "0.1" } -tracing = { version = "0.1", features = ["release_max_level_debug"] } +tracing = { version = "0.1", features = ["release_max_level_info"] } tracing-subscriber = "0.3" transitive = "1.2.0" vec_map = "0.8" diff --git a/aries_fzn/src/aries/constraint/abs.rs b/aries_fzn/src/aries/constraint/abs.rs index 841f9797f..74668535c 100644 --- a/aries_fzn/src/aries/constraint/abs.rs +++ b/aries_fzn/src/aries/constraint/abs.rs @@ -1,7 +1,7 @@ use aries::model::Label; use aries::model::Model; use aries::model::lang::IVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinEq; @@ -40,11 +40,11 @@ impl Post for Abs { let plus_a = self.a; let sum = vec![ - NFLinearSumItem { + ScaledVar { var: plus_a.into(), factor: 1, }, - NFLinearSumItem { + ScaledVar { var: minus_a.into(), factor: 1, }, diff --git a/aries_fzn/src/aries/constraint/lin_eq.rs b/aries_fzn/src/aries/constraint/lin_eq.rs index a5a4f51a0..1591f3299 100644 --- a/aries_fzn/src/aries/constraint/lin_eq.rs +++ b/aries_fzn/src/aries/constraint/lin_eq.rs @@ -1,7 +1,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinGe; @@ -13,16 +13,16 @@ use crate::aries::constraint::LinLe; /// where `v[i]` are variables, `b` and `c[i]` constants. #[derive(Debug)] pub struct LinEq { - sum: Vec, + sum: Vec, b: IntCst, } impl LinEq { - pub fn new(sum: Vec, b: IntCst) -> Self { + pub fn new(sum: Vec, b: IntCst) -> Self { Self { sum, b } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_eq_half.rs b/aries_fzn/src/aries/constraint/lin_eq_half.rs index 30954b259..de4cb9635 100644 --- a/aries_fzn/src/aries/constraint/lin_eq_half.rs +++ b/aries_fzn/src/aries/constraint/lin_eq_half.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinGeHalf; @@ -16,17 +16,17 @@ use crate::aries::constraint::LinLeHalf; /// `b` and `c[i]` constants. #[derive(Debug)] pub struct LinEqHalf { - sum: Vec, + sum: Vec, b: IntCst, r: BVar, } impl LinEqHalf { - pub fn new(sum: Vec, b: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, b: IntCst, r: BVar) -> Self { Self { sum, b, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_eq_reif.rs b/aries_fzn/src/aries/constraint/lin_eq_reif.rs index 8fe3b0ee7..fbd8f180e 100644 --- a/aries_fzn/src/aries/constraint/lin_eq_reif.rs +++ b/aries_fzn/src/aries/constraint/lin_eq_reif.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::AndReif; @@ -17,17 +17,17 @@ use crate::aries::constraint::LinLeReif; /// `b` and `c[i]` constants. #[derive(Debug)] pub struct LinEqReif { - sum: Vec, + sum: Vec, b: IntCst, r: BVar, } impl LinEqReif { - pub fn new(sum: Vec, b: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, b: IntCst, r: BVar) -> Self { Self { sum, b, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_ge.rs b/aries_fzn/src/aries/constraint/lin_ge.rs index c6777ce48..d5ac6665a 100644 --- a/aries_fzn/src/aries/constraint/lin_ge.rs +++ b/aries_fzn/src/aries/constraint/lin_ge.rs @@ -1,7 +1,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinLe; @@ -12,16 +12,16 @@ use crate::aries::constraint::LinLe; /// where `v[i]` are variables, `b` and `c[i]` constants. #[derive(Debug)] pub struct LinGe { - items: Vec, + items: Vec, lb: IntCst, } impl LinGe { - pub fn new(items: Vec, lb: IntCst) -> Self { + pub fn new(items: Vec, lb: IntCst) -> Self { Self { items, lb } } - pub fn items(&self) -> &Vec { + pub fn items(&self) -> &Vec { &self.items } @@ -32,7 +32,7 @@ impl LinGe { impl Post for LinGe { fn post(&self, model: &mut Model) { - let minus = |i: &NFLinearSumItem| NFLinearSumItem { + let minus = |i: &ScaledVar| ScaledVar { var: i.var, factor: -i.factor, }; diff --git a/aries_fzn/src/aries/constraint/lin_ge_half.rs b/aries_fzn/src/aries/constraint/lin_ge_half.rs index 43fa02ff5..d3f779941 100644 --- a/aries_fzn/src/aries/constraint/lin_ge_half.rs +++ b/aries_fzn/src/aries/constraint/lin_ge_half.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinLeHalf; @@ -15,17 +15,17 @@ use crate::aries::constraint::LinLeHalf; /// `lb` and `c[i]` constants. #[derive(Debug)] pub struct LinGeHalf { - sum: Vec, + sum: Vec, lb: IntCst, r: BVar, } impl LinGeHalf { - pub fn new(sum: Vec, lb: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, lb: IntCst, r: BVar) -> Self { Self { sum, lb, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_ge_reif.rs b/aries_fzn/src/aries/constraint/lin_ge_reif.rs index 2929efdeb..901655726 100644 --- a/aries_fzn/src/aries/constraint/lin_ge_reif.rs +++ b/aries_fzn/src/aries/constraint/lin_ge_reif.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinLeReif; @@ -15,17 +15,17 @@ use crate::aries::constraint::LinLeReif; /// `lb` and `c[i]` constants. #[derive(Debug)] pub struct LinGeReif { - sum: Vec, + sum: Vec, lb: IntCst, r: BVar, } impl LinGeReif { - pub fn new(sum: Vec, lb: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, lb: IntCst, r: BVar) -> Self { Self { sum, lb, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_le.rs b/aries_fzn/src/aries/constraint/lin_le.rs index b8cc48224..107410e86 100644 --- a/aries_fzn/src/aries/constraint/lin_le.rs +++ b/aries_fzn/src/aries/constraint/lin_le.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::linear::NFLinearLeq; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use aries::reif::ReifExpr; use crate::aries::Post; @@ -13,16 +13,16 @@ use crate::aries::Post; /// where `v[i]` are variables, `b` and `c[i]` constants. #[derive(Debug)] pub struct LinLe { - items: Vec, + items: Vec, ub: IntCst, } impl LinLe { - pub fn new(items: Vec, ub: IntCst) -> Self { + pub fn new(items: Vec, ub: IntCst) -> Self { Self { items, ub } } - pub fn items(&self) -> &Vec { + pub fn items(&self) -> &Vec { &self.items } diff --git a/aries_fzn/src/aries/constraint/lin_le_half.rs b/aries_fzn/src/aries/constraint/lin_le_half.rs index a70e67d52..f340146fc 100644 --- a/aries_fzn/src/aries/constraint/lin_le_half.rs +++ b/aries_fzn/src/aries/constraint/lin_le_half.rs @@ -5,7 +5,7 @@ use aries::model::lang::BVar; use aries::model::lang::IVar; use aries::model::lang::linear::LinearSum; use aries::model::lang::linear::LinearTerm; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; @@ -17,17 +17,17 @@ use crate::aries::Post; /// `ub` and `c[i]` constants. #[derive(Debug)] pub struct LinLeHalf { - sum: Vec, + sum: Vec, ub: IntCst, r: BVar, } impl LinLeHalf { - pub fn new(sum: Vec, ub: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, ub: IntCst, r: BVar) -> Self { Self { sum, ub, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_le_reif.rs b/aries_fzn/src/aries/constraint/lin_le_reif.rs index fc83d6a57..9777d0824 100644 --- a/aries_fzn/src/aries/constraint/lin_le_reif.rs +++ b/aries_fzn/src/aries/constraint/lin_le_reif.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinGeHalf; @@ -17,17 +17,17 @@ use crate::aries::constraint::Ne; /// `ub` and `c[i]` constants. #[derive(Debug)] pub struct LinLeReif { - sum: Vec, + sum: Vec, ub: IntCst, r: BVar, } impl LinLeReif { - pub fn new(sum: Vec, ub: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, ub: IntCst, r: BVar) -> Self { Self { sum, ub, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_ne.rs b/aries_fzn/src/aries/constraint/lin_ne.rs index f916d460a..4e06e50e5 100644 --- a/aries_fzn/src/aries/constraint/lin_ne.rs +++ b/aries_fzn/src/aries/constraint/lin_ne.rs @@ -4,7 +4,7 @@ use aries::model::Model; use aries::model::lang::IVar; use aries::model::lang::linear::LinearSum; use aries::model::lang::linear::LinearTerm; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; @@ -14,16 +14,16 @@ use crate::aries::Post; /// where `v[i]` are variables, `b` and `c[i]` constants. #[derive(Debug)] pub struct LinNe { - sum: Vec, + sum: Vec, b: IntCst, } impl LinNe { - pub fn new(sum: Vec, b: IntCst) -> Self { + pub fn new(sum: Vec, b: IntCst) -> Self { Self { sum, b } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/lin_ne_reif.rs b/aries_fzn/src/aries/constraint/lin_ne_reif.rs index c1792269f..31c0ebe43 100644 --- a/aries_fzn/src/aries/constraint/lin_ne_reif.rs +++ b/aries_fzn/src/aries/constraint/lin_ne_reif.rs @@ -2,7 +2,7 @@ use aries::core::IntCst; use aries::model::Label; use aries::model::Model; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use crate::aries::Post; use crate::aries::constraint::LinGeReif; @@ -17,17 +17,17 @@ use crate::aries::constraint::OrReif; /// `b` and `c[i]` constants. #[derive(Debug)] pub struct LinNeReif { - sum: Vec, + sum: Vec, b: IntCst, r: BVar, } impl LinNeReif { - pub fn new(sum: Vec, b: IntCst, r: BVar) -> Self { + pub fn new(sum: Vec, b: IntCst, r: BVar) -> Self { Self { sum, b, r } } - pub fn sum(&self) -> &Vec { + pub fn sum(&self) -> &Vec { &self.sum } diff --git a/aries_fzn/src/aries/constraint/test.rs b/aries_fzn/src/aries/constraint/test.rs index ce29a601c..7cbb65895 100644 --- a/aries_fzn/src/aries/constraint/test.rs +++ b/aries_fzn/src/aries/constraint/test.rs @@ -9,7 +9,7 @@ use aries::core::VarRef; use aries::model::Model; use aries::model::lang::BVar; use aries::model::lang::IVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use aries::solver::SearchLimit; use aries::solver::Solver; use itertools::Itertools; @@ -154,7 +154,7 @@ pub(super) fn basic_int_model_3() -> (Model, IVar, IVar, IVar) { /// The linear sum is 3\*x + 2\*y with bound 13. pub(super) fn basic_lin_model() -> ( Model, - Vec, + Vec, IVar, IVar, IntCst, @@ -168,11 +168,11 @@ pub(super) fn basic_lin_model() -> ( let b = 13; let sum = vec![ - NFLinearSumItem { + ScaledVar { var: x.into(), factor: c_x, }, - NFLinearSumItem { + ScaledVar { var: y.into(), factor: c_y, }, diff --git a/aries_fzn/src/fzn/constraint/builtins/bool_lin_eq.rs b/aries_fzn/src/fzn/constraint/builtins/bool_lin_eq.rs index 995a09df8..afaf7bd18 100644 --- a/aries_fzn/src/fzn/constraint/builtins/bool_lin_eq.rs +++ b/aries_fzn/src/fzn/constraint/builtins/bool_lin_eq.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use aries::core::VarRef; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -110,16 +110,16 @@ impl Encode for BoolLinEq { translation: &HashMap, ) -> Box> { let translate = |v: Rc| translation.get(v.id()).unwrap(); - let mut sum: Vec = self + let mut sum: Vec = self .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1), factor: *x.0, }) .collect(); - sum.push(NFLinearSumItem { + sum.push(ScaledVar { var: *translation.get(self.c.id()).unwrap(), factor: -1, }); diff --git a/aries_fzn/src/fzn/constraint/builtins/bool_lin_le.rs b/aries_fzn/src/fzn/constraint/builtins/bool_lin_le.rs index 080fdf41f..20a443272 100644 --- a/aries_fzn/src/fzn/constraint/builtins/bool_lin_le.rs +++ b/aries_fzn/src/fzn/constraint/builtins/bool_lin_le.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use aries::core::VarRef; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -113,7 +113,7 @@ impl Encode for BoolLinLe { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_eq.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_eq.rs index ddcf215f9..864fcf14b 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_eq.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_eq.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use aries::core::VarRef; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -112,7 +112,7 @@ impl Encode for IntLinEq { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_imp.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_imp.rs index 14ba1c506..371af5357 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_imp.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_imp.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use aries::core::VarRef; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -127,7 +127,7 @@ impl Encode for IntLinEqImp { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1.id()), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_reif.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_reif.rs index 1950276fa..5a519138d 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_reif.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_eq_reif.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use aries::core::VarRef; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -127,7 +127,7 @@ impl Encode for IntLinEqReif { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1.id()), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_le.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_le.rs index a2172f400..b4181dca6 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_le.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_le.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use aries::core::VarRef; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -112,7 +112,7 @@ impl Encode for IntLinLe { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_le_imp.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_le_imp.rs index a4cd5be7e..0af3eb3c0 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_le_imp.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_le_imp.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use aries::core::VarRef; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -127,7 +127,7 @@ impl Encode for IntLinLeImp { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1.id()), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_le_reif.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_le_reif.rs index 819a8a8ae..f26d819ab 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_le_reif.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_le_reif.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use aries::core::VarRef; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -127,7 +127,7 @@ impl Encode for IntLinLeReif { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1.id()), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_ne.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_ne.rs index a9f9c46f3..db7e93821 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_ne.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_ne.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use aries::core::VarRef; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -112,7 +112,7 @@ impl Encode for IntLinNe { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1), factor: *x.0, }) diff --git a/aries_fzn/src/fzn/constraint/builtins/int_lin_ne_reif.rs b/aries_fzn/src/fzn/constraint/builtins/int_lin_ne_reif.rs index dc682551f..6c02632af 100644 --- a/aries_fzn/src/fzn/constraint/builtins/int_lin_ne_reif.rs +++ b/aries_fzn/src/fzn/constraint/builtins/int_lin_ne_reif.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use aries::core::VarRef; use aries::model::lang::BVar; -use aries::model::lang::linear::NFLinearSumItem; +use aries::model::lang::linear::ScaledVar; use flatzinc::ConstraintItem; use crate::aries::Post; @@ -127,7 +127,7 @@ impl Encode for IntLinNeReif { .a .iter() .zip(self.b.clone()) - .map(|x| NFLinearSumItem { + .map(|x| ScaledVar { var: *translate(x.1.id()), factor: *x.0, }) diff --git a/ci/ape-val.sh b/ci/ape-val.sh new file mode 100755 index 000000000..9c0b90630 --- /dev/null +++ b/ci/ape-val.sh @@ -0,0 +1,46 @@ +# Runs APE's validator on a all plan files in planning/problem/upf +# +# +# Some pointer for generating plans: (here for tamer) +# cd planning/problems/upf +# find . -type d -exec sh -c 'cd "{}" && up oneshot-planning --pddl domain.pddl problem.pddl --engine tamer --plan problem.tamer.plan || true' \; + +set -e # Exit on first error + +# Path to planner and validators (defaults to ci build) +APE="${PLANNER:-target/ci/ape} " +HDDL_VAL="${HDDL_VAL:-planning/ext/val-hddl}" +PDDL_VAL="${PDDL_VAL:-planning/ext/val-pddl}" + +# Time allowed for each run (defaults to 90s) +TIMEOUT="${TIMEOUT:-5s}" + +echo "Building..." +cargo build --profile ci --bin ape + +PLAN_FILES=$(find planning/problems/upf -name *.plan | sort) + +for PLAN_FILE in $PLAN_FILES +do + echo "" + echo "Plan: ${PLAN_FILE}" + PROBLEM_FILE=`${APE} find-problem ${PLAN_FILE}` + DOMAIN_FILE=`${APE} find-domain ${PROBLEM_FILE}` + + VAL_CMD="${PDDL_VAL} ${DOMAIN_FILE} ${PROBLEM_FILE} ${PLAN_FILE}" + + # Run VAL with some post-processing to + # - exit with error on invalid plan + # - extract only the computed plan quality on the stdout and save in in $PLAN_QUALITY + PLAN_QUALITY=`${VAL_CMD} | awk -v cmd="${VAL_CMD}" '/Plan valid/{ok=1} ok && /Final value:/ {print $3; exit} END{if(!ok) {print "INVALID (from val)\n> " cmd >"/dev/stderr"; exit 1}}'` + echo "VAL plan quality: ${PLAN_QUALITY}" + timeout ${TIMEOUT} ${APE} validate ${PLAN_FILE} --expected-objective ${PLAN_QUALITY} + + # Just check that the plan-optimizer does not crash... + # echo "OPT PRESENCE: " optimize-plan ${PLAN_FILE} -r action-presence + # timeout ${TIMEOUT} ${APE} optimize-plan ${PLAN_FILE} -r action-presence > /dev/null + # echo "OPT TIME: " optimize-plan ${PLAN_FILE} -r start-time + # timeout ${TIMEOUT} ${APE} optimize-plan ${PLAN_FILE} -r start-time > /dev/null + # echo "OPT PRESENCE TIME: " optimize-plan ${PLAN_FILE} -r action-presence -r start-time + timeout ${TIMEOUT} ${APE} optimize-plan ${PLAN_FILE} -r action-presence -r start-time > /dev/null +done 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/engine/Cargo.toml b/planning/engine/Cargo.toml index 7de096290..936c59615 100644 --- a/planning/engine/Cargo.toml +++ b/planning/engine/Cargo.toml @@ -13,6 +13,8 @@ derive_more = { workspace = true } itertools = { workspace = true } im = { workspace = true } smallvec = { workspace = true } +tracing = { workspace = true } +tracing-subscriber = { workspace = true } planx = { path = "../planx" } timelines = { package = "aries-timelines", path = "../timelines" } 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))) +) diff --git a/planning/engine/src/encode.rs b/planning/engine/src/encode.rs index 40482eaeb..b26fa76e3 100644 --- a/planning/engine/src/encode.rs +++ b/planning/engine/src/encode.rs @@ -1,20 +1,25 @@ //! A number of utility functions for converting from `planx` to `aries-timelines` pub mod constraints; +pub mod encoding; pub mod required_values; +pub mod tags; use aries::{ core::literals::ConjunctionBuilder, model::lang::{ - FAtom, - expr::{and, eq}, + BoolExpr, + expr::{and, eq, lin_eq}, }, prelude::*, reif::ReifExpr, }; 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 planx::{ExprId, Fun, Message, Model, Res, Sym, TimeRef, Timestamp, errors::Spanned}; +use timelines::{ + Effect, EffectOp, IntExp, IntTerm, Sched, StateVar, SymAtom, TaskId, Time, constraints::HasValueAt, + symbols::ObjectEncoding, +}; use crate::encode::{constraints::ConditionConstraint, required_values::RequiredValues}; @@ -44,6 +49,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> { @@ -52,6 +58,7 @@ impl<'a> Scope<'a> { end: sched.horizon, presence: Lit::TRUE, args: im::OrdMap::new(), + source: None, } } } @@ -68,6 +75,7 @@ pub fn condition_to_constraint( required_values: Option<&mut RequiredValues>, ) -> Res { let expr = model.env.node(expr); + let timepoint = reify_timing(tp, model, sched, bindings)?; let constraint = match expr.expr() { planx::Expr::StateVariable(fluent_id, args) => { let fluent = model.env.fluents.get(*fluent_id); @@ -82,9 +90,10 @@ pub fn condition_to_constraint( }; let c = HasValueAt { state_var, - value: Lit::TRUE.into(), - timepoint: reify_timing(tp, model, sched, bindings)?, + value: IntTerm::TRUE, + timepoint, prez: bindings.presence, + source: bindings.source, }; ConditionConstraint::HasValue(c) } @@ -93,22 +102,31 @@ 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), + ConditionConstraint::EqZero(sum) => ConditionConstraint::NeqZero(sum), + ConditionConstraint::NeqZero(sum) => ConditionConstraint::EqZero(sum), + ConditionConstraint::LeqZero(_) => todo!(), } } planx::Expr::App(planx::Fun::Eq, exprs) if exprs.len() == 2 => { - let e1 = reify_sym(exprs[0], model, sched, bindings)?; - let e2 = reify_sym(exprs[1], model, sched, bindings)?; - ConditionConstraint::Eq(e1, e2) + let e1 = reify_expression(exprs[0], Some(timepoint), model, sched, bindings)?; + let e2 = reify_expression(exprs[1], Some(timepoint), model, sched, bindings)?; + ConditionConstraint::EqZero(e1 - e2) + } + planx::Expr::App(planx::Fun::Leq, exprs) if exprs.len() == 2 => { + let lhs = reify_expression(exprs[0], Some(timepoint), model, sched, bindings)?; + let rhs = reify_expression(exprs[1], Some(timepoint), model, sched, bindings)?; + ConditionConstraint::LeqZero(lhs - rhs) } - e => todo!("{e:?}"), + _ => return Err(expr.todo("not supported")), }; // update the required values if requested by caller @@ -117,26 +135,27 @@ 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(_, _) => {} - ConditionConstraint::Neq(_, _) => {} + ConditionConstraint::EqZero(_) => {} // TODO: are those handled in reifications? + ConditionConstraint::NeqZero(_) => {} + ConditionConstraint::LeqZero(_) => {} //TODO } } Ok(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 @@ -149,19 +168,18 @@ pub fn convert_effect( args, }; let op = match x.operation { - planx::EffectOp::Assign(e) => { - let val = reify_bool(e, model, sched)?; - EffectOp::Assign(val) - } - _ => todo!(), + planx::EffectOp::Assign(v) => EffectOp::Assign(reify_expression_to_term(v, Some(t), model, sched, bindings)?), + planx::EffectOp::Increase(v) => EffectOp::Step(reify_expression_to_term(v, Some(t), model, sched, bindings)?), + planx::EffectOp::Decrease(v) => EffectOp::Step(-reify_expression_to_term(v, Some(t), model, sched, bindings)?), }; let eff = timelines::Effect { transition_start: t, - transition_end: if transition_time { t + FAtom::EPSILON } else { t }, + transition_end: if transition_time { t + sched.epsilon } else { t }, mutex_end: sched.new_timepoint(), state_var: sv, operation: op, prez: bindings.presence, + source: bindings.source, }; Ok(eff) } @@ -171,25 +189,30 @@ 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(), args, }; // we manually create the mutex-end since it may have a negative value if canceledd by an initial positive effect - let mutex_end: Time = sched.model.new_fvar(-1, INT_CST_MAX, sched.time_scale, "_").into(); + let mutex_end: Time = sched.model.new_ivar(-1, INT_CST_MAX, "_").into(); let eff = timelines::Effect { transition_start: t, 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, }; sched.add_effect(eff); } @@ -213,12 +236,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 @@ -227,8 +251,8 @@ pub fn convert_to_pddl_set_semantics(effs: Vec, sched: &mut Sched) -> Ve // they can be placed at the same timepoit && sched .model - .var_domain(e.transition_end.num) - .overlaps(&sched.model.var_domain(o.transition_end.num)) // TODO: we ignore the denominator here, which may not be correct in temporal planning + .var_domain(e.transition_end) + .overlaps(&sched.model.var_domain(o.transition_end)) // they arguments are compatible && e.state_var .args @@ -262,7 +286,7 @@ pub fn convert_to_pddl_set_semantics(effs: Vec, sched: &mut Sched) -> Ve override_conditions.push(sched.model.reify(eq(e.transition_start, overrider.transition_start))); // overrider must have the same state variable arguments for (a1, a2) in e.state_var.args.iter().zip_eq(overrider.state_var.args.iter()) { - override_conditions.push(sched.model.reify(eq(*a1, *a2))); + override_conditions.push(lin_eq(*a1, *a2).reified(&mut sched.model)); } let lits = override_conditions.build(); let cancelled_by = sched.model.reify(ReifExpr::And(lits.into_lits())); @@ -282,43 +306,128 @@ pub fn convert_to_pddl_set_semantics(effs: Vec, sched: &mut Sched) -> Ve with_set_semantics } -pub fn reify_timing(t: Timestamp, model: &Model, sched: &mut Sched, binding: &Scope) -> Res { +pub fn reify_timing(t: Timestamp, model: &Model, sched: &mut Sched, binding: &Scope) -> Res