diff --git a/ci/sat.py b/ci/sat.py index 0b026118..d042cd93 100755 --- a/ci/sat.py +++ b/ci/sat.py @@ -9,7 +9,7 @@ import time os.system("cargo build --profile ci --bin aries-sat") -solver = "target/ci/aries-sat --threads 1" +solver = "target/ci/aries-sat" solver_cmd = solver + " {params} --source {archive} {instance}" @@ -42,4 +42,3 @@ def run_all(archive, sat): run_all("examples/sat/instances/test-sat.zip", sat=True) run_all("examples/sat/instances/test-unsat.zip", sat=False) - diff --git a/examples/knapsack/main.rs b/examples/knapsack/main.rs index 59d9adaa..bfd3aba0 100644 --- a/examples/knapsack/main.rs +++ b/examples/knapsack/main.rs @@ -1,6 +1,6 @@ #![allow(clippy::needless_range_loop)] -use aries::core::{IntCst, Lit, INT_CST_MAX}; +use aries::core::{IntCst, INT_CST_MAX}; use aries::model::extensions::AssignmentExt; use aries::model::lang::linear::LinearSum; use aries::model::lang::IVar; diff --git a/examples/sat/main.rs b/examples/sat/main.rs index 6721b397..c3e046d0 100644 --- a/examples/sat/main.rs +++ b/examples/sat/main.rs @@ -104,12 +104,12 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option) -> Re let choices: Vec<_> = model.state.variables().map(|v| Lit::geq(v, 1)).collect(); let solver = Box::new(Solver::new(model)); - let search_params: Vec<_> = opt.search.split(",").collect(); + let search_params: Vec<_> = opt.search.split(',').collect(); let num_threads = search_params.len(); let conflict_params = |conf: &str| { let mut params = Params::default(); - for opt in conf.split(":") { + for opt in conf.split(':') { let handled = params.configure(opt); if !handled { panic!("UNSUPPORTED OPTION: {opt}") @@ -119,8 +119,8 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option) -> Re }; let mut par_solver = ParSolver::new(solver, num_threads, |id, solver| { - let search_params: Vec<_> = search_params[id].split("/").collect(); - let stable_params = if search_params.len() > 0 { + let search_params: Vec<_> = search_params[id].split('/').collect(); + let stable_params = if !search_params.is_empty() { search_params[0] } else { "+lrb:+p+l:-neg" diff --git a/examples/scheduling/src/search.rs b/examples/scheduling/src/search.rs index cfabc7e7..9778b630 100644 --- a/examples/scheduling/src/search.rs +++ b/examples/scheduling/src/search.rs @@ -82,12 +82,14 @@ struct Strat { pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_threads: usize) -> ParSolver { let mut base_solver = Box::new(base); - let mut load_conf = |conf: &str| -> Strat { + let load_conf = |conf: &str| -> Strat { let mut mode = Mode::Stable; - let mut params = conflicts::Params::default(); - params.heuristic = conflicts::Heuristic::LearningRate; - params.active = conflicts::ActiveLiterals::Reasoned; - params.impact_measure = ImpactMeasure::LBD; + let mut params = conflicts::Params { + heuristic: conflicts::Heuristic::LearningRate, + active: conflicts::ActiveLiterals::Reasoned, + impact_measure: ImpactMeasure::LBD, + ..Default::default() + }; for opt in conf.split(':') { if params.configure(opt) { // handled @@ -111,7 +113,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th SearchStrategy::Default => "stable:+sol", SearchStrategy::Custom(conf) => conf.as_str(), }; - let all_strats = conf.split("/").map(|s| load_conf(s)).collect_vec(); + let all_strats = conf.split('/').map(load_conf).collect_vec(); let decision_lits: Vec = base_solver .model @@ -131,8 +133,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th Mode::Stable => (2000, 1.2), // stable: few restarts Mode::Focused => (800, 1.0), // focused: always aggressive restarts }; - let brancher = brancher.with_restarts(restart_period, restart_update); - brancher + brancher.with_restarts(restart_period, restart_update) }; // build a brancher that alternates between the proposed strategies @@ -160,7 +161,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th .collect_vec(); // conflict based search, possibly alternating between several strategies - let branchers = strats.into_iter().map(|strat| build_brancher(strat)).collect_vec(); + let branchers = strats.into_iter().map(build_brancher).collect_vec(); let brancher = round_robin(branchers); // search strategy. For the first one simply add a greedy EST strategy to bootstrap the search diff --git a/planning/planners/src/bin/lcp.rs b/planning/planners/src/bin/lcp.rs index 71b5610a..e2dde851 100644 --- a/planning/planners/src/bin/lcp.rs +++ b/planning/planners/src/bin/lcp.rs @@ -65,6 +65,15 @@ pub struct Opt { } fn main() -> Result<()> { + // Terminate the process if a thread panics. + // take_hook() returns the default hook in case when a custom one is not set + let orig_hook = std::panic::take_hook(); + std::panic::set_hook(Box::new(move |panic_info| { + // invoke the default handler and exit the process + orig_hook(panic_info); + std::process::exit(1); + })); + let opt: Opt = Opt::from_args(); // set up logger diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index f3a4f581..da605470 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -10,29 +10,16 @@ use anyhow::{Context, Result}; use aries::core::state::Conflict; use aries::core::*; use aries::model::extensions::{AssignmentExt, Shaped}; -use aries::model::lang::linear::{LinearSum, LinearTerm}; -use aries::model::lang::{expr::*, Kind, Type}; +use aries::model::lang::linear::LinearSum; +use aries::model::lang::{expr::*, IVar, Kind}; use aries::model::lang::{FAtom, FVar, IAtom, Variable}; -use aries::solver::Solver; use aries_planning::chronicles::constraints::encode_constraint; -use aries_planning::chronicles::printer::Printer; use aries_planning::chronicles::*; use env_param::EnvParam; +use std::cmp::{max, min}; use std::collections::{HashMap, HashSet}; -use std::convert::TryFrom; use std::ptr; -/// Parameter that activates the debug view of the resource constraints. -/// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_DEBUG`. -/// Possible values are `false`(default) and `true`. -pub static RESOURCE_CONSTRAINT_DEBUG: EnvParam = EnvParam::new("ARIES_RESOURCE_CONSTRAINT_DEBUG", "false"); - -/// Parameter that activates the usage of timepoints to encode the increase's literals. -/// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS`. -/// Possible values are `false` and `true` (default). -pub static RESOURCE_CONSTRAINT_TIMEPOINTS: EnvParam = - EnvParam::new("ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS", "true"); - /// Parameter that activates the temporal relaxation of temporal constraints of a task's /// interval and the its methods intervals. The temporal relaxation can be used when /// using an acting system to allow the interval of a method to be included in the interval @@ -390,6 +377,31 @@ fn enforce_refinement(t: TaskRef, supporters: Vec, model: &mut Model) { } } +/// Reify an integer atom to a linear sum evaluated to zero if not present. +fn reify_or_zero(model: &mut Model, atom: IAtom, lit: Lit) -> LinearSum { + if atom.var == IVar::ZERO { + // Constant variable + if atom.shift == 0 { + LinearSum::zero() + } else { + let prez = IVar::new(lit.variable()); + LinearSum::of(vec![prez * atom.shift]) + } + } else { + // Real variable + let prez = model.reify(and([lit, model.presence_literal(atom.var.into())])); + let lb = model.lower_bound(atom.var); + let ub = model.upper_bound(atom.var); + let lbl = model.get_label(atom.var).unwrap().clone(); + let var = model.new_ivar(min(lb, 0), max(ub, 0), lbl); + let eq_0 = model.reify(eq(var, 0)); + let eq_atom = model.reify(eq(var, atom.var)); + model.enforce(implies(prez, eq_atom), []); + model.enforce(implies(!prez, eq_0), []); + reify_or_zero(model, atom.shift.into(), prez) + var + } +} + /// Encode a metric in the problem and returns an integer that should minimized in order to optimize the metric. pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAtom { match metric { @@ -407,15 +419,9 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto } // for each action, create an optional variable that evaluate to 1 if the action is present and 0 otherwise - let action_costs: Vec = action_presence - .iter() - .map(|(ch_id, p)| { - model - .new_optional_ivar(1, 1, *p, Container::Instance(*ch_id).var(VarType::Cost)) - .or_zero(*p) - }) - .collect(); - let action_costs = LinearSum::of(action_costs); + let action_costs: LinearSum = action_presence.iter().fold(LinearSum::zero(), |acc, (_ch_id, p)| { + acc + reify_or_zero(model, 1.into(), *p) + }); // make the sum of the action costs equal a `plan_length` variable. let plan_length = model.new_ivar(0, INT_CST_MAX, VarLabel(Container::Base, VarType::Cost)); @@ -435,15 +441,9 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto } // for each action, create an optional variable that evaluate to the cost if the action is present and 0 otherwise - let action_costs: Vec = costs - .iter() - .map(|&(ch_id, p, cost)| { - model - .new_optional_ivar(cost, cost, p, Container::Instance(ch_id).var(VarType::Cost)) - .or_zero(p) - }) - .collect(); - let action_costs = LinearSum::of(action_costs); + let action_costs: LinearSum = costs.iter().fold(LinearSum::zero(), |acc, (_ch_id, p, cost)| { + acc + reify_or_zero(model, (*cost).into(), *p) + }); // make the sum of the action costs equal a `plan_cost` variable. let plan_cost = model.new_ivar(0, INT_CST_MAX, VarLabel(Container::Base, VarType::Cost)); @@ -478,11 +478,6 @@ fn is_assignment(eff: &Effect) -> bool { matches!(eff.operation, EffectOp::Assign(_)) } -/// Returns whether the effect is an increase. -fn is_increase(eff: &Effect) -> bool { - matches!(eff.operation, EffectOp::Increase(_)) -} - /// Returns whether the state variable is numeric. fn is_integer(sv: &StateVar) -> bool { matches!(sv.fluent.return_type().into(), Kind::Int) @@ -789,30 +784,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result solver.propagate()?; } - { - // Resource constraints - encode_resource_constraints(&mut solver, &effs, &conds, &eff_mutex_ends); - - if RESOURCE_CONSTRAINT_DEBUG.get() { - println!("\n=============================== Constraints =============================="); - Printer::print_reif_constraints(&solver.get_shape().constraints, &solver.model); - - println!("\n=========================== Before Propagation ==========================="); - solver.model.print_state(); - - let after = |solver: &Solver| { - println!("\n============================ After Propagation ==========================="); - solver.model.print_state(); - }; - - let propagation = solver.propagate(); - after(&solver); - propagation?; - } else { - solver.propagate()?; - } - } - let metric = metric.map(|metric| add_metric(pb, &mut solver.model, metric)); symmetry::add_symmetry_breaking(pb, &mut solver.model, &encoding); @@ -824,355 +795,3 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result encoding, }) } - -/* ========================================================================== */ -/* Resource Constraints */ -/* ========================================================================== */ - -fn encode_resource_constraints( - solver: &mut Box>, - effs: &[(EffID, Lit, &Effect)], - conds: &[(CondID, Lit, &Condition)], - eff_mutex_ends: &HashMap, -) { - /* ============================= Variables setup ============================ */ - - let span = tracing::span!(tracing::Level::TRACE, "resources"); - let _span = span.enter(); - let mut num_resource_constraints = 0; - - // Get the effects and the conditions on numeric state variables. - // Filter those who are not present. - let assignments: Vec<_> = effs - .iter() - .filter(|(_, prez, eff)| !solver.model.entails(!*prez) && is_assignment(eff) && is_integer(&eff.state_var)) - .collect(); - let increases: Vec<_> = effs - .iter() - .filter(|(_, prez, eff)| !solver.model.entails(!*prez) && is_increase(eff) && is_integer(&eff.state_var)) - .collect(); - let mut conditions: Vec<_> = conds - .iter() - .filter(|(_, prez, cond)| !solver.model.entails(!*prez) && is_integer(&cond.state_var)) - .map(|&(_, prez, cond)| (prez, cond.clone())) - .collect(); - - /* =============================== Assignments ============================== */ - - tracing::trace_span!("assignments").in_scope(|| { - // Force the new assigned values to be in the state variable domain. - for &&(_, prez, eff) in &assignments { - let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { - unreachable!() - }; - let EffectOp::Assign(val) = eff.operation else { - unreachable!() - }; - let val: IAtom = val.try_into().expect("Not integer assignment to an int state variable"); - solver.enforce(geq(val, lb), [prez]); - solver.enforce(leq(val, ub), [prez]); - num_resource_constraints += 1; - } - }); - - /* ================================ Increases =============================== */ - - // Convert the increase effects into conditions in order to check that the new value is in the state variable domain. - tracing::trace_span!("increases").in_scope(|| { - for &&(eff_id, prez, eff) in &increases { - assert!( - eff.transition_start + FAtom::EPSILON == eff.transition_end && eff.min_mutex_end.is_empty(), - "Only instantaneous effects are supported" - ); - // Get the bounds of the state variable. - let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { - unreachable!() - }; - // Create a new variable with those bounds. - let var = solver - .model - .new_ivar(lb, ub, Container::Instance(eff_id.instance_id) / VarType::Reification); - // Check that the state variable value is equals to that new variable. - // It will force the state variable value to be in the bounds of the new variable. - conditions.push(( - prez, - Condition { - start: eff.transition_end, - end: eff.transition_end, - state_var: eff.state_var.clone(), - value: var.into(), - }, - )); - } - }); - - /* =============================== Conditions =============================== */ - - /* - * For each condition `R == z`, a set of linear sum constraints of the form - * `la_j*ca_j + li_jk*ci_jk + ... + li_jm*ci_jm - la_j*z == 0` are created. - * - * The `la_j` literal is true if and only if the associated assignment effect `e_j` is the last one for the condition. - * A disjunctive clause will force to have at least one `la_j`. - * The `ca_j` value is the value of the assignment effect `e_j`. - * The `li_j*` literals are true if and only if: - * - `la_j` is true - * - the associated increase effect `e_*` is between `e_j` and the condition - * The `ci_j*` values are the value of the increase effects `e_*`. - * The `z` variable is the value of the condition. - * - * With all these literals, only one constraint will be taken into account: the one associated with the last assignment. - */ - tracing::trace_span!("conditions").in_scope(|| { - for (prez_cond, cond) in conditions { - assert_eq!(cond.start, cond.end, "Only the instantaneous conditions are supported"); - - // Returns false if the effect can never support the condition. - let eff_compatible_with_cond = |solver: &Solver, prez_eff: Lit, eff: &Effect| { - !solver.model.state.exclusive(prez_eff, prez_cond) - && unifiable_sv(&solver.model, &cond.state_var, &eff.state_var) - }; - - let compatible_assignments = assignments - .iter() - .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) - .collect::>(); - let compatible_increases = increases - .iter() - .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) - .collect::>(); - - // Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j`. - let la_ca_ta_pa = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { - create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_mutex_ends, solver) - } else { - create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, eff_mutex_ends, solver) - }; - - // Force to have at least one assignment. - let la_disjuncts = la_ca_ta_pa.iter().map(|(la, _, _, _)| *la).collect::>(); - solver.enforce(or(la_disjuncts), [prez_cond]); - - /* - * Matrix to store the `li_j*` literals and `ci_j*` values. - * - * `li_j*` is true if and only if the associated increase effect `e_*`: - * - is present - * - is before the condition - * - is after the assignment effect `e_j` - * - has the same state variable as the condition - * - `la_j` is true - * - the assignment effect associated to `la_j` is present - * - the condition is present - */ - let m_li_ci = la_ca_ta_pa - .iter() - .map(|(la, _, ta, pa)| { - compatible_increases - .iter() - .map(|(_, prez_eff, eff)| { - let mut li_conjunction: Vec = Vec::with_capacity(12); - // `la_j` is true - li_conjunction.push(*la); - // the assignment effect assiciated to `la_j` is present - li_conjunction.push(*pa); - // the condition is present - li_conjunction.push(prez_cond); - // is present - li_conjunction.push(*prez_eff); - // is before the condition - li_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); - // is after the assignment effect `e_j` - li_conjunction.push(solver.reify(f_lt(*ta, eff.transition_end))); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - li_conjunction.push(solver.reify(eq(a, b))); - } - // Create the `li_j*` literal. - let li_lit = solver.reify(and(li_conjunction)); - debug_assert!(solver.model.entails(solver.model.presence_literal(li_lit.variable()))); - - // Get the `ci_j*` value. - let EffectOp::Increase(eff_val) = eff.operation.clone() else { - unreachable!() - }; - (li_lit, eff_val) - }) - .collect::>() - }) - .collect::>(); - - // Create the linear sum constraints. - for (&(la, ca, _, _), li_ci) in la_ca_ta_pa.iter().zip(m_li_ci) { - // Create the sum. - let mut sum = LinearSum::zero(); - sum += LinearSum::with_lit( - ca, - solver.reify(and([la, solver.model.presence_literal(ca.var.into())])), - ); - for (li, ci) in li_ci.iter() { - sum += ci.map_with_lit(|t| { - solver.reify(and([t.lit(), *li, solver.model.presence_literal(t.var().into())])) - }); - } - let cond_val = - IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); - sum -= LinearSum::with_lit( - cond_val, - solver.reify(and([la, solver.model.presence_literal(cond_val.var.into())])), - ); - sum = sum.simplify(); - - // Check that all the literals of the sum are always defined. - // It is wrapped in a `debug_assert!` for performance in release mode. - debug_assert!({ - for term in sum.terms() { - let prez = solver.model.presence_literal(term.lit().variable()); - debug_assert!(solver.model.entails(prez)); - } - true - }); - - // Force the sum to be equals to 0. - solver.enforce(sum.clone().geq(0), [prez_cond]); - solver.enforce(sum.leq(0), [prez_cond]); - num_resource_constraints += 1; - } - } - }); - tracing::debug!(%num_resource_constraints); -} - -/** -Vector to store the `la_j` literals, `ca_j` values, the end of the transition time point of the effect `e_j` -and the presence of the assignment effect. - -`la_j` is true if and only if the associated assignment effect `e_j`: - - is present - - is before the condition - - has the same state variable as the condition - - for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` - - the condition is present -**/ -fn create_la_vector_without_timepoints( - assignments: Vec<&&(EffID, Lit, &Effect)>, - cond: &Condition, - prez_cond: Lit, - eff_mutex_ends: &HashMap, - solver: &mut Solver, -) -> Vec<(Lit, IAtom, FAtom, Lit)> { - assignments - .iter() - .map(|(eff_id, prez_eff, eff)| { - let mut la_conjunction: Vec = Vec::with_capacity(32); - // is present - la_conjunction.push(*prez_eff); - // is before the condition - la_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - la_conjunction.push(solver.reify(eq(a, b))); - } - // for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` - // This implies constraint is expressed as a disjunction. - for (other_eff_id, prez_other_eff, other_eff) in assignments.iter() { - // same effect: continue - if eff_id == other_eff_id { - continue; - } - let mut disjunction: Vec = Vec::with_capacity(12); - // is not present - disjunction.push(!*prez_other_eff); - // is after the condition - disjunction.push(solver.reify(f_lt(cond.end, other_eff.transition_end))); - // has a state variable different from the condition - debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = other_eff.state_var.args[idx]; - disjunction.push(solver.reify(neq(a, b))); - } - // is before the effect `e_j` - disjunction.push(solver.reify(f_lt(eff_mutex_ends[other_eff_id], eff.transition_end))); - - let disjunction_lit = solver.reify(or(disjunction.clone())); - la_conjunction.push(disjunction_lit); - } - // the condition is present - la_conjunction.push(prez_cond); - - // Create the `la_j` literal. - let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver.model.entails(solver.model.presence_literal(la_lit.variable()))); - - // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { - unreachable!() - }; - let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - - // Get the end of the transition time point of the effect `e_j`. - let ta = eff.transition_end; - (la_lit, ca, ta, *prez_eff) - }) - .collect::>() -} - -/** -Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j` -and the presence of the assignment effect. - -`la_j` is true if and only if the associated assignment effect `e_j`: - - is present - - has the same state variable as the condition - - the condition is between the end of the transition and the mutex end - - the condition is present -**/ -fn create_la_vector_with_timepoints( - assignments: Vec<&&(EffID, Lit, &Effect)>, - cond: &Condition, - prez_cond: Lit, - eff_mutex_ends: &HashMap, - solver: &mut Solver, -) -> Vec<(Lit, IAtom, FAtom, Lit)> { - assignments - .iter() - .map(|(eff_id, prez_eff, eff)| { - let mut la_conjunction: Vec = Vec::with_capacity(32); - // is present - la_conjunction.push(*prez_eff); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - la_conjunction.push(solver.reify(eq(a, b))); - } - // the condition is between the start and the end of the effect - la_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); - la_conjunction.push(solver.reify(f_leq(cond.end, eff_mutex_ends[eff_id]))); - // the condition is present - la_conjunction.push(prez_cond); - - // Create the `la_j` literal. - let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver.model.entails(solver.model.presence_literal(la_lit.variable()))); - - // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { - unreachable!() - }; - let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - - // Get the end of the transition time point of the effect `e_j`. - let ta = eff.transition_end; - (la_lit, ca, ta, *prez_eff) - }) - .collect::>() -} diff --git a/planning/planning/src/chronicles/concrete.rs b/planning/planning/src/chronicles/concrete.rs index a23b79b3..4d70cb51 100644 --- a/planning/planning/src/chronicles/concrete.rs +++ b/planning/planning/src/chronicles/concrete.rs @@ -60,12 +60,7 @@ pub trait Substitution { } fn sub_linear_term(&self, term: &LinearTerm) -> LinearTerm { - LinearTerm::new( - term.factor(), - self.sub_ivar(term.var()), - self.sub_lit(term.lit()), - term.denom(), - ) + LinearTerm::new(term.factor(), self.sub_ivar(term.var()), term.denom()) } fn sub_linear_sum(&self, sum: &LinearSum) -> LinearSum { @@ -536,7 +531,6 @@ impl VarSet { self.add_atom(term.var()); self.add_atom(term.factor()); self.add_atom(term.denom()); - self.add_lit(term.lit()); } fn add_linear_sum(&mut self, sum: &LinearSum) { diff --git a/planning/unified/plugin/up_aries/solver.py b/planning/unified/plugin/up_aries/solver.py index 42f12e3d..7d52d068 100644 --- a/planning/unified/plugin/up_aries/solver.py +++ b/planning/unified/plugin/up_aries/solver.py @@ -50,7 +50,7 @@ "SCHEDULING", # "CONTINGENT", "ACTION_BASED_MULTI_AGENT", "TAMP", # PROBLEM_TYPE - "SIMPLE_NUMERIC_PLANNING", + # "SIMPLE_NUMERIC_PLANNING", # TODO # "GENERAL_NUMERIC_PLANNING", # TIME "CONTINUOUS_TIME", diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index b7290df7..1d20436a 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -78,7 +78,7 @@ impl Domains { } #[cfg(test)] - fn new_presence_literal(&mut self, scope: Lit) -> Lit { + pub fn new_presence_literal(&mut self, scope: Lit) -> Lit { let lit = self.new_var(0, 1).geq(1); self.add_implication(lit, scope); lit @@ -664,7 +664,9 @@ impl Domains { debug_assert!(self.entails(!invalid_lit)); explanation.push(!invalid_lit); match cause { - DirectOrigin::Decision | DirectOrigin::Encoding => {} + DirectOrigin::Decision | DirectOrigin::Encoding => { + explanation.push(invalid_lit); + } DirectOrigin::ExternalInference(cause) => { // print!("[ext {:?}] ", cause.writer); // ask for a clause (l1 & l2 & ... & ln) => lit diff --git a/solver/src/model/extensions/assignments.rs b/solver/src/model/extensions/assignments.rs index 7019674e..b3973faf 100644 --- a/solver/src/model/extensions/assignments.rs +++ b/solver/src/model/extensions/assignments.rs @@ -1,7 +1,8 @@ use crate::core::state::{FixedDomain, IntDomain, OptDomain}; use crate::core::*; use crate::model::extensions::SavedAssignment; -use crate::model::lang::{Atom, Cst, FAtom, IAtom, IVar, SAtom}; +use crate::model::lang::linear::LinearSum; +use crate::model::lang::{Atom, Cst, IAtom, IVar, SAtom}; use crate::model::symbols::SymId; use crate::model::symbols::{ContiguousSymbols, TypedSym}; use num_rational::Rational32; @@ -41,10 +42,18 @@ pub trait AssignmentExt { } } - /// Returns the fixed-point domain of the atom. - fn f_domain(&self, fixed: impl Into) -> FixedDomain { - let fixed = fixed.into(); - FixedDomain::new(self.var_domain(fixed.num), fixed.denom) + /// Returns the fixed-point domain of the linear sum. + /// Can also be used with a FAtom. + fn f_domain(&self, sum: impl Into) -> FixedDomain { + let sum: LinearSum = sum.into(); + let (lb, ub) = sum + .terms() + .iter() + .fold((sum.constant(), sum.constant()), |(lb, ub), t| { + let (l, u) = self.domain_of(t.var()); + (lb + l * t.factor(), ub + u * t.factor()) + }); + FixedDomain::new(IntDomain::new(lb, ub), sum.denom()) } fn domain_of(&self, atom: impl Into) -> (IntCst, IntCst) { diff --git a/solver/src/model/lang.rs b/solver/src/model/lang.rs index 0c961893..64bc4dd8 100644 --- a/solver/src/model/lang.rs +++ b/solver/src/model/lang.rs @@ -7,6 +7,7 @@ mod fixed; mod int; pub mod linear; pub mod max; +pub mod mul; pub mod reification; mod sym; mod validity_scope; diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs index 2127b182..fb967890 100644 --- a/solver/src/model/lang/linear.rs +++ b/solver/src/model/lang/linear.rs @@ -9,12 +9,9 @@ use std::collections::BTreeMap; /* LinearTerm */ /* ========================================================================== */ -/// A linear term of the form `a/b * X * P` where: +/// A linear term of the form `a/b * X` where: /// - `a` and `b` are integer constants /// - `X` is an integer variable. -/// - `P` is a non-optional literal interpreted as 0 if False and 1 if true. -/// -/// If `P` is true, it **required** that the expression is defined, meaning that both `X` and `P` are present. #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub struct LinearTerm { factor: IntCst, @@ -25,15 +22,19 @@ pub struct LinearTerm { impl std::fmt::Display for LinearTerm { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { if self.factor != 1 { - if self.factor < 0 { - write!(f, "({})", self.factor)?; + if self.factor == -1 { + write!(f, "-")?; } else { write!(f, "{}", self.factor)?; } + } + if self.factor.abs() != 1 && self.var != IVar::ONE { write!(f, "*")?; } if self.var != IVar::ONE { write!(f, "{:?}", self.var)?; + } else if self.factor.abs() == 1 { + write!(f, "1")?; } Ok(()) } @@ -123,10 +124,26 @@ pub struct LinearSum { impl std::fmt::Display for LinearSum { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { for (i, e) in self.terms.iter().enumerate() { - if i != 0 { + if e.factor < 0 { + if i != 0 { + write!(f, " - ")?; + } else { + write!(f, "-")?; + } + } else if i > 0 { write!(f, " + ")?; } - write!(f, "{e}")?; + if e.factor.abs() != 1 { + write!(f, "{}", e.factor.abs())?; + } + if e.factor.abs() != 1 && e.var != IVar::ONE { + write!(f, "*")?; + } + if e.var != IVar::ONE { + write!(f, "{:?}", e.var)?; + } else if e.factor.abs() == 1 { + write!(f, "1")?; + } } if self.constant != 0 { if !self.terms.is_empty() { @@ -247,7 +264,7 @@ impl LinearSum { terms: term_map .into_iter() .filter(|(v, f)| *f != 0 && *v != IVar::ZERO) - .filter(|(v, _)| !(*v == IVar::ONE)) // Has been grouped into the constant + .filter(|(v, _)| *v != IVar::ONE) // Has been grouped into the constant .map(|(v, f)| LinearTerm { factor: f, var: v, @@ -429,15 +446,19 @@ pub struct NFLinearSumItem { impl std::fmt::Display for NFLinearSumItem { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { if self.factor != 1 { - if self.factor < 0 { - write!(f, "({})", self.factor)?; + if self.factor == -1 { + write!(f, "-")?; } else { write!(f, "{}", self.factor)?; } + } + if self.factor.abs() != 1 && self.var != VarRef::ONE { write!(f, "*")?; } if self.var != VarRef::ONE { write!(f, "{:?}", self.var)?; + } else if self.factor.abs() == 1 { + write!(f, "1")?; } Ok(()) } @@ -468,12 +489,19 @@ impl std::fmt::Display for NFLinearLeq { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { for (i, e) in self.sum.iter().enumerate() { if e.factor < 0 { - write!(f, " - ")?; + if i != 0 { + write!(f, " - ")?; + } else { + write!(f, "-")?; + } } else if i > 0 { write!(f, " + ")?; } if e.factor.abs() != 1 { - write!(f, "{} * ", e.factor.abs())?; + write!(f, "{}", e.factor.abs())?; + } + if e.factor.abs() != 1 && e.var != VarRef::ONE { + write!(f, "*")?; } if e.var != VarRef::ONE { write!(f, "{:?}", e.var)?; @@ -705,6 +733,38 @@ mod tests { } } + #[test] + fn test_term_display() { + let var = IVar::new(VarRef::from_u32(5)); + // Constant terms + assert_eq!(format!("{}", LinearTerm::constant_int(1)), "1"); + assert_eq!(format!("{}", LinearTerm::constant_int(-1)), "-1"); + assert_eq!(format!("{}", LinearTerm::constant_int(5)), "5"); + assert_eq!(format!("{}", LinearTerm::constant_int(-5)), "-5"); + assert_eq!(format!("{}", LinearTerm::constant_rational(1, 10)), "1"); + assert_eq!(format!("{}", LinearTerm::constant_rational(-1, 10)), "-1"); + assert_eq!(format!("{}", LinearTerm::constant_rational(5, 10)), "5"); + assert_eq!(format!("{}", LinearTerm::constant_rational(-5, 10)), "-5"); + // Pseudo-constant terms + assert_eq!(format!("{}", LinearTerm::int(1, IVar::ONE)), "1"); + assert_eq!(format!("{}", LinearTerm::int(-1, IVar::ONE)), "-1"); + assert_eq!(format!("{}", LinearTerm::int(5, IVar::ONE)), "5"); + assert_eq!(format!("{}", LinearTerm::int(-5, IVar::ONE)), "-5"); + assert_eq!(format!("{}", LinearTerm::rational(1, IVar::ONE, 10)), "1"); + assert_eq!(format!("{}", LinearTerm::rational(-1, IVar::ONE, 10)), "-1"); + assert_eq!(format!("{}", LinearTerm::rational(5, IVar::ONE, 10)), "5"); + assert_eq!(format!("{}", LinearTerm::rational(-5, IVar::ONE, 10)), "-5"); + // Variable terms + assert_eq!(format!("{}", LinearTerm::int(1, var)), "var5"); + assert_eq!(format!("{}", LinearTerm::int(-1, var)), "-var5"); + assert_eq!(format!("{}", LinearTerm::int(5, var)), "5*var5"); + assert_eq!(format!("{}", LinearTerm::int(-5, var)), "-5*var5"); + assert_eq!(format!("{}", LinearTerm::rational(1, var, 10)), "var5"); + assert_eq!(format!("{}", LinearTerm::rational(-1, var, 10)), "-var5"); + assert_eq!(format!("{}", LinearTerm::rational(5, var, 10)), "5*var5"); + assert_eq!(format!("{}", LinearTerm::rational(-5, var, 10)), "-5*var5"); + } + /* =========================== LinearSum Tests ========================== */ #[test] @@ -1029,6 +1089,33 @@ mod tests { } } + #[test] + fn test_sum_display() { + let var = IVar::new(VarRef::from_u32(5)); + // Simple addition + let sum = LinearSum::of(vec![ + LinearTerm::rational(1, var, 10), + LinearTerm::constant_rational(5, 10), + LinearTerm::rational(5, var, 10), + LinearTerm::constant_rational(1, 10), + ]); + assert_eq!(format!("{}", sum), "var5 + 5 + 5*var5 + 1"); + // Simple subtraction + let sum = LinearSum::of(vec![ + LinearTerm::rational(1, var, 10), + LinearTerm::constant_rational(-5, 10), + LinearTerm::rational(-5, var, 10), + LinearTerm::constant_rational(-1, 10), + ]); + assert_eq!(format!("{}", sum), "var5 - 5 - 5*var5 - 1"); + // Complete subtraction + let sum = LinearSum::of(vec![ + LinearTerm::rational(-1, var, 10), + LinearTerm::constant_rational(-5, 10), + ]); + assert_eq!(format!("{}", sum), "-var5 - 5"); + } + /* ================================ Utils =============================== */ #[test] diff --git a/solver/src/model/lang/max.rs b/solver/src/model/lang/max.rs index c5d21504..a296ab4e 100644 --- a/solver/src/model/lang/max.rs +++ b/solver/src/model/lang/max.rs @@ -5,7 +5,7 @@ use crate::reif::ReifExpr; use itertools::Itertools; use std::fmt::{Debug, Formatter}; -/// Constraint equivalent to `lhs = max { e | e \in rhs } +/// Constraint equivalent to `lhs = max { e | e \in rhs }` pub struct EqMax { lhs: IAtom, rhs: Vec, @@ -20,7 +20,7 @@ impl EqMax { } } -/// Constraint equivalent to `lhs = min { e | e \in rhs } +/// Constraint equivalent to `lhs = min { e | e \in rhs }` pub struct EqMin { lhs: IAtom, rhs: Vec, diff --git a/solver/src/model/lang/mul.rs b/solver/src/model/lang/mul.rs new file mode 100644 index 00000000..4784f7ad --- /dev/null +++ b/solver/src/model/lang/mul.rs @@ -0,0 +1,15 @@ +use crate::core::{Lit, VarRef}; +use std::fmt::{Debug, Formatter}; + +#[derive(Eq, PartialEq, Hash, Clone)] +pub struct NFEqVarMulLit { + pub lhs: VarRef, + pub rhs: VarRef, + pub lit: Lit, +} + +impl Debug for NFEqVarMulLit { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?} = {:?} * {:?}", self.lhs, self.lit, self.rhs) + } +} diff --git a/solver/src/reasoners/cp/linear.rs b/solver/src/reasoners/cp/linear.rs index 8f8c71c3..966ced43 100644 --- a/solver/src/reasoners/cp/linear.rs +++ b/solver/src/reasoners/cp/linear.rs @@ -262,7 +262,7 @@ impl Propagator for LinearSumLeq { // this is the element to explain // move its upper bound to the RHS let a_ub = (literal.bound_value().as_int() as i64).saturating_mul(factor); - // the inference is: factor * a.var <= a_ub + // the inference is: factor * e.var <= a_ub // e.var <= a_ub / factor // because e.var is integral, we can increase a_ub until its is immediately before the next multiple of factor // without changing the result @@ -593,7 +593,7 @@ mod tests { // propagate match s.propagate(&mut d, INFERENCE_CAUSE) { Ok(()) => { - // propagation successfull, check that all inferences have correct explanations + // propagation successful, check that all inferences have correct explanations check_events(&d, &mut s); } Err(contradiction) => { diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 5514866b..7c03a55a 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -2,6 +2,7 @@ pub mod linear; pub mod max; +pub mod mul; use crate::backtrack::{Backtrack, DecLvl, ObsTrailCursor}; use crate::collections::ref_store::{RefMap, RefVec}; @@ -12,10 +13,12 @@ use crate::core::{IntCst, Lit, SignedVar, VarRef, INT_CST_MAX, INT_CST_MIN}; use crate::create_ref_type; use crate::model::extensions::AssignmentExt; use crate::model::lang::linear::NFLinearLeq; -use crate::reasoners::cp::linear::{LinearSumLeq, SumElem}; -use crate::reasoners::cp::max::AtLeastOneGeq; +use crate::model::lang::mul::NFEqVarMulLit; use crate::reasoners::{Contradiction, ReasonerId, Theory}; use anyhow::Context; +use mul::VarEqVarMulLit; +use crate::reasoners::cp::linear::{LinearSumLeq, SumElem}; +use crate::reasoners::cp::max::AtLeastOneGeq; use std::cmp::Ordering; use std::collections::{HashMap, HashSet}; @@ -149,6 +152,15 @@ impl Cp { self.add_propagator(propagator); } + pub fn add_eq_var_mul_lit_constraint(&mut self, mul: &NFEqVarMulLit) { + let propagator = VarEqVarMulLit { + reified: mul.lhs, + original: mul.rhs, + lit: mul.lit, + }; + self.add_propagator(propagator); + } + pub fn add_propagator(&mut self, propagator: impl Into) { // TODO: handle validity scopes let propagator = propagator.into(); diff --git a/solver/src/reasoners/cp/mul.rs b/solver/src/reasoners/cp/mul.rs new file mode 100644 index 00000000..5c536cab --- /dev/null +++ b/solver/src/reasoners/cp/mul.rs @@ -0,0 +1,456 @@ +use std::cmp::{max, min}; + +use crate::{ + core::{ + state::{Explanation, Term}, + Lit, Relation, VarRef, + }, + model::extensions::AssignmentExt, + reasoners::Contradiction, + reif, +}; + +use super::Propagator; + +#[derive(Clone, Debug)] +/// Propagator for the constraint `reified <=> original * lit` +pub(super) struct VarEqVarMulLit { + pub reified: VarRef, + pub original: VarRef, + pub lit: Lit, +} + +impl std::fmt::Display for VarEqVarMulLit { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?} <=> {:?} * {:?}", self.reified, self.original, self.lit) + } +} + +impl Propagator for VarEqVarMulLit { + fn setup(&self, id: super::PropagatorId, context: &mut super::Watches) { + context.add_watch(self.reified, id); + context.add_watch(self.original, id); + context.add_watch(self.lit.variable(), id); + } + + fn propagate( + &self, + domains: &mut crate::core::state::Domains, + cause: crate::core::state::Cause, + ) -> Result<(), crate::reasoners::Contradiction> { + let n = domains.trail().len(); + + let orig_prez = domains.presence_literal(self.original); + debug_assert!(domains.implies(self.lit, orig_prez)); + + if domains.entails(self.lit) { + // lit is true, so reified = original + let (orig_lb, orig_ub) = domains.bounds(self.original); + let (reif_lb, reif_ub) = domains.bounds(self.reified); + + domains.set_lb(self.reified, orig_lb, cause)?; + domains.set_ub(self.reified, orig_ub, cause)?; + domains.set_lb(self.original, reif_lb, cause)?; + domains.set_ub(self.original, reif_ub, cause)?; + } else if domains.entails(!self.lit) { + // lit is false, so reified = 0 + domains.set_lb(self.reified, 0, cause)?; + domains.set_ub(self.reified, 0, cause)?; + } else { + // lit is not fixed + let (orig_lb, orig_ub) = domains.bounds(self.original); + let (reif_lb, reif_ub) = domains.bounds(self.reified); + + if reif_lb > orig_ub || reif_ub < orig_lb { + // intersection(dom(reif), dom(orig)) is empty, so lit = false and reified = 0 + domains.set(!self.lit, cause)?; + domains.set_lb(self.reified, 0, cause)?; + domains.set_ub(self.reified, 0, cause)?; + } else if reif_lb > 0 || reif_ub < 0 { + // reified != 0, so lit = true + domains.set(self.lit, cause)?; + } else if domains.entails(orig_prez) { + // original is present, can reduce the bounds of reified while keeping 0 in the domain + domains.set_lb(self.reified, min(0, orig_lb), cause)?; + domains.set_ub(self.reified, max(0, orig_ub), cause)?; + } + } + + if n != domains.trail().len() { + // At least one domain has been modified + self.propagate(domains, cause) + } else { + Ok(()) + } + } + + fn explain( + &self, + literal: Lit, + state: &crate::core::state::Domains, + out_explanation: &mut crate::core::state::Explanation, + ) { + // At least one element of the constraint must be the subject of the explanation + debug_assert!([self.reified, self.original, self.lit.variable()] + .iter() + .any(|&v| v == literal.variable())); + + let (reif_lb, reif_ub) = state.bounds(self.reified); + let (orig_lb, orig_ub) = state.bounds(self.original); + let orig_prez = state.presence_literal(self.original); + + if literal == self.lit { + // Explain why lit is true + // reified != 0, so lit = true + if reif_lb > 0 { + out_explanation.push(self.reified.geq(reif_lb)); + } else if reif_ub < 0 { + out_explanation.push(self.reified.leq(reif_ub)); + } + } else if literal == !self.lit { + // Explain why lit is false + // intersection(dom(reif), dom(orig)) is empty, so lit = false + if reif_lb > orig_ub { + out_explanation.push(self.original.leq(orig_ub)); + out_explanation.push(self.reified.geq(reif_lb)); + } + if reif_ub < orig_lb { + out_explanation.push(self.original.geq(orig_lb)); + out_explanation.push(self.reified.leq(reif_ub)); + } + } else { + let (var, rel, val) = literal.unpack(); + if var == self.reified { + // Explain the bounds of reified + match rel { + Relation::Gt => { + if val < 0 { + if state.entails(!orig_prez) { + out_explanation.push(!orig_prez); + } else if state.entails(!self.lit) { + out_explanation.push(!self.lit); + } else if state.entails(orig_prez) { + out_explanation.push(orig_prez); + out_explanation.push(self.original.gt(val)); + } + } else if state.entails(self.lit) { + out_explanation.push(self.lit); + out_explanation.push(self.original.gt(val)); + } + } + Relation::Leq => { + if val >= 0 { + if state.entails(!orig_prez) { + out_explanation.push(!orig_prez); + } else if state.entails(!self.lit) { + out_explanation.push(!self.lit); + } else if state.entails(orig_prez) { + out_explanation.push(orig_prez); + out_explanation.push(self.original.leq(val)); + } + } else if state.entails(self.lit) { + out_explanation.push(self.lit); + out_explanation.push(self.original.leq(val)); + } + } + }; + } else if var == self.original && state.entails(self.lit) { + // Explain the bounds of original + out_explanation.push(self.lit); + match rel { + Relation::Gt => out_explanation.push(self.reified.gt(val)), + Relation::Leq => out_explanation.push(self.reified.leq(val)), + }; + } + } + } + + fn clone_box(&self) -> Box { + Box::new(self.clone()) + } +} + +#[cfg(test)] +mod tests { + use itertools::Itertools; + use rand::prelude::SmallRng; + use rand::seq::SliceRandom; + use rand::{Rng, SeedableRng}; + + use crate::backtrack::Backtrack; + use crate::core::literals::Disjunction; + use crate::core::state::{Event, Origin}; + use crate::core::{IntCst, Relation}; + use crate::{ + core::state::{Cause, Domains, Explainer, Explanation, InferenceCause, InvalidUpdate}, + reasoners::{Contradiction, ReasonerId}, + }; + + use super::*; + + fn mul(reif: VarRef, orig: VarRef, lit: Lit) -> VarEqVarMulLit { + VarEqVarMulLit { + reified: reif, + original: orig, + lit, + } + } + + fn check_bounds(v: VarRef, d: &Domains, lb: IntCst, ub: IntCst) { + assert_eq!(d.lb(v), lb); + assert_eq!(d.ub(v), ub); + } + + #[test] + fn test_propagation_with_true_lit() { + let mut d = Domains::new(); + let r = d.new_var(-5, 10); + let o = d.new_var(-10, 5); + let c = mul(r, o, Lit::TRUE); + + // Check initial bounds + check_bounds(r, &d, -5, 10); + check_bounds(o, &d, -10, 5); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, -5, 5); + check_bounds(o, &d, -5, 5); + } + + #[test] + fn test_propagation_with_false_lit() { + let mut d = Domains::new(); + let r = d.new_var(-5, 10); + let o = d.new_var(-10, 5); + let c = mul(r, o, Lit::FALSE); + + // Check initial bounds + check_bounds(r, &d, -5, 10); + check_bounds(o, &d, -10, 5); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, 0, 0); + check_bounds(o, &d, -10, 5); + } + + #[test] + fn test_propagation_with_non_zero_reif() { + let mut d = Domains::new(); + let p = d.new_presence_literal(Lit::TRUE); + let r = d.new_var(1, 10); + let o = d.new_optional_var(-10, 5, p); + let l = d.new_presence_literal(p); + let c = mul(r, o, l); + + // Check initial bounds + check_bounds(r, &d, 1, 10); + check_bounds(o, &d, -10, 5); + check_bounds(l.variable(), &d, 0, 1); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, 1, 5); + check_bounds(o, &d, 1, 5); + check_bounds(l.variable(), &d, 1, 1); + } + + #[test] + fn test_propagation_with_exclusive_bounds() { + let mut d = Domains::new(); + let p = d.new_presence_literal(Lit::TRUE); + let r = d.new_var(-5, 0); + let o = d.new_optional_var(1, 5, p); + let l = d.new_presence_literal(p); + let c = mul(r, o, l); + + // Check initial bounds + check_bounds(r, &d, -5, 0); + check_bounds(o, &d, 1, 5); + check_bounds(l.variable(), &d, 0, 1); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, 0, 0); + check_bounds(o, &d, 1, 5); + check_bounds(l.variable(), &d, 0, 0); + } + + static INFERENCE_CAUSE: Cause = Cause::Inference(InferenceCause { + writer: ReasonerId::Cp, + payload: 0, + }); + + /// Test that triggers propagation of random decisions and checks that the explanations are minimal + #[test] + fn test_explanations() { + let mut rng = SmallRng::seed_from_u64(0); + // function that returns a given number of decisions to be applied later + // it use the RNG above to drive its random choices + let mut pick_decisions = |d: &Domains, min: usize, max: usize| -> Vec { + let num_decisions = rng.gen_range(min..=max); + let vars = d.variables().filter(|v| !d.is_bound(*v)).collect_vec(); + let mut lits = Vec::with_capacity(num_decisions); + for _ in 0..num_decisions { + let var_id = rng.gen_range(0..vars.len()); + let var = vars[var_id]; + let (lb, ub) = d.bounds(var); + let below: bool = rng.gen(); + let lit = if below { + let ub = rng.gen_range(lb..ub); + Lit::leq(var, ub) + } else { + let lb = rng.gen_range((lb + 1)..=ub); + Lit::geq(var, lb) + }; + lits.push(lit); + } + lits + }; + // new rng for local use + let mut rng = SmallRng::seed_from_u64(0); + + // repeat a large number of random tests + for _ in 0..1000 { + // create the constraint + let mut d = Domains::new(); + let p = d.new_presence_literal(Lit::TRUE); + let lit = d.new_presence_literal(p); + let original = d.new_optional_var(-10, 10, p); + let reified = d.new_var(-10, 10); + let mut c = VarEqVarMulLit { reified, original, lit }; + println!("\nConstraint: {c:?} with prez(original) = {p:?}"); + + // pick a random set of decisions + let decisions = pick_decisions(&d, 1, 10); + println!("Decisions: {decisions:?}"); + + // get a copy of the domain on which to apply all decisions + let mut d = d.clone(); + d.save_state(); + + // apply all decisions + for dec in decisions { + d.set(dec, Cause::Decision); + } + + // propagate + match c.propagate(&mut d, INFERENCE_CAUSE) { + Ok(()) => { + // propagation successful, check that all inferences have correct explanations + check_events(&d, &mut c); + } + Err(contradiction) => { + // propagation failure, check that the contradiction is a valid one + let explanation = match contradiction { + Contradiction::InvalidUpdate(InvalidUpdate(lit, cause)) => { + let mut expl = Explanation::with_capacity(16); + expl.push(!lit); + d.add_implying_literals_to_explanation(lit, cause, &mut expl, &mut c); + expl + } + Contradiction::Explanation(expl) => expl, + }; + let mut d = d.clone(); + d.reset(); + // get the conjunction and shuffle it + // note that we do not check minimality here + let mut conjuncts = explanation.lits; + conjuncts.shuffle(&mut rng); + for &conjunct in &conjuncts { + let ret = d.set(conjunct, Cause::Decision); + if ret.is_err() { + println!("Invalid update: {conjunct:?}"); + } + } + + assert!( + c.propagate(&mut d, INFERENCE_CAUSE).is_err(), + "Explanation: {conjuncts:?}\n {c:?}" + ); + } + } + } + } + + /// Check that all events since the last decision have a minimal explanation + pub fn check_events(d: &Domains, explainer: &mut (impl Propagator + Explainer)) { + let events = d + .trail() + .events() + .iter() + .rev() + .take_while(|ev| ev.cause != Origin::DECISION) + .cloned() + .collect_vec(); + // check that all events have minimal explanations + for ev in &events { + check_event_explanation(d, ev, explainer); + } + } + + /// Checks that the event has a minimal explanation + pub fn check_event_explanation(d: &Domains, ev: &Event, explainer: &mut (impl Propagator + Explainer)) { + let implied = ev.new_literal(); + // generate explanation + let implicants = d.implying_literals(implied, explainer).unwrap(); + let clause = Disjunction::new(implicants.iter().map(|l| !*l).collect_vec()); + // check minimality + check_explanation_minimality(d, implied, clause, explainer); + } + + pub fn check_explanation_minimality( + domains: &Domains, + implied: Lit, + clause: Disjunction, + propagator: &dyn Propagator, + ) { + let mut domains = domains.clone(); + // println!("=== original trail ==="); + // domains.trail().print(); + domains.reset(); + assert!(!domains.entails(implied)); + + // gather all decisions not already entailed at root level + let mut decisions = clause + .literals() + .iter() + .copied() + .filter(|&l| !domains.entails(l)) + .map(|l| !l) + .collect_vec(); + + for _rotation_id in 0..decisions.len() { + // println!("Clause: {implied:?} <- {decisions:?}"); + for i in 0..decisions.len() { + let l = decisions[i]; + if domains.entails(l) { + continue; + } + // println!("Decide {l:?}"); + domains.decide(l); + propagator + .propagate(&mut domains, INFERENCE_CAUSE) + .expect("failed prop"); + + let decisions_left = decisions[i + 1..] + .iter() + .filter(|&l| !domains.entails(*l)) + .collect_vec(); + + if !decisions_left.is_empty() { + assert!(!domains.entails(implied), "Not minimal, useless: {:?}", &decisions_left) + } + } + + // println!("=== Post trail ==="); + // solver.trail().print(); + assert!( + domains.entails(implied), + "Literal {implied:?} not implied after all implicants ({decisions:?}) enforced" + ); + decisions.rotate_left(1); + } + } +} diff --git a/solver/src/reasoners/eq/dense.rs b/solver/src/reasoners/eq/dense.rs index d4adcb48..96226a33 100644 --- a/solver/src/reasoners/eq/dense.rs +++ b/solver/src/reasoners/eq/dense.rs @@ -1213,7 +1213,7 @@ mod tests { fn random_model(seed: u64) -> Model { let mut rng = SmallRng::seed_from_u64(seed); - let objects = vec!["alice", "bob", "chloe", "donald", "elon"]; + let objects = ["alice", "bob", "chloe", "donald", "elon"]; let num_objects = rng.gen_range(1..5); let objects = objects[0..num_objects].to_vec(); let symbols = SymbolTable::from(vec![("obj", objects.clone())]); @@ -1225,7 +1225,6 @@ mod tests { let num_scopes = rng.gen_range(0..3); let scopes = (0..=num_scopes) - .into_iter() .map(|i| { if i == 0 { Lit::TRUE diff --git a/solver/src/reasoners/sat/clauses/mod.rs b/solver/src/reasoners/sat/clauses/mod.rs index 7bbd6a80..a767b6f0 100644 --- a/solver/src/reasoners/sat/clauses/mod.rs +++ b/solver/src/reasoners/sat/clauses/mod.rs @@ -190,6 +190,13 @@ impl Clause { debug_assert!(lvl0 >= lvl1); debug_assert!(self.unwatched.iter().all(|l| lvl1 >= priority(*l))); + if value_of(self.watch1) == Some(true) { + // clause is satisfied, leave the watches untouched (true literals would be the watches) + return; + } + debug_assert_ne!(value_of(self.watch1), Some(true)); + debug_assert_ne!(value_of(self.watch2), Some(true)); + if self.watch1 == !presence(self.watch2) { self.swap_watches() } else if self.watch2 == !presence(self.watch1) { diff --git a/solver/src/reasoners/stn/theory.rs b/solver/src/reasoners/stn/theory.rs index b7bd7289..2a4f0e1b 100644 --- a/solver/src/reasoners/stn/theory.rs +++ b/solver/src/reasoners/stn/theory.rs @@ -478,7 +478,6 @@ impl StnTheory { for edge in path { let enabler = self.constraints[edge].enabler.expect("inactive constraint"); out_explanation.push(enabler.active); - out_explanation.push(model.presence(enabler.active.variable())); } } TheoryPropagationCause::Bounds { source, target } => { diff --git a/solver/src/reif/mod.rs b/solver/src/reif/mod.rs index 41ba5017..e442d12f 100644 --- a/solver/src/reif/mod.rs +++ b/solver/src/reif/mod.rs @@ -4,6 +4,7 @@ use crate::core::{IntCst, Lit, SignedVar, VarRef}; use crate::model::lang::alternative::NFAlternative; use crate::model::lang::linear::NFLinearLeq; use crate::model::lang::max::NFEqMax; +use crate::model::lang::mul::NFEqVarMulLit; use crate::model::lang::ValidityScope; use crate::model::{Label, Model}; use std::fmt::{Debug, Formatter}; @@ -32,6 +33,7 @@ pub enum ReifExpr { Linear(NFLinearLeq), Alternative(NFAlternative), EqMax(NFEqMax), + EqVarMulLit(NFEqVarMulLit), } impl std::fmt::Display for ReifExpr { @@ -48,6 +50,7 @@ impl std::fmt::Display for ReifExpr { ReifExpr::Linear(l) => write!(f, "{l}"), ReifExpr::EqMax(em) => write!(f, "{em:?}"), ReifExpr::Alternative(alt) => write!(f, "{alt:?}"), + ReifExpr::EqVarMulLit(em) => write!(f, "{em:?}"), } } } @@ -75,6 +78,7 @@ impl ReifExpr { ReifExpr::Linear(lin) => lin.validity_scope(presence), ReifExpr::Alternative(alt) => ValidityScope::new([presence(alt.main)], []), ReifExpr::EqMax(eq_max) => ValidityScope::new([presence(eq_max.lhs.variable())], []), + ReifExpr::EqVarMulLit(em) => ValidityScope::new([presence(em.lhs)], []), } } @@ -89,6 +93,7 @@ impl ReifExpr { OptDomain::Present(lb, ub) if lb == ub => lb, _ => panic!(), }; + let lvalue = |lit: Lit| assignment.value(lit).unwrap(); let sprez = |svar: SignedVar| prez(svar.variable()); let svalue = |svar: SignedVar| { if svar.is_plus() { @@ -202,6 +207,13 @@ impl ReifExpr { Some(true) } } + ReifExpr::EqVarMulLit(NFEqVarMulLit { lhs, rhs, lit }) => { + if prez(*lhs) && prez(*rhs) { + Some(value(*lhs) == (lvalue(*lit) as i32) * value(*rhs)) + } else { + None + } + } } } } @@ -254,6 +266,7 @@ impl Not for ReifExpr { ReifExpr::Linear(lin) => ReifExpr::Linear(!lin), ReifExpr::Alternative(_) => panic!("Alternative is a constraint and cannot be negated"), ReifExpr::EqMax(_) => panic!("EqMax is a constraint and cannot be negated"), + ReifExpr::EqVarMulLit(_) => panic!("EqVarMulLit is a constraint and cannot be negated"), } } } diff --git a/solver/src/solver/parallel/signals.rs b/solver/src/solver/parallel/signals.rs index 586a4ff0..dd723036 100644 --- a/solver/src/solver/parallel/signals.rs +++ b/solver/src/solver/parallel/signals.rs @@ -7,7 +7,7 @@ use std::sync::atomic::{AtomicUsize, Ordering}; use std::sync::Arc; /// The maximum size of a clause that can be shared with other threads. -static MAX_CLAUSE_SHARING_SIZE: EnvParam = EnvParam::new("ARIES_MAX_CLAUSE_SHARING_SIZE", "6"); +static MAX_CLAUSE_SHARING_SIZE: EnvParam = EnvParam::new("ARIES_MAX_CLAUSE_SHARING_SIZE", "3"); static THREAD_ID_COUNTER: AtomicUsize = AtomicUsize::new(0); pub type ThreadID = usize; diff --git a/solver/src/solver/search/conflicts.rs b/solver/src/solver/search/conflicts.rs index adf0f082..f7efc92c 100644 --- a/solver/src/solver/search/conflicts.rs +++ b/solver/src/solver/search/conflicts.rs @@ -350,9 +350,8 @@ impl ConflictBasedBrancher { } } - pub fn set_default_value(&mut self, _var: VarRef, _val: IntCst) { - todo!() - // self.default_assignment.values.insert(var, val); + pub fn set_default_value(&mut self, var: VarRef, val: IntCst) { + self.default_assignment.set_from_phase(var, val) } /// Increase the activity of the variable and perform an reordering in the queue. diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 579a99cd..264c4f0f 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -403,6 +403,10 @@ impl Solver { Ok(()) } + ReifExpr::EqVarMulLit(mul) => { + self.reasoners.cp.add_eq_var_mul_lit_constraint(mul); + Ok(()) + } } }