feat(planning): Extend symmetry breaking to numeric planning problems

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,6 +39,7 @@
     "blink": 5,
     "invert": 7,
 }
+SLOW_THRESHOLD = 5
 VALID_STATUS = {Status.SOLVED_SATISFICING, Status.SOLVED_OPTIMALLY}
 
 IS_GITHUB_ACTIONS = os.getenv("GITHUB_ACTIONS") == "true"
@@ -57,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
@@ -80,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(
@@ -180,11 +188,22 @@ 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] = []
 
+timing: Dict[str, float] = {}
+status: Dict[str, str] = {}
+
 try:
     for i, folder in enumerate(problems):
         separator(
@@ -194,7 +213,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"
@@ -207,32 +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)
-                    write(f"Elapsed time: {time.time() - start:.3f} s", light=True)
-                    write(f"Status: {result.status}", light=True)
+                    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:
@@ -243,57 +263,96 @@ 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_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
 finally:
     # 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, 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)

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 {
@@ -745,25 +735,31 @@ 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;
         }
 
         tracing::debug!(%num_numeric_assignment_coherence_constraints);
         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;
 
         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"
@@ -772,12 +768,17 @@ 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);
             // 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_post_increase(inc_id.instance_id, inc_id.eff_id),
                 prez,
                 Condition {
                     start: inc.transition_end,
@@ -801,21 +802,24 @@ 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;
             }
-            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();
 
             for &(ass_id, ass_prez, ass) in &assigns {
                 if solver.model.entails(!ass_prez) {
@@ -851,11 +855,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 +900,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 +928,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]);
         }