From d782097f454cf31def5a90d2050c9507217f8207 Mon Sep 17 00:00:00 2001
From: Roland Godet <r.godet@outlook.fr>
Date: Mon, 25 Nov 2024 12:37:53 +0100
Subject: [PATCH 1/8] ci(ipc): store slow results

---
 ci/ipc.py | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/ci/ipc.py b/ci/ipc.py
index 5a4773ab..605bbcd9 100644
--- a/ci/ipc.py
+++ b/ci/ipc.py
@@ -39,6 +39,7 @@
     "blink": 5,
     "invert": 7,
 }
+SLOW_THRESHOLD = 1
 VALID_STATUS = {Status.SOLVED_SATISFICING, Status.SOLVED_OPTIMALLY}
 
 IS_GITHUB_ACTIONS = os.getenv("GITHUB_ACTIONS") == "true"
@@ -184,6 +185,7 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
 invalid: List[str] = []
 unsolved: List[Tuple[str, str]] = []
 update_depth: List[str] = []
+slow: List[Tuple[str, float]] = []
 
 try:
     for i, folder in enumerate(problems):
@@ -194,7 +196,7 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
             blue=True,
         )
 
-        out_file = f"/tmp/aries-{folder.stem}.log"
+        out_file = f"/tmp/aries-{folder.stem}.log"  # nosec: B108
 
         try:
             domain = folder / "domain.pddl"
@@ -231,8 +233,11 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
                     start = time.time()
                     result = planner.solve(upf_pb, output_stream=output)
                     write("Resolution status", cyan=True)
-                    write(f"Elapsed time: {time.time() - start:.3f} s", light=True)
+                    timing = time.time() - start
+                    write(f"Elapsed time: {timing:.3f} s", light=True)
                     write(f"Status: {result.status}", light=True)
+                    if timing > SLOW_THRESHOLD:
+                        slow.append((folder.stem, timing))
 
                     # Update max depth
                     if not has_max_depth:
@@ -255,6 +260,7 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
 
                     # Unsolved problem
                     else:
+                        write(Path(out_file).read_text(encoding="utf-8"), yellow=True)
                         unsolved.append((folder.stem, result.status.name))
                         write("Unsolved problem", bold=True, red=True)
 
@@ -279,6 +285,12 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
         for res in valid:
             print(res)
 
+    if slow:
+        big_separator(title=f"Slow: {len(slow)}", bold=True, yellow=True)
+        offset = max(map(len, map(lambda t: t[0], slow))) + 3
+        for res, timing in sorted(slow, key=lambda t: t[1], reverse=True):
+            print(f"{res:<{offset}} {timing:.3f} s")
+
     if invalid:
         big_separator(title=f"Invalid: {len(invalid)}", bold=True, red=True)
         for res in invalid:

From 1ebca9539a55df17f01a2f6b1cf09f193c82be99 Mon Sep 17 00:00:00 2001
From: Roland Godet <r.godet@outlook.fr>
Date: Mon, 25 Nov 2024 13:08:16 +0100
Subject: [PATCH 2/8] ci(ipc): save best results for comparison

---
 ci/ipc.py | 115 ++++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 81 insertions(+), 34 deletions(-)

diff --git a/ci/ipc.py b/ci/ipc.py
index 605bbcd9..877e9e4f 100644
--- a/ci/ipc.py
+++ b/ci/ipc.py
@@ -4,7 +4,7 @@
 import subprocess  # nosec: B404
 import sys
 import time
-from typing import List, Optional, Tuple
+from typing import Dict, List, Optional, Tuple
 
 from unified_planning.engines.results import PlanGenerationResultStatus as Status
 from unified_planning.io.pddl_reader import PDDLReader
@@ -39,7 +39,7 @@
     "blink": 5,
     "invert": 7,
 }
-SLOW_THRESHOLD = 1
+SLOW_THRESHOLD = 5
 VALID_STATUS = {Status.SOLVED_SATISFICING, Status.SOLVED_OPTIMALLY}
 
 IS_GITHUB_ACTIONS = os.getenv("GITHUB_ACTIONS") == "true"
@@ -58,7 +58,14 @@ def write(text: str = "", **markup: bool) -> None:
     esc = [ESC_TABLE[name] for name, value in markup.items() if value]
     if esc:
         text = "".join(f"\x1b[{cod}m" for cod in esc) + text + "\x1b[0m"
-    print(text)
+    print(text, end="")
+
+
+def write_line(text: str = "", **markup: bool) -> None:
+    """Write a line of text with ANSI escape sequences for formatting."""
+    write(text, **markup)
+    if not text.endswith("\n"):
+        print()
 
 
 # pylint: disable=too-many-arguments
@@ -81,8 +88,8 @@ def separator(
     if len(line) + len(sep.rstrip()) <= width:
         line += sep.rstrip()
     if github_group and IS_GITHUB_ACTIONS:
-        write(f"::group::{title}")
-    write(f"{before}{line}{after}", **markup)
+        write_line(f"::group::{title}")
+    write_line(f"{before}{line}{after}", **markup)
 
 
 def big_separator(
@@ -181,11 +188,21 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
 if len(sys.argv) > 1:
     problems = [pb for pb in problems if pb.stem in sys.argv[1:]]
 
+last_results: Dict[str, Tuple[str, float]] = {}
+last_results_file = Path("/tmp/aries_ci_ipc_last_best_results.csv")  # nosec: B108
+if last_results_file.exists():
+    lines = last_results_file.read_text(encoding="utf-8").splitlines()
+    for _line in lines:
+        pb, s, t = _line.split(",")
+        last_results[pb] = (s, float(t))
+
 valid: List[str] = []
 invalid: List[str] = []
 unsolved: List[Tuple[str, str]] = []
 update_depth: List[str] = []
-slow: List[Tuple[str, float]] = []
+
+timing: Dict[str, float] = {}
+status: Dict[str, str] = {}
 
 try:
     for i, folder in enumerate(problems):
@@ -209,35 +226,33 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
                 max_depth = 100  # pylint: disable=invalid-name
 
             with open(out_file, mode="w+", encoding="utf-8") as output:
-                write(f"Output log: {output.name}\n")
+                write_line(f"Output log: {output.name}\n")
 
                 with OneshotPlanner(
                     name="aries",
                     params={"max-depth": max_depth},
                 ) as planner:
                     # Problem Kind
-                    write("Problem Kind", cyan=True)
-                    write(str(upf_pb.kind), light=True)
-                    write()
+                    write_line("Problem Kind", cyan=True)
+                    write_line(str(upf_pb.kind), light=True)
+                    write_line()
 
                     # Unsupported features
                     unsupported = upf_pb.kind.features.difference(
                         planner.supported_kind().features
                     )
                     if unsupported:
-                        write("Unsupported Features", cyan=True)
-                        write("\n".join(unsupported), light=True)
-                        write()
+                        write_line("Unsupported Features", cyan=True)
+                        write_line("\n".join(unsupported), light=True)
+                        write_line()
 
                     # Resolution
                     start = time.time()
                     result = planner.solve(upf_pb, output_stream=output)
-                    write("Resolution status", cyan=True)
-                    timing = time.time() - start
-                    write(f"Elapsed time: {timing:.3f} s", light=True)
-                    write(f"Status: {result.status}", light=True)
-                    if timing > SLOW_THRESHOLD:
-                        slow.append((folder.stem, timing))
+                    write_line("Resolution status", cyan=True)
+                    timing[folder.stem] = time.time() - start
+                    write_line(f"Elapsed time: {timing[folder.stem]:.3f} s", light=True)
+                    write_line(f"Status: {result.status}", light=True)
 
                     # Update max depth
                     if not has_max_depth:
@@ -248,31 +263,37 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
 
                     # Solved problem
                     if result.status in VALID_STATUS:
-                        write("\nValidating plan by Val", cyan=True)
+                        write_line("\nValidating plan by Val", cyan=True)
                         out_path = Path(output.name)
                         extract_plan_for_val(result.plan, domain, problem, out_path)
                         if validate_plan_with_val(problem, domain, out_path):
-                            write("Plan is valid", bold=True, green=True)
+                            write_line("Plan is valid", bold=True, green=True)
                             valid.append(folder.stem)
+                            status[folder.stem] = "valid"
                         else:
-                            write("Plan is invalid", bold=True, red=True)
+                            write_line("Plan is invalid", bold=True, red=True)
                             invalid.append(folder.stem)
+                            status[folder.stem] = "invalid"
 
                     # Unsolved problem
                     else:
-                        write(Path(out_file).read_text(encoding="utf-8"), yellow=True)
+                        write_line(
+                            Path(out_file).read_text(encoding="utf-8"), yellow=True
+                        )
                         unsolved.append((folder.stem, result.status.name))
-                        write("Unsolved problem", bold=True, red=True)
+                        status[folder.stem] = result.status.name.lower()
+                        write_line("Unsolved problem", bold=True, red=True)
 
         except Exception as e:  # pylint: disable=broad-except
             unsolved.append((folder.stem, "Error"))
-            write(f"Error: {e}", bold=True, red=True)
-            write()
-            write(Path(out_file).read_text(encoding="utf-8"), yellow=True)
+            status[folder.stem] = "error"
+            write_line(f"Error: {e}", bold=True, red=True)
+            write_line()
+            write_line(Path(out_file).read_text(encoding="utf-8"), yellow=True)
 
         finally:
             if IS_GITHUB_ACTIONS:
-                write("::endgroup::")
+                write_line("::endgroup::")
 
 except KeyboardInterrupt:
     pass
@@ -280,32 +301,58 @@ def validate_plan_with_val(pb: Path, dom: Path, plan: Path) -> bool:
     # Summary
     separator(title="Summary", bold=True, blue=True)
 
+    csv_data = ""  # pylint: disable=invalid-name
+    for folder in problems:
+        t = min(  # type: ignore
+            timing[folder.stem],
+            (
+                last_results[folder.stem][1]
+                if folder.stem in last_results
+                else float("inf")
+            ),
+        )
+        csv_data += f"{folder.stem},{status[folder.stem]},{t}\n"
+    last_results_file.write_text(csv_data, encoding="utf-8")
+
     if valid:
         big_separator(title=f"Valid: {len(valid)}", bold=True, green=True)
+        offset = max(map(len, valid)) + 3
         for res in valid:
-            print(res)
+            time_str = f" {last_results[res][1]:.3f} -> " if res in last_results else ""
+            time_str += f"{timing[res]:.3f}"
+            write(f"{res:<{offset}} ")
+            if res in last_results and timing[res] < last_results[res][1]:
+                write_line(time_str, bold=True, green=True)
+            elif (
+                res in last_results
+                and timing[res] - last_results[res][1] > SLOW_THRESHOLD
+            ):
+                write_line(time_str, red=True)
+            else:
+                write_line(time_str)
 
+    slow = list(filter(lambda t: t[1] > SLOW_THRESHOLD, timing.items()))
     if slow:
         big_separator(title=f"Slow: {len(slow)}", bold=True, yellow=True)
         offset = max(map(len, map(lambda t: t[0], slow))) + 3
-        for res, timing in sorted(slow, key=lambda t: t[1], reverse=True):
-            print(f"{res:<{offset}} {timing:.3f} s")
+        for res, t in sorted(slow, key=lambda t: t[1], reverse=True):  # type: ignore
+            write_line(f"{res:<{offset}} {t:.3f}")
 
     if invalid:
         big_separator(title=f"Invalid: {len(invalid)}", bold=True, red=True)
         for res in invalid:
-            print(res)
+            write_line(res)
 
     if unsolved:
         big_separator(title=f"Unsolved: {len(unsolved)}", bold=True, red=True)
         offset = max(map(len, map(lambda t: t[0], unsolved))) + 3
         for res, reason in unsolved:
-            print(f"{res:<{offset}} {reason}")
+            write_line(f"{res:<{offset}} {reason}")
 
     if update_depth:
         big_separator(title=f"Updated depth: {len(update_depth)}", bold=True)
         for res in update_depth:
-            print(res)
+            write_line(res)
 
     EXIT_CODE = 0 if not invalid and not unsolved else 1
     big_separator(title=f"End with code {EXIT_CODE}", bold=True)

From b94790cee284630602c8f164ebbbda52f77692f0 Mon Sep 17 00:00:00 2001
From: Roland Godet <r.godet@outlook.fr>
Date: Tue, 26 Nov 2024 15:42:31 +0100
Subject: [PATCH 3/8] feat(planning): numeric symmetry breaking

---
 planning/planners/src/encode.rs          | 41 ++++++++-------
 planning/planners/src/encode/symmetry.rs | 67 ++++++++++++++++--------
 planning/planners/src/encoding.rs        | 43 +++++++++++----
 3 files changed, 98 insertions(+), 53 deletions(-)

diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs
index 040e5fa2..5525b9a5 100644
--- a/planning/planners/src/encode.rs
+++ b/planning/planners/src/encode.rs
@@ -12,7 +12,7 @@ use aries::core::*;
 use aries::model::extensions::{AssignmentExt, Shaped};
 use aries::model::lang::linear::LinearSum;
 use aries::model::lang::mul::EqVarMulLit;
-use aries::model::lang::{expr::*, Atom, IVar, Kind, Type};
+use aries::model::lang::{expr::*, Atom, IVar, Type};
 use aries::model::lang::{FAtom, FVar, IAtom, Variable};
 use aries_planning::chronicles::constraints::encode_constraint;
 use aries_planning::chronicles::*;
@@ -486,16 +486,6 @@ pub struct EncodedProblem {
     pub encoding: Encoding,
 }
 
-/// Returns whether the effect is an assignment.
-fn is_assignment(eff: &Effect) -> bool {
-    matches!(eff.operation, EffectOp::Assign(_))
-}
-
-/// Returns whether the state variable is numeric.
-fn is_integer(sv: &StateVar) -> bool {
-    matches!(sv.fluent.return_type().into(), Kind::Int)
-}
-
 /// Returns whether two state variables are unifiable.
 fn unifiable_sv(model: &Model, sv1: &StateVar, sv2: &StateVar) -> bool {
     sv1.fluent == sv2.fluent && model.unifiable_seq(&sv1.args, &sv2.args)
@@ -664,7 +654,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
 
         for &(cond_id, prez_cond, cond) in &conds {
             // skip conditions on numeric state variables, they are supported by numeric support constraints
-            if is_integer(&cond.state_var) {
+            if is_numeric(&cond.state_var) {
                 continue;
             }
             if solver.model.entails(!prez_cond) {
@@ -736,7 +726,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
         let mut num_numeric_assignment_coherence_constraints = 0;
 
         for &(_, prez, ass) in &assigns {
-            if !is_integer(&ass.state_var) {
+            if !is_numeric(&ass.state_var) {
                 continue;
             }
             let Type::Int { lb, ub } = ass.state_var.fluent.return_type() else {
@@ -755,15 +745,16 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
         solver.propagate()?;
     }
 
-    let mut increase_coherence_conditions: Vec<(Lit, Condition)> = Vec::with_capacity(incs.len());
+    let mut increase_coherence_conditions: Vec<(CondID, Lit, Condition)> = Vec::with_capacity(incs.len());
     {
         // numeric increase coherence constraints
         let span = tracing::span!(tracing::Level::TRACE, "numeric increase coherence");
         let _span = span.enter();
         let mut num_numeric_increase_coherence_constraints = 0;
+        let mut next_cond_id = 10000; // TODO: use a proper ID
 
         for &(inc_id, prez, inc) in &incs {
-            assert!(is_integer(&inc.state_var));
+            assert!(is_numeric(&inc.state_var));
             assert!(
                 inc.transition_start + FAtom::EPSILON == inc.transition_end && inc.min_mutex_end.is_empty(),
                 "Only instantaneous increases are supported"
@@ -778,6 +769,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
             // Check that the state variable value is equals to the new variable `var`.
             // It will force the state variable to be in the bounds of the new variable after the increase.
             increase_coherence_conditions.push((
+                CondID::new(inc_id.instance_id, next_cond_id),
                 prez,
                 Condition {
                     start: inc.transition_end,
@@ -786,6 +778,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                     value: var.into(),
                 },
             ));
+            next_cond_id += 1;
             num_numeric_increase_coherence_constraints += 1;
         }
 
@@ -801,14 +794,14 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
 
         let numeric_conds: Vec<_> = conds
             .iter()
-            .filter(|(_, _, cond)| is_integer(&cond.state_var))
-            .map(|&(_, prez, cond)| (prez, cond.clone()))
+            .filter(|(_, _, cond)| is_numeric(&cond.state_var))
+            .map(|&(id, prez, cond)| (id, prez, cond.clone()))
             .chain(increase_coherence_conditions)
             .collect();
 
-        for (cond_prez, cond) in &numeric_conds {
+        for (cond_id, cond_prez, cond) in &numeric_conds {
             // skip conditions on non-numeric state variables, they have already been supported by support constraints
-            assert!(is_integer(&cond.state_var));
+            assert!(is_numeric(&cond.state_var));
             if solver.model.entails(!*cond_prez) {
                 continue;
             }
@@ -816,6 +809,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                 unreachable!()
             };
             let mut supported: Vec<Lit> = Vec::with_capacity(128);
+            let mut inc_support: HashMap<EffID, Vec<Lit>> = HashMap::new();
 
             for &(ass_id, ass_prez, ass) in &assigns {
                 if solver.model.entails(!ass_prez) {
@@ -851,11 +845,12 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                 if solver.model.entails(!supported_by) {
                     continue;
                 }
+                encoding.tag(supported_by, Tag::Support(*cond_id, ass_id));
 
                 // the expected condition value
                 let mut cond_val_sum = LinearSum::from(ass_val) - cond_val;
 
-                for &(_, inc_prez, inc) in &incs {
+                for &(inc_id, inc_prez, inc) in &incs {
                     if solver.model.entails(!inc_prez) {
                         continue;
                     }
@@ -895,6 +890,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                     if solver.model.entails(!active_inc) {
                         continue;
                     }
+                    inc_support.entry(inc_id).or_default().push(active_inc);
                     for term in inc_val.terms() {
                         // compute some static implication for better propagation
                         let p = solver.model.presence_literal(term.var().into());
@@ -922,6 +918,11 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                 num_numeric_support_constraints += 1;
             }
 
+            for (inc_id, inc_support) in inc_support {
+                let supported_by_inc = solver.reify(or(inc_support));
+                encoding.tag(supported_by_inc, Tag::Support(*cond_id, inc_id));
+            }
+
             solver.enforce(or(supported), [*cond_prez]);
         }
 
diff --git a/planning/planners/src/encode/symmetry.rs b/planning/planners/src/encode/symmetry.rs
index 46c5bd14..a4b56e2e 100644
--- a/planning/planners/src/encode/symmetry.rs
+++ b/planning/planners/src/encode/symmetry.rs
@@ -4,7 +4,7 @@ use analysis::CausalSupport;
 use aries::core::Lit;
 use aries::model::extensions::AssignmentExt;
 use aries::model::lang::expr::{and, f_leq, implies, or};
-use aries_planning::chronicles::analysis::{Feature, Metadata};
+use aries_planning::chronicles::analysis::Metadata;
 use aries_planning::chronicles::{ChronicleOrigin, FiniteProblem};
 use env_param::EnvParam;
 use itertools::Itertools;
@@ -46,7 +46,7 @@ impl std::str::FromStr for SymmetryBreakingType {
 }
 
 fn supported_by_psp(meta: &Metadata) -> bool {
-    !meta.class.is_hierarchical() && !meta.features.contains(&Feature::Numeric)
+    !meta.class.is_hierarchical()
 }
 
 pub fn add_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encoding: &Encoding) {
@@ -139,7 +139,13 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         .sorted()
         .dedup()
         .collect_vec();
-    let mut causal_link: HashMap<(ChronicleId, CondID), Lit> = Default::default();
+
+    #[derive(Clone, Copy)]
+    struct Link {
+        active: Lit,
+        exclusive: bool,
+    }
+    let mut causal_link: HashMap<(ChronicleId, CondID), Link> = Default::default();
     let mut conds_by_templates: HashMap<TemplateID, HashSet<CondID>> = Default::default();
     for template in &templates {
         conds_by_templates.insert(*template, HashSet::new());
@@ -164,7 +170,13 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         // non-optional literal that is true iff the causal link is active
         let link_active = model.reify(and([v, model.presence_literal(v.variable())]));
         // list of outgoing causal links of the supporting action
-        causal_link.insert((eff.instance_id, cond), link_active);
+        causal_link.insert(
+            (eff.instance_id, cond),
+            Link {
+                active: link_active,
+                exclusive: eff.is_assign,
+            },
+        );
     }
 
     let sort = |conds: HashSet<CondID>| {
@@ -185,7 +197,12 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
     };
     let conds_by_templates: HashMap<TemplateID, Vec<CondID>> =
         conds_by_templates.into_iter().map(|(k, v)| (k, sort(v))).collect();
-    let supports = |ch: ChronicleId, cond: CondID| causal_link.get(&(ch, cond)).copied().unwrap_or(Lit::FALSE);
+    let supports = |ch: ChronicleId, cond: CondID| {
+        causal_link.get(&(ch, cond)).copied().unwrap_or(Link {
+            active: Lit::FALSE,
+            exclusive: true,
+        })
+    };
 
     for template_id in &templates {
         let conditions = &conds_by_templates[template_id];
@@ -206,32 +223,36 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         //     }
         // }
 
-        for (i, instance) in instances.iter().copied().enumerate() {
-            let mut clause = Vec::with_capacity(64);
+        for (i, crt_instance) in instances.iter().copied().enumerate() {
+            let mut clause = Vec::with_capacity(conditions.len());
             if i > 0 {
-                let prev = instances[i - 1];
+                let prv_instance = instances[i - 1];
 
-                // the chronicle is allowed to support a condition only if the previous chronicle
-                // supports a condition at an earlier level
-                for (cond_index, cond) in conditions.iter().enumerate() {
+                // The current instance is allowed to support a condition only if the previous instance
+                // supports a condition at an earlier level or at the same level.
+                for (j, crt_cond) in conditions.iter().enumerate() {
                     clause.clear();
-                    clause.push(!supports(*instance, *cond));
 
-                    for prev_cond in &conditions[0..cond_index] {
-                        clause.push(supports(*prev, *prev_cond));
+                    let crt_link = supports(*crt_instance, *crt_cond);
+                    let prv_link = supports(*prv_instance, *crt_cond);
+                    clause.push(!crt_link.active);
+                    if !(crt_link.exclusive && prv_link.exclusive) {
+                        clause.push(prv_link.active);
                     }
+
+                    for prv_cond in &conditions[0..j] {
+                        let crt_link = supports(*crt_instance, *prv_cond);
+                        let prv_link = supports(*prv_instance, *prv_cond);
+                        if crt_link.exclusive && prv_link.exclusive {
+                            clause.push(prv_link.active);
+                        } else {
+                            clause.push(model.reify(and([prv_link.active, !crt_link.active])));
+                        }
+                    }
+
                     model.enforce(or(clause.as_slice()), []);
                 }
             }
-            clause.clear();
-            if discard_useless_supports {
-                // enforce that a chronicle be present only if it supports at least one condition
-                clause.push(!pb.chronicles[*instance].chronicle.presence);
-                for cond in conditions {
-                    clause.push(supports(*instance, *cond))
-                }
-                model.enforce(or(clause.as_slice()), []);
-            }
         }
     }
 
diff --git a/planning/planners/src/encoding.rs b/planning/planners/src/encoding.rs
index 470dafe2..989ae86c 100644
--- a/planning/planners/src/encoding.rs
+++ b/planning/planners/src/encoding.rs
@@ -1,5 +1,5 @@
-use aries::core::Lit;
 use aries::model::lang::FAtom;
+use aries::{core::Lit, model::lang::Kind};
 use aries_planning::chronicles::*;
 use env_param::EnvParam;
 use std::collections::{BTreeSet, HashSet};
@@ -31,10 +31,16 @@ pub struct EffID {
     pub instance_id: ChronicleId,
     /// Index of the effect in the effects of the instance
     pub eff_id: usize,
+    /// Whether the effect is an assignment
+    pub is_assign: bool,
 }
 impl EffID {
-    pub fn new(instance_id: usize, eff_id: usize) -> Self {
-        Self { instance_id, eff_id }
+    pub fn new(instance_id: usize, eff_id: usize, is_assign: bool) -> Self {
+        Self {
+            instance_id,
+            eff_id,
+            is_assign,
+        }
     }
 }
 pub type ChronicleId = usize;
@@ -64,22 +70,34 @@ impl Encoding {
 /// - a literal that is true iff the effect is present in the solution.
 pub fn effects(pb: &FiniteProblem) -> impl Iterator<Item = (EffID, Lit, &Effect)> {
     pb.chronicles.iter().enumerate().flat_map(|(instance_id, ch)| {
-        ch.chronicle
-            .effects
-            .iter()
-            .enumerate()
-            .map(move |(eff_id, eff)| (EffID { instance_id, eff_id }, ch.chronicle.presence, eff))
+        ch.chronicle.effects.iter().enumerate().map(move |(eff_id, eff)| {
+            (
+                EffID::new(instance_id, eff_id, is_assignment(eff)),
+                ch.chronicle.presence,
+                eff,
+            )
+        })
     })
 }
 
+/// Returns true if the effect is an assignment effect.
+pub fn is_assignment(eff: &Effect) -> bool {
+    matches!(eff.operation, EffectOp::Assign(_))
+}
+
 /// Iterator over all assignment effects in a finite problem.
 pub fn assignments(pb: &FiniteProblem) -> impl Iterator<Item = (EffID, Lit, &Effect)> {
-    effects(pb).filter(|(_, _, eff)| matches!(eff.operation, EffectOp::Assign(_)))
+    effects(pb).filter(|(_, _, eff)| is_assignment(eff))
+}
+
+/// Returns true if the effect is an increase effect.
+pub fn is_increase(eff: &Effect) -> bool {
+    matches!(eff.operation, EffectOp::Increase(_))
 }
 
 /// Iterator over all increase effects in a finite problem.
 pub fn increases(pb: &FiniteProblem) -> impl Iterator<Item = (EffID, Lit, &Effect)> {
-    effects(pb).filter(|(_, _, eff)| matches!(eff.operation, EffectOp::Increase(_)))
+    effects(pb).filter(|(_, _, eff)| is_increase(eff))
 }
 
 /// Iterates over all conditions in a finite problem.
@@ -97,6 +115,11 @@ pub fn conditions(pb: &FiniteProblem) -> impl Iterator<Item = (CondID, Lit, &Con
     })
 }
 
+/// Returns true if the state variable is numeric.
+pub fn is_numeric(sv: &StateVar) -> bool {
+    matches!(sv.fluent.return_type().into(), Kind::Int)
+}
+
 pub struct TaskRef<'a> {
     pub presence: Lit,
     pub start: FAtom,

From 6612433ded3cc468fba200f8d2ba1598d1717851 Mon Sep 17 00:00:00 2001
From: Roland Godet <r.godet@outlook.fr>
Date: Mon, 9 Dec 2024 08:46:54 +0100
Subject: [PATCH 4/8] docs(planning): Explication for the lexicographic
 ordering

---
 planning/planners/src/encode/symmetry.rs | 36 ++++++++++++++++++------
 1 file changed, 27 insertions(+), 9 deletions(-)

diff --git a/planning/planners/src/encode/symmetry.rs b/planning/planners/src/encode/symmetry.rs
index a4b56e2e..e2931ee4 100644
--- a/planning/planners/src/encode/symmetry.rs
+++ b/planning/planners/src/encode/symmetry.rs
@@ -223,34 +223,52 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
         //     }
         // }
 
+        // An instance of the template is allowed to support a condition only if the previous instance
+        // supports a condition at an earlier level or at the same level.
+        //
+        // Noting X = [x_1, x_2, ..., x_n] where x_i <=> previous instance supports condition i
+        // and    Y = [y_1, y_2, ..., y_n] where y_i <=> current instance supports condition i
+        // We ensure that X >= Y in the lexicographic order.
+        //
+        // This is done recursively for 1 <= j <= n:
+        //     X[1:j] >= Y[1:j] <=> (x_j >= y_j OR there exists i < j such that x_i > y_i)
+        //                       AND X[1:j-1] >= Y[1:j-1]
+        //
+        // Because we are dealing with literals, we can simplify the comparison to:
+        //     x > y <=> x AND !y    if x and y are not exclusive
+        //     x > y <=> x           if x and y are exclusive
+        //     x >= y <=> x OR !y    if x and y are not exclusive
+        //     x >= y <=> !y         if x and y are exclusive
         for (i, crt_instance) in instances.iter().copied().enumerate() {
             let mut clause = Vec::with_capacity(conditions.len());
             if i > 0 {
                 let prv_instance = instances[i - 1];
 
-                // The current instance is allowed to support a condition only if the previous instance
-                // supports a condition at an earlier level or at the same level.
                 for (j, crt_cond) in conditions.iter().enumerate() {
-                    clause.clear();
-
-                    let crt_link = supports(*crt_instance, *crt_cond);
-                    let prv_link = supports(*prv_instance, *crt_cond);
-                    clause.push(!crt_link.active);
+                    clause.clear(); // Stores the disjunction for the first part of X[1:j] >= Y[1:j]
+                    let prv_link = supports(*prv_instance, *crt_cond); // x_j
+                    let crt_link = supports(*crt_instance, *crt_cond); // y_j
+                    clause.push(!crt_link.active); // x_j >= y_j
                     if !(crt_link.exclusive && prv_link.exclusive) {
+                        // x_j >= y_j (not exclusive)
                         clause.push(prv_link.active);
                     }
 
                     for prv_cond in &conditions[0..j] {
-                        let crt_link = supports(*crt_instance, *prv_cond);
-                        let prv_link = supports(*prv_instance, *prv_cond);
+                        let prv_link = supports(*prv_instance, *prv_cond); // x_k
+                        let crt_link = supports(*crt_instance, *prv_cond); // y_k
                         if crt_link.exclusive && prv_link.exclusive {
+                            // x_k > y_k (exclusive)
                             clause.push(prv_link.active);
                         } else {
+                            // x_k > y_k (not exclusive)
                             clause.push(model.reify(and([prv_link.active, !crt_link.active])));
                         }
                     }
 
+                    // (x_j >= y_j OR there exists i < j such that x_i > y_i)
                     model.enforce(or(clause.as_slice()), []);
+                    // X[1:j-1] >= Y[1:j-1] has been enforced by the previous iteration of the loop
                 }
             }
         }

From da8ce5bf4a4856f4438d7b4ef299f915698d4461 Mon Sep 17 00:00:00 2001
From: Roland Godet <r.godet@outlook.fr>
Date: Mon, 9 Dec 2024 09:09:02 +0100
Subject: [PATCH 5/8] feat(planning): detect fixed fluents as numeric

---
 planning/planners/src/encode.rs   | 18 +++++++++++++-----
 planning/planners/src/encoding.rs |  2 +-
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs
index 5525b9a5..e6d88475 100644
--- a/planning/planners/src/encode.rs
+++ b/planning/planners/src/encode.rs
@@ -735,9 +735,15 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
             let EffectOp::Assign(val) = ass.operation else {
                 unreachable!()
             };
-            let Atom::Int(val) = val else { unreachable!() };
-            solver.enforce(geq(val, lb), [prez]);
-            solver.enforce(leq(val, ub), [prez]);
+            if let Atom::Int(val) = val {
+                solver.enforce(geq(val, lb), [prez]);
+                solver.enforce(leq(val, ub), [prez]);
+            } else if let Atom::Fixed(val) = val {
+                solver.enforce(f_geq(val, FAtom::new((lb * val.denom).into(), val.denom)), [prez]);
+                solver.enforce(f_leq(val, FAtom::new((ub * val.denom).into(), val.denom)), [prez]);
+            } else {
+                unreachable!();
+            }
             num_numeric_assignment_coherence_constraints += 1;
         }
 
@@ -805,8 +811,10 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
             if solver.model.entails(!*cond_prez) {
                 continue;
             }
-            let Atom::Int(cond_val) = cond.value else {
-                unreachable!()
+            let cond_val = match cond.value {
+                Atom::Int(val) => FAtom::new(val, 1),
+                Atom::Fixed(val) => val,
+                _ => unreachable!(),
             };
             let mut supported: Vec<Lit> = Vec::with_capacity(128);
             let mut inc_support: HashMap<EffID, Vec<Lit>> = HashMap::new();
diff --git a/planning/planners/src/encoding.rs b/planning/planners/src/encoding.rs
index 989ae86c..4b7143b4 100644
--- a/planning/planners/src/encoding.rs
+++ b/planning/planners/src/encoding.rs
@@ -117,7 +117,7 @@ pub fn conditions(pb: &FiniteProblem) -> impl Iterator<Item = (CondID, Lit, &Con
 
 /// Returns true if the state variable is numeric.
 pub fn is_numeric(sv: &StateVar) -> bool {
-    matches!(sv.fluent.return_type().into(), Kind::Int)
+    matches!(sv.fluent.return_type().into(), Kind::Int) || matches!(sv.fluent.return_type().into(), Kind::Fixed(_))
 }
 
 pub struct TaskRef<'a> {

From 744d539c08dbdca95c4be9ba3b6afa50319f688f Mon Sep 17 00:00:00 2001
From: Roland Godet <r.godet@outlook.fr>
Date: Wed, 11 Dec 2024 11:34:19 +0100
Subject: [PATCH 6/8] fix(planning): add mis-removed condition

---
 planning/planners/src/encode/symmetry.rs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/planning/planners/src/encode/symmetry.rs b/planning/planners/src/encode/symmetry.rs
index e2931ee4..52df5c13 100644
--- a/planning/planners/src/encode/symmetry.rs
+++ b/planning/planners/src/encode/symmetry.rs
@@ -271,6 +271,15 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
                     // X[1:j-1] >= Y[1:j-1] has been enforced by the previous iteration of the loop
                 }
             }
+            clause.clear();
+            if discard_useless_supports {
+                // enforce that a chronicle be present only if it supports at least one condition
+                clause.push(!pb.chronicles[*crt_instance].chronicle.presence);
+                for cond in conditions {
+                    clause.push(supports(*crt_instance, *cond).active);
+                }
+                model.enforce(or(clause.as_slice()), []);
+            }
         }
     }
 

From dcc73e8aadc150e4eb705c034cb1da80d591aeb9 Mon Sep 17 00:00:00 2001
From: Arthur Bit-Monnot <abitmonnot@laas.fr>
Date: Tue, 17 Dec 2024 13:51:27 +0100
Subject: [PATCH 7/8] fix(planning): correctly represent synthetic conditions
 introduced for numerics

---
 planning/planners/src/encode.rs               |  4 +---
 planning/planners/src/encode/symmetry.rs      |  7 +++++--
 planning/planners/src/encoding.rs             | 19 +++++++++++++++----
 planning/planners/src/search/causal.rs        |  7 ++++++-
 .../analysis/detrimental_supports.rs          | 17 +++++++++++++----
 .../planning/src/chronicles/analysis/mod.rs   |  2 +-
 6 files changed, 41 insertions(+), 15 deletions(-)

diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs
index e6d88475..f8c23362 100644
--- a/planning/planners/src/encode.rs
+++ b/planning/planners/src/encode.rs
@@ -757,7 +757,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
         let span = tracing::span!(tracing::Level::TRACE, "numeric increase coherence");
         let _span = span.enter();
         let mut num_numeric_increase_coherence_constraints = 0;
-        let mut next_cond_id = 10000; // TODO: use a proper ID
 
         for &(inc_id, prez, inc) in &incs {
             assert!(is_numeric(&inc.state_var));
@@ -775,7 +774,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
             // Check that the state variable value is equals to the new variable `var`.
             // It will force the state variable to be in the bounds of the new variable after the increase.
             increase_coherence_conditions.push((
-                CondID::new(inc_id.instance_id, next_cond_id),
+                CondID::new_post_increase(inc_id.instance_id, inc_id.eff_id),
                 prez,
                 Condition {
                     start: inc.transition_end,
@@ -784,7 +783,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
                     value: var.into(),
                 },
             ));
-            next_cond_id += 1;
             num_numeric_increase_coherence_constraints += 1;
         }
 
diff --git a/planning/planners/src/encode/symmetry.rs b/planning/planners/src/encode/symmetry.rs
index 52df5c13..31d8de1b 100644
--- a/planning/planners/src/encode/symmetry.rs
+++ b/planning/planners/src/encode/symmetry.rs
@@ -292,7 +292,10 @@ fn add_plan_space_symmetry_breaking(pb: &FiniteProblem, model: &mut Model, encod
 #[allow(unused)]
 fn print_cond(cid: CondID, pb: &FiniteProblem, model: &Model) {
     let ch = &pb.chronicles[cid.instance_id];
-    let cond = &ch.chronicle.conditions[cid.cond_id];
-    let s = model.shape.symbols.format(&[cond.state_var.fluent.sym]);
+    let state_var = match cid.cond_id {
+        analysis::CondOrigin::ExplicitCondition(cond_id) => &ch.chronicle.conditions[cond_id].state_var,
+        analysis::CondOrigin::PostIncrease(eff_id) => &ch.chronicle.effects[eff_id].state_var,
+    };
+    let s = model.shape.symbols.format(&[state_var.fluent.sym]);
     print!("  {:?}:{}", ch.origin, s)
 }
diff --git a/planning/planners/src/encoding.rs b/planning/planners/src/encoding.rs
index 4b7143b4..eb78d286 100644
--- a/planning/planners/src/encoding.rs
+++ b/planning/planners/src/encoding.rs
@@ -1,5 +1,6 @@
 use aries::model::lang::FAtom;
 use aries::{core::Lit, model::lang::Kind};
+pub use aries_planning::chronicles::analysis::CondOrigin;
 use aries_planning::chronicles::*;
 use env_param::EnvParam;
 use std::collections::{BTreeSet, HashSet};
@@ -16,11 +17,21 @@ pub struct CondID {
     /// Index of the instance in which the condition appears
     pub instance_id: ChronicleId,
     /// Index of the condition in the instance
-    pub cond_id: usize,
+    pub cond_id: CondOrigin,
 }
+
 impl CondID {
-    pub fn new(instance_id: usize, cond_id: usize) -> Self {
-        Self { instance_id, cond_id }
+    pub fn new_explicit(instance_id: usize, cond_id: usize) -> Self {
+        Self {
+            instance_id,
+            cond_id: CondOrigin::ExplicitCondition(cond_id),
+        }
+    }
+    pub fn new_post_increase(instance_id: usize, eff_id: usize) -> Self {
+        Self {
+            instance_id,
+            cond_id: CondOrigin::PostIncrease(eff_id),
+        }
     }
 }
 
@@ -111,7 +122,7 @@ pub fn conditions(pb: &FiniteProblem) -> impl Iterator<Item = (CondID, Lit, &Con
             .conditions
             .iter()
             .enumerate()
-            .map(move |(cond_id, cond)| (CondID::new(instance_id, cond_id), ch.chronicle.presence, cond))
+            .map(move |(cond_id, cond)| (CondID::new_explicit(instance_id, cond_id), ch.chronicle.presence, cond))
     })
 }
 
diff --git a/planning/planners/src/search/causal.rs b/planning/planners/src/search/causal.rs
index 88283c28..d3dd1283 100644
--- a/planning/planners/src/search/causal.rs
+++ b/planning/planners/src/search/causal.rs
@@ -7,6 +7,7 @@ use aries::model::lang::{SAtom, Type};
 use aries::model::symbols::TypedSym;
 use aries::solver::search::{Decision, SearchControl};
 use aries::solver::stats::Stats;
+use aries_planning::chronicles::analysis::CondOrigin;
 use aries_planning::chronicles::{ChronicleInstance, Condition, Effect, FiniteProblem, StateVar, VarLabel};
 use env_param::EnvParam;
 use std::collections::HashSet;
@@ -36,7 +37,11 @@ impl ManualCausalSearch {
         &self.problem.chronicles[chronicle_id]
     }
     fn cond(&self, cond_id: CondID) -> &Condition {
-        &self.ch(cond_id.instance_id).chronicle.conditions[cond_id.cond_id]
+        if let CondOrigin::ExplicitCondition(cond_index) = cond_id.cond_id {
+            &self.ch(cond_id.instance_id).chronicle.conditions[cond_index]
+        } else {
+            panic!("Condition is implicit")
+        }
     }
     fn eff(&self, eff_id: EffID) -> &Effect {
         &self.ch(eff_id.instance_id).chronicle.effects[eff_id.eff_id]
diff --git a/planning/planning/src/chronicles/analysis/detrimental_supports.rs b/planning/planning/src/chronicles/analysis/detrimental_supports.rs
index 5268592a..64333ab8 100644
--- a/planning/planning/src/chronicles/analysis/detrimental_supports.rs
+++ b/planning/planning/src/chronicles/analysis/detrimental_supports.rs
@@ -175,7 +175,16 @@ pub struct TemplateCondID {
     /// id of the chronicle template in which the condition occurs
     pub template_id: usize,
     /// Index of the condition in the template's conditions
-    pub cond_id: usize,
+    pub cond_id: CondOrigin,
+}
+
+#[derive(Ord, PartialOrd, Eq, PartialEq, Hash, Copy, Clone, Debug)]
+pub enum CondOrigin {
+    /// This originates from the i-th condition of the chronicle
+    ExplicitCondition(usize),
+    /// This is a synthetic condition representing the value of the state variables after an increase effect.
+    /// It is the i-th effect of the chronicle.
+    PostIncrease(usize),
 }
 #[derive(Hash, Copy, Clone, Eq, PartialEq, Debug)]
 pub struct TemplateEffID {
@@ -193,7 +202,7 @@ pub struct CausalSupport {
 }
 
 impl CausalSupport {
-    pub fn new(eff_template: usize, eff_id: usize, cond_template: usize, cond_id: usize) -> Self {
+    pub fn new(eff_template: usize, eff_id: usize, cond_template: usize, cond_id: CondOrigin) -> Self {
         Self {
             supporter: TemplateEffID {
                 template_id: eff_template,
@@ -213,7 +222,7 @@ impl CausalSupport {
             },
             condition: TemplateCondID {
                 template_id: cond.template_id,
-                cond_id: cond.cond_id,
+                cond_id: CondOrigin::ExplicitCondition(cond.cond_id),
             },
         }
     }
@@ -377,7 +386,7 @@ fn gather_detrimental_supports(
                         },
                         condition: TemplateCondID {
                             template_id: c.template_id,
-                            cond_id: c.cond_id,
+                            cond_id: CondOrigin::ExplicitCondition(c.cond_id),
                         },
                     });
                 }
diff --git a/planning/planning/src/chronicles/analysis/mod.rs b/planning/planning/src/chronicles/analysis/mod.rs
index 2985c0e3..ffeada91 100644
--- a/planning/planning/src/chronicles/analysis/mod.rs
+++ b/planning/planning/src/chronicles/analysis/mod.rs
@@ -10,7 +10,7 @@ mod static_fluents;
 
 pub use crate::chronicles::analysis::features::*;
 use crate::chronicles::preprocessing::action_rolling::RollCompilation;
-pub use detrimental_supports::{CausalSupport, TemplateCondID, TemplateEffID};
+pub use detrimental_supports::{CausalSupport, CondOrigin, TemplateCondID, TemplateEffID};
 pub use static_fluents::is_static;
 
 pub type TemplateID = usize;

From a2732088243354ee1137d8c3c72f0533f5ee6e80 Mon Sep 17 00:00:00 2001
From: Arthur Bit-Monnot <abitmonnot@laas.fr>
Date: Tue, 17 Dec 2024 14:35:03 +0100
Subject: [PATCH 8/8] perf(planning): Avoid unecessary bound-checking
 conditions on unbounded state variables.

---
 planning/planners/src/encode.rs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs
index f8c23362..721bd32d 100644
--- a/planning/planners/src/encode.rs
+++ b/planning/planners/src/encode.rs
@@ -768,6 +768,10 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
             let Type::Int { lb, ub } = inc.state_var.fluent.return_type() else {
                 unreachable!()
             };
+
+            if lb == INT_CST_MIN && ub == INT_CST_MAX {
+                continue;
+            }
             let var = solver
                 .model
                 .new_ivar(lb, ub, Container::Instance(inc_id.instance_id) / VarType::Reification);